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

   1 (*#* #stop file *)
   2
   3 Require Export terms_defs.
   4
   5       Fixpoint bref_map [g:nat->nat; d:nat; t:T] : T := Cases t of
   6          | (TSort n)     => (TSort n)
   7          | (TBRef n)     =>
   8             if (blt n d) then (TBRef n) else (TBRef (g n))
   9          | (TTail k u t) =>
  10             (TTail k (bref_map g d u) (bref_map g (s k d) t))
  11       end.
  12
  13       Definition lift : nat -> nat -> T -> T :=
  14                         [h](bref_map [x](plus x h)).
  15
  16    Section lift_rw. (********************************************************)
  17
  18       Theorem lift_sort: (n:?; h,d:?) (lift h d (TSort n)) = (TSort n).
  19       XAuto.
  20       Qed.
  21
  22       Theorem lift_bref_lt: (n:?; h,d:?) (lt n d) ->
  23                             (lift h d (TBRef n)) = (TBRef n).
  24       Intros; Unfold lift; Simpl.
  25       Replace (blt n d) with true; XAuto.
  26       Qed.
  27
  28       Theorem lift_bref_ge: (n:?; h,d:?) (le d n) ->
  29                             (lift h d (TBRef n)) = (TBRef (plus n h)).
  30
  31       Intros; Unfold lift; Simpl.
  32       Replace (blt n d) with false; XAuto.
  33       Qed.
  34
  35       Theorem lift_tail: (k:?; u,t:?; h,d:?)
  36                          (lift h d (TTail k u t)) =
  37                          (TTail k (lift h d u) (lift h (s k d) t)).
  38       XAuto.
  39       Qed.
  40
  41       Theorem lift_bind: (b:?; u,t:?; h,d:?)
  42                          (lift h d (TTail (Bind b) u t)) =
  43                          (TTail (Bind b) (lift h d u) (lift h (S d) t)).
  44       XAuto.
  45       Qed.
  46
  47       Theorem lift_flat: (f:?; u,t:?; h,d:?)
  48                          (lift h d (TTail (Flat f) u t)) =
  49                          (TTail (Flat f) (lift h d u) (lift h d t)).
  50       XAuto.
  51       Qed.
  52
  53    End lift_rw.
  54
  55       Hints Resolve lift_bref_lt lift_bind lift_flat : ltlc.
  56
  57       Tactic Definition LiftTailRw :=
  58          Repeat (Rewrite lift_tail Orelse Rewrite lift_bind Orelse Rewrite lift_flat).
  59
  60       Tactic Definition LiftTailRwBack :=
  61          Repeat (Rewrite <- lift_tail Orelse Rewrite <- lift_bind Orelse Rewrite <- lift_flat).
  62
  63    Section lift_gen. (*******************************************************)
  64
  65       Theorem lift_gen_sort: (h,d,n:?; t:?) (TSort n) = (lift h d t) ->
  66                              t = (TSort n).
  67       XElim t; Intros.
  68 (* case 1 : TSort *)
  69       XAuto.
  70 (* case 2 : TBRef n0 *)
  71       Apply (lt_le_e n0 d); Intros.
  72 (* case 2.1 : n0 < d *)
  73       Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
  74 (* case 2.2 : n0 >= d *)
  75       Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
  76 (* case 3 : TTail k *)
  77       Rewrite lift_tail in H1; Inversion H1.
  78       Qed.
  79
  80       Theorem lift_gen_bref_lt: (h,d,n:?) (lt n d) ->
  81                                 (t:?) (TBRef n) = (lift h d t) ->
  82                                 t = (TBRef n).
  83       XElim t; Intros.
  84 (* case 1 : TSort *)
  85       XAuto.
  86 (* case 2 : TBRef n0 *)
  87       Apply (lt_le_e n0 d); Intros.
  88 (* case 2.1 : n0 < d *)
  89       Rewrite lift_bref_lt in H0; XAuto.
  90 (* case 2.2 : n0 >= d *)
  91       Rewrite lift_bref_ge in H0; [ Inversion H0; Clear H0 | XAuto ].
  92       Rewrite H3 in H; Clear H3 n.
  93       EApply le_false; [ Apply H1 | XEAuto ].
  94 (* case 3 : TTail k *)
  95       Rewrite lift_tail in H2; Inversion H2.
  96       Qed.
  97
  98       Theorem lift_gen_bref_false: (h,d,n:?) (le d n) -> (lt n (plus d h)) ->
  99                                    (t:?) (TBRef n) = (lift h d t) ->
 100                                     (P:Prop) P.
 101       XElim t; Intros.
 102 (* case 1 : TSort *)
 103       Inversion H1.
 104 (* case 2 : TBRef n0 *)
 105       Apply (lt_le_e n0 d); Intros.
 106 (* case 2.1 : n0 < d *)
 107       Rewrite lift_bref_lt in H1; [ Inversion H1; Clear H1 | XAuto ].
 108       Rewrite <- H4 in H2; Clear H4 n0.
 109       EApply le_false; [ Apply H | XEAuto ].
 110 (* case 2.2 : n0 >= d *)
 111       Rewrite lift_bref_ge in H1; [ Inversion H1; Clear H1 | XAuto ].
 112       Rewrite H4 in H0; Clear H4.
 113       EApply le_false; [ Apply H2 | XEAuto ].
 114 (* case 3 : TTail k *)
 115       Rewrite lift_tail in H3; Inversion H3.
 116       Qed.
 117
 118       Theorem lift_gen_bref_ge: (h,d,n:?) (le d n) ->
 119                                 (t:?) (TBRef (plus n h)) = (lift h d t) ->
 120                                 t = (TBRef n).
 121       XElim t; Intros.
 122 (* case 1 : TSort *)
 123       Inversion H0.
 124 (* case 2 : TBRef n0 *)
 125       Apply (lt_le_e n0 d); Intros.
 126 (* case 2.1 : n0 < d *)
 127       Rewrite lift_bref_lt in H0; [ Inversion H0; Clear H0 | XAuto ].
 128       Rewrite <- H3 in H1; Clear H3 n0.
 129       EApply le_false; [ Apply H | XEAuto ].
 130 (* case 2.2 : n0 >= d *)
 131       Rewrite lift_bref_ge in H0; [ Inversion H0; XEAuto | XAuto ].
 132 (* case 3 : TTail k *)
 133       Rewrite lift_tail in H2; Inversion H2.
 134       Qed.
 135
 136 (* NOTE: lift_gen_tail should be used instead of these two *) (**)
 137       Theorem lift_gen_bind: (b:?; u,t,x:?; h,d:?)
 138                              (TTail (Bind b) u t) = (lift h d x) ->
 139                              (EX y z | x = (TTail (Bind b) y z) &
 140                                        u = (lift h d y) &
 141                                        t = (lift h (S d) z)
 142                              ).
 143       XElim x; Intros.
 144 (* case 1 : TSort *)
 145       Inversion H.
 146 (* case 2 : TBRef n *)
 147       Apply (lt_le_e n d); Intros.
 148 (* case 2.1 : n < d *)
 149       Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
 150 (* case 2.2 : n >= d *)
 151       Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
 152 (* case 3 : TTail k *)
 153       Rewrite lift_tail in H1; Inversion H1.
 154       XEAuto.
 155       Qed.
 156
 157       Theorem lift_gen_flat: (f:?; u,t,x:?; h,d:?)
 158                              (TTail (Flat f) u t) = (lift h d x) ->
 159                              (EX y z | x = (TTail (Flat f) y z) &
 160                                        u = (lift h d y) &
 161                                         t = (lift h d z)
 162                              ).
 163       XElim x; Intros.
 164 (* case 1 : TSort *)
 165       Inversion H.
 166 (* case 2 : TBRef n *)
 167       Apply (lt_le_e n d); Intros.
 168 (* case 2.1 : n < d *)
 169       Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
 170 (* case 2.2 : n >= d *)
 171       Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
 172 (* case 3 : TTail k *)
 173       Rewrite lift_tail in H1; Inversion H1.
 174       XEAuto.
 175       Qed.
 176
 177    End lift_gen.
 178
 179       Tactic Definition LiftGenBase :=
 180          Match Context With
 181             | [ H: (TSort ?0) = (lift ?1 ?2 ?3) |- ? ] ->
 182                LApply (lift_gen_sort ?1 ?2 ?0 ?3); [ Clear H; Intros | XAuto ]
 183             | [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
 184                 H3: (TBRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
 185                Apply (lift_gen_bref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
 186             | [ H: (TBRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
 187                LApply (lift_gen_bref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
 188                LApply H_x; [ Clear H_x; Intros H_x | Arith7' ?1; XAuto ];
 189                LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];
 190                Apply H_x
 191             | [ H: (TBRef (plus ?0 ?1)) = (lift ?1 ?2 ?3) |- ? ] ->
 192                LApply (lift_gen_bref_ge ?1 ?2 ?0); [ Intros H_x | XAuto ];
 193                LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
 194             | [ H1: (TBRef ?0) = (lift ?1 ?2 ?3); H2: (lt ?0 ?4) |- ? ] ->
 195                LApply (lift_gen_bref_lt ?1 ?2 ?0);
 196                [ Intros H_x | Apply lt_le_trans with m:=?4; XEAuto ];
 197                LApply (H_x ?3); [ Clear H_x H1; Intros | XAuto ]
 198             | [ H: (TBRef ?0) = (lift ?1 ?2 ?3) |- ? ] ->
 199                LApply (lift_gen_bref_lt ?1 ?2 ?0); [ Intros H_x | XEAuto ];
 200                LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
 201             | [ H: (TTail (Bind ?0) ?1 ?2) = (lift ?3 ?4 ?5) |- ? ] ->
 202                LApply (lift_gen_bind ?0 ?1 ?2 ?5 ?3 ?4); [ Clear H; Intros H | XAuto ];
 203                XElim H; Intros
 204             | [ H: (TTail (Flat ?0) ?1 ?2) = (lift ?3 ?4 ?5) |- ? ] ->
 205                LApply (lift_gen_flat ?0 ?1 ?2 ?5 ?3 ?4); [ Clear H; Intros H | XAuto ];
 206                XElim H; Intros.
 207
 208    Section lift_props. (*****************************************************)
 209
 210       Theorem lift_r: (t:?; d:?) (lift (0) d t) = t.
 211       XElim t; Intros.
 212 (* case 1: TSort *)
 213       XAuto.
 214 (* case 2: TBRef n *)
 215       Apply (lt_le_e n d); Intros.
 216 (* case 2.1: n < d *)
 217       Rewrite lift_bref_lt; XAuto.
 218 (* case 2.2: n >= d *)
 219       Rewrite lift_bref_ge; XAuto.
 220 (* case 3: TTail *)
 221       LiftTailRw; XAuto.
 222       Qed.
 223
 224       Theorem lift_bref_gt : (d,n:?) (lt d n) ->
 225                              (lift (1) d (TBRef (pred n))) = (TBRef n).
 226       Intros.
 227       Rewrite lift_bref_ge.
 228 (* case 1: first branch *)
 229       Rewrite <- plus_sym; Simpl; Rewrite <- (S_pred n d); XAuto.
 230 (* case 2: second branch *)
 231       Apply le_S_n; Rewrite <- (S_pred n d); XAuto.
 232       Qed.
 233
 234    End lift_props.
 235
 236       Hints Resolve lift_r lift_bref_gt : ltlc.