단순한 형식의 람다 계산식에서 닫힌 용어의 자유 변수에 대한 유도 가설

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에있는 자유 변수 세트가 컨텍스트에 유형이있는 변수 안에 있어야한다는 것을 표현해야합니다.