The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

(* As replied by Adam, you want to produce and not to consume.
   Furthermore, as I show below, you have not a lot of choice in your  
production
        (only identity works), and what you wanted to produce cannot be 
produced
	the way you thought as "exists l', g l l'" can never be structuraly  
inferior
	to "f a a'", as you break the induction by the introduction of the  
"exists".

        Here is maybe what you wanted to have.

	I never use Scheme or Combined Scheme (but I don't have opinions on  
whether
	                                       it is a good way or not to have  
mutual
                                               induction),
	and I think that (when it is possible) using mutual Lemma is often a  
simpler
        to do what you want (I recognize it is not always the case as it is 
less
                             powerful than Scheme & co.),
        as shown here.
*)

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').

Fact totalf :
    forall a a', f a a' -> a = a'
with totalg :
    forall l l', g l l' -> l = l'.
Proof.
 (* the totalf proof *)
 intros a a' H; destruct H as [n | a a' l l' n Ha Hl].
  reflexivity.
 rewrite (totalf a a' Ha).
 rewrite (totalg l l' Hl).
 reflexivity.
 (* the totalg proof *)
 intros l l' H; destruct H as [| a a' l l' Ha Hl].
  reflexivity.
 rewrite (totalf a a' Ha).
 rewrite (totalg l l' Hl).
 reflexivity.
Qed.
(*
Le Wed, 09 Dec 2009 12:26:50 +0100, Thomas Thüm <thomas.thuem AT st.ovgu.de>  
a écrit:

> 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... *)
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
*)