(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require Export tlist_defs. Require Export clt_defs. Fixpoint lref_map [f:nat->nat; d:nat; t:T] : T := Cases t of | (TSort n) => (TSort n) | (TLRef i) => (TLRef (if (blt i d) then i else (f i))) | (THead k u t) => (THead k (lref_map f d u) (lref_map f (s k d) t)) end. Definition lift : nat -> nat -> T -> T := [h,i,t:?](lref_map [x:?](plus x h) i t). Hint f3NNT : ld := Resolve (f_equal3 nat nat T). Fixpoint lifts [h:nat; d:nat; ts:TList] : TList := Cases ts of | TNil => TNil | (TCons t ts) => (TCons (lift h d t) (lifts h d ts)) end. Section lift_rw. (********************************************************) Lemma lift_sort: (n:?; h,d:?) (lift h d (TSort n)) = (TSort n). Proof. XAuto. Qed. Hints Resolve sym_equal : ld. Lemma lift_lref_lt: (n:?; h,d:?) (lt n d) -> (lift h d (TLRef n)) = (TLRef n). Proof. Intros; Unfold lift; Simpl. Replace (blt n d) with true; XAuto. Qed. Lemma lift_lref_ge: (n:?; h,d:?) (le d n) -> (lift h d (TLRef n)) = (TLRef (plus n h)). Proof. Intros; Unfold lift; Simpl. Replace (blt n d) with false; XAuto. Qed. Lemma lift_head: (k:?; u,t:?; h,d:?) (lift h d (THead k u t)) = (THead k (lift h d u) (lift h (s k d) t)). Proof. XAuto. Qed. Lemma lift_bind: (b:?; u,t:?; h,d:?) (lift h d (THead (Bind b) u t)) = (THead (Bind b) (lift h d u) (lift h (S d) t)). Proof. XAuto. Qed. Lemma lift_flat: (f:?; u,t:?; h,d:?) (lift h d (THead (Flat f) u t)) = (THead (Flat f) (lift h d u) (lift h d t)). Proof. XAuto. Qed. End lift_rw. Tactic Definition LiftHeadRw := Repeat (Rewrite lift_head Orelse Rewrite lift_bind Orelse Rewrite lift_flat). Tactic Definition LiftHeadRwBack := Repeat (Rewrite <- lift_head Orelse Rewrite <- lift_bind Orelse Rewrite <- lift_flat). Section lift_gen_base. (**************************************************) Hints Resolve sym_eq : ld. Lemma lift_gen_sort: (h,d,n:?; t:?) (TSort n) = (lift h d t) -> t = (TSort n). Proof. XElim t; Intros. (* case 1 : TSort *) XAuto. (* case 2 : TLRef n0 *) Apply (lt_le_e n0 d); Intros. (* case 2.1 : n0 < d *) Rewrite lift_lref_lt in H; XInv; XAuto. (* case 2.2 : n0 >= d *) Rewrite lift_lref_ge in H; XInv; XAuto. (* case 3 : THead k *) Rewrite lift_head in H1; XInv. Qed. Lemma lift_gen_lref: (t:?; d,h,i:?) (TLRef i) = (lift h d t) -> ((lt i d) /\ t = (TLRef i)) \/ (le (plus d h) i) /\ t = (TLRef (minus i h)). Proof. XElim t; Intros. (* case 1: TSort *) Rewrite lift_sort in H; XInv. (* case 2: TLRef n *) Apply (lt_le_e n d); Intros. (* case 2.1: n < d *) Rewrite lift_lref_lt in H; [ Idtac | XAuto ]. XInv; Subst; XAuto. (* case 2.2: n >= d *) Rewrite lift_lref_ge in H; [ Idtac | XAuto ]. XInv; Subst; Rewrite minus_plus_r; XAuto. (* case 3: TSort *) Rewrite lift_head in H1; XInv. Qed. Hints Resolve lt_le_S lt_le_trans : ld. (* NOTE: lift_gen_lref should be used instead of these three *) (**) Lemma lift_gen_lref_lt: (h,d,n:?) (lt n d) -> (t:?) (TLRef n) = (lift h d t) -> t = (TLRef n). Proof. Intros; XDecomPoseClear H0 '(lift_gen_lref ? ? ? ? H0); Subst; [ XAuto | EApply le_false; [ Apply H2 | XAuto ] ]. Qed. Hints Resolve simpl_lt_plus_r : ld. Lemma lift_gen_lref_false: (h,d,n:?) (le d n) -> (lt n (plus d h)) -> (t:?) (TLRef n) = (lift h d t) -> (P:Prop) P. Proof. Intros; XDecomPoseClear H1 '(lift_gen_lref ? ? ? ? H1); Subst; EApply le_false; [ EApply H | XAuto | EApply H3 | XAuto ]. Qed. Hints Resolve simpl_plus_r : ld. Lemma lift_gen_lref_ge: (h,d,n:?) (le d n) -> (t:?) (TLRef (plus n h)) = (lift h d t) -> t = (TLRef n). Proof. Intros; XDecomPoseClear H0 '(lift_gen_lref ? ? ? ? H0); Subst; [ EApply le_false; [ Apply H | XDEAuto 4 ] | XAuto ]. Qed. Lemma lift_gen_head: (k:?; u,t,x:?; h,d:?) (THead k u t) = (lift h d x) -> (EX y z | x = (THead k y z) & u = (lift h d y) & t = (lift h (s k d) z) ). Proof. XElim x; Intros. (* case 1 : TSort *) Rewrite lift_sort in H; XInv. (* case 2 : TLRef n *) Apply (lt_le_e n d); Intros. (* case 2.1 : n < d *) Rewrite lift_lref_lt in H; [ XInv | XAuto ]. (* case 2.2 : n >= d *) Rewrite lift_lref_ge in H; [ XInv | XAuto ]. (* case 3 : THead k *) Rewrite lift_head in H1; XInv; Subst; XDEAuto 2. Qed. (* NOTE: lift_gen_head should be used instead of these two *) (**) Lemma lift_gen_bind: (b:?; u,t,x:?; h,d:?) (THead (Bind b) u t) = (lift h d x) -> (EX y z | x = (THead (Bind b) y z) & u = (lift h d y) & t = (lift h (S d) z) ). Proof. Intros; XDecomPoseClear H '(lift_gen_head ? ? ? ? ? ? H). Subst; XDEAuto 2. Qed. Lemma lift_gen_flat: (f:?; u,t,x:?; h,d:?) (THead (Flat f) u t) = (lift h d x) -> (EX y z | x = (THead (Flat f) y z) & u = (lift h d y) & t = (lift h d z) ). Proof. Intros; XDecomPoseClear H '(lift_gen_head ? ? ? ? ? ? H). Subst; XDEAuto 2. Qed. End lift_gen_base. 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: (TLRef ?2) = (lift ?3 ?1 ?4) |- ? ] -> Apply (lift_gen_lref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto | [ _: (TLRef ?1) = (lift (S ?1) (0) ?2) |- ? ] -> EApply lift_gen_lref_false; [ Idtac | Idtac | XDEAuto 2 ]; XDEAuto 2 | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] -> LApply (lift_gen_lref_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: (TLRef (plus ?0 ?1)) = (lift ?1 ?2 ?3) |- ? ] -> LApply (lift_gen_lref_ge ?1 ?2 ?0); [ Intros H_x | XAuto ]; LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ] | [ H1: (TLRef ?0) = (lift ?1 ?2 ?3); H2: (lt ?0 ?4) |- ? ] -> LApply (lift_gen_lref_lt ?1 ?2 ?0); [ Intros H_x | Apply lt_le_trans with m:=?4; XDEAuto 2 ]; LApply (H_x ?3); [ Clear H_x H1; Intros | XAuto ] | [ H: (TLRef ?0) = (lift ?1 ?2 ?3) |- ? ] -> LApply (lift_gen_lref_lt ?1 ?2 ?0); [ Intros H_x | XDEAuto 2 ]; LApply (H_x ?3); [ Clear H_x H; Intros | XAuto ] | [ H: (TLRef ?) = (lift ? ? ?) |- ? ] -> XDecomPoseClear H '(lift_gen_lref ? ? ? ? H); Subst | [ H: (THead (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: (THead (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 ). Tactic Definition LiftXGenBase := ( Match Context With | [ H: (TSort ?) = (lift ? ? ?) |- ? ] -> XPoseClear H '(lift_gen_sort ? ? ? ? H); Subst | [ H: (TLRef ?) = (lift ? ? ?) |- ? ] -> XDecomPoseClear H '(lift_gen_lref ? ? ? ? H); Subst | [ H: (THead ? ? ?) = (lift ? ? ?) |- ? ] -> XDecomPoseClear H '(lift_gen_head ? ? ? ? ? ? H); Subst ). Section lift_props. (*****************************************************) Lemma thead_x_lift_y_y: (k:?; t,v:?; h,d:?) (THead k v (lift h d t)) = t -> (P:Prop) P. Proof. XElim t; Intros; XInv. (* case 3: THead *) Rewrite H3 in H0; Clear H H2 H3 k v. (**) Rewrite lift_head in H1; EApply H0; XDEAuto 2. Qed. Hints Resolve sym_eq : ld. Lemma lift_r: (t:?; d:?) (lift (0) d t) = t. Proof. XElim t; Intros. (* case 1: TSort *) XAuto. (* case 2: TLRef n *) Apply (lt_le_e n d); Intros. (* case 2.1: n < d *) Rewrite lift_lref_lt; XAuto. (* case 2.2: n >= d *) Rewrite lift_lref_ge; XAuto. (* case 3: THead *) LiftHeadRw; XAuto. Qed. Lemma lift_lref_gt : (d,n:?) (lt d n) -> (lift (1) d (TLRef (pred n))) = (TLRef n). Proof. Intros. Rewrite lift_lref_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. Tactic Definition TInv := ( Match Context With | [ _: (THead ? ? (lift ? ? ?0)) = ?0 |- ? ] -> EApply thead_x_lift_y_y; XDEAuto 2 | [ |- ? ] -> TInvBase ). Section lift_tle_props. (*************************************************) Lemma lift_tle: (t:?; h,d:?) (tle t (lift h d t)). Proof. Unfold tle; XElim t; Simpl; Intros. (* case 1: TSort *) XAuto. (* case 2: TLRef *) XAuto. (* case 3: THead *) XPoseClear H '(H h d); XPoseClear H0 '(H0 h (s k d)); XAuto. Qed. End lift_tle_props. Hints Resolve lift_tle : ld. Section lifts_props. (****************************************************) Lemma lifts_tapp: (h,d:?; v:?; vs:?) (lifts h d (TApp vs v)) = (TApp (lifts h d vs) (lift h d v)). Proof. XElim vs; Simpl; Intros; [ Idtac | Rewrite H ]; XAuto. Qed. End lifts_props.