Mutual-Mutual Induction

[Thomas Thüm]

Hello all,

a problem struggles me since week concerning mutual induction. I have done
proofs using mutual induction, but now it seems that I have to do a proof
using mutual induction in a case of a proof using mutual induction. I
simplified the definitions and would really appreciate your help that I can
finish my master thesis in time. ;)

My simplified definitions make absolutely no sense, don't try to find one...
;) Basically, I have two very similar mutual-inductive structures and a
mutual-inductive relation on the elements of both. The proof tries to proof
similarities between elements of the structures, if they are in relation.

I attached my tries to proof this.

Thanks in advance,
Thomas

-----

Require Export List.

Inductive term : Prop :=
  | tvar : term
  | tlist : term -> list term -> term.

Inductive typing : term -> Prop :=
  | t_var : typing tvar
  | t_list : forall (t:term) (l:list term),
      typing t -> typings l -> typing (tlist t l)
with typings : list term -> Prop :=
  | ts_nil : typings nil
  | ts_cons : forall (t:term) (l:list term),
      typings l -> typing t -> typings (t::l).

Inductive typing2 : term -> Prop :=
  | t2_var : typing2 tvar
  | t2_list : forall (t:term) (l:list term),
      typing2 t -> typings2 l -> typing2 (tlist t l)
with typings2 : list term -> Prop :=
  | ts2_nil : typings2 nil
  | ts2_cons : forall (t:term) (l:list term),
      typings2 l -> typing2 t -> typings2 (t::l).

Scheme typing_ind2 := Minimality for typing Sort Prop
with typings_ind2 := Minimality for typings Sort Prop.

Inductive relation : term -> term -> Prop :=
  | r_var : relation tvar tvar
  | r_list : forall (t t':term) (l l':list term),
      relation t t' -> relations l l' ->
      relation (tlist t l) (tlist t' l')
with relations : list term -> list term -> Prop :=
  | rs_nil : relations nil nil
  | rs_cons : forall (t t':term) (l l':list term),
      relations l l' -> relation t t' -> relations (t::l) (t'::l').

Scheme relation_ind2 := Minimality for relation Sort Prop
with relations_ind2 := Minimality for relations Sort Prop.

Theorem weird : forall (t:term),
  typing t ->
  forall (t':term), relation t t' -> typing2 t'.
Proof.
  intros t Ht t' Hr.
Check typing_ind2.
  apply typing_ind2 with (P:=typing2) (P0:=typings2); intros.
    apply t2_var.

    apply t2_list; assumption.

    apply ts2_nil.

    apply ts2_cons; assumption.

    admit. (* here is my problem *)
Qed.

(* I would solve the goal by inversion on Hr, if "relation" would
   not be mutual. But in this case I think that I also need to
   define a useful induction principle on my own using Scheme.
   (Defined above.)

   But it is not clear to me how to apply it.

   Then, I tried to rewrite the theorem and prove it the other way
   arround. *)

Theorem weird2 : forall (t t':term),
  relation t t' -> typing t -> typing2 t'.
Proof.
  apply (relation_ind2
    (fun t t' => typing t -> typing2 t')
    (fun l l' => typings l -> typings2 l')).
    intros; apply t2_var.

    intros t t' l l' Hr Ht Hrs Hts.
    (*apply (typing_ind2 typing2 typings2).*)
Admitted.

(* The later command cannot be applied since it is impossible to
   unify tlist t' l' and tlist t l.

   I also thought of defining a mutual induction principle on all
   four definitions *)

Scheme typing_mut := Minimality for typing Sort Prop
with typings_mut := Minimality for typings Sort Prop
with relation_mut := Minimality for relation Sort Prop
with relations_mut := Minimality for relations Sort Prop.

(* Unfortunately, this results in an error message that typing and
   relation are not mutually defined.

   Any suggestions how to proof my theorem? *)


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

[Adam Chlipala-3]

Thomas Thüm wrote:
> Inductive term : Prop :=
>   | tvar : term
>   | tlist : term -> list term -> term.
>  

The problem stems from the fact that you've put [term] in [Prop], which
makes [term] values proofs, as far as Coq is concerned.  Coq is
consistent with proof irrelevance, so you won't be able to prove any
fact that requires distinguishing between [tvar] and [tlist] terms.  I
think your theorem really requires the ability to do so.  I was able to
prove the theorem uneventfully after moving [term] to [Set].

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

[Thomas Thüm]

Frederic, thanks for your pointer. It looks interesting, although I cannot
use it, as I'm proving properties that partly rely on existing definitions
that I do not want to change (at the moment).

-----

Adam, thanks, you are right. It happened while simplifying my definitions. I
changed the type from Prop to Set and also added the type nat, that
specifies a variable. See below, I propagated this change also in the
definitions for typing and typing2.

> I was able to prove the theorem uneventfully after moving [term] to [Set].

I'm still not able to prove this, I have exactly the same problems.

-----

Require Export List.

Inductive term : Set :=
  | tvar : nat -> term
  | tlist : term -> list term -> term.

Inductive typing : term -> Prop :=
  | t_var : forall (n:nat), typing (tvar n)
  | t_list : forall (t:term) (l:list term),
      typing t -> typings l -> typing (tlist t l)
with typings : list term -> Prop :=
  | ts_nil : typings nil
  | ts_cons : forall (t:term) (l:list term),
      typings l -> typing t -> typings (t::l).

Inductive typing2 : term -> Prop :=
  | t2_var : forall (n:nat), typing2 (tvar n)
  | t2_list : forall (t:term) (l:list term),
      typing2 t -> typings2 l -> typing2 (tlist t l)
with typings2 : list term -> Prop :=
  | ts2_nil : typings2 nil
  | ts2_cons : forall (t:term) (l:list term),
      typings2 l -> typing2 t -> typings2 (t::l).

Scheme typing_ind2 := Minimality for typing Sort Prop
with typings_ind2 := Minimality for typings Sort Prop.

Inductive relation : term -> term -> Prop :=
  | r_var : forall (n m:nat), relation (tvar n) (tvar m)
  | r_list : forall (t t':term) (l l':list term),
      relation t t' -> relations l l' ->
      relation (tlist t l) (tlist t' l')
with relations : list term -> list term -> Prop :=
  | rs_nil : relations nil nil
  | rs_cons : forall (t t':term) (l l':list term),
      relations l l' -> relation t t' -> relations (t::l) (t'::l').

Scheme relation_ind2 := Minimality for relation Sort Prop
with relations_ind2 := Minimality for relations Sort Prop.

Theorem weird : forall (t:term),
  typing t ->
  forall (t':term), relation t t' -> typing2 t'.
Proof.
  intros t Ht t' Hr.
Check typing_ind2.
  apply typing_ind2 with (P:=typing2) (P0:=typings2); intros.
    apply t2_var.

    apply t2_list; assumption.

    apply ts2_nil.

    apply ts2_cons; assumption.

    admit. (* here is my problem *)
Qed.

(* I would solve the goal by inversion on Hr, if "relation" would
   not be mutual. But in this case I think that I also need to
   define a useful induction principle on my own using Scheme.
   (Defined above.)

   But it is not clear to me how to apply it.

   Then, I tried to rewrite the theorem and prove it the other way
   arround. *)

Theorem weird2 : forall (t t':term),
  relation t t' -> typing t -> typing2 t'.
Proof.
  apply (relation_ind2
    (fun t t' => typing t -> typing2 t')
    (fun l l' => typings l -> typings2 l')).
    intros; apply t2_var.

    intros t t' l l' Hr Ht Hrs Hts.
    (*apply (typing_ind2 typing2 typings2).*)
Admitted.

(* The later command cannot be applied since it is impossible to
   unify tlist t' l' and tlist t l.

   I also thought of defining a mutual induction principle on all
   four definitions *)

Scheme typing_mut := Minimality for typing Sort Prop
with typings_mut := Minimality for typings Sort Prop
with relation_mut := Minimality for relation Sort Prop
with relations_mut := Minimality for relations Sort Prop.

(* Unfortunately, this results in an error message that typing and
   relation are not mutually defined.

   Any suggestions how to proof my theorem? *)

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

[Adam Chlipala-3]

Thomas Thüm wrote:

> I'm still not able to prove this, I have exactly the same problems.
>
> -----
>
> [snip]
>
> Theorem weird : forall (t:term),
>   typing t ->
>   forall (t':term), relation t t' -> typing2 t'.
> Proof.
>   intros t Ht t' Hr.
> Check typing_ind2.
>   apply typing_ind2 with (P:=typing2) (P0:=typings2); intros

You are choosing overly weak induction hypotheses.  You need
[relation]'s arguments to vary with your induction variable; the code
you give keeps [relation]'s arguments fixed over the whole induction.  
The proof really is trivial if you change the IHs to include
[relation]/[relations].  You don't need any nested inductions.

Let us know if trying this change doesn't leave the way clear.

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

[Bruno De Fraine-2]

Hello Thomas,

On 12 Nov 2009, at 08:53, Thomas Thüm wrote:

>> I was able to prove the theorem uneventfully after moving [term] to [Set].
>
> I'm still not able to prove this, I have exactly the same problems.

I find this kind of mutual induction works better if you generate a combined scheme (see refman, sec. 10.3.1) and formulate the goal for both relation/relations (or both typing/typings).

Using your definitions I did:

Hint Constructors typing typings typing2 typings2 relation relations.

Scheme relation_relations_ind := Minimality for relation Sort Prop
with relations_relation_ind := Minimality for relations Sort Prop.

Combined Scheme relation_mutind from relation_relations_ind, relations_relation_ind.

Lemma weird':
  (forall t t', relation t t' -> typing t -> typing2 t') /\
  (forall l l', relations l l' -> typings l -> typings2 l').
Proof.
apply relation_mutind; intros; try (inversion H3; subst); auto.
Qed.

Theorem weird:
  forall t t', typing t -> relation t t' -> typing2 t'.
Proof.
destruct weird' as (Hw,_).
eauto.
Qed.

HTH,
Bruno

--
Bruno De Fraine
Vrije Universiteit Brussel
Faculty of Sciences, DINF - SOFT
Room 10F744, Pleinlaan 2, B-1050 Brussels
tel: [phone]
e-mail: Bruno.De.Fraine@...




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

[Thomas Thüm]

Bruno, thanks for your solution. Apparently, this works fine for the example
that I've posted. :)

But as far as I can tell it only works, since the number of mutual
definitions in typing/typings and relation/relations is identical (2 in each
case). Unfortunately, this is not the case in what I really need to proof.
There, typing consists of three mutually definitions.

Hence, I come up with slightly changed definitions that hopefully better
represent my problem.

Thanks for your efforts,
Thomas

----- My definitions and an unsuccessful try with the combined scheme -----

Require Export List.

Inductive term : Set :=
  | tvar : nat -> term
  | tlist : term -> list term -> term.

Inductive w : term -> term -> Prop :=
  | w_var : forall (n m:nat), n < m -> w (tvar n) (tvar m)
  | w_list : forall (t t':term) (l l':list term),
      w t t' -> w (tlist t l) (tlist t' l').

Inductive typing : term -> Prop :=
  | t_var : forall (n:nat), typing (tvar n)
  | t_list : forall (t:term) (l:list term),
      typing t -> wtypings l -> typing (tlist t l)
with wtyping : term -> Prop :=
  | wt : forall (t t':term), typing t -> w t t' -> wtyping t'
with wtypings : list term -> Prop :=
  | ts_nil : wtypings nil
  | ts_cons : forall (t:term) (l:list term),
      wtypings l -> wtyping t -> wtypings (t::l).

Inductive typing2 : term -> Prop :=
  | t2_var : forall (n:nat), typing2 (tvar n)
  | t2_list : forall (t:term) (l:list term),
      typing2 t -> wtypings2 l -> typing2 (tlist t l)
with wtyping2 : term -> Prop :=
  | wt2 : forall (t t':term), typing2 t -> w t t' -> wtyping2 t'
with wtypings2 : list term -> Prop :=
  | ts2_nil : wtypings2 nil
  | ts2_cons : forall (t:term) (l:list term),
      wtypings2 l -> wtyping2 t -> wtypings2 (t::l).

Inductive relation : term -> term -> Prop :=
  | r_var : forall (n m:nat), relation (tvar n) (tvar m)
  | r_list : forall (t t':term) (l l':list term),
      relation t t' -> relations l l' ->
      relation (tlist t l) (tlist t' l')
with relations : list term -> list term -> Prop :=
  | rs_nil : relations nil nil
  | rs_cons : forall (t t':term) (l l':list term),
      relations l l' -> relation t t' -> relations (t::l) (t'::l').

Hint Constructors w typing wtyping wtypings typing2 wtyping2
  wtypings2 relation relations.

Scheme relation_relations_ind := Minimality for relation Sort Prop
with relations_relation_ind := Minimality for relations Sort Prop.

Combined Scheme relation_mutind from relation_relations_ind,
  relation_relations_ind, relations_relation_ind.

Lemma weird3':
  (forall t t', relation t t' -> typing t -> typing2 t') /\
  (forall t t', relation t t' -> wtyping t -> wtyping2 t') /\
  (forall l l', relations l l' -> wtypings l -> wtypings2 l').
Proof.
  apply relation_mutind.


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

[Thomas Thüm]

My problem is solved, thanks to Bruno. Some hours ago, he wrote me how to
use the combined scheme:

> Scheme relation_relations_ind := Minimality for relation Sort Prop
> with relations_relation_ind := Minimality for relations Sort Prop.
>
> Combined Scheme relation_mutind from relation_relations_ind,
>  relation_relations_ind, relations_relation_ind.

The idea was to combine typing and wtyping into one case:

> Lemma weird3:
>   (forall t t', relation t t' -> (typing t -> typing2 t') /\ (wtyping t ->
wtyping2 t')) /\
>   (forall l l', relations l l' -> wtypings l -> wtypings2 l').
> Proof.
>   apply relation_mutind.

Note, that also my second example was wrong in the sense, that the negation
of the above theorem can be proved. (Bruno proved this.) Anyway, the example
was just to explain my problem.

Although this induction principle is useful it is not very strong. My proof
contains many cases that are very similar. I just started working with Coq
so I can't tell if a change to Coq to better support mutual inductions is
possible or worth (I'm not sure how often such mutual inductions do appear).

Thanks for your help,
Thomas

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

[Adam Chlipala-3]

Thomas Thüm wrote:
> Although this induction principle is useful it is not very strong.

What do you mean?  I can't think of a stronger principle that is still
sound.

> My proof
> contains many cases that are very similar. I just started working with Coq
> so I can't tell if a change to Coq to better support mutual inductions is
> possible or worth (I'm not sure how often such mutual inductions do appear).
>  

It's hard for me to picture better support for mutual induction, in any
sense that has a significant impact on the effort required to build
proofs.  What do you have in mind?

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