単純型のラムダ計算の閉じた項の自由変数の帰納仮説

Question

単純な型のラムダ計算をCoqで形式化しようとしています。空のコンテキストは空です。

これは正式化の関連部分です。

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) 

と言います。私は、表現の上に誘導を試み、正しい帰納仮説を得るために定理を再定式化しましたが、それを理解できませんでした。

このプロパティを定義して証明する正しい方法は何ですか？

ソリューション

はejgallegoさんのコメントへのイヴanswerと感謝の後、私は最初に一般化補題を証明しました。

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の空き変数のセットがコンテキスト内の型を持つ変数の中になければならないことを表現する必要があります。