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

   1 Require lift_props.
   2 Require drop_props.
   3 Require pc3_props.
   4 Require pc3_gen.
   5 Require ty0_defs.
   6 Require ty0_gen.
   7 Require ty0_props.
   8 Require ty0_sred.
   9
  10 (*#* #caption "corollaries of subject reduction" #clauses *)
  11
  12 (*#* #stop file *)
  13
  14    Section ty0_gen. (********************************************************)
  15
  16       Tactic Definition IH e :=
  17          Match Context With
  18             [ H0: (t:?; d:?) ?1 = (lift ?2 d t) -> ?; H1: ?1 = (lift ?2 ?3 ?4) |- ? ] ->
  19             LApply (H0 ?4 ?3); [ Clear H0 H1; Intros H0 | XAuto ];
  20             LApply (H0 e); [ Clear H0; Intros H0 | XEAuto ];
  21             LApply H0; [ Clear H0; Intros H0 | XAuto ];
  22             XElim H0; Intros.
  23
  24 (*#* #start file *)
  25
  26 (*#* #caption "generation lemma for lift" *)
  27 (*#* #cap #cap t2 #alpha c in C1, e in C2, t1 in T, x in T1, d in i *)
  28
  29       Theorem ty0_gen_lift: (g:?; c:?; t1,x:?; h,d:?)
  30                             (ty0 g c (lift h d t1) x) ->
  31                             (e:?) (wf0 g e) -> (drop h d c e) ->
  32                             (EX t2 | (pc3 c (lift h d t2) x) & (ty0 g e t1 t2)).
  33
  34 (*#* #stop file *)
  35
  36       Intros until 1; InsertEq H '(lift h d t1);
  37       UnIntro H d; UnIntro H t1; XElim H; Intros;
  38       Rename x0 into t3; Rename x1 into d0.
  39 (* case 1: ty0_conv *)
  40       IH e; XEAuto.
  41 (* case 2: ty0_sort *)
  42       LiftGenBase; Rewrite H0; Clear H0 t.
  43       EApply ex2_intro; [ Rewrite lift_sort; XAuto | XAuto ].
  44 (* case 3: ty0_abbr *)
  45       Apply (lt_le_e n d0); Intros.
  46 (* case 3.1: n < d0 *)
  47       LiftGenBase; DropS; Rewrite H3; Clear H3 t3.
  48       Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
  49       Rewrite (lt_plus_minus n d0) in H5; [ DropDis; IH x1 | XAuto ].
  50       EApply ex2_intro;
  51       [ Rewrite lift_d; [ EApply pc3_lift; XEAuto | XEAuto ]
  52       | EApply ty0_abbr; XEAuto ].
  53 (* case 3.2: n >= d0 *)
  54       Apply (lt_le_e n (plus d0 h)); Intros.
  55 (* case 3.2.1: n < d0 + h *)
  56       LiftGenBase.
  57 (* case 3.2.2: n >= d0 + h *)
  58       Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ].
  59       LiftGenBase; DropDis; Rewrite H3; Clear H3 t3.
  60       EApply ex2_intro; [ Idtac | EApply ty0_abbr; XEAuto ].
  61       Rewrite lift_free; [ Idtac | XEAuto | XAuto ].
  62       Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto.
  63 (* case 4: ty0_abst *)
  64       Apply (lt_le_e n d0); Intros.
  65 (* case 4.1: n < d0 *)
  66       LiftGenBase; Rewrite H3; Clear H3 t3.
  67       Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
  68       Rewrite (lt_plus_minus n d0) in H5; [ DropDis; Rewrite H0; IH x1 | XAuto ].
  69       EApply ex2_intro; [ Rewrite lift_d | EApply ty0_abst ]; XEAuto.
  70 (* case 4.2: n >= d0 *)
  71       Apply (lt_le_e n (plus d0 h)); Intros.
  72 (* case 4.2.1: n < d0 + h *)
  73       LiftGenBase.
  74 (* case 4.2.2: n >= d0 + h *)
  75       Rewrite (le_plus_minus_sym h n) in H3; [ Idtac | XEAuto ].
  76       LiftGenBase; DropDis; Rewrite H3; Clear H3 t3.
  77       EApply ex2_intro; [ Idtac | EApply ty0_abst; XEAuto ].
  78       Rewrite lift_free; [ Idtac | XEAuto | XAuto ].
  79       Rewrite <- plus_n_Sm; Rewrite <- le_plus_minus; XEAuto.
  80 (* case 5: ty0_bind *)
  81       LiftGenBase; Rewrite H5; Rewrite H8; Rewrite H8 in H2; Clear H5 t3.
  82       Move H0 after H2; IH e; IH '(CTail e (Bind b) x0); Ty0Correct.
  83       EApply ex2_intro; [ Rewrite lift_bind; XEAuto | XEAuto ].
  84 (* case 6: ty0_appl *)
  85       LiftGenBase; Rewrite H3; Rewrite H6; Clear H3 c t3 x y.
  86       IH e; IH e; Pc3Gen; Pc3T; Pc3Gen; Pc3T.
  87       Move H3 after H12; Ty0Correct; Ty0SRed; Ty0GenBase; Wf0Ty0.
  88       EApply ex2_intro;
  89       [ Rewrite lift_flat; Apply pc3_thin_dx;
  90         Rewrite lift_bind; Apply pc3_tail_21; [ EApply pc3_pr3_x | Idtac ]
  91       | EApply ty0_appl;
  92         [ EApply ty0_conv
  93         | EApply ty0_conv; [ EApply ty0_bind | Idtac | Idtac ] ]
  94       ]; XEAuto.
  95 (* case 7: ty0_cast *)
  96       LiftGenBase; Rewrite H3; Rewrite H6; Rewrite H6 in H0.
  97       IH e; IH e; Pc3Gen; XEAuto.
  98       Qed.
  99
 100    End ty0_gen.
 101
 102       Tactic Definition Ty0Gen :=
 103          Match Context With
 104             | [ H0: (ty0 ?1 ?2 (lift ?3 ?4 ?5) ?6);
 105                 H1: (drop ?3 ?4 ?2 ?7) |- ? ] ->
 106                LApply (ty0_gen_lift ?1 ?2 ?5 ?6 ?3 ?4); [ Clear H0; Intros H0 | XAuto ];
 107                LApply (H0 ?7); [ Clear H0; Intros H0 | XEAuto ];
 108                LApply H0; [ Clear H0 H1; Intros H0 | XAuto ];
 109                XElim H0; Intros
 110             | [ H0: (ty0 ?1 ?2 (lift ?3 ?4 ?5) ?6);
 111                  _: (wf0 ?1 ?7) |- ? ] ->
 112                LApply (ty0_gen_lift ?1 ?2 ?5 ?6 ?3 ?4); [ Clear H0; Intros H0 | XAuto ];
 113                LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
 114                LApply H0; [ Clear H0; Intros H0 | XAuto ];
 115                XElim H0; Intros
 116             | _ -> Ty0GenContext.
 117
 118    Section ty0_sred_props. (*************************************************)
 119
 120 (*#* #start file *)
 121
 122 (*#* #caption "drop preserves well-formedness" *)
 123 (*#* #cap #alpha c in C1, e in C2, d in i *)
 124
 125       Theorem wf0_drop: (c,e:?; d,h:?) (drop h d c e) ->
 126                         (g:?) (wf0 g c) -> (wf0 g e).
 127
 128 (*#* #stop proof *)
 129
 130       XElim c.
 131 (* case 1: CSort *)
 132       Intros; DropGenBase; Rewrite H; XAuto.
 133 (* case 2: CTail k *)
 134       Intros c IHc; XElim k; (
 135       XElim d;
 136       [ XEAuto
 137       | Intros d IHd; Intros;
 138         DropGenBase; Rewrite H; Rewrite H1 in H0; Clear IHd H H1 e t;
 139         Inversion H0; Clear H3 H4 b0 u ]).
 140 (* case 2.1: Bind, d > 0 *)
 141       Ty0Gen; XEAuto.
 142       Qed.
 143
 144 (*#* #start proof *)
 145
 146 (*#* #caption "type reduction" *)
 147 (*#* #cap #cap c, t1, t2 #alpha u in T *)
 148
 149       Theorem ty0_tred: (g:?; c:?; u,t1:?) (ty0 g c u t1) ->
 150                         (t2:?) (pr3 c t1 t2) -> (ty0 g c u t2).
 151
 152 (*#* #stop proof *)
 153
 154       Intros; Ty0Correct; Ty0SRed; EApply ty0_conv; XEAuto.
 155       Qed.
 156
 157 (*#* #start proof *)
 158
 159 (*#* #caption "subject conversion" *)
 160 (*#* #cap #cap c, u1, u2, t1, t2 *)
 161
 162       Theorem ty0_sconv: (g:?; c:?; u1,t1:?) (ty0 g c u1 t1) ->
 163                          (u2,t2:?) (ty0 g c u2 t2) ->
 164                          (pc3 c u1 u2) -> (pc3 c t1 t2).
 165
 166 (*#* #stop file *)
 167
 168       Intros; Pc3Unfold; Repeat Ty0SRed; XEAuto.
 169       Qed.
 170
 171
 172    End ty0_sred_props.
 173
 174 (*#* #start file *)
 175
 176 (*#* #single *)