Induction hypothesis for free variables of closed term in the simply typed lambda calculus

Question

I am trying to formalize the simply typed lambda calculus in Coq and have a problem stating the lemma that the set of free variables of a well-typed expression in an empty context is empty.

Here is the relevant part of may formalisation.

Require Import Coq.Arith.Arith.
Require Import Coq.MSets.MSets.
Require Import Coq.FSets.FMaps.

Inductive type : Set :=
| tunit : type
| tfun : type -> type -> type.

Module Var := Nat.
Definition var : Set := Var.t.
Module VarSet := MSetAVL.Make Var.
Module VarSetFacts := MSetFacts.Facts VarSet.
Module VarSetProps := MSetProperties.Properties VarSet.
Module Context := FMapWeakList.Make Var.
Module ContextFacts := FMapFacts.Facts Context.
Module ContextProps := FMapFacts.Properties Context.
Definition context := Context.t type.
Definition context_empty : context := Context.empty type.

Inductive expr : Set :=
| eunit : expr
| evar : var -> expr
| eabs : var -> type -> expr -> expr
| eapp : expr -> expr -> expr.

Fixpoint free_vars (e : expr) : VarSet.t :=
  match e with
  | eunit => VarSet.empty
  | evar y => VarSet.singleton y
  | eabs y _ e => VarSet.remove y (free_vars e)
  | eapp e1 e2 => VarSet.union (free_vars e1) (free_vars e2)
  end.

Inductive has_type : context -> expr -> type -> Prop :=
| has_type_unit : forall c,
    has_type c eunit tunit

| has_type_var : forall c x t,
    Context.find x c = Some t ->
    has_type c (evar x) t

| has_type_abs : forall c x t1 t2 e,
    has_type (Context.add x t1 c) e t2 ->
    has_type c (eabs x t1 e) (tfun t1 t2)

| has_type_app : forall c e1 e2 t1 t2,
    has_type c e1 (tfun t1 t2) ->
    has_type c e2 t1 ->
    has_type c (eapp e1 e2) t2.

Check has_type_ind.

Lemma has_type_empty_context_free_vars : forall e t,
  has_type context_empty e t ->
  VarSet.Empty (free_vars e).
Proof.
  intros e t H.
  remember context_empty as c.
  induction H; subst.
  - apply VarSet.empty_spec.
  - rewrite ContextFacts.empty_o in H.
    congruence.
  - simpl.
    admit. (* Wrong induction hypothesis *)
  - simpl.
    rewrite VarSetProps.empty_union_1; auto.
Admitted.

The problem seems to be that my induction hypothesis is wrong. It merely says

Context.add x t1 context_empty = context_empty ->
  VarSet.Empty (free_vars e)

which is trivially true, since the hypothesis is false. I tried an induction over the expression and to reformulate the theorem to get the right induction hypothesis, but could not figure it out.

What is the correct way to define and prove this property?

Solution

Following Yves' answer and thanks to ejgallego's comment, I first proved a generalized lemma.

Lemma has_type_free_vars_in_context : forall c e t,
  has_type c e t ->
  VarSet.For_all (fun x => Context.mem x c = true) (free_vars e).
Proof.
  intros c e t H.
  induction H; simpl.
  - intros x contra.
    apply VarSetFacts.empty_iff in contra.
    inversion contra.
  - intros y H2.
    apply Context.mem_1.
    apply ContextFacts.in_find_iff.
    apply VarSet.singleton_spec in H2.
    subst.
    rewrite H.
    discriminate.
  - intros y H2.
    unfold VarSet.For_all in *.
    apply VarSet.remove_spec in H2 as [H2 H3].
    specialize (IHhas_type y H2).
    rewrite ContextFacts.add_neq_b in IHhas_type; auto.
  - intros x H2.
    apply VarSet.union_spec in H2 as [H2 | H2]; auto.
Qed.

And used to use it to prove my theorem.

Lemma has_type_empty_context_free_vars : forall e t,
  has_type context_empty e t ->
  VarSet.Empty (free_vars e).
Proof.
  intros e t H.
  apply has_type_free_vars_in_context in H.
  induction (free_vars e) using VarSetProps.set_induction.
  - assumption.
  - rename t0_1 into s.
    rename t0_2 into s'.
    apply VarSetProps.Add_Equal in H1.
    unfold VarSet.For_all in *.
    specialize (H x).
    rewrite H1 in H.
    specialize (H (VarSetFacts.add_1 s eq_refl)).
    Search (Context.empty).
    rewrite ContextFacts.empty_a in H.
    discriminate.
Qed.

It now works. Thank you very much. Is there a way to refactor this solution for more automation, better readability, better maintenance, etc.?

Search _ VarSet.For_all. will give you some help, anyways the definition is directly utilizable, as it is just a regular lemma: For_all P s := forall x : elt, x \in s -> P x. so if you have a proof of membership for x, you can derive P x directly. — ejgallego
Thanks, it now works. Do you have some advices to improve the proofs? — authchir

Yves Yves · Accepted Answer · 2017-12-02T13:21:14

You were right to perform induction on the hypothesis of statement "has_type ...", but you probably need to load the induction. In other words, you need to prove a stronger statement, make the environment a variable, and express that the set of free variables in e must be inside the variables that have a type in your context.

Induction hypothesis for free variables of closed term in the simply typed lambda calculus

Solution

1 Answers