Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] proofs related to mutually inductive language constructs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proofs related to mutually inductive language constructs


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page