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_lift. (***************************************************)
   8
   9 (*#* #caption "generation lemma for lift" *)
  10 (*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *)
  11
  12       Theorem pr3_gen_lift: (c:?; t1,x:?; h,d:?) (pr3 c (lift h d t1) x) ->
  13                             (e:?) (drop h d c e) ->
  14                             (EX t2 | x = (lift h d t2) & (pr3 e t1 t2)).
  15       Intros until 1; InsertEq H '(lift h d t1);
  16       UnIntro H t1; XElim H; Clear y x; Intros; Rename x into t4.
  17 (* case 1 : pr3_refl *)
  18       XEAuto.
  19 (* case 2 : pr3_sing *)
  20       Rewrite H2 in H; Pr2Gen.
  21       LApply (H1 x); [ Clear H1; Intros H1 | XAuto ].
  22       LApply (H1 e); [ Clear H1; Intros H1 | XAuto ].
  23       XElim H1; XEAuto.
  24       Qed.
  25
  26    End pr3_gen_lift.
  27
  28    Section pr3_gen_lref. (***************************************************)
  29
  30       Theorem pr3_gen_lref: (c:?; x:?; n:?) (pr3 c (TLRef n) x) ->
  31                             x = (TLRef n) \/
  32                             (EX d u v | (drop n (0) c (CTail d (Bind Abbr) u)) &
  33                                         (pr3 d u v) &
  34                                         x = (lift (S n) (0) v)
  35                             ).
  36       Intros; InsertEq H '(TLRef n); XElim H; Clear y x; Intros.
  37 (* case 1: pr3_refl *)
  38       XAuto.
  39 (* case 2: pr3_sing *)
  40       Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
  41 (* case 2.1: pr2_free *)
  42       XAuto.
  43 (* case 2.2: pr2_delta *)
  44       Rewrite H4 in H0; Clear H1 H4 t2.
  45       LApply (pr3_gen_lift c x1 t3 (S n) (0)); [ Clear H0; Intros | XAuto ].
  46       LApply (H x0); [ Clear H; Intros | XEAuto ].
  47       XElim H; XEAuto.
  48       Qed.
  49
  50    End pr3_gen_lref.
  51
  52    Section pr3_gen_bind. (***************************************************)
  53
  54       Tactic Definition IH :=
  55          Match Context With
  56             | [ H: (u,t:T) (TTail (Bind Void) ?1 ?2) = (TTail (Bind Void) u t) -> ? |- ? ] ->
  57                LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
  58                XDecompose H
  59             | [ H: (u,t:T) (TTail (Bind Abbr) ?1 ?2) = (TTail (Bind Abbr) u t) -> ? |- ? ] ->
  60                LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
  61                XDecompose H.
  62
  63       Theorem pr3_gen_void: (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Void) u1 t1) x) ->
  64                             (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
  65                                         (pr3 c u1 u2) & (b:?; u:?)
  66                                         (pr3 (CTail c (Bind b) u) t1 t2)
  67                             ) \/
  68                             (pr3 (CTail c (Bind Void) u1) t1 (lift (1) (0) x)).
  69       Intros until 1; InsertEq H '(TTail (Bind Void) u1 t1);
  70       UnIntro t1 H; UnIntro u1 H; XElim H; Intros.
  71 (* case 1 : pr3_refl *)
  72       Rewrite H; XEAuto.
  73 (* case 2 : pr3_sing *)
  74       Rewrite H2 in H; Clear H2 t0; Pr2Gen.
  75 (* case 2.1 : short step: compatibility *)
  76       Rewrite H3 in H1; Clear H0 H3 t2.
  77       IH; Try Pr3Context; Try Rewrite H2; XEAuto.
  78 (* case 2.2 : short step: zeta *)
  79       XEAuto.
  80       Qed.
  81
  82       Theorem pr3_gen_abbr: (c:?; u1,t1,x:?) (pr3 c (TTail (Bind Abbr) u1 t1) x) ->
  83                             (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
  84                                         (pr3 c u1 u2) &
  85                                         (pr3 (CTail c (Bind Abbr) u1) t1 t2)
  86                             ) \/
  87                             (pr3 (CTail c (Bind Abbr) u1) t1 (lift (1) (0) x)).
  88       Intros until 1; InsertEq H '(TTail (Bind Abbr) u1 t1);
  89       UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
  90       Rename x into u1; Rename x0 into t4.
  91 (* case 1: pr3_refl *)
  92       Rewrite H; XEAuto.
  93 (* case 2: pr3_sing *)
  94       Rewrite H2 in H; Clear H2 t1; Pr2Gen.
  95 (* case 2.1: short step: compatibility *)
  96       Rewrite H3 in H1; Clear H0 H3 t2.
  97       IH; Repeat Pr3Context;
  98       Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
  99       XEAuto.
 100 (* case 2.2: short step: beta *)
 101       Rewrite H3 in H1; Clear H0 H3 t1.
 102       IH; Repeat Pr3Context;
 103       Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
 104       XEAuto.
 105 (* case 2.3: short step: delta *)
 106       Rewrite H3 in H1; Clear H0 H3 t2.
 107       IH; Repeat Pr3Context;
 108       Try (Rewrite H0; Clear H0 t3; Left; EApply ex3_2_intro);
 109       XDEAuto 7.
 110 (* case 2.4: short step: zeta *)
 111       XEAuto.
 112       Qed.
 113
 114    End pr3_gen_bind.
 115
 116       Tactic Definition Pr3Gen :=
 117          Match Context With
 118             | [ H: (pr3 ?1 (TLRef ?2) ?3) |- ? ] ->
 119                LApply (pr3_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ];
 120                XDecompose H
 121             | [ H: (pr3 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
 122                LApply (pr3_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
 123                XDecompose H
 124             | [ H: (pr3 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
 125                LApply (pr3_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
 126                XDecompose H
 127             | [ H0: (pr3 ?1 (lift ?2 ?3 ?4) ?5);
 128                 H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
 129                LApply (pr3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
 130                LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
 131                XDecompose H0
 132             | _ -> Pr3GenBase.