The Coq mailing list

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

Edsko de Vries a écrit :
> Hi Thomas,
>
> You're applying the induction hypothesis too late. If you do
>
> Lemma preservationOfSubstitution: forall (G:context) (x:termType) (t 
> s:term)
>    (T S:type),
>    typing ((x, S) :: G) t T ->
>    typing G s S ->
>    typing G (termSubst x s t) T.
> Proof.
>   induction t.
>
> instead of doing itnros first, you'll find that the T in the induction 
> hypothesis is universally quantified.
>
> Generally, if you do induction over something, you should avoid 
> introducing unnecessary other variables first as your induction 
> hypothesis might not be useable.
(* 1 *)
I also add some completion to your statement:
"Generally, if you do induction over something, you should avoid 
generalizing unnecessary other variables first as your induction 
hypothesis might really heavy."

(* 2 *)
Test your goals...:

Assume:

Lemma preservationOfSubstitution: forall (G:context) (x:termType) (t s:term)
   (T S:type),
   typing ((x, S) :: G) t T ->
   typing G s S ->
   typing G (termSubst x s t) T.



Then the type of

preservationOfSubstitution [(0, 0);(1, 1)] 0 (termVar 0) (termVar 1) (typeVar 
0) (typeVar 1) (...) (...)

would be:

typing [(0, 0);(1, 1)] (typeVar 1) 0

which is wrong!
That is:
x : Ty, x : Tx, y : Ty |- (var)x : Tx =>
x : Tx, y : Ty |- (var)y : Ty =>
x : Tx, y : Ty |- [x -> y](var)x : Tx

(* 3 *)
Choose better your inductive hypothesis (which in fact is not t here, 
but "_ : typing ((x, S) :: G) t T")

(* 4 *)
Do not have "constant" parameters in your inductive types (it can be 
painful to deal with them...)

"Inductive typing (G : context) : term -> type -> Prop := ..." is better 
than
"Inductive typing : context -> term -> type -> Prop := ...".
(or use:

Inductive typing : context -> term -> type -> Prop :=
| typingVar : forall (G1 G2:context) (x:termType) (T:type),
    typing (List.app G1 (List.cons (x,T) G2)) (termVar x) T
| typingApp : forall (G:context) (t1 t2:term) (T11 T12:type),
    typing G t1 (typeFun T11 T12) ->
    typing G t2 T11 ->
    typing G (termApp t1 t2) T12

)

(* 5 *)
Don't hesitate to use Notations (at least defined ones).
so use a::b rather than List.cons a b
or a++b rather than List.app a b
That is not more efficient, but more readable.

(* 6 *)
Take a look at the standard library to have ideas

(exists G1:context, exists G2:context,
      G = List.app G1 (List.cons (x,T) G2))

is not as clear as:

In (x, T) G 


Summary:
* try to get counter examples before beginning
* when defining functions/inductive types think of their use to make 
them convenient
(all constant parameters at the beginning, I often write "Definition 
foo a b c := fix ..." instead of "Fixpoint foo a b c ...",
 and "Inductive Foo (a : A) (b : B) (c : C) : ..." instead of 
"Inductive Foo : A -> B -> C -> ...")
* introduce ALL variables (whatever their sort: Prop, Type, Set, nat, 
bool, ...)
* generalize on all NECESSARY ones for induction so you have a 
minimalist but sufficient system for your proof.
 (often, all these variables are at the end of the lemmas for 
dependence reasons, but not always, so you just have
   to introduce all variables until the one of the induction, that is 
what is done with "induction" tactic)

To conclude here is what I may have done (and did for you)

*Require Import Arith.
Require Import List.

(*** SYNTAX ***)

(* type T *)
Definition typeType := nat.
Inductive type : Set :=
| typeVar : typeType -> type
| typeFun : type -> type -> type.

(* term t *)
Definition termType := nat.
Inductive term : Set :=
| termVar : termType -> term
| termApp : term -> term -> term.

(* context Gamma *)
Definition context : Set := list (termType*type).

(*** AUXILIARY ***)

(* equality between terms *)
Lemma eqTermType: forall (x y:termType), {x = y} + {x <> y}.
Proof.
 auto with *.
Qed.

(* [x->s]t --- substitution of variable x by term s in term t *)
Fixpoint termSubst (x:termType) (s t:term) : term :=
 match t with
 | (termVar x1) => if eqTermType x1 x then s else (termVar x1)
 | (termApp t1 t2) => termApp (termSubst x s t1) (termSubst x s t2)
end.
Notation "[ x >> s ] t" :=
(termSubst x s t) (at level 100).

(*** TYPING ***)

Inductive typing (G : context) : term -> type -> Prop :=
| typingVar : forall (x:termType) (T:type),
    In (x, T) G ->
    typing G (termVar x) T
| typingApp : forall (t1 t2:term) (T11 T12:type),
    typing G t1 (typeFun T11 T12) ->
    typing G t2 T11 ->
    typing G (termApp t1 t2) T12.
Notation "{{ G |- <[ t ]> : T }}" :=
(typing G t T).

(*** PRESERVATION ***)

Lemma Weakening: forall (G:context) (x:termType) (T S:type) (t:term),
   {{G |- <[t]>: T}} -> {{(x, S) :: G |- <[t]>: T}}.
Proof.
 intros.
 induction H.
   apply typingVar; intuition.
   apply typingApp with T11; intuition.
Defined.

Lemma preservationOfSubstitution: forall (G:context) (x:termType) (t s:term)
   (T S:type),
   (forall K, In (x, K) G -> K = S) ->
   {{(x, S) :: G |- <[t]>: T}} ->
   {{G |- <[s]>: S}} ->
   {{(x, S) :: G |- <[[x >> s]t]>: T}}.
Proof.
 intros G x t s T S H K.
 induction K; simpl in *; intuition.
   destruct (eqTermType x0 x); auto.
     inversion H2; rewrite <- H4; apply Weakening; auto.
     destruct n; inversion H2; auto.
   destruct (eqTermType x0 x); auto.
     rewrite e in H2; clear e x0.
     rewrite (H T H2); apply Weakening; auto.
     apply typingVar; intuition.
   apply typingApp with T11; auto.
Qed.*


> Hope that helps,
>
> Edsko
>
> --------------------------------------------------------
> 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