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

   1 Require pc3_props.
   2 Require ty0_defs.
   3
   4 (*#* #caption "generation lemma of typing" #clauses *)
   5
   6    Section ty0_gen_base. (***************************************************)
   7
   8 (*#* #caption "generation lemma for sorts" *)
   9 (*#* #cap #cap c #alpha x in T, n in h *)
  10
  11       Theorem ty0_gen_sort: (g:?; c:?; x:?; n:?)
  12                             (ty0 g c (TSort n) x) ->
  13                             (pc3 c (TSort (next g n)) x).
  14
  15 (*#* #stop proof *)
  16
  17       Intros until 1; InsertEq H '(TSort n); XElim H; Intros.
  18 (* case 1 : ty0_conv *)
  19       XEAuto.
  20 (* case 2 : ty0_sort *)
  21       Inversion H0; XAuto.
  22 (* case 3 : ty0_abbr *)
  23       Inversion H3.
  24 (* case 4 : ty0_abst *)
  25       Inversion H3.
  26 (* case 5 : ty0_bind *)
  27       Inversion H5.
  28 (* case 6 : ty0_appl *)
  29       Inversion H3.
  30 (* case 7 : ty0_cast *)
  31       Inversion H3.
  32       Qed.
  33
  34 (*#* #start proof *)
  35
  36 (*#* #caption "generation lemma for bound references" *)
  37 (*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
  38
  39       Theorem ty0_gen_lref: (g:?; c:?; x:?; n:?) (ty0 g c (TLRef n) x) ->
  40                             (EX e u t | (pc3 c (lift (S n) (0) t) x) &
  41                                         (drop n (0) c (CTail e (Bind Abbr) u)) &
  42                                         (ty0 g e u t)
  43                             ) \/
  44                             (EX e u t | (pc3 c (lift (S n) (0) u) x) &
  45                                         (drop n (0) c (CTail e (Bind Abst) u)) &
  46                                         (ty0 g e u t)
  47                             ).
  48
  49 (*#* #stop proof *)
  50
  51       Intros until 1; InsertEq H '(TLRef n); XElim H; Intros.
  52 (* case 1 : ty0_conv *)
  53       LApply H2; [ Clear H2; Intros H2 | XAuto ].
  54       XElim H2; Intros; XElim H2; XEAuto.
  55 (* case 2 : ty0_sort *)
  56       Inversion H0.
  57 (* case 3 : ty0_abbr *)
  58       Inversion H3 ; Rewrite H5 in H0; XEAuto.
  59 (* case 4 : ty0_abst *)
  60       Inversion H3; Rewrite H5 in H0; XEAuto.
  61 (* case 5 : ty0_bind *)
  62       Inversion H5.
  63 (* case 6 : ty0_appl *)
  64       Inversion H3.
  65 (* case 7 : ty0_cast *)
  66       Inversion H3.
  67       Qed.
  68
  69 (*#* #start proof *)
  70
  71 (*#* #caption "generation lemma for binders" *)
  72 (*#* #cap #cap c #alpha x in T, t1 in U1, t2 in U2, u in V, t in U, t0 in U3 *)
  73
  74       Theorem ty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty0 g c (TTail (Bind b) u t1) x) ->
  75                             (EX t2 t t0 | (pc3 c (TTail (Bind b) u t2) x) &
  76                                           (ty0 g c u t) &
  77                                           (ty0 g (CTail c (Bind b) u) t1 t2) &
  78                                           (ty0 g (CTail c (Bind b) u) t2 t0)
  79                             ).
  80
  81 (*#* #stop proof *)
  82
  83       Intros until 1; InsertEq H '(TTail (Bind b) u t1); XElim H; Intros.
  84 (* case 1 : ty0_conv *)
  85       LApply H2; [ Clear H2; Intros H2 | XAuto ].
  86       XElim H2; XEAuto.
  87 (* case 2 : ty0_sort *)
  88       Inversion H0.
  89 (* case 3 : ty0_abbr *)
  90       Inversion H3.
  91 (* case 4 : ty0_abst *)
  92       Inversion H3.
  93 (* case 5 : ty0_bind *)
  94       Inversion H5.
  95       Rewrite H7 in H1; Rewrite H7 in H3.
  96       Rewrite H8 in H; Rewrite H8 in H1; Rewrite H8 in H3.
  97       Rewrite H9 in H1; XEAuto.
  98 (* case 6 : ty0_appl *)
  99       Inversion H3.
 100 (* case 7 : ty0_cast *)
 101       Inversion H3.
 102       Qed.
 103
 104 (*#* #start proof *)
 105
 106 (*#* #caption "generation lemma for applications" *)
 107 (*#* #cap #cap c #alpha x in T, v in U1, w in V1, u in V2, t in U2 *)
 108
 109       Theorem ty0_gen_appl: (g:?; c:?; w,v,x:?) (ty0 g c (TTail (Flat Appl) w v) x) ->
 110                             (EX u t | (pc3 c (TTail (Flat Appl) w (TTail (Bind Abst) u t)) x) &
 111                                       (ty0 g c v (TTail (Bind Abst) u t)) &
 112                                       (ty0 g c w u)
 113                             ).
 114
 115 (*#* #stop proof *)
 116
 117       Intros until 1; InsertEq H '(TTail (Flat Appl) w v); XElim H; Intros.
 118 (* case 1 : ty0_conv *)
 119       LApply H2; [ Clear H2; Intros H2 | XAuto ].
 120       XElim H2; XEAuto.
 121 (* case 2 : ty0_sort *)
 122       Inversion H0.
 123 (* case 3 : ty0_abbr *)
 124       Inversion H3.
 125 (* case 4 : ty0_abst *)
 126       Inversion H3.
 127 (* case 5 : ty0_bind *)
 128       Inversion H5.
 129 (* case 6 : ty0_appl *)
 130       Inversion H3; Rewrite H5 in H; Rewrite H6 in H1; XEAuto.
 131 (* case 7 : ty0_cast *)
 132       Inversion H3.
 133       Qed.
 134
 135 (*#* #start proof *)
 136
 137 (*#* #caption "generation lemma for type casts" *)
 138 (*#* #cap #cap c #alpha x in T, t2 in V, t1 in U *)
 139
 140       Theorem ty0_gen_cast: (g:?; c:?; t1,t2,x:?)
 141                             (ty0 g c (TTail (Flat Cast) t2 t1) x) ->
 142                             (pc3 c t2 x) /\ (ty0 g c t1 t2).
 143
 144 (*#* #stop proof *)
 145
 146       Intros until 1; InsertEq H '(TTail (Flat Cast) t2 t1); XElim H; Intros.
 147 (* case 1 : ty0_conv *)
 148       LApply H2; [ Clear H2; Intros H2 | XAuto ].
 149       XElim H2; XEAuto.
 150 (* case 2 : ty0_sort *)
 151       Inversion H0.
 152 (* case 3 : ty0_abbr *)
 153       Inversion H3.
 154 (* case 4 : ty0_abst *)
 155       Inversion H3.
 156 (* case 5 : ty0_bind *)
 157       Inversion H5.
 158 (* case 6 : ty0_appl *)
 159       Inversion H3.
 160 (* case 7 : ty0_cast *)
 161       Inversion H3; Rewrite H5 in H; Rewrite H5 in H1; Rewrite H6 in H; XAuto.
 162       Qed.
 163
 164    End ty0_gen_base.
 165
 166       Tactic Definition Ty0GenBase :=
 167          Match Context With
 168             | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
 169                LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
 170             | [ H: (ty0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
 171                LApply (ty0_gen_lref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
 172                XElim H; Intros H; XElim H; Intros
 173             | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
 174                LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
 175                XElim H; Intros
 176             | [ H: (ty0 ?1 ?2 (TTail (Flat Appl) ?3 ?4) ?5) |- ? ] ->
 177                LApply (ty0_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
 178                XElim H; Intros
 179             | [ H: (ty0 ?1 ?2 (TTail (Flat Cast) ?3 ?4) ?5) |- ? ] ->
 180                LApply (ty0_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];
 181                XElim H; Intros.
 182
 183 (*#* #start file *)
 184
 185 (*#* #single *)