----- Original Message ----
> From: Colin Paul Adams <co...@colina.demon.co.uk>
> To: Daniel Fischer <daniel.is.fisc...@googlemail.com>
> Cc: haskell-cafe@haskell.org
> Sent: Tue, December 21, 2010 1:11:37 PM
> Subject: Re: [Haskell-cafe] Proof in Haskell
>
> >>>>> "Daniel" == Daniel Fischer <daniel.is.fisc...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
