The Coq mailing list

[Thomas Th�m <thomas.thuem AT st.ovgu.de>]

Hi all,

I was wondering how to create a useful induction principle to prove
properties on mutual definitions. It is clear how to generate induction
principles for mutual definitions, but I cannot apply them in my case. I
could imagine to write an induction principle by hand, but hopefully there
is an automatic way?

Thanks,
Thomas

-----

Require Export List.

Inductive exp : Type :=
| e_var : nat -> exp
| e_meth : exp -> nat -> list exp -> exp.

(* For simplicity, only identical expression (lists of expressions) are in
the relation f (g). *)

Inductive f : exp -> exp -> Prop :=
| f_var : forall n,
    f (e_var n) (e_var n)
| f_meth : forall a a' l l' n,
    f a a' ->
    g l l' ->
    f (e_meth a n l) (e_meth a' n l')

with g : list exp -> list exp -> Prop :=
| g_nil :
    g nil nil
| g_cons : forall a a' l l',
    f a a' ->
    g l l' ->
    g (a::l) (a'::l').

Scheme f_ind2 := Minimality for f Sort Prop
with g_ind2 := Minimality for g Sort Prop.
Combined Scheme fg_mutind from f_ind2, g_ind2.

Fact total :
    ( forall a, exists a', f a a' ) /\
    ( forall l, exists l', g l l' ).
Proof.

(* fg_mutind cannot be applied... *)