The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

I don't think this is just an issue with fiddly behavior of the 
inversion tactic.  You couldn't prove the same theorem on paper with a 
single inversion, either.  You need induction.

The definition of [ctx_cons] allows multiple derivations of the same 
fact.  The nondeterminism comes from the order in which you consider the 
variables.

So, the particular [ctx_cons] derivation you have as a hypothesis may 
not consider variable [x] "last."

On 11/22/2015 03:27 AM, Flávio Leonardo Cavalcanti de Moura wrote:
> 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.