helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v

   1 Require Export pc3_defs.
   2
   3 (*#* #stop record *)
   4
   5       Record G : Set := {
   6          f     : nat -> nat;
   7          f_inc : (n:?) (lt n (f n))
   8       }.
   9
  10 (*#* #start record *)
  11
  12 (*#* #caption "typing",
  13    "well formed context sort", "well formed context binder",
  14    "conversion rule", "typed sort", "typed reference to abbreviation",
  15    "typed reference to abstraction", "typed binder", "typed application",
  16    "typed cast"
  17 *)
  18       Inductive wf0 [g:G] : C -> Prop :=
  19          | wf0_sort : (m:?) (wf0 g (CSort m))
  20          | wf0_bind : (c:?; u,t:?) (ty0 g c u t) ->
  21                       (b:?) (wf0 g (CTail c (Bind b) u))
  22       with ty0 [g:G] : C -> T -> T -> Prop :=
  23 (* structural rules *)
  24          | ty0_conv : (c:?; t2,t:?) (ty0 g c t2 t) ->
  25                       (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
  26                       (ty0 g c u t2)
  27 (* axiom rules *)
  28          | ty0_sort : (c:?) (wf0 g c) ->
  29                       (m:?) (ty0 g c (TSort m) (TSort (f g m)))
  30          | ty0_abbr : (c:?) (wf0 g c) ->
  31                       (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
  32                       (t:?) (ty0 g d u t) ->
  33                       (ty0 g c (TBRef n) (lift (S n) (0) t))
  34          | ty0_abst : (c:?) (wf0 g c) ->
  35                       (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
  36                       (t:?) (ty0 g d u t) ->
  37                       (ty0 g c (TBRef n) (lift (S n) (0) u))
  38          | ty0_bind : (c:?; u,t:?) (ty0 g c u t) ->
  39                       (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
  40                       (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
  41                       (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
  42          | ty0_appl : (c:?; w,u:?) (ty0 g c w u) ->
  43                       (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
  44                       (ty0 g c (TTail (Flat Appl) w v)
  45                                (TTail (Flat Appl) w (TTail (Bind Abst) u t))
  46                       )
  47          | ty0_cast : (c:?; t1,t2:?) (ty0 g c t1 t2) ->
  48                       (t0:?) (ty0 g c t2 t0) ->
  49                       (ty0 g c (TTail (Flat Cast) t2 t1) t2).
  50
  51       Hint wf0 : ltlc := Constructors wf0.
  52
  53       Hint ty0 : ltlc := Constructors ty0.
  54
  55 (*#* #caption "generation lemma of typing" #clauses ty0_gen_base *)
  56
  57    Section ty0_gen_base. (***************************************************)
  58
  59 (*#* #caption "generation lemma for sort" *)
  60 (*#* #cap #cap c #alpha x in T, n in h *)
  61
  62       Theorem ty0_gen_sort: (g:?; c:?; x:?; n:?)
  63                             (ty0 g c (TSort n) x) ->
  64                             (pc3 c (TSort (f g n)) x).
  65
  66 (*#* #stop proof *)
  67
  68       Intros until 1; InsertEq H '(TSort n); XElim H; Intros.
  69 (* case 1 : ty0_conv *)
  70       XEAuto.
  71 (* case 2 : ty0_sort *)
  72       Inversion H0; XAuto.
  73 (* case 3 : ty0_abbr *)
  74       Inversion H3.
  75 (* case 4 : ty0_abst *)
  76       Inversion H3.
  77 (* case 5 : ty0_bind *)
  78       Inversion H5.
  79 (* case 6 : ty0_appl *)
  80       Inversion H3.
  81 (* case 7 : ty0_cast *)
  82       Inversion H3.
  83       Qed.
  84
  85 (*#* #start proof *)
  86
  87 (*#* #caption "generation lemma for bound reference" *)
  88 (*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
  89
  90       Theorem ty0_gen_bref: (g:?; c:?; x:?; n:?) (ty0 g c (TBRef n) x) ->
  91                             (EX e u t | (pc3 c (lift (S n) (0) t) x) &
  92                                         (drop n (0) c (CTail e (Bind Abbr) u)) &
  93                                         (ty0 g e u t)
  94                             ) \/
  95                             (EX e u t | (pc3 c (lift (S n) (0) u) x) &
  96                                         (drop n (0) c (CTail e (Bind Abst) u)) &
  97                                         (ty0 g e u t)
  98                             ).
  99
 100 (*#* #stop proof *)
 101
 102       Intros until 1; InsertEq H '(TBRef n); XElim H; Intros.
 103 (* case 1 : ty0_conv *)
 104       LApply H2; [ Clear H2; Intros H2 | XAuto ].
 105       XElim H2; Intros; XElim H2; XEAuto.
 106 (* case 2 : ty0_sort *)
 107       Inversion H0.
 108 (* case 3 : ty0_abbr *)
 109       Inversion H3 ; Rewrite H5 in H0; XEAuto.
 110 (* case 4 : ty0_abst *)
 111       Inversion H3; Rewrite H5 in H0; XEAuto.
 112 (* case 5 : ty0_bind *)
 113       Inversion H5.
 114 (* case 6 : ty0_appl *)
 115       Inversion H3.
 116 (* case 7 : ty0_cast *)
 117       Inversion H3.
 118       Qed.
 119
 120 (*#* #start proof *)
 121
 122 (*#* #caption "generation lemma for binder" *)
 123 (*#* #cap #cap c #alpha x in T, t1 in U1, t2 in U2, u in V, t in U, t0 in U3 *)
 124
 125       Theorem ty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty0 g c (TTail (Bind b) u t1) x) ->
 126                             (EX t2 t t0 | (pc3 c (TTail (Bind b) u t2) x) &
 127                                           (ty0 g c u t) &
 128                                           (ty0 g (CTail c (Bind b) u) t1 t2) &
 129                                           (ty0 g (CTail c (Bind b) u) t2 t0)
 130                             ).
 131
 132 (*#* #stop proof *)
 133
 134       Intros until 1; InsertEq H '(TTail (Bind b) u t1); XElim H; Intros.
 135 (* case 1 : ty0_conv *)
 136       LApply H2; [ Clear H2; Intros H2 | XAuto ].
 137       XElim H2; XEAuto.
 138 (* case 2 : ty0_sort *)
 139       Inversion H0.
 140 (* case 3 : ty0_abbr *)
 141       Inversion H3.
 142 (* case 4 : ty0_abst *)
 143       Inversion H3.
 144 (* case 5 : ty0_bind *)
 145       Inversion H5.
 146       Rewrite H7 in H1; Rewrite H7 in H3.
 147       Rewrite H8 in H; Rewrite H8 in H1; Rewrite H8 in H3.
 148       Rewrite H9 in H1; XEAuto.
 149 (* case 6 : ty0_appl *)
 150       Inversion H3.
 151 (* case 7 : ty0_cast *)
 152       Inversion H3.
 153       Qed.
 154
 155 (*#* #start proof *)
 156
 157 (*#* #caption "generation lemma for application" *)
 158 (*#* #cap #cap c #alpha x in T, v in U1, w in V1, u in V2, t in U2 *)
 159
 160       Theorem ty0_gen_appl: (g:?; c:?; w,v,x:?) (ty0 g c (TTail (Flat Appl) w v) x) ->
 161                             (EX u t | (pc3 c (TTail (Flat Appl) w (TTail (Bind Abst) u t)) x) &
 162                                       (ty0 g c v (TTail (Bind Abst) u t)) &
 163                                       (ty0 g c w u)
 164                             ).
 165
 166 (*#* #stop proof *)
 167
 168       Intros until 1; InsertEq H '(TTail (Flat Appl) w v); XElim H; Intros.
 169 (* case 1 : ty0_conv *)
 170       LApply H2; [ Clear H2; Intros H2 | XAuto ].
 171       XElim H2; XEAuto.
 172 (* case 2 : ty0_sort *)
 173       Inversion H0.
 174 (* case 3 : ty0_abbr *)
 175       Inversion H3.
 176 (* case 4 : ty0_abst *)
 177       Inversion H3.
 178 (* case 5 : ty0_bind *)
 179       Inversion H5.
 180 (* case 6 : ty0_appl *)
 181       Inversion H3; Rewrite H5 in H; Rewrite H6 in H1; XEAuto.
 182 (* case 7 : ty0_cast *)
 183       Inversion H3.
 184       Qed.
 185
 186 (*#* #start proof *)
 187
 188 (*#* #caption "generation lemma for cast" *)
 189 (*#* #cap #cap c #alpha x in T, t2 in V, t1 in U *)
 190
 191       Theorem ty0_gen_cast: (g:?; c:?; t1,t2,x:?)
 192                             (ty0 g c (TTail (Flat Cast) t2 t1) x) ->
 193                             (pc3 c t2 x) /\ (ty0 g c t1 t2).
 194
 195 (*#* #stop proof *)
 196
 197       Intros until 1; InsertEq H '(TTail (Flat Cast) t2 t1); XElim H; Intros.
 198 (* case 1 : ty0_conv *)
 199       LApply H2; [ Clear H2; Intros H2 | XAuto ].
 200       XElim H2; XEAuto.
 201 (* case 2 : ty0_sort *)
 202       Inversion H0.
 203 (* case 3 : ty0_abbr *)
 204       Inversion H3.
 205 (* case 4 : ty0_abst *)
 206       Inversion H3.
 207 (* case 5 : ty0_bind *)
 208       Inversion H5.
 209 (* case 6 : ty0_appl *)
 210       Inversion H3.
 211 (* case 7 : ty0_cast *)
 212       Inversion H3; Rewrite H5 in H; Rewrite H5 in H1; Rewrite H6 in H; XAuto.
 213       Qed.
 214
 215    End ty0_gen_base.
 216
 217       Tactic Definition Ty0GenBase :=
 218          Match Context With
 219             | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
 220                LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
 221             | [ H: (ty0 ?1 ?2 (TBRef ?3) ?4) |- ? ] ->
 222                LApply (ty0_gen_bref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
 223                XElim H; Intros H; XElim H; Intros
 224             | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
 225                LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
 226                XElim H; Intros
 227             | [ H: (ty0 ?1 ?2 (TTail (Flat Appl) ?3 ?4) ?5) |- ? ] ->
 228                LApply (ty0_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
 229                XElim H; Intros
 230             | [ H: (ty0 ?1 ?2 (TTail (Flat Cast) ?3 ?4) ?5) |- ? ] ->
 231                LApply (ty0_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];
 232                XElim H; Intros.
 233
 234    Section wf0_props. (******************************************************)
 235
 236       Theorem wf0_ty0 : (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
 237       Intros; XElim H; XAuto.
 238       Qed.
 239
 240       Hints Resolve wf0_ty0 : ltlc.
 241
 242       Theorem wf0_drop_O : (c,e:?; h:?) (drop h (0) c e) ->
 243                            (g:?) (wf0 g c) -> (wf0 g e).
 244       XElim c.
 245 (* case 1 : CSort *)
 246       Intros; DropGenBase; Rewrite H; XAuto.
 247 (* case 2 : CTail k *)
 248       Intros c IHc; XElim k; (
 249       XElim h; Intros; DropGenBase;
 250       [ Rewrite H in H0; XAuto | Inversion H1; XEAuto ] ).
 251       Qed.
 252
 253    End wf0_props.
 254
 255       Hints Resolve wf0_ty0 wf0_drop_O : ltlc.
 256
 257       Tactic Definition Wf0Ty0 :=
 258          Match Context With
 259             [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
 260                LApply (wf0_ty0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
 261                Inversion_clear H_x.
 262
 263       Tactic Definition Wf0DropO :=
 264          Match Context With
 265             | [ _: (drop ?1 (0) ?2 ?3); _: (wf0 ?4 ?2) |- ? ] ->
 266                LApply (wf0_drop_O ?2 ?3 ?1); [ Intros H_x | XAuto ];
 267                LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
 268
 269    Section wf0_facilities. (*************************************************)
 270
 271       Theorem wf0_drop_wf0 : (g:?; c:?) (wf0 g c) ->
 272                              (b:?; e:?; u:?; h:?)
 273                              (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
 274       Intros.
 275       Wf0DropO; Inversion H1; XEAuto.
 276       Qed.
 277
 278       Theorem ty0_drop_wf0 : (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
 279                              (b:?; e:?; u:?; h:?)
 280                              (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
 281       Intros.
 282       EApply wf0_drop_wf0; [ Idtac | EApply H0 ]; XEAuto.
 283       Qed.
 284
 285    End wf0_facilities.
 286
 287       Hints Resolve wf0_drop_wf0 ty0_drop_wf0 : ltlc.
 288
 289       Tactic Definition DropWf0 :=
 290          Match Context With
 291             | [ _: (ty0 ?1 ?2 ?3 ?4);
 292                 _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
 293                LApply (ty0_drop_wf0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
 294                LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ]
 295             | [ _: (wf0 ?1 ?2);
 296                 _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
 297                LApply (wf0_drop_wf0 ?1 ?2); [ Intros H_x | XAuto ];
 298                LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ].
 299
 300 (*#* #start file *)
 301
 302 (*#* #single *)