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