--- /dev/null
+(*#* #stop file *)
+
+Require Export terms_defs.
+
+ Fixpoint bref_map [g:nat->nat; d:nat; t:T] : T := Cases t of
+ | (TSort n) => (TSort n)
+ | (TBRef n) =>
+ if (blt n d) then (TBRef n) else (TBRef (g n))
+ | (TTail k u t) =>
+ (TTail k (bref_map g d u) (bref_map g (s k d) t))
+ end.
+
+ Definition lift : nat -> nat -> T -> T :=
+ [h](bref_map [x](plus x h)).
+
+ Section lift_rw. (********************************************************)
+
+ Theorem lift_sort: (n:?; h,d:?) (lift h d (TSort n)) = (TSort n).
+ XAuto.
+ Qed.
+
+ Theorem lift_bref_lt: (n:?; h,d:?) (lt n d) ->
+ (lift h d (TBRef n)) = (TBRef n).
+ Intros; Unfold lift; Simpl.
+ Replace (blt n d) with true; XAuto.
+ Qed.
+
+ Theorem lift_bref_ge: (n:?; h,d:?) (le d n) ->
+ (lift h d (TBRef n)) = (TBRef (plus n h)).
+
+ Intros; Unfold lift; Simpl.
+ Replace (blt n d) with false; XAuto.
+ Qed.
+
+ Theorem lift_tail: (k:?; u,t:?; h,d:?)
+ (lift h d (TTail k u t)) =
+ (TTail k (lift h d u) (lift h (s k d) t)).
+ XAuto.
+ Qed.
+
+ Theorem lift_bind: (b:?; u,t:?; h,d:?)
+ (lift h d (TTail (Bind b) u t)) =
+ (TTail (Bind b) (lift h d u) (lift h (S d) t)).
+ XAuto.
+ Qed.
+
+ Theorem lift_flat: (f:?; u,t:?; h,d:?)
+ (lift h d (TTail (Flat f) u t)) =
+ (TTail (Flat f) (lift h d u) (lift h d t)).
+ XAuto.
+ Qed.
+
+ End lift_rw.
+
+ Hints Resolve lift_bref_lt lift_bind lift_flat : ltlc.
+
+ Tactic Definition LiftTailRw :=
+ Repeat (Rewrite lift_tail Orelse Rewrite lift_bind Orelse Rewrite lift_flat).
+
+ Tactic Definition LiftTailRwBack :=
+ Repeat (Rewrite <- lift_tail Orelse Rewrite <- lift_bind Orelse Rewrite <- lift_flat).
+
+ Section lift_gen. (*******************************************************)
+
+ Theorem lift_gen_sort: (h,d,n:?; t:?) (TSort n) = (lift h d t) ->
+ t = (TSort n).
+ XElim t; Intros.
+(* case 1 : TSort *)
+ XAuto.
+(* case 2 : TBRef n0 *)
+ Apply (lt_le_e n0 d); Intros.
+(* case 2.1 : n0 < d *)
+ Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+(* case 2.2 : n0 >= d *)
+ Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+(* case 3 : TTail k *)
+ Rewrite lift_tail in H1; Inversion H1.
+ Qed.
+
+ Theorem lift_gen_bref_lt: (h,d,n:?) (lt n d) ->
+ (t:?) (TBRef n) = (lift h d t) ->
+ t = (TBRef n).
+ XElim t; Intros.
+(* case 1 : TSort *)
+ XAuto.
+(* case 2 : TBRef n0 *)
+ Apply (lt_le_e n0 d); Intros.
+(* case 2.1 : n0 < d *)
+ Rewrite lift_bref_lt in H0; XAuto.
+(* case 2.2 : n0 >= d *)
+ Rewrite lift_bref_ge in H0; [ Inversion H0; Clear H0 | XAuto ].
+ Rewrite H3 in H; Clear H3 n.
+ EApply le_false; [ Apply H1 | XEAuto ].
+(* case 3 : TTail k *)
+ Rewrite lift_tail in H2; Inversion H2.
+ Qed.
+
+ Theorem lift_gen_bref_false: (h,d,n:?) (le d n) -> (lt n (plus d h)) ->
+ (t:?) (TBRef n) = (lift h d t) ->
+ (P:Prop) P.
+ XElim t; Intros.
+(* case 1 : TSort *)
+ Inversion H1.
+(* case 2 : TBRef n0 *)
+ Apply (lt_le_e n0 d); Intros.
+(* case 2.1 : n0 < d *)
+ Rewrite lift_bref_lt in H1; [ Inversion H1; Clear H1 | XAuto ].
+ Rewrite <- H4 in H2; Clear H4 n0.
+ EApply le_false; [ Apply H | XEAuto ].
+(* case 2.2 : n0 >= d *)
+ Rewrite lift_bref_ge in H1; [ Inversion H1; Clear H1 | XAuto ].
+ Rewrite H4 in H0; Clear H4.
+ EApply le_false; [ Apply H2 | XEAuto ].
+(* case 3 : TTail k *)
+ Rewrite lift_tail in H3; Inversion H3.
+ Qed.
+
+ Theorem lift_gen_bref_ge: (h,d,n:?) (le d n) ->
+ (t:?) (TBRef (plus n h)) = (lift h d t) ->
+ t = (TBRef n).
+ XElim t; Intros.
+(* case 1 : TSort *)
+ Inversion H0.
+(* case 2 : TBRef n0 *)
+ Apply (lt_le_e n0 d); Intros.
+(* case 2.1 : n0 < d *)
+ Rewrite lift_bref_lt in H0; [ Inversion H0; Clear H0 | XAuto ].
+ Rewrite <- H3 in H1; Clear H3 n0.
+ EApply le_false; [ Apply H | XEAuto ].
+(* case 2.2 : n0 >= d *)
+ Rewrite lift_bref_ge in H0; [ Inversion H0; XEAuto | XAuto ].
+(* case 3 : TTail k *)
+ Rewrite lift_tail in H2; Inversion H2.
+ Qed.
+
+(* NOTE: lift_gen_tail should be used instead of these two *) (**)
+ Theorem lift_gen_bind: (b:?; u,t,x:?; h,d:?)
+ (TTail (Bind b) u t) = (lift h d x) ->
+ (EX y z | x = (TTail (Bind b) y z) &
+ u = (lift h d y) &
+ t = (lift h (S d) z)
+ ).
+ XElim x; Intros.
+(* case 1 : TSort *)
+ Inversion H.
+(* case 2 : TBRef n *)
+ Apply (lt_le_e n d); Intros.
+(* case 2.1 : n < d *)
+ Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+(* case 2.2 : n >= d *)
+ Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+(* case 3 : TTail k *)
+ Rewrite lift_tail in H1; Inversion H1.
+ XEAuto.
+ Qed.
+
+ Theorem lift_gen_flat: (f:?; u,t,x:?; h,d:?)
+ (TTail (Flat f) u t) = (lift h d x) ->
+ (EX y z | x = (TTail (Flat f) y z) &
+ u = (lift h d y) &
+ t = (lift h d z)
+ ).
+ XElim x; Intros.
+(* case 1 : TSort *)
+ Inversion H.
+(* case 2 : TBRef n *)
+ Apply (lt_le_e n d); Intros.
+(* case 2.1 : n < d *)
+ Rewrite lift_bref_lt in H; [ Inversion H | XAuto ].
+(* case 2.2 : n >= d *)
+ Rewrite lift_bref_ge in H; [ Inversion H | XAuto ].
+(* case 3 : TTail k *)
+ Rewrite lift_tail in H1; Inversion H1.
+ XEAuto.
+ Qed.
+
+ End lift_gen.
+
+ Tactic Definition LiftGenBase :=
+ Match Context With
+ | [ H: (TSort ?0) = (lift ?1 ?2 ?3) |- ? ] ->
+ LApply (lift_gen_sort ?1 ?2 ?0 ?3); [ Clear H; Intros | XAuto ]
+ | [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
+ H3: (TBRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
+ Apply (lift_gen_bref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
+ | [ H: (TBRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
+ LApply (lift_gen_bref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
+ LApply H_x; [ Clear H_x; Intros H_x | Arith7' ?1; XAuto ];
+ LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];
+ Apply H_x
+ | [ H: (TBRef (plus ?0 ?1)) = (lift ?1 ?2 ?3) |- ? ] ->
+ LApply (lift_gen_bref_ge ?1 ?2 ?0); [ Intros H_x | XAuto ];
+ LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
+ | [ H1: (TBRef ?0) = (lift ?1 ?2 ?3); H2: (lt ?0 ?4) |- ? ] ->
+ LApply (lift_gen_bref_lt ?1 ?2 ?0);
+ [ Intros H_x | Apply lt_le_trans with m:=?4; XEAuto ];
+ LApply (H_x ?3); [ Clear H_x H1; Intros | XAuto ]
+ | [ H: (TBRef ?0) = (lift ?1 ?2 ?3) |- ? ] ->
+ LApply (lift_gen_bref_lt ?1 ?2 ?0); [ Intros H_x | XEAuto ];
+ LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ]
+ | [ H: (TTail (Bind ?0) ?1 ?2) = (lift ?3 ?4 ?5) |- ? ] ->
+ LApply (lift_gen_bind ?0 ?1 ?2 ?5 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros
+ | [ H: (TTail (Flat ?0) ?1 ?2) = (lift ?3 ?4 ?5) |- ? ] ->
+ LApply (lift_gen_flat ?0 ?1 ?2 ?5 ?3 ?4); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros.
+
+ Section lift_props. (*****************************************************)
+
+ Theorem lift_r: (t:?; d:?) (lift (0) d t) = t.
+ XElim t; Intros.
+(* case 1: TSort *)
+ XAuto.
+(* case 2: TBRef n *)
+ Apply (lt_le_e n d); Intros.
+(* case 2.1: n < d *)
+ Rewrite lift_bref_lt; XAuto.
+(* case 2.2: n >= d *)
+ Rewrite lift_bref_ge; XAuto.
+(* case 3: TTail *)
+ LiftTailRw; XAuto.
+ Qed.
+
+ Theorem lift_bref_gt : (d,n:?) (lt d n) ->
+ (lift (1) d (TBRef (pred n))) = (TBRef n).
+ Intros.
+ Rewrite lift_bref_ge.
+(* case 1: first branch *)
+ Rewrite <- plus_sym; Simpl; Rewrite <- (S_pred n d); XAuto.
+(* case 2: second branch *)
+ Apply le_S_n; Rewrite <- (S_pred n d); XAuto.
+ Qed.
+
+ End lift_props.
+
+ Hints Resolve lift_r lift_bref_gt : ltlc.
projects / helm.git / blobdiff