Commit 079f6d5b authored by Gaspard Ferey's avatar Gaspard Ferey

WIP

parent 1788e90f
......@@ -12,6 +12,8 @@ Parameter Var : Set.
Axiom var_dec : forall (x y:Var), {x = y} + {x <> y}.
Axiom var_inf : forall l, exists x:Var, ~ (In x l).
(* ************ Terms ************ *)
Inductive term : Set :=
......@@ -225,11 +227,13 @@ Inductive typing : context -> term -> term -> Prop :=
| TyType : forall Γ, Γ -> Γ type : kind
| TyPi : forall L Γ A B s,
Γ A : type ->
(forall x, ~(In x L) -> Γ , x : A B : s) -> Γ Π A ~ B : s
(forall x, ~(In x L) -> Γ , x : A (close B x) : s) ->
Γ Π A ~ B : s
| TyAbs : forall L Γ A B t s,
Γ A : type ->
(forall x, ~ (In x L) -> Γ, x : A B : s) ->
(forall x, ~ (In x L) -> Γ, x : A t : B) -> Γ λ A ~ t : Π A ~ B
(forall x, ~ (In x L) -> Γ, x : A (close B x) : s) ->
(forall x, ~ (In x L) -> Γ, x : A (close t x) : (close 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)
where "Γ '⊢' t ':' A" := (typing Γ t A)
......@@ -240,5 +244,3 @@ with well_formed : context -> Prop :=
| WFRel : forall Γ A s t u, Γ A : s -> Γ t : A -> Γ u : A -> Γ -> Γ, t u
where "Γ ✓" := (well_formed Γ).
Require Import List.
Require Import LPTerm.
Parameter OtherVars : Set.
Axiom o_var_dec : forall (x y:OtherVars), {x = y} + {x <> y}.
Axiom o_var_inf : forall (l : list OtherVars), exists x, ~ (In x l).
Inductive Var :=
| Ctype | Cι| Co | Carrow | Cη | Cimpl | Cfa | Cε
| V_a | V_b | V_c | V_x | V_y | V_z | V_F | V_G | V_X | V_Y | V_Z | V_f | V_g
| V_other : OtherVars -> Var.
Theorem var_dec : forall (x y:Var), {x = y} + {x <> y}.
Proof.
intros. induction x ; induction y; try (apply left; easy); try (apply right; easy).
destruct (o_var_dec o o0).
- left. rewrite e. easy.
- right. intro. apply n.
Qed.
Axiom var_inf : forall l, exists x:Var, ~ (In x l).
Parameter type : Var.
Parameter ι : Var.
Parameter o : Var.
......@@ -48,8 +72,8 @@ Theorem STT_WF : STT ✓.
Proof.
try repeat apply util_rul_decl || apply util_var_decl.
constructor.
- intro. apply WFVarK. constructor. constructor.
- intro. constructor. apply TyAxiom. easy. repeat constructor.
- intro. apply WFVarK. intro. inversion H0. inversion H1. constructor. constructor.
- intro. constructor. intro. inversion H0. inversion H1. subst. apply TyAxiom. easy. repeat constructor.
- intro. constructor. apply TyAxiom. easy. repeat constructor.
- intro. constructor. apply TyPi. constructor.
+ easy.
......
......@@ -6,10 +6,32 @@ Require Import LPTerm.
Theorem FV_decl1 : forall Γ t u, Γ t : u -> forall v, In v (FV t) -> Defined_var Γ v.
Proof.
intros. induction H.
- inversion H0. subst. exists A ; easy. inversion H2.
- inversion H0.
- apply IHtyping.
intros. induction t; try inversion H0.
- subst. 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 (Defined_var (Γ, x : A) v).
-- apply H2. intro. apply H4. simpl. right. easy. easy.
-- induction H5. inversion H5 ; subst.
++ contradict H4. simpl. auto.
++ econstructor. apply H11.
+ destruct (in_app_or (FV A) (FV t) v H0).
* apply IHtyping. easy.
* destruct (var_inf (v :: L)). assert (Defined_var (Γ, x : A) v).
-- apply H4. intro. apply H6. simpl. right. easy. easy.
-- induction H7. inversion H7; subst.
++ contradict H6. simpl. auto.
++ econstructor.apply H13.
+ destruct (in_app_or (FV t) (FV u) v H0).
* apply IHtyping1. easy.
* apply IHtyping2. easy.
+ apply IHtyping1. easy.
- contradict H1.
- destruct (in_app_or (FV t1) (FV t2) v H0).
+ apply IHt1.
Qed.
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.
......
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