The Coq mailing list

[flaviomoura AT unb.br (Flávio Leonardo Cavalcanti de Moura)]

Hi there, 

I am trying to prove a property that should be straightforward, but due
to a kind of renaming of the inversion tactic, I don't know how to complete 
the
proof. I am doing an adaptation of B. Pierce SF course, in which contexts (for
 cbv simply typed lambda calculus) are
defined as follows:

Definition partial_map (A:Type) := var -> option A.

Definition empty {A:Type} : partial_map A := (fun _ => None). 

Definition extend {A:Type} (Gamma : partial_map A) (x:var) (T : A) :=
  fun x' => if eq_var_dec x x' then Some T else Gamma x'.

Definition context := partial_map ty.

I want to prove subject reduction for the (general) simply typed lambda 
calculus,
so I defined consistency of contexts as follows:

Inductive ctx_cons: context -> Prop :=
| empty_cons: ctx_cons empty
| nempt_cons: forall Gamma x U, ctx_cons Gamma -> Gamma x = None -> ctx_cons 
(extend Gamma x U).  

Now I want to prove that:

Lemma subctx_cons: forall (Gamma:context) (x:var) (U:ty), ctx_cons (extend 
Gamma x U) -> ctx_cons Gamma.

It should be straightforward by inversion tactic on the hypothesis H:
ctx_cons (extend Gamma x U), but instead of getting as hypothesis
ctx_cons Gamma, coq generates the following for the second case of the 
definition:

 Gamma : context
  x : var
  U : ty
  H : ctx_cons (extend Gamma x U)
  Gamma0 : context
  x0 : var
  U0 : ty
  H1 : ctx_cons Gamma0
  H2 : Gamma0 x0 = None
  H0 : extend Gamma0 x0 U0 = extend Gamma x U
  ============================
   ctx_cons Gamma

I don't see how to prove, for instance, that Gamma = Gamma0 because they
don't need to be syntactic the same...

Thanks in advance for any help.

Best regards, 
Flávio.