STT.v 2.92 KB
Newer Older
Gaspard Ferey's avatar
Gaspard Ferey committed
1

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
2
Require Import List.
Gaspard Ferey's avatar
Gaspard Ferey committed
3
Require Import LPTerm.
Gaspard Ferey's avatar
Gaspard Ferey committed
4 5 6 7
Require Import WF.
Require Import conversion.
Require Import properties.

Gaspard Ferey's avatar
Gaspard Ferey committed
8

Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
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's avatar
Gaspard Ferey committed
32 33 34 35 36 37
Parameter type  : Var.
Parameter ι     : Var.
Parameter o     : Var.
Parameter arrow : Var.
Parameter η     : Var.
Parameter impl  : Var.
38 39
Parameter fa    : Var.
Parameter ε     : Var.
Gaspard Ferey's avatar
Gaspard Ferey committed
40

Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
41
Parameter a b c x y z F G X Y Z f g : Var.
Gaspard Ferey's avatar
Gaspard Ferey committed
42

Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
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's avatar
WIP  
Gaspard Ferey committed
52
,  type  : TType
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
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's avatar
Gaspard Ferey committed
72 73 74 75
.

Theorem STT_WF : STT .
Proof.
Gaspard Ferey's avatar
WIP.  
Gaspard Ferey committed
76 77
  try repeat apply util_rul_decl || apply util_var_decl.
  constructor.
Gaspard Ferey's avatar
WIP  
Gaspard Ferey committed
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's avatar
WIP.  
Gaspard Ferey committed
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.