The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Sun, Mar 11, 2007 at 09:40:54AM +0100, Pierre Castéran wrote:
> 
> Hi,
> 
>   Did you try structural induction (e.g. on G or t) plus inversion
> on some predicate (e.g. typeof) ?

Ah, yes, that might work in this particular case, since only one typing
rule will apply to any term. I would still like to know if it would be
possible by induction on typeof itself, but thanks for the suggestion!

>   If no simple solution work, it may be useful to send a minimal
> environnment with adequate definitions for us to experiment solutions.

Ok, I've tried to minimize the example: the example below is fully
self-contained. The proof talks about preservation of types under
substitution in the lambda calculus, but that really doesn't matter, and
in fact I've cut out almost all the details. We have an inductive type
"Term"; for the current purposes, all that matters is that it is
recursive:

  Inductive Term : Set := abs : Term -> Term.

We have a type corresponding to (typing) contexts, two functions f and g
on contexts. 

  Variable context : Set.

  Variable f : context -> context.
  Variable g : context -> context.

  Inductive welltyped : context -> Term -> Prop :=
    | T_abs : forall (G:context) (t:Term),
        welltyped (f G) t -> welltyped G (abs t).

We then define the "welltyped" relation (a cut-down version of the
"typeof" relation), and a permutation lemma that states that if a term
is welltyped in a context (f (g G)), then it is welltyped in a context
(g (f G)).

  Hypothesis permutation : forall (G:context) (t:Term),
    welltyped (f (g G)) t -> welltyped (g (f G)) t. 

Now, I need to prove some property Q:

  Variable Q : Prop.

  Lemma preservation_under_subst : 
    forall (t:Term) (G:context), welltyped (g G) t -> Q.

It turns out actually that we can prove this with your suggestion, using
structural induction on the term t, rather than on the derivation of
welltyped t:

  Lemma preservation_under_subst : 
    forall (t:Term) (G:context), welltyped (g G) t -> Q.
  induction t.
  intros G Ht.
  inversion Ht.
  apply IHt with (G := (f G)).
  apply permutation ; assumption.
  Qed.

But I cannot do a proof on the derivation of welltyped. First attempt
uses the "cut-technique" from Coq'Art 8.4.3:

  Lemma preservation_under_subst2:
    forall (t:Term) (G:context), welltyped (g G) t -> Q.
  intros t G.
  cut(forall G':context, welltyped G' t -> G' = g G -> Q).
  intros ; apply (H (g G)) ; reflexivity || assumption.
  intros G' Ht.
  generalize Ht.
  elim Ht.
  intros.
  subst G0.
  Admitted.

At the point of the "Admitted" we're stuck, because to be able to use
the induction hypothesis, we'd have to prove that (f (g G)) = (g G),
which is impossible. We can get a bit further by universally quantifying
G in the cut:

  Lemma preservation_under_subst3:
    forall (t:Term) (G:context), welltyped (g G) t -> Q.
  intros t G0.
  cut(forall G':context, welltyped G' t -> forall (G:context), G' = g G -> Q).
  intros ; eapply (H (g G0)); reflexivity || assumption.
  intros G' Ht.
  generalize Ht.
  elim Ht.
  intros.
  subst G.
  Admitted.

But again, we get stuck at the point of "Admitted": to be able to use
the induction hypothesis, we'd have to prove that (f (g G)) = (g (f G)),
which is closer to what we can prove (the permutation lemma), but still
too strong. 

Edsko