21 Dec
2010
21 Dec
'10
5:58 p.m.
On Tue, Dec 21, 2010 at 5:02 PM, Daniel Fischer
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.