Re: [Haskell-cafe] Proof in Haskell

21 Dec 2010


      On Tuesday 21 December 2010 20:11:37, Colin Paul Adams wrote:
...
...
...
...
...
...
"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?
Hit send before I finished thinking, it should hold.