The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Who said that nobody would ever read Sect. 8.4.3 of Coq'Art.

It is a rare case when you need both to do a proof by induction and have 
some of the arguments be non-variables.  For this reason, Coq provides 
only two tactics: one is elim (and I consider induction to be only a 
derivative of elim), and the other is inversion.  The construct with 
equalities is actually performed by inversion, and long practice has 
taught us that this almost always yielded inductions hypotheses that 
were unusable.

The example of Coq'Art 8.4.3 happens to be a lucky case, because the 
induction hypothesis has the
constraint "i0 = WhileDo b i" but this constraint will be satisfied by 
the sub-proof of execution.
This comes from the fact that the semantic definition contains the 
following constructor, where exactly the same term "(WhileDo e i)" 
occurs twice:

execWhileTrue :
 forall (s s1 s2:state)(i:inst)(e:bexp),
    eval b s e = Some true -> exec s i s1 -> exec s1 (WhileDo e i) s2 
-> exec s (WhileDo i) s2

(p. 240).

The proof by induction that occurs on p. 243 actually is a proof by 
induction on the length of
a branch where the subject of the semantic judgment is always the same 
"WhileDo e i".

If this technique does not fit your needs, it must be because you want 
to distinguish the length of branches through another "filter" than just 
being equal to "WhileDo e i"

I suggest you reorganize your proof to make the right filter appear.  In 
other words, you should prove:

forall G' t T, typeof G' t T -> Q G' t T

where Q is chosen to be stronger than

forall x S s (pf:disjoint eq_var_dec (x::fv s)(bv t)), G' = upd x S G ->
 typeof G s S -> typeof G (subst x s t pf) T

The above two line is not exactly what you have been doing so far.

Here is an example of strengthening:

Definition Q (G':context)(t:Term)(T:Type) :=
forall pf:disjoin eq_var_dec (f2 G'::fv s)(bv t), P G' -> typeof (f1 G') 
s (f3 S)

where P is an arbitrary predicate on the context type
such that forall x S G, G'=upd x S G->P G',
f1 is an arbitrary function such that forall x S G, f1(upd x S G) = G,
f2 is an arbitrary function such that forall x S G, f2(upd x S G) = x, and
f3 is an arbitrary function such that forall x S G, f3(upd x S G) = S

Here is another example of strengthening:

Definition Q (G':context)(t:Term)(T:Type) :=
 forall x S s (pf:disjoint eq_var_dec (x::fv s)(bv t)), G' = upd x S G ->
 typeof G s S -> typeof G (subst x s t pf) T /\
 Q' G' t T.

Where the predicate Q' is designed to cover the cases that are not 
covered by the filter
  exists x, exists S, exists G,  G' = upd x S G

Philosophically, this fits the general observation that when a proof by 
induction fails, you need to strengthen the statement you want to 
prove.  Imposing the shape (upd x S G) gives too weak a statement,
so you may want to relax this constraint by using a more general predicate.

Please tell us back whether this was useful.

Yves

Ps.  Here is another idea: try as an exercise to imagine encoding a 
many-sorted algebra (or two mutually inductive types) using a single 
type: you end up mixing all the constructors in the single type.  Now, if
you want to mimick proofs by mutual induction, you need to exhibit two 
predicates, one for each the mutually inductive types and apply each one 
only on the terms obtained with the relevant constructors.
In the proof on p. 243, this is what we do: we consider only the 
sub-inductive type consisting only of executions of while loops, but if 
we wanted to consider a larger sub-inductive type (say while loops and  
assignments) we would have to use a stronger approach.  The second 
approach of strengthening above is actually inspired by the way we 
simulated mutually inductive types in Coq at a time when Coq did not 
have mutually inductive types.