简单类型λ演算中闭项自由变量的归纳假设

Question

我试图在 Coq 中形式化简单类型的 lambda 演算，但在陈述引理时遇到问题，即空上下文中类型良好的表达式的自由变量集为空。

这里是五月形式化的相关部分。

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.

问题好像是我的归纳假设是错误的。它只是说

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

这完全正确，因为假设是错误的。我尝试对表达式进行归纳并重新表述定理以获得正确的归纳假设，但无法弄清楚。

定义和证明这个属性的正确方法是什么？

解决方案

跟随 Yves 的并感谢 ejgallego 的评论，我首先证明了一个广义引理。

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.

并用来证明我的定理。

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.

现在可以了。非常感谢。有没有办法重构这个解决方案以获得更多的自动化、更好的可读性、更好的维护等？

Answer 1

你对语句"has_type ..."的假设进行归纳是正确的，但你可能需要加载归纳。换句话说，您需要证明一个更强的陈述，使环境成为一个变量，并表示 e 中的自由变量集必须在您的上下文中具有类型的变量内部。

简单类型λ演算中闭项自由变量的归纳假设

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

coq

lambda-calculus

induction

解决方案