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

   1 Require Export pr1_defs.
   2 Require Export pr2_defs.
   3
   4 (*#* #caption "axioms for the relation $\\PrT{}{}{}$",
   5    "reflexivity", "single step transitivity"
   6 *)
   7 (*#* #cap #cap c, t, t1, t2, t3 *)
   8
   9       Inductive pr3 [c:C] : T -> T -> Prop :=
  10          | pr3_refl: (t:?) (pr3 c t t)
  11          | pr3_sing: (t2,t1:?) (pr2 c t1 t2) ->
  12                      (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
  13
  14 (*#* #stop file *)
  15
  16       Hint pr3: ltlc := Constructors pr3.
  17
  18    Section pr3_gen_base. (***************************************************)
  19
  20       Theorem pr3_gen_sort: (c:?; x:?; n:?) (pr3 c (TSort n) x) ->
  21                             x = (TSort n).
  22       Intros; InsertEq H '(TSort n); XElim H; Clear y x; Intros.
  23 (* case 1: pr3_refl *)
  24       XAuto.
  25 (* case 2: pr3_sing *)
  26       Rewrite H2 in H; Clear H2 t1; Pr2GenBase; XAuto.
  27       Qed.
  28
  29       Tactic Definition IH :=
  30          Match Context With
  31             | [ H: (u,t:T) (TTail (Bind Abst) ?1 ?2) = (TTail (Bind Abst) u t) -> ? |- ? ] ->
  32                LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
  33                XDecompose H
  34             | [ H: (u,t:T) (TTail (Flat Appl) ?1 ?2) = (TTail (Flat Appl) u t) -> ? |- ? ] ->
  35                LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
  36                XDecompose H
  37             | [ H: (u,t:T) (TTail (Flat Cast) ?1 ?2) = (TTail (Flat Cast) u t) -> ? |- ? ] ->
  38                LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
  39                XDecompose H.
  40
  41       Theorem pr3_gen_abst: (c:?; u1,t1,x:?)
  42                             (pr3 c (TTail (Bind Abst) u1 t1) x) ->
  43                             (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
  44                                         (pr3 c u1 u2) & (b:?; u:?)
  45                                         (pr3 (CTail c (Bind b) u) t1 t2)
  46                             ).
  47       Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1);
  48       UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
  49       Rename x into u0; Rename x0 into t0.
  50 (* case 1 : pr3_refl *)
  51       XEAuto.
  52 (* case 2 : pr3_sing *)
  53       Rewrite H2 in H; Clear H0 H2 t1; Pr2GenBase.
  54       Rewrite H0 in H1; Clear H0 t2; IH; XEAuto.
  55       Qed.
  56
  57       Theorem pr3_gen_appl: (c:?; u1,t1,x:?)
  58                             (pr3 c (TTail (Flat Appl) u1 t1) x) -> (OR
  59                             (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
  60                                         (pr3 c u1 u2) & (pr3 c t1 t2)
  61                             ) |
  62                             (EX y1 z1 u2 t2 | (pr3 c (TTail (Bind Abbr) u2 t2) x) &
  63                                               (pr3 c u1 u2) &
  64                                               (pr3 c t1 (TTail (Bind Abst) y1 z1)) &
  65                                               (b:?; u:?) (pr3 (CTail c (Bind b) u) z1 t2)
  66                             ) |
  67                             (EX b y1 z1 z2 u2 v2 t2 |
  68                                (pr3 c (TTail (Bind b) v2 z2) x) & ~b=Abst &
  69                                (pr3 c u1 u2) &
  70                                (pr3 c t1 (TTail (Bind b) y1 z1)) &
  71                                (pr3 c y1 v2) & (pr0 z1 t2))
  72                             ).
  73       Intros; InsertEq H '(TTail (Flat Appl) u1 t1).
  74       UnIntro t1 H; UnIntro u1 H.
  75       XElim H; Clear y x; Intros;
  76       Rename x into u0; Rename x0 into t0.
  77 (* case 1: pr3_refl *)
  78       XEAuto.
  79 (* case 2: pr3_sing *)
  80       Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
  81 (* case 2.1: short step: compatibility *)
  82       Rewrite H3 in H1; Clear H0 H3 t2.
  83       IH; Try (Rewrite H0; Clear H0 t3); XDEAuto 6.
  84 (* case 2.2: short step: beta *)
  85       Rewrite H4 in H0; Rewrite H3; Clear H1 H3 H4 t0 t2; XEAuto.
  86 (* case 2.3: short step: upsilon *)
  87       Rewrite H5 in H0; Rewrite H4; Clear H1 H4 H5 t0 t2; XEAuto.
  88       Qed.
  89
  90       Theorem pr3_gen_cast: (c:?; u1,t1,x:?)
  91                             (pr3 c (TTail (Flat Cast) u1 t1) x) ->
  92                             (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
  93                                         (pr3 c u1 u2) & (pr3 c t1 t2)
  94                             ) \/
  95                             (pr3 c t1 x).
  96       Intros; InsertEq H '(TTail (Flat Cast) u1 t1);
  97       UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
  98       Rename x into u0; Rename x0 into t0.
  99 (* case 1: pr3_refl *)
 100       Rewrite H; Clear H t; XEAuto.
 101 (* case 2: pr3_sing *)
 102       Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
 103 (* case 2.1: short step: compatinility *)
 104       Rewrite H3 in H1; Clear H0 H3 t2;
 105       IH; Try Rewrite H0; XEAuto.
 106 (* case 2.2: short step: epsilon *)
 107       XEAuto.
 108       Qed.
 109
 110    End pr3_gen_base.
 111
 112       Tactic Definition Pr3GenBase :=
 113          Match Context With
 114             | [ H: (pr3 ?1 (TSort ?2) ?3) |- ? ] ->
 115                LApply (pr3_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ]
 116             | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
 117                LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
 118                XDecompose H
 119             | [ H: (pr3 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] ->
 120                LApply (pr3_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
 121                XDecompose H
 122             | [ H: (pr3 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] ->
 123                LApply (pr3_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
 124                XDecompose H.
 125
 126    Section pr3_props. (******************************************************)
 127
 128       Theorem pr3_pr2: (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2).
 129       XEAuto.
 130       Qed.
 131
 132       Theorem pr3_t: (t2,t1,c:?) (pr3 c t1 t2) ->
 133                       (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
 134       Intros until 1; XElim H; XEAuto.
 135       Qed.
 136
 137       Theorem pr3_thin_dx: (c:?; t1,t2:?) (pr3 c t1 t2) ->
 138                            (u:?; f:?) (pr3 c (TTail (Flat f) u t1)
 139                                              (TTail (Flat f) u t2)).
 140       Intros; XElim H; XEAuto.
 141       Qed.
 142
 143       Theorem pr3_tail_1: (c:?; u1,u2:?) (pr3 c u1 u2) ->
 144                           (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
 145       Intros until 1; XElim H; Intros.
 146 (* case 1: pr3_refl *)
 147       XAuto.
 148 (* case 2: pr3_sing *)
 149       EApply pr3_sing; [ Apply pr2_tail_1; Apply H | XAuto ].
 150       Qed.
 151
 152       Theorem pr3_tail_2: (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) ->
 153                           (pr3 c (TTail k u t1) (TTail k u t2)).
 154       Intros until 1; XElim H; Intros.
 155 (* case 1: pr3_refl *)
 156       XAuto.
 157 (* case 2: pr3_sing *)
 158       EApply pr3_sing; [ Apply pr2_tail_2; Apply H | XAuto ].
 159       Qed.
 160
 161       Hints Resolve pr3_tail_1 pr3_tail_2 : ltlc.
 162
 163       Theorem pr3_tail_21: (c:?; u1,u2:?) (pr3 c u1 u2) ->
 164                            (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) ->
 165                            (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
 166       Intros.
 167       EApply pr3_t; [ Apply pr3_tail_2 | Apply pr3_tail_1 ]; XAuto.
 168       Qed.
 169
 170       Theorem pr3_tail_12: (c:?; u1,u2:?) (pr3 c u1 u2) ->
 171                            (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) ->
 172                            (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
 173       Intros.
 174       EApply pr3_t; [ Apply pr3_tail_1 | Apply pr3_tail_2 ]; XAuto.
 175       Qed.
 176
 177       Theorem pr3_shift: (h:?; c,e:?) (drop h (0) c e) ->
 178                          (t1,t2:?) (pr3 c t1 t2) ->
 179                          (pr3 e (app c h t1) (app c h t2)).
 180       Intros until 2; XElim H0; Clear t1 t2; Intros.
 181 (* case 1: pr3_refl *)
 182       XAuto.
 183 (* case 2: pr3_sing *)
 184       XEAuto.
 185       Qed.
 186
 187       Theorem pr3_pr1: (t1,t2:?) (pr1 t1 t2) -> (c:?) (pr3 c t1 t2).
 188       Intros until 1; XElim H; XEAuto.
 189       Qed.
 190
 191    End pr3_props.
 192
 193       Hints Resolve pr3_pr2 pr3_t pr3_pr1
 194                     pr3_thin_dx pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.