Commit 2558937b authored by Gaspard Ferey's avatar Gaspard Ferey

Proofs are working !

parent 6d2a5c7d
......@@ -101,17 +101,24 @@ Notation "[ ]" := CEmpty (at level 0).
Notation "Γ ',' x ':' A" := (CVar x A Γ) (at level 30, x at level 30).
Notation "Γ ',' t '≡' u" := (CRel t u Γ) (at level 30, t at level 30).
Definition pop_context (c:context) : context :=
match c with
| CEmpty => c
| CVar _ _ c => c
| CRel _ _ c => c
Definition pop_context (Γ:context) : context :=
match Γ with
| CEmpty => Γ
| CVar _ _ Γ => Γ
| CRel _ _ Γ => Γ
end.
Fixpoint defined_vars (Γ:context) : list Var :=
match Γ with
| CEmpty => nil
| CVar x _ Γ => cons x (defined_vars Γ)
| CRel _ _ Γ => (defined_vars Γ)
end.
Reserved Notation "x ':' A '∈' Γ" (at level 80, A at level 80, Γ at level 80).
Inductive InCtx : context -> Var -> term -> Prop :=
| INow : forall Γ x A, x : A (Γ, x : A)
| IAfterV : forall Γ A x y B, x : A Γ -> x : A (Γ, y : B)
| IAfterV : forall Γ A x y B, x : A Γ -> x <> y -> x : A (Γ, y : B)
| IAfterR : forall Γ A x t u, x : A Γ -> x : A (Γ, t u)
where "x ':' A ∈ Γ" := (InCtx Γ x A).
......@@ -128,6 +135,24 @@ Definition Fresh_var Γ v := ~ (Defined_var Γ v).
Notation "x '∈' Γ" := (Defined_var Γ x) (at level 90).
Notation "x '∉' Γ" := (Fresh_var Γ x) (at level 90).
Theorem defined_eq : forall Γ v, Defined_var Γ v <-> In v (defined_vars Γ).
Proof.
intros.
split; intros.
- induction H. induction H.
+ left. easy.
+ right. easy.
+ easy.
- induction Γ.
+ contradiction H.
+ destruct (var_dec v v0).
* subst. econstructor. econstructor.
* assert (v Γ). apply IHΓ. destruct H. contradiction n. easy. easy.
destruct H0. econstructor. apply IAfterV. apply H0. easy.
+ assert (v Γ). apply IHΓ. exact H.
destruct H0. econstructor. apply IAfterR. apply H0.
Qed.
(* ************ Locally nameless representation ************ *)
......@@ -287,7 +312,7 @@ Inductive typing : context -> term -> term -> Prop :=
(forall x, ~ (In x L) -> Γ, x : A t[x] : B[x]) ->
Γ λ A ~ t : Π A ~ B
| TyApp : forall Γ t u A B, Γ t : Π A ~ B -> Γ u : A -> Γ t @ u : B [0 <- u]
| TyConv : forall Γ t A B s, (Γ t : A) -> (Γ B : s) -> Γ A B -> (Γ t : B)
| TyConv : forall Γ t A B s, Γ t : A -> Γ B : s -> Γ A B -> Γ t : B
where "Γ '⊢' t ':' A" := (typing Γ t A)
with well_formed : context -> Prop :=
| WFEmpty : [ ]
......
......@@ -4,29 +4,80 @@ Require Import List.
Require Import LPTerm.
Theorem types_WF : forall Γ t u, Γ t : u -> Γ .
Lemma types_WF : forall Γ t u, Γ t : u -> Γ .
Proof. intros. induction H; easy. Qed.
Theorem vardecl_WF : forall Γ x A, Γ, x : A -> Γ .
Lemma vardecl_WF : forall Γ x A, Γ, x : A -> Γ .
Proof.
intros.
remember (Γ, x : A) as Γ2.
induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0.
Qed.
Theorem ruldecl_WF : forall Γ t u, Γ, t u -> Γ .
Lemma ruldecl_WF : forall Γ t u, Γ, t u -> Γ .
Proof.
intros.
remember (Γ, t u) as Γ2.
induction H; inversion HeqΓ2; subst; eapply types_WF; apply H0.
Qed.
Theorem lemma_open_k_FV : forall x B t, In x (FV B) -> forall k, In x (FV (B[k <- t])).
Proof.
do 4 intro.
induction B; intros; try inversion H.
- subst. left. easy.
- inversion H0.
- simpl. eapply in_or_app. edestruct (in_app_or (FV B1) (FV B2) x H).
+ left. eapply IHB1. easy.
+ right. eapply IHB2. easy.
- simpl. eapply in_or_app. edestruct (in_app_or (FV B1) (FV B2) x H).
+ left. eapply IHB1. easy.
+ right. eapply IHB2. easy.
- simpl. eapply in_or_app. edestruct (in_app_or (FV B1) (FV B2) x H).
+ left. eapply IHB1. easy.
+ right. eapply IHB2. easy.
Qed.
Theorem lemma_open_FV : forall x B t, In x (FV B) -> In x (FV (B[t])).
Proof. intros. exact (lemma_open_k_FV x B (# t) H 0). Qed.
Theorem FV_decl_t : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> v Γ.
Proof.
intros.
induction H.
- inversion H0. subst. exists A. easy. inversion H2.
- inversion H0.
- destruct (in_app_or (FV A) (FV B) v H0).
+ apply IHtyping. easy.
+ destruct (var_inf (v :: L)).
assert (v Γ, x : A).
* apply H2.
++ intro. apply H4. right. easy.
++ apply lemma_open_FV. easy.
* inversion H5. inversion H6; subst.
++ contradiction H4. left. easy.
++ exists x0. easy.
- destruct (in_app_or (FV A) (FV t) v H0).
+ apply IHtyping. easy.
+ destruct (var_inf (v :: L)).
assert (v Γ, x : A).
* apply H4.
++ intro. apply H6. right. easy.
++ apply lemma_open_FV. easy.
* inversion H7. inversion H8; subst.
++ contradiction H6. left. easy.
++ exists x0. easy.
- destruct (in_app_or (FV t) (FV u) v H0).
+ apply IHtyping1. easy.
+ apply IHtyping2. easy.
- apply IHtyping1. easy.
Qed.
Reserved Notation "Γ '⊂' Γ'" (at level 80).
Inductive weaker : context -> context -> Prop :=
| WeakRefl : forall Γ , Γ Γ
| WeakVarDecl : forall Γ x A, Γ Γ, x : A
| WeakVarDecl : forall Γ x A, x Γ -> Γ Γ, x : A
| WeakRulDecl : forall Γ t u, Γ Γ, t u
| WeakNextVarDecl : forall Γ Γ' x A, Γ Γ' -> Γ, x : A Γ', x : A
| WeakNextRulDecl : forall Γ Γ' t u, Γ Γ' -> Γ, t u Γ', t u
......@@ -37,11 +88,11 @@ Proof.
intros.
induction H.
- easy.
- apply IAfterV. easy.
- apply IAfterV. easy. intro. subst. contradiction H. econstructor. exact H0.
- apply IAfterR. easy.
- remember (Γ, x0 : A0) as Γ2. induction H0.
+ inversion HeqΓ2. subst. apply INow.
+ inversion HeqΓ2. subst. apply IAfterV. apply IHweaker. easy.
+ inversion HeqΓ2. subst. apply IAfterV. apply IHweaker. easy. easy.
+ inversion HeqΓ2.
- remember (Γ, t u) as Γ2. induction H0 ; inversion HeqΓ2.
subst. apply IAfterR. apply IHweaker. easy.
......@@ -68,8 +119,74 @@ Proof.
intros. intro. apply H0. destruct H1. exists x0. eapply subset_var_decl. apply H. easy.
Qed.
Notation weak_compatibility C := (forall Γ A B, C Γ A B -> forall Γ', Γ Γ' -> Γ' -> C Γ' A B).
Theorem weak : forall Γ Γ' t u, Γ t : u -> Γ Γ' -> Γ' -> Γ' t : u.
Theorem weak_comp_hβ : weak_compatibility RW_Head_Beta.
Proof. intros. inversion H. econstructor. Qed.
Theorem weak_comp_hΓ : weak_compatibility RW_Head_Gamma.
Proof.
intros.
inversion H; subst.
econstructor.
eapply subset_rul_decl. apply H0. easy.
Qed.
Notation weak_comp_func F := (forall (C:ConvScheme), weak_compatibility C -> weak_compatibility (F C)).
Theorem weak_comp_Union : forall (C C':ConvScheme),
weak_compatibility C -> weak_compatibility C' -> weak_compatibility (ConvUnion C C').
Proof.
intros. generalize dependent Γ'.
induction H1; intros.
+ apply CV1. eapply H. apply H1. easy. easy.
+ apply CV2. eapply H0. apply H1. easy. easy.
Qed.
Theorem weak_comp_CC : weak_comp_func ContextClosure.
Proof.
intros. generalize dependent Γ'.
induction H0; intros.
+ apply CCHere. eapply H. apply H0. easy. easy.
+ apply CCApp1. eapply H. apply H0. easy. easy.
+ apply CCApp2. eapply H. apply H0. easy. easy.
+ eapply CCAbs1. eapply H. apply H0. easy. easy.
+ apply CCAbs2. eapply H. apply H0. easy. easy.
+ apply CCPi1. eapply H. apply H0. easy. easy.
+ apply CCPi2. eapply H. apply H0. easy. easy.
Qed.
Theorem weak_comp_RT : weak_comp_func RTClosure.
Proof.
intros. generalize dependent Γ'.
induction H0; intros.
- apply RWRule. eapply H. apply H0. easy. easy.
- apply RWRefl.
- eapply RWTrans. apply IHRTClosure1. easy. easy. apply IHRTClosure2. easy. easy.
Qed.
Theorem weak_comp_RST : weak_comp_func RSTClosure.
Proof.
intros. generalize dependent Γ'.
induction H0; intros.
- apply CVRefl.
- apply CVSym. apply IHRSTClosure. easy. easy.
- eapply CVTrans. apply IHRSTClosure1. easy. easy. apply IHRSTClosure2. easy. easy.
- apply CVRule. eapply H. apply H0. easy. easy.
Qed.
Theorem weak_conv : forall Γ A B, Γ A B -> forall Γ', Γ Γ' -> Γ' -> Γ' A B.
Proof.
apply weak_comp_RST.
apply weak_comp_Union.
apply weak_comp_CC.
apply weak_comp_hβ.
apply weak_comp_CC.
apply weak_comp_hΓ.
Qed.
Theorem weak_typ : forall Γ Γ' t u, Γ t : u -> Γ Γ' -> Γ' -> Γ' t : u.
Proof.
intros.
generalize dependent Γ'.
......@@ -78,9 +195,38 @@ Proof.
- apply TyType. easy.
- eapply TyPi.
+ apply IHtyping. easy. easy.
+ intro. intro. apply H1. apply H4. apply WeakNextVarDecl. easy. econstructor.
Admitted.
+ intros. apply H1.
assert (~ In x ( (defined_vars Γ') ++ L)).
* apply H4.
* intro. apply H4. apply in_or_app. right. easy.
* econstructor. easy.
* econstructor.
++ intro. apply H4. apply in_or_app. left. apply defined_eq. easy.
++ apply IHtyping. easy. easy.
- eapply TyAbs.
+ apply IHtyping. easy. easy.
+ intros. apply H1.
assert (~ In x ( (defined_vars Γ') ++ L)).
* apply H6.
* intro. apply H6. apply in_or_app. right. easy.
* econstructor. easy.
* econstructor.
++ intro. apply H6. apply in_or_app. left. apply defined_eq. easy.
++ apply IHtyping. easy. easy.
+ intros. apply H3.
* intro. apply H6. apply in_or_app. right. easy.
* econstructor. easy.
* econstructor.
++ intro. apply H6. apply in_or_app. left. apply defined_eq. easy.
++ apply IHtyping. easy. easy.
- eapply TyApp.
+ apply IHtyping1. easy. easy.
+ apply IHtyping2. easy. easy.
- eapply TyConv.
+ apply IHtyping1. easy. easy.
+ apply IHtyping2. easy. easy.
+ eapply weak_conv. apply H1. easy. easy.
Qed.
Theorem not_in_not_eq {A:Type} : forall (x v : A) l, ~ (In x (v::l)) -> x <> v.
Proof. intros. intro. apply H. now left. Qed.
......@@ -118,12 +264,81 @@ Proof.
assumption.
Qed.
Theorem right_arr_type : forall Γ t u AB, Γ t ~> u : AB ->
exists A L, forall x, ~In x L -> Γ, x : A close u x : type \/ u = type .
Lemma FV_close_k : forall v A u k, In v (FV (A [k <- u])) -> In v (FV A) \/ In v (FV u).
Proof.
Admitted.
intros. generalize dependent k.
induction A; intros.
- inversion H.
- inversion H.
- inversion H; subst. left. easy. inversion H0.
- cbn in H. destruct (k =? n); subst. right. easy. left. easy.
- cbn in H. destruct (in_app_or _ _ _ H).
+ destruct (IHA1 _ H0).
* left. eapply in_or_app. left. easy.
* right. easy.
+ destruct (IHA2 _ H0).
* left. eapply in_or_app. right. easy.
* right. easy.
- cbn in H. destruct (in_app_or _ _ _ H).
+ destruct (IHA1 _ H0).
* left. eapply in_or_app. left. easy.
* right. easy.
+ destruct (IHA2 _ H0).
* left. eapply in_or_app. right. easy.
* right. easy.
- cbn in H. destruct (in_app_or _ _ _ H).
+ destruct (IHA1 _ H0).
* left. eapply in_or_app. left. easy.
* right. easy.
+ destruct (IHA2 _ H0).
* left. eapply in_or_app. right. easy.
* right. easy.
Qed.
Theorem FV_decl_u : forall Γ t u, Γ t : u -> forall v, In v (FV u) -> v Γ.
Proof.
intros. generalize dependent v.
induction H; intros.
- induction H0; assert (v Γ).
+ inversion H; subst.
* destruct (FV_decl_t _ _ _ H5 _ H1). exists x0. easy.
* destruct (FV_decl_t _ _ _ H5 _ H1). exists x0. easy.
+ inversion H0. exists x0. econstructor. apply H2. intro. subst. inversion H; subst.
* apply H5. exists x0. easy.
* apply H5. exists x0. easy.
+ apply IHInCtx. eapply vardecl_WF. apply H. easy.
+ inversion H3. exists x0. apply IAfterV. easy. intro. subst. inversion H; subst.
* apply H7. exists x0. easy.
* apply H7. exists x0. easy.
+ apply IHInCtx. eapply ruldecl_WF. apply H. easy.
+ inversion H2. exists x0. apply IAfterR. easy.
- inversion H0.
- destruct (var_inf ((defined_vars Γ) ++ (cons v L))).
assert (v Γ, x : A).
+ apply H1. intro. apply H3. apply in_or_app. right. right. easy. easy.
+ destruct H4. remember (Γ, x : A) as Γ'. inversion H4; subst.
* inversion H5; subst. contradiction H3. apply in_or_app. right. left. easy.
* inversion H7; subst. exists x0; easy.
* inversion H6.
- destruct (in_app_or (FV A) (FV B) v H4).
+ eapply FV_decl_t. apply H. easy.
+ destruct (var_inf ((defined_vars Γ) ++ (cons v L))).
assert (v Γ, x : A).
* apply H3. intro. apply H6. apply in_or_app. right. right. easy.
apply lemma_open_FV. easy.
* destruct H7. remember (Γ, x : A) as Γ'. inversion H7; subst.
-- inversion H8; subst. contradiction H6. apply in_or_app. right. left. easy.
-- inversion H10; subst. exists x0; easy.
-- inversion H9.
- destruct (FV_close_k _ _ _ _ H1).
+ apply IHtyping1. simpl. apply in_or_app. right. easy.
+ exact (FV_decl_t _ _ _ H0 _ H2).
- exact (FV_decl_t _ _ _ H0 _ H2).
Qed.
Theorem FV_decl1 : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> v Γ.
Theorem FV_decl1 : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> v Γ.
Proof.
intros Γ t ; revert Γ ; induction t; intros ; try inversion H0.
- subst. induction H.
......@@ -162,6 +377,11 @@ Proof.
- admit.
Qed.
Theorem right_arr_type : forall Γ t u AB, Γ t ~> u : AB ->
exists A L, forall x, ~In x L -> Γ, x : A close u x : type \/ u = type .
Proof.
Admitted.
Theorem FV_decl1 : forall Γ x A t u, Γ, x : A -> ~ In x (FV t) -> ~ In x (FV u) -> Γ t : u -> Γ, x: A t : u.
Proof.
do 5 intro.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment