coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <sozeau AT lri.fr>
- To: Ersoy Bayramoglu <ersoy.bayramoglu AT epfl.ch>
- Cc: coq-club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] proofs related to mutually inductive language constructs
- Date: Sun, 24 Aug 2008 00:23:03 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Le 23 août 08 à 04:05, Ersoy Bayramoglu a écrit :
Thanks for the explanation. I managed to prove the theorems. Scheme didn't turn out to be as scary as it looked after all. If anyone knows any alternative way, it would be interesting to hear it, though.
Hi,
there is a new way to define lemmas on mutual inductive types in 8.2, as follows:
Inductive term : Set :=
| app : term_list -> term
with term_list : Set :=
| nil_list | cons_list (t:term) (l:term_list).
Lemma foo : forall (t : term), exists l, t = app l
with bar : forall (l : term_list), l = nil_list \/ exists l', exists l'', l = cons_list (app l') l''.
induction t. exists t ; reflexivity.
induction l. left ; auto. right. destruct (foo t). exists x ; subst t. exists l. reflexivity.
Qed.
The implementation uses the undocumented [fix] tactic which can be used to build
non-structurally recursive fixpoints so you have to take care to use the proper
induction schemas in each subgoal. Also, it seems limited in the way it
recognizes the mutual inductive you are working on, but it may work for you.
Hope this helps,
-- Matthieu
- [Coq-Club] proofs related to mutually inductive language constructs, Ersoy Bayramoglu
- Re: [Coq-Club] proofs related to mutually inductive language constructs,
Adam Chlipala
- Re: [Coq-Club] proofs related to mutually inductive language constructs,
Ersoy Bayramoglu
- Re: [Coq-Club] proofs related to mutually inductive language constructs, Matthieu Sozeau
- Re: [Coq-Club] proofs related to mutually inductive language constructs,
Ersoy Bayramoglu
- Re: [Coq-Club] proofs related to mutually inductive language constructs,
Adam Chlipala
Archive powered by MhonArc 2.6.16.