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

   1 (*#* #stop file *)
   2
   3 Require pr2_gen.
   4 Require pr3_defs.
   5 Require pr3_props.
   6
   7    Section pr3_gen_void. (***************************************************)
   8
   9       Tactic Definition IH :=
  10          Match Context With
  11             [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] ->
  12                LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
  13                XElim H1; Intros H1; XElim H1; Intros.
  14
  15       Theorem pr3_gen_void : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) ->
  16                              (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
  17                                          (pr3 c u1 u2) & (b:?; u:?)
  18                                          (pr3 (CTail c (Bind b) u) t1 t2)
  19                              ) \/
  20                              (EX u | (pr3 c u1 u) &
  21                                      (pr3 (CTail c (Bind Void) u) t1 (lift (1) (0) x))
  22                              ).
  23       Intros until 1; InsertEq H '(TTail (Bind Void) u1 t1);
  24       UnIntro t1 H; UnIntro u1 H; XElim H; Intros.
  25 (* case 1 : pr3_r *)
  26       Rewrite H; XEAuto.
  27 (* case 2 : pr3_u *)
  28       Rewrite H2 in H; Clear H2 t0; Pr2Gen.
  29 (* case 2.1 : short step: compatibility *)
  30       Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
  31 (* case 2.1.1 : long step: compatibility *)
  32       Rewrite H; Rewrite H in H0; XEAuto.
  33 (* case 2.1.2 : long step: zeta *)
  34       XEAuto.
  35 (* case 2.2 : short step: zeta *)
  36       Clear H1; Right.
  37       EApply ex2_intro; [ XAuto | Idtac ].
  38       EApply pr3_u; [ Idtac | EApply pr3_lift ].
  39       XEAuto. XAuto. XAuto.
  40       Qed.
  41
  42    End pr3_gen_void.
  43
  44    Section pr3_gen_abbr. (***************************************************)
  45
  46       Tactic Definition IH :=
  47          LApply (H1 x0 x1); [ Clear H1; Intros H1 | XAuto ];
  48          XElim H1;
  49          [ Intros H1; XElim H1;
  50            Do 4 Intro; Intros H_x; XElim H_x;
  51            [ Intros | Intros H_x; XElim H_x; Intros ]
  52          | Intros H1; XElim H1; Intros ].
  53
  54       Theorem pr3_gen_abbr : (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) ->
  55                              (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
  56                                          (pr3 c u1 u2) &
  57                                          ((b:?; u:?) (pr3 (CTail c (Bind b) u) t1 t2)) \/
  58                                          (EX u3 t3 y | (pr3 c (TTail (Bind Abbr) u3 t3) x) &
  59                                                        (pr3 c u1 u3) &
  60                                                        (b:?; u:?) (pr3 (CTail c (Bind b) u) t1 y) &
  61                                                        (subst0 (0) u3 y t3)
  62                                          )
  63                              ) \/
  64                              (EX u | (pr3 c u1 u) &
  65                                      (pr3 (CTail c (Bind Abbr) u) t1 (lift (1) (0) x))
  66                              ).
  67       Intros until 1; InsertEq H '(TTail (Bind Abbr) u1 t1);
  68       UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
  69       Rename x into u1; Rename x0 into t4.
  70 (* case 1 : pr3_r *)
  71       Rewrite H; XEAuto.
  72 (* case 2 : pr3_u *)
  73       Rewrite H2 in H; Clear H2 t1; Pr2Gen.
  74 (* case 2.1 : short step: compatibility *)
  75       Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
  76 (* case 2.1.1 : long step: compatibility *)
  77       Rewrite H; Rewrite H in H0; Clear H t3.
  78       Left; EApply ex3_2_intro; XEAuto.
  79 (* case 2.1.2 : long step: delta *)
  80       Rewrite H; Rewrite H in H0; Rewrite H in H4; Clear H t3.
  81       Left; EApply ex3_2_intro;
  82       [ XEAuto | XEAuto
  83       | Right; EApply ex4_3_intro;
  84         [ EApply pr3_t; [ XAuto | Apply H4 ] | XEAuto | Idtac | Apply H7 ] ].
  85       XEAuto.
  86 (* case 2.1.3 : long step: zeta *)
  87       XEAuto.
  88 (* case 2.2 : short step: delta *)
  89       Rewrite H in H0; Rewrite H in H1; Clear H t2; IH.
  90 (* case 2.2.1 : long step: compatibility *)
  91       Left; EApply ex3_2_intro;
  92       [ XEAuto | XEAuto
  93       | Right; EApply ex4_3_intro; [ Rewrite H | Idtac | Idtac | Apply H4 ] ].
  94       XAuto. XAuto. XAuto.
  95 (* case 2.2.2 : long step: delta *)
  96       Left; EApply ex3_2_intro;
  97       [ XEAuto | XEAuto
  98       | Right; EApply ex4_3_intro;
  99         [ EApply pr3_t; [ Apply pr3_tail_12 | Apply H5 ]
 100         | Idtac | Idtac | Apply H4 ] ].
 101       XAuto. EApply pr3_t; [ Apply H7 | XEAuto ]. XAuto. XAuto.
 102 (* case 2.2.3 : long step: zeta *)
 103       Right; Apply ex2_intro with x := x0; [ XAuto | Idtac ].
 104       Apply pr3_u with t2 := x; [ XAuto | Idtac ].
 105       Apply pr3_u with t2 := x1; [ XEAuto | Idtac ].
 106       Pr3Context; XAuto.
 107 (* case 2.3 : short step: zeta *)
 108       Clear H1; Right.
 109       EApply ex2_intro; [ XAuto | Idtac ].
 110       EApply pr3_u; [ Idtac | EApply pr3_lift ].
 111       XEAuto. XAuto. XAuto.
 112       Qed.
 113
 114    End pr3_gen_abbr.
 115
 116    Section pr3_gen_abst. (***************************************************)
 117
 118       Theorem pr3_gen_abst : (c:?; u1,t1,x:?)
 119                              (pr3 c (TTail (Bind Abst) u1 t1) x) ->
 120                              (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
 121                                          (pr3 c u1 u2) & (b:?; u:?)
 122                                          (pr3 (CTail c (Bind b) u) t1 t2)
 123                              ).
 124       Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1);
 125       UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
 126       Rename x into u1; Rename x0 into t4.
 127 (* case 1 : pr3_r *)
 128       Rewrite H; XEAuto.
 129 (* case 2 : pr3_u *)
 130       Rewrite H2 in H; Clear H2 t1.
 131       Pr2GenBase.
 132       LApply (H1 x0 x1); [ Clear H H1; Intros | XAuto ].
 133       XElim H; XEAuto.
 134       Qed.
 135
 136    End pr3_gen_abst.
 137
 138    Section pr3_gen_lift. (***************************************************)
 139
 140 (*#* #start file *)
 141
 142 (*#* #caption "generation lemma for lift" *)
 143 (*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *)
 144
 145       Theorem pr3_gen_lift : (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) ->
 146                              (e:?) (drop h d c e) ->
 147                              (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)).
 148
 149 (*#* #stop file *)
 150
 151       Intros until 1; InsertEq H '(lift h d t1);
 152       UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4.
 153 (* case 1 : pr3_r *)
 154       XEAuto.
 155 (* case 2 : pr3_u *)
 156       Rewrite H2 in H; Pr2Gen.
 157       LApply (H1 x); [ Clear H1; Intros H1 | XAuto ].
 158       LApply (H1 e); [ Clear H1; Intros H1 | XAuto ].
 159       XElim H1; XEAuto.
 160       Qed.
 161
 162    End pr3_gen_lift.
 163
 164       Tactic Definition Pr3Gen :=
 165          Match Context With
 166             | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
 167                LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
 168                XElim H; Intros
 169             | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
 170                LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
 171                XElim H;
 172                [ Intros H; XElim H;
 173                  Do 4 Intro; Intros H_x; XElim H_x;
 174                  [ Intros | Intros H_x; XElim H_x; Intros ]
 175                | Intros H; XElim H; Intros ]
 176             | [ H: (pr3 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
 177                LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
 178                XElim H; Intros H; XElim H; Intros
 179             | [ H0: (pr3 ?1 (lift ?2 ?3 ?4) ?5);
 180                 H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
 181                LApply (pr3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
 182                LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
 183                XElim H0; Intros
 184             | _ -> Pr2Gen.