[Haskell-cafe] Proof in Haskell

[Brandon Moore]

----- Original Message ----
> From: Colin Paul Adams <colin at colina.demon.co.uk>
> To: Daniel Fischer <daniel.is.fischer at googlemail.com>
> Cc: haskell-cafe at haskell.org
> Sent: Tue, December 21, 2010 1:11:37 PM
> Subject: Re: [Haskell-cafe] Proof in Haskell
> 
> >>>>> "Daniel" == Daniel Fischer <daniel.is.fischer at googlemail.com>  writes:
> 
>     Daniel> On Tuesday 21 December 2010 19:34:11,  Felipe Almeida Lessa wrote:
>     >> 
> > Theorem  mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
>      >> induction x; simpl; auto.  rewrite IHx1; rewrite IHx2;  trivial.
>     >> Qed.
> 
>     Daniel> Since  mirror (mirror x) = x doesn't hold in Haskell, I take
>      Daniel> it that Coq doesn't allow infinite structures?
> 
> Why doesn't it  hold?

You are both onto something. It is true, but the Coq proof only covered
finite trees. Infinite tree could be defined with coinduction, but even that
doesn't allow the possibility of bottoms in the tree.

CoInductive Tree (A:Set) :=
  Branch (l r : Tree A) | Leaf.

CoFixpoint mirror {A:Set} (x : Tree A) : Tree A :=
  match x with
  | Leaf => Leaf A
  | Branch l r => Branch A (mirror r) (mirror l)
  end.

Also, you'd have to define some notion of Bisimilarity rather than working
with the direct equality.

CoInductive bisimilar {A : Set} : Tree A -> Tree A -> Prop :=
  | bisim_Leaf : bisimilar (Leaf A) (Leaf A)
  | bisim_Branch (l1 r1 l2 r2 : Tree A) : bisimilar l1 l2 -> bisimilar r1 r2 -> 
bisimilar (Branch A l1 r1) (Branch A l2 r2).

I was hoping to write a proof, but it's much more annoying to work with 
coinductive definitions.

Brandon