The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

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