The Coq mailing list

[Thomas Th�m <thomas.thuem AT st.ovgu.de>]

Hi all,

I’m working on a formalization of the simply-typed lambda calculus. I need
induction for a particular proof and I think the induction hypotheses are
wrong. I attached the definitions at the end of the mail, note that this is
already a reduced version, where I left out some cases for simplicity.

Running all the code below Coq leads me to the following output:

...
T : type
...
IHt1 : typing ((x, S) :: G) t1 T -> typing G (termSubst x s t1) T
IHt2 : typing ((x, S) :: G) t2 T -> typing G (termSubst x s t2) T
...

But I would expect it to be (see rule typingApp below):

...
T : type
T11 : type
...
IHt1 : typing ((x, S) :: G) t1 (typeFun T11 T) -> typing G (termSubst x s
t1) (typeFun T11 T)
IHt2 : typing ((x, S) :: G) t2 T11 -> typing G (termSubst x s t2) T11
...

Clearly, "induction t as [...T11...]" does not work since Coq uses the bound
variable T.

Am I wrong?

Thanks in advance,
Thomas

-----

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.

(*** TYPING ***)

Inductive typing : context -> term -> type -> Prop :=
 | typingVar : forall (G:context) (x:termType) (T:type),
     (exists G1:context, exists G2:context,
       G = List.app G1 (List.cons (x,T) G2)) ->
     typing G (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.

(*** PRESERVATION ***)

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.
  intros.
  induction t.
  admit.