(****************************************************************************) (* *) (* 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 flt_defs. Require Export drop_defs. Inductive clear : C -> C -> Prop := | clear_bind: (b:?; e:?; u:?) (clear (CHead e (Bind b) u) (CHead e (Bind b) u)) | clear_flat: (e,c:?) (clear e c) -> (f:?; u:?) (clear (CHead e (Flat f) u) c). Hint clear : ld := Constructors clear. Inductive getl [h:nat; c1:C; c2:C] : Prop := | getl_intro: (e:?) (drop h (0) c1 e) -> (clear e c2) -> (getl h c1 c2). Hint getl : ld := Constructors getl. Definition cimp: C -> C -> Prop := [c1,c2:?] (b:?; d1:?; w:?; h:?) (getl h c1 (CHead d1 (Bind b) w)) -> (EX d2 | (getl h c2 (CHead d2 (Bind b) w))). Section clear_gen_base. (*************************************************) Lemma clear_gen_sort: (x:?; n:?) (clear (CSort n) x) -> (P:Prop) P. Proof. Intros; InsertEq H '(CSort n); XElim H; Clear y x; Intros; XInv. Qed. Lemma clear_gen_bind: (b:?; e,x:?; u:?) (clear (CHead e (Bind b) u) x) -> x = (CHead e (Bind b) u). Proof. Intros; InsertEq H '(CHead e (Bind b) u); XElim H; Clear y x; Intros; XInv; Subst; XAuto. Qed. Lemma clear_gen_flat: (f:?; e,x:?; u:?) (clear (CHead e (Flat f) u) x) -> (clear e x). Proof. Intros; InsertEq H '(CHead e (Flat f) u); XElim H; Clear y x; Intros; XInv; Subst; XAuto. Qed. Lemma clear_gen_flat_r: (f:?; x,e:?; u:?) (clear x (CHead e (Flat f) u)) -> (P:Prop) P. Proof. Intros; InsertEq H '(CHead e (Flat f) u). XElim H; Intros; [ XInv | Subst; XAuto ]. Qed. Lemma clear_gen_all: (c1,c2:?) (clear c1 c2) -> (EX b e u | c2 = (CHead e (Bind b) u)). Proof. Intros; XElim H; Clear c1 c2; Intros; Subst; Try (XDecompose H0; Subst); XDEAuto 2. Qed. End clear_gen_base. Tactic Definition ClearGenBase := ( Match Context With | [ H: (clear (CSort ?1) ?0) |- ? ] -> EApply clear_gen_sort; Apply H | [ H: (clear (CHead ?1 (Bind ?2) ?3) ?0) |- ? ] -> LApply (clear_gen_bind ?2 ?1 ?0 ?3); [ Clear H; Intros H | XAuto ]; Subst | [ H: (clear (CHead ?1 (Flat ?2) ?3) ?0) |- ? ] -> LApply (clear_gen_flat ?2 ?1 ?0 ?3); [ Clear H; Intros H | XAuto ] | [ H: (clear ?0 (CHead ?1 (Flat ?2) ?3)) |- ? ] -> EApply (clear_gen_flat_r ?2 ?0 ?1 ?3); Apply H ). Tactic Definition ClearGenAll := ( Match Context With | [ H: (clear ?1 ?2) |- ? ] -> LApply (clear_gen_all ?1 ?2); [ Intros H_x | XAuto ]; XDecompose H_x; Subst ). Section drop_clear. (*****************************************************) Hint discr : ld := Extern 4 (drop ? ? ? ?) Simpl. Lemma drop_clear: (c1,c2:?; i:?) (drop (S i) (0) c1 c2) -> (EX b e v | (clear c1 (CHead e (Bind b) v)) & (drop i (0) e c2) ). Proof. XElim c1; Intros; DropGenBase. (* case 1: CSort *) XInv; XInv. (* case 2: CHead k *) NewInduction k. (* case 2.1: Bind *) XDEAuto 2. (* case 2.2: Flat *) LApply (H c2 i); [ Clear H; Intros H | XAuto ]. XDecompose H; XDEAuto 3. Qed. Lemma drop_clear_O: (b:?; c,e1:?; u:?) (clear c (CHead e1 (Bind b) u)) -> (e2:?; i:?) (drop i (0) e1 e2) -> (drop (S i) (0) c e2). Proof. XElim c; Intros; Try NewInduction k; ClearGenBase. (* case 1: bind *) XInv; Subst; XAuto. (* case 2: flat *) XDEAuto 4. Qed. Lemma drop_clear_S: (x2,x1:?; h,d:?) (drop h (S d) x1 x2) -> (b:?; c2:?; u:?) (clear x2 (CHead c2 (Bind b) u)) -> (EX c1 | (clear x1 (CHead c1 (Bind b) (lift h d u))) & (drop h d c1 c2) ). Proof. XElim x2; Intros. (* case 1: CSort *) ClearGenBase. (* case 2: CHead k *) DropGenBase; Subst. NewInduction k; ClearGenBase. (* case 2.1: Bind *) XInv; Subst; XDEAuto 2. (* case 2.2: Flat *) LApply (H x h d); [ Clear H H2; Intros H | XAuto ]. LApply (H b c2 u); [ Clear H H1; Intros H | XAuto ]. XDecompose H; XDEAuto 3. Qed. End drop_clear. Tactic Definition DropClear := ( Match Context With | [ H: (drop (S ?3) (0) ?1 ?2) |- ? ] -> LApply (drop_clear ?1 ?2 ?3); [ Clear H; Intros H | XAuto ]; XDecompose H | [ H0: (drop ?1 (S ?2) ?3 ?4); H1: (clear ?4 (CHead ?5 (Bind ?6) ?7)) |- ? ] -> LApply (drop_clear_S ?4 ?3 ?1 ?2); [ Clear H0; Intros H0 | XAuto ]; LApply (H0 ?6 ?5 ?7); [ Clear H0 H1; Intros H0 | XAuto ]; XDecompose H0 ). Section clear_props. (****************************************************) Lemma clear_clear: (c1,c2:?) (clear c1 c2) -> (clear c2 c2). Proof. XElim c1; Intros; Try NewInduction k; ClearGenBase; XAuto. Qed. Theorem clear_mono: (c,c1:?) (clear c c1) -> (c2:?) (clear c c2) -> c1 = c2. Proof. XElim c; Intros; Try NewInduction k; Repeat ClearGenBase; XAuto. Qed. Theorem clear_trans: (c1,c:?) (clear c1 c) -> (c2:?) (clear c c2) -> (clear c1 c2). Proof. XElim c1; Intros; Try NewInduction k; Repeat ClearGenBase; XDEAuto 3. Qed. Lemma clear_ctail: (b:?; c1,c2:?; u2:?) (clear c1 (CHead c2 (Bind b) u2)) -> (k:?; u1:?) (clear (CTail k u1 c1) (CHead (CTail k u1 c2) (Bind b) u2)). Proof. XElim c1; Intros; Simpl; Try NewInduction k; ClearGenBase; XInv; Subst; XAuto. Qed. End clear_props. Hints Resolve clear_ctail : ld. Tactic Definition ClearDis := ( Match Context With | [ H1: (clear ?1 ?); H2: (clear ?1 ?) |- ? ] -> XPoseClear H2 '(clear_mono ? ? H1 ? H2); XInv; Subst ). Section getl_gen_base. (**************************************************) Lemma getl_gen_all: (c1,c2:?; i:?) (getl i c1 c2) -> (EX e | (drop i (0) c1 e) & (clear e c2)). Proof. Intros; XElim H; XDEAuto 2. Qed. Tactic Definition GetLGenBase := ( Match Context With | [ H: (getl ?0 ?1 ?2) |- ? ] -> LApply (getl_gen_all ?1 ?2 ?0); [ Clear H; Intros H | XAuto ]; XDecompose H; Subst ). Lemma getl_gen_sort: (n,h:?; x:?) (getl h (CSort n) x) -> (P:Prop) P. Proof. Intros; GetLGenBase; DropGenBase; Subst; ClearGenBase. Qed. Lemma getl_gen_O: (e,x:?) (getl (0) e x) -> (clear e x). Proof. Intros; GetLGenBase; DropGenBase; Subst; XDEAuto 2. Qed. Lemma getl_gen_S: (k:?; c,x:?; u:?; h:?) (getl (S h) (CHead c k u) x) -> (getl (r k h) c x). Proof. Intros; GetLGenBase; DropGenBase; XDEAuto 2. Qed. Lemma getl_gen_2: (c1,c2:?; i:?) (getl i c1 c2) -> (EX b c v | c2 = (CHead c (Bind b) v)). Proof. Intros; GetLGenBase; ClearGenAll; XDEAuto 2. Qed. End getl_gen_base. Tactic Definition GetLGenBase := ( Match Context With | [ H: (getl ?0 (CSort ?2) ?3) |- ? ] -> EApply (getl_gen_sort ?2 ?0 ?3); Apply H | [ H: (getl (0) ?0 ?1) |- ? ] -> LApply (getl_gen_O ?0 ?1); [ Clear H; Intros H | XAuto ] | [ H: (getl (S ?0) (CHead ?1 ?2 ?3) ?4) |- ? ] -> LApply (getl_gen_S ?2 ?1 ?4 ?3 ?0); [ Clear H; Intros | XAuto ] | [ H: (getl ?0 ?1 ?2) |- ? ] -> LApply (getl_gen_all ?1 ?2 ?0); [ Clear H; Intros H | XAuto ]; XDecompose H; Subst ). Tactic Definition GetLGen2 := ( Match Context With | [ H: (getl ? ? ?) |- ? ] -> XDecomPose '(getl_gen_2 ? ? ? H); XInv; Subst ). Section getl_props. (*****************************************************) Lemma getl_refl: (b:?; c:?; u:?) (getl (0) (CHead c (Bind b) u) (CHead c (Bind b) u)). Proof. XDEAuto 2. Qed. Hints Resolve drop_clear_O clear_trans : ld. Lemma clear_getl_trans: (i:?; c2,c3:?) (getl i c2 c3) -> (c1:?) (clear c1 c2) -> (getl i c1 c3). Proof. XElim i. (* case 1: i = 0 *) Intros; GetLGenBase; XDEAuto 3. (* case 2: i > 0 *) XElim c2; Simpl; Intros; Try NewInduction k; GetLGenBase. (* case 2.1: Bind *) GetLGenBase; XDEAuto 3. (* case 2.2: Flat *) ClearGenBase. Qed. Lemma getl_clear_trans: (i:?; c1,c2:?) (getl i c1 c2) -> (c3:?) (clear c2 c3) -> (getl i c1 c3). Proof. Intros; GetLGenBase; ClearGenAll; ClearGenBase; XDEAuto 2. Qed. Lemma getl_head: (k:?; h:?; c,e:?) (getl (r k h) c e) -> (u:?) (getl (S h) (CHead c k u) e). Proof. Intros; GetLGenBase; XDEAuto 3. Qed. Lemma getl_flat: (c,e:?; h:?) (getl h c e) -> (f:?; u:?) (getl h (CHead c (Flat f) u) e). Proof. Intros; GetLGenBase; NewInduction h. (* case 1: h = 0 *) DropGenBase; Subst; XDEAuto 3. (* case 2: h > 0 *) XDEAuto 3. Qed. Lemma getl_drop: (b:?; c,e:?; u:?; h:?) (getl h c (CHead e (Bind b) u)) -> (drop (S h) (0) c e). Proof. XElim c. (* case 1: CSort *) Intros; GetLGenBase; Subst; XInv. (* case 2: CHead *) XElim h; Intros; GetLGenBase. (* case 2.1: h = 0 *) NewInduction k; ClearGenBase. (* case 2.1.1: Bind *) XInv; Subst; XAuto. (* case 2.1.2: Flat *) XDEAuto 3. (* case 2.2: h > 0 *) Apply drop_drop; RRw; XDEAuto 2. (**) (* explicit constructor *) Qed. Hints Resolve getl_head getl_flat : ld. Lemma getl_clear_bind: (b:?; c,e1:?; v:?) (clear c (CHead e1 (Bind b) v)) -> (e2:?; n:?) (getl n e1 e2) -> (getl (S n) c e2). Proof. XElim c; Intros; Try NewInduction k; ClearGenBase; XInv; Subst; XDEAuto 3. Qed. Lemma getl_ctail: (b:?; c,d:?; u:?; i:?) (getl i c (CHead d (Bind b) u)) -> (k:?; v:?) (getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)). Proof. Intros; GetLGenBase; XDEAuto 4. Qed. Hints Resolve getl_refl : ld. Lemma getl_ctail_clen: (b:?; t:?; c:?) (EX n | (getl (clen c) (CTail (Bind b) t c) (CHead (CSort n) (Bind b) t)) ). Proof. XElim c; Simpl; Intros. (* case 1: CSort *) XDEAuto 2. (* case 2: CHead *) XDecompose H; NewInduction k; Simpl; XDEAuto 3. Qed. Lemma getl_dec: (c:?; i:?) (EX e b v | (getl i c (CHead e (Bind b) v))) \/ ((d:?) (getl i c d) -> (P:Prop) P). Proof. XElim c. (* case 1: CSort *) Intros; Right; Intros; GetLGenBase. (* case 2: CHead *) XElim i; Intros. (* case 2.1: i = 0 *) NewInduction k. (* case 2.1.1: Bind *) XDEAuto 3. (* case 2.1.2: Bind *) XDecomPoseClear H '(H (0)). (* case 2.2.1: getl 0 exists *) XDEAuto 4. (* case 2.2.2: getl 0 does not exist *) Right; Intros; GetLGenBase; ClearGenBase; EApply H0; XDEAuto 2. (**) (* case 2.2: i > 0 *) XDecomPoseClear H '(H (r k n)). (* case 2.2.1: getl (r k n) exists *) XDEAuto 4. (* case 2.2.2: getl (r k n) does not exist *) Right; Intros; GetLGenBase; EApply H1; XDEAuto 2. Qed. End getl_props. Hints Resolve getl_refl getl_head getl_flat getl_ctail getl_clear_bind : ld. Tactic Definition GetLDrop := ( Match Context With | [ _: (getl ?1 ?2 (CHead ?3 (Bind ?4) ?5)) |- ? ] -> LApply (getl_drop ?4 ?2 ?3 ?5 ?1); [ Intros | XAuto ] ). Section getl_flt_props. (*************************************************) Lemma clear_cle: (c1,c2:?) (clear c1 c2) -> (cle c2 c1). Proof. Unfold cle; XElim c1; Simpl; Intros; Try NewInduction k; ClearGenBase; XAuto. Qed. Hints Resolve clear_cle : ld. Lemma getl_flt: (b:?; c,e:?; u:?; i:?) (getl i c (CHead e (Bind b) u)) -> (flt e u c (TLRef i)). Proof. XElim c. (* case 1: CSort *) Intros; GetLGenBase. (* case 2: CHead *) XElim i; Intros; GetLGenBase. (* case 2.1: i = 0 *) NewInduction k; ClearGenBase; XInv; Subst; XDEAuto 3. (* case 2.2: i > 0 *) XPoseClear H '(H ? ? ? H1); Clear H1. Apply flt_arith2 with i:=(r k n); XAuto. Qed. End getl_flt_props. Section more_getl_gen_base. (*********************************************) Lemma getl_gen_flat: (f:?; e,d:?; v:?; i:?) (getl i (CHead e (Flat f) v) d) -> (getl i e d). Proof. XElim i; Intros; GetLGenBase. (* case 1: i = 0 *) ClearGenBase; XDEAuto 2. (* case 2: i > 0 *) XAuto. Qed. Lemma getl_gen_bind: (b:?; e,d:?; v:?; i:?) (getl i (CHead e (Bind b) v) d) -> (i = (0) /\ d = (CHead e (Bind b) v)) \/ (EX j | i = (S j) & (getl j e d)). Proof. XElim i; Intros; GetLGenBase. (* case 1: i = 0 *) ClearGenBase; XAuto. (* case 2: i > 0 *) XDEAuto 3. Qed. Lemma getl_gen_tail: (k:?; b:?; u1,u2:?; c2,c1:?; i:?) (getl i (CTail k u1 c1) (CHead c2 (Bind b) u2)) -> (EX e | c2 = (CTail k u1 e) & (getl i c1 (CHead e (Bind b) u2))) \/ (EX n | i = (clen c1) & k = (Bind b) & u1 = u2 & c2 = (CSort n)). Proof. XElim c1; XElim i; Simpl; Intros; GetLGenBase. (* case 1: CSort, i = 0 *) NewInduction k; Repeat ClearGenBase; XInv; Subst; XDEAuto 3. (* case 2: CSort, i > 0 *) GetLGenBase. (* case 3: CHead, i = 0 *) NewInduction k0; ClearGenBase; XInv; Subst. (* case 3.1: Bind *) XDEAuto 3. (* case 3.2: Bind *) LApply (H (0)); [ Clear H H0; Intros H | XDEAuto 2 ]. XDecompose H; Subst; XDEAuto 4. (* case 4: CHead, i > 0 *) XDecomPoseClear H '(H ? H1); Subst; Clear H1; Try (Rewrite <- H3; Clear H3; Rewrite s_r); XDEAuto 4. Qed. End more_getl_gen_base. Tactic Definition GetLXGenBase := ( Match Context With | [ H: (getl ? (CHead ? (Bind ?) ?) ?) |- ? ] -> XDecomPoseClear H '(getl_gen_bind ? ? ? ? ? H) | [ H: (getl ? (CHead ? (Flat ?) ?) ?) |- ? ] -> XPoseClear H '(getl_gen_flat ? ? ? ? ? H) | [ H: (getl ? (CTail ? ? ?) (CHead ? (Bind ?) ?)) |- ? ] -> XDecomPoseClear H '(getl_gen_tail ? ? ? ? ? ? ? H); Subst | [ |- ? ] -> GetLGenBase ). Section cimp_props. (*****************************************************) Lemma cimp_flat_sx: (f:?; c:?; v:?) (cimp (CHead c (Flat f) v) c). Proof. Unfold cimp; Intros. NewInduction h; GetLGenBase. (* case 1: h = 0 *) ClearGenBase; XDEAuto 3. (* case 2: h > 0 *) XDEAuto 2. Qed. Lemma cimp_flat_dx: (f:?; c:?; v:?) (cimp c (CHead c (Flat f) v)). Proof. Unfold cimp; XDEAuto 3. Qed. Lemma cimp_bind: (c1,c2:?) (cimp c1 c2) -> (b:?; v:?) (cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v)). Proof. Unfold cimp; Intros. NewInduction h; GetLGenBase. (* case 1: h = 0 *) ClearGenBase; XInv; Subst; XDEAuto 2. (* case 2: h > 0 *) Clear IHh; XDecomPose '(H ? ? ? ? H0); Clear H H0; XDEAuto 3. Qed. End cimp_props. Hints Resolve cimp_flat_sx cimp_flat_dx cimp_bind : ld.