The Coq mailing list

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

(* please, remove me when you "reply all" as I am already in  
coq-club AT pauillac.inria.fr,
   I need only one exemplar of this mail;
   I know, this mailing list is not the best configured one... *)

(* Le Wed, 09 Dec 2009 22:55:49 +0100, Thomas Thüm  
<thomas.thuem AT st.ovgu.de> a écrit:

> Thanks for your answers. I cannot imagine how to use your ideas, when f  
> and
> g do not relate exactly identical expressions.
>
> > For simplicity, only identical expression (lists of expressions) are in
> the relation f (g).
>
> Let me describe, how I would prove my theorem in informal math.
>
> Assume, we want to prove the two theorems A and B, where f and g are  
> defined
> mutually inductive.
>
> A: forall a, exists a', f a a'
> B: forall l, exists l', g l l'
>
> First, I would prove A by assuming B using induction on a.
>
> Second, I would prove B by assuming A using induction on l.
*)

Require Export List.

Inductive exp : Type :=
| e_var : nat -> exp
| e_meth : exp -> nat -> list_exp -> exp
with list_exp : Type :=
| nil : list_exp
| cons : exp -> list_exp -> list_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 (cons a l) (cons a' l').

Fact totalf :
    forall a, exists a', f a a'
with totalg :
    forall l, exists l', g l l'.
Proof.
 destruct a as [n|a n l].
  exists (e_var n); left.
 destruct (totalf a) as [a' Ha].
 destruct (totalg l) as [l' Hl].
 exists (e_meth a' n l').
 exact (f_meth a a' l l' n Ha Hl).
 (**)
 destruct l as [|a l].
 exists nil; left.
 destruct (totalf a) as [a' Ha].
 destruct (totalg l) as [l' Hl].
 exists (cons a' l').
 exact (g_cons a a' l l' Ha Hl).
Qed.

(*
> My question is, how do I do this in Coq? (The "Fact ... with ..." looks
> pretty close to what I need, but I couldn't get it working without a=a'  
> and
> l=l'.)
>
> Thomas

I had to modify the Inductive exp, to tell Coq that list_exp and exp are  
structurally related,
thing that the Fact ... with ... . doesn't infer.

> --------------------------------------------------------
> 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
*)

(* another way is to make induction "by hand" which needs well
understanding of the induction mechanism, since you don't rely
on automatically guardedness of the "induction" tactic
(that is, if you are not cautious, the proof can fail when you call "Qed")
*)

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 (cons a l) (cons a' l').

Definition g_trick (REC : forall a, exists a', f a a') :
 forall (l : list exp), exists l', g l l'.
Proof.
  intro H.
  induction l.
   eexists; left.
  destruct IHl; destruct (H a).
  eexists; right; eassumption.
Defined.
 (* Note the trick to keep transparent, necessary for a good induction *)

Fact totalf : forall a, exists a', f a a'.
Proof.
 refine (fix totalf (a : exp) := _); destruct a.
  eexists; left.
 destruct (g_trick totalf l). (* g_trick totalf is totalg, see later *)
 destruct (totalf a).
 eexists; right; eassumption.
Qed.

Fact totalg : forall l, exists l', g l l'.
Proof.
 exact (g_trick totalf). (* g_trick totalf can be used as totalg, see  
sooner *)
Qed.

(* so for this case, I assume that Scheme is not a bad idea;
   but the Scheme pros will tell you more about it than I *)

(*
--
Cédric AUGER

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