The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-11-22 9:27 GMT+01:00 Flávio Leonardo Cavalcanti de Moura <flaviomoura AT unb.br>:

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.

​I do not think this is provable in Coq.

Adam said that you need at least induction, but in fact, even with induction​, I doubt you can prove it.

Although what follows is not a proof of the fact that it is unprovable, I hope to convince you, that, at least, it is not as trivial as it seems.

Consider var=unit and A=bool, to simplify.

Now, we have 3 possible partial_map (assuming functionnal extensionnality):

pm_bot := fun _ => None (* pm_bot = empty *)

pm_true := fun _ => Some true

pm_false := fun _ => Some false

Always assuming functionnal extensionnality, we have: "extend pm_bot tt true = extend pm_false tt true = extend pm_true tt true".

Thus, "P := nempt_cons pm_bot tt true empty_cons (eq_refl None)" is a proof of "ctx_cons (extend pm_bot tt true)".

Thus it is also a proof of "ctx_cons (extend pm_false tt true)".

Now, you can see your previous context as:

​​  pm_false : context
  tt : var
  true : ty
  P : ctx_cons (extend pm_false tt true)
  pm_bot : context
  tt : var
  true : ty
  empty_cons : ctx_cons pm_bot
  eq_refl None : pm_bot tt = None
  extensionnality … : extend pm_bot tt true = extend pm_false tt true
  ============================
   ctx_cons pm_false

As you can see, you end up with Gamma0 different from Gamma.

Of course, "ctx_cons pm_false" remains provable, but with a direct construction, not the inversion.

Indeed, what you had in mind was that at this point you should have "Gamma = pm_bot", which is not necessarily the case here.

In a more general setting where var is not simply unit, and A not simply bool, things can be even more complex, and I suspect them not to be always provable.

Well, I assumed functionnal extensionnality. This axiom is often assumed to be consistent with Coq without any additionnal axiom.

The point is that with such an axiom, extend is not inversible, you can have several extension leading to the same partial map.

Inversion tactic works mainly when your data types are inductives.

For instance, if you had defined partial_map as:

Inductive partial_map (A : Type) :=

| pm_empty : partial_map A

| pm_extend : var -> A -> partial_map A -> partial_map A.

and coerce its evaluation with

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

  fix eval_ pm :=

  match pm with

  | pm_empty => fun _ => None

  | pm_extend x v pm => fun y => if eq_var_dec x y then Some v else eval_ pm y

  end.

Then for the same reasons as previously, you could not prove easily:

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

where "extend" is your own definition applied to "@eval A Gamma" instead of Gamma.

Still, you could prove

​

​Lemma subctx_cons: forall (Gamma:context) (x:var) (U:ty), ctx_cons2 (pm_extend Gamma x U) -> ctx_cons2 Gamma.
​

​Inductive ctx_cons2: context -> Prop :=
| empty_cons: ctx_cons pm_empty
| nempt_cons: forall Gamma x U, ctx_cons2 Gamma -> eval Gamma x = None -> ctx_cons2 (pm_extend Gamma x U).

Simply because this time, pm_extend is injective (given Gamma x and U, there is only one Gamma0 x0 and U0 such that pm_extend Gamma x U = pm_extend Gamma0 x0 U0).