Re: [Haskell-cafe] Proof in Haskell

----- Original Message ----

From: Colin Paul Adams To: Daniel Fischer Cc: haskell-cafe@haskell.org Sent: Tue, December 21, 2010 1:11:37 PM Subject: Re: [Haskell-cafe] Proof in Haskell

...

...

...

...

...

"Daniel" == Daniel Fischer 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