STT.v 2.92 KB
 Gaspard Ferey committed Sep 11, 2018 1 `````` `````` Gaspard Ferey committed Sep 14, 2018 2 ``````Require Import List. `````` Gaspard Ferey committed Sep 11, 2018 3 ``````Require Import LPTerm. `````` Gaspard Ferey committed Sep 19, 2018 4 5 6 7 ``````Require Import WF. Require Import conversion. Require Import properties. `````` Gaspard Ferey committed Sep 11, 2018 8 `````` `````` Gaspard Ferey committed Sep 14, 2018 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 ``````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). `````` Gaspard Ferey committed Sep 11, 2018 32 33 34 35 36 37 ``````Parameter type : Var. Parameter ι : Var. Parameter o : Var. Parameter arrow : Var. Parameter η : Var. Parameter impl : Var. `````` François Thiré committed Sep 11, 2018 38 39 ``````Parameter fa : Var. Parameter ε : Var. `````` Gaspard Ferey committed Sep 11, 2018 40 `````` `````` Gaspard Ferey committed Sep 13, 2018 41 ``````Parameter a b c x y z F G X Y Z f g : Var. `````` Gaspard Ferey committed Sep 11, 2018 42 `````` `````` Gaspard Ferey committed Sep 13, 2018 43 44 45 46 47 48 49 50 51 `````` Theorem util_var_decl c x A : c ✓ -> (c ✓ -> c, x : A ✓) -> c, x : A ✓. Proof. exact (fun x f => f x). Qed. Theorem util_rul_decl c t u : c ✓ -> (c ✓ -> c, t ≡ u ✓) -> c, t ≡ u ✓. Proof. exact (fun x f => f x). Qed. Definition STT := [] `````` Gaspard Ferey committed Sep 20, 2018 52 ``````, type : TType `````` Gaspard Ferey committed Sep 13, 2018 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 ``````, ι : # type , o : # type , arrow : # type ~> # type ~> # type , η : # type ~> TType , ε : # η @ # o ~> # η @ # o , impl : # η @ # o ~> # η @ # o ~> # η @ # o , fa : a ; # type ~> (# η @ # a ~> # η @ # o) ~> (# η @ # o) , x ; # type => y ; # type => # η @ (# arrow @ # x @ # y) ≡ x ; # type => y ; # type => (# η @ # x ~> # η @ # y) , x ; # type => y ; # type => # ε @ (# impl @ # x @ # y) ≡ x ; # type => y ; # type => (# ε @ # x ~> #ε @ # y) , a ; # type => f ; # type => # ε @ (#fa @ #a @ #f) ≡ a ; # type => f ; # type => z ; (#η @ #a) => # ε @ (#f @ #x) `````` Gaspard Ferey committed Sep 11, 2018 72 73 74 75 ``````. Theorem STT_WF : STT ✓. Proof. `````` Gaspard Ferey committed Sep 13, 2018 76 77 `````` try repeat apply util_rul_decl || apply util_var_decl. constructor. `````` Gaspard Ferey committed Sep 14, 2018 78 79 `````` - intro. apply WFVarK. intro. inversion H0. inversion H1. constructor. constructor. - intro. constructor. intro. inversion H0. inversion H1. subst. apply TyAxiom. easy. repeat constructor. `````` Gaspard Ferey committed Sep 13, 2018 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 `````` - intro. constructor. apply TyAxiom. easy. repeat constructor. - intro. constructor. apply TyPi. constructor. + easy. + repeat constructor. + intros. apply TyPi. * constructor. apply util_var_decl. -- easy. -- intro. apply WFVarT. apply TyAxiom. easy. repeat constructor. -- repeat constructor. * intros. apply TyAxiom. apply util_var_decl. apply util_var_decl. easy. intros. constructor. apply TyAxiom. easy. repeat constructor. intros. constructor. apply TyAxiom. easy. repeat constructor. repeat constructor. - intro. apply WFVarK. constructor. + constructor. easy. repeat constructor. + intros. constructor. constructor. constructor. easy. repeat constructor. - intros. apply WFVarT. constructor. + apply Qed.``````