The Coq mailing list

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

Dear Cedric and Adam, 

Thank you very much for your comments. In fact, working with an inductively
defined context (instead of a partial function) allows such a
straightforward proof by inversion that I had in mind. Therefore, the 
nondeterminism
mostly comes from the non-inductive structure of the context, and
therefore extend is not invertible and Coq cannot infer that a context is
either empty or (extend Gamma x U) for some Gamma, x and U. 

Best regards, 
Flávio.

Inductive context :=
| ctx_empty : context 
| ctx_extend : context -> var -> ty -> context.

Fixpoint eval (c: context) (y: var): option ty :=
  match c with
    | ctx_empty => None
    | ctx_extend pm' x T => if eq_var_dec x y then Some T else eval pm' y
  end.

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

Lemma subctx_cons: forall Gamma x U, ctx_cons (ctx_extend Gamma x U) -> 
ctx_cons Gamma.
Proof.
  intros Gamma x U H.
  inversion H; subst. assumption.
Qed.



Cedric Auger 
<sedrikov AT gmail.com>
 writes:

> 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).