[Haskell-cafe] Proof in Haskell

[Felipe Almeida Lessa]

On Tue, Dec 21, 2010 at 5:02 PM, Daniel Fischer
<daniel.is.fischer at googlemail.com> wrote:
> 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.
>
> Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq
> doesn't allow infinite structures?

Even if the theorem does hold with infinite structures, I don't really
know the answer to your question.  I'm just starting to study Coq in
my free time =).  My guess would be "no", because functions need to be
total.  But that's just a wild guess, and you shouldn't take my word
for it =).

Cheers!

-- 
Felipe.