(****************************************************************************) (* *) (* 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 getl_defs. Inductive csubv: C -> C -> Prop := | csubv_sort: (n:?) (csubv (CSort n) (CSort n)) | csubv_void: (c1,c2:?) (csubv c1 c2) -> (v1,v2:?) (csubv (CHead c1 (Bind Void) v1) (CHead c2 (Bind Void) v2) ) | csubv_bind: (c1,c2:?) (csubv c1 c2) -> (b1:?) ~b1=Void -> (b2:?; v1,v2:?) (csubv (CHead c1 (Bind b1) v1) (CHead c2 (Bind b2) v2)) | csubv_flat: (c1,c2:?) (csubv c1 c2) -> (f1,f2:?; v1,v2:?) (csubv (CHead c1 (Flat f1) v1) (CHead c2 (Flat f2) v2)). Hint csubv : ld := Constructors csubv. Section csubv_props_base. (***********************************************) Lemma csubv_bind_same: (c1,c2:?) (csubv c1 c2) -> (b:?; v1,v2:?) (csubv (CHead c1 (Bind b) v1) (CHead c2 (Bind b) v2) ). Proof. XElim b; XAuto. Qed. Hints Resolve csubv_bind_same : ld. Lemma csubv_refl: (c:?) (csubv c c). Proof. XElim c; Try XElim k; XAuto. Qed. End csubv_props_base. Hints Resolve csubv_bind_same csubv_refl : ld. Section csubv_drop_base. (************************************************) Lemma csubv_drop_conf: (c1,c2:?) (csubv c1 c2) -> (e1:?; h:?) (drop h (0) c1 e1) -> (EX e2 | (csubv e1 e2) & (drop h (0) c2 e2)). Proof. Intros until 1; XElim H; Clear c1 c2; Intros. (* case 1: csubv_sort *) DropGenBase; Subst; XInv; XDEAuto 2. (* case 2: csubv_void *) NewInduction h; DropGenBase. (* case 2.1: h = 0 *) Subst; XDEAuto 3. (* case 2.2: h > 0 *) Clear IHh; XDecomPoseClear H0 '(H0 ? ? H1); Clear H1; XDEAuto 3. (* case 3: csubv_bind *) NewInduction h; DropGenBase. (* case 3.1: h = 0 *) Subst; XDEAuto 3. (* case 3.2: h > 0 *) Clear IHh; XDecomPoseClear H0 '(H0 ? ? H2); Clear H2; XDEAuto 3. (* case 4: csubv_void *) NewInduction h; DropGenBase. (* case 4.1: h = 0 *) Subst; XDEAuto 3. (* case 2.2: h > 0 *) Clear IHh; XDecomPoseClear H0 '(H0 ? ? H1); Clear H1; XDEAuto 3. Qed. End csubv_drop_base. Section csubv_clear_base. (***********************************************) Lemma csubv_clear_conf: (c1,c2:?) (csubv c1 c2) -> (b1:?; d1:?; v1:?) (clear c1 (CHead d1 (Bind b1) v1)) -> (EX b2 d2 v2 | (csubv d1 d2) & (clear c2 (CHead d2 (Bind b2) v2)) ). Proof. Intros until 1; XElim H; Clear c1 c2; Intros; ClearGenBase; XInv; Subst; [ XDEAuto 2 | XDEAuto 2 | Idtac ]. (* case 4: csubv_flat *) XDecomPose '(H0 ? ? ? H1); Clear H0 H1; XDEAuto 3. Qed. Lemma csubv_clear_conf_void: (c1,c2:?) (csubv c1 c2) -> (d1:?; v1:?) (clear c1 (CHead d1 (Bind Void) v1)) -> (EX d2 v2 | (csubv d1 d2) & (clear c2 (CHead d2 (Bind Void) v2)) ). Proof. Intros until 1; XElim H; Clear c1 c2; Intros; ClearGenBase; XInv; Subst; [ XDEAuto 2 | EqFalse | Idtac ]. (* case 4: csubv_flat *) XDecomPose '(H0 ? ? H1); Clear H0 H1; XDEAuto 3. Qed. End csubv_clear_base. Section csubv_getl_base. (************************************************) Lemma csubv_getl_conf: (c1,c2:?) (csubv c1 c2) -> (b1:?; d1:?; v1:?; i:?) (getl i c1 (CHead d1 (Bind b1) v1)) -> (EX b2 d2 v2 | (csubv d1 d2) & (getl i c2 (CHead d2 (Bind b2) v2)) ). Proof. Intros; GetLGenBase. XDecomPose '(csubv_drop_conf ? ? H ? ? H1); Clear H H1. XDecomPose '(csubv_clear_conf ? ? H0 ? ? ? H2); Clear H0 H2. XDEAuto 3. Qed. Lemma csubv_getl_conf_void: (c1,c2:?) (csubv c1 c2) -> (d1:?; v1:?; i:?) (getl i c1 (CHead d1 (Bind Void) v1)) -> (EX d2 v2 | (csubv d1 d2) & (getl i c2 (CHead d2 (Bind Void) v2)) ). Proof. Intros; GetLGenBase. XDecomPose '(csubv_drop_conf ? ? H ? ? H1); Clear H H1. XDecomPose '(csubv_clear_conf_void ? ? H0 ? ? H2); Clear H0 H2. XDEAuto 3. Qed. End csubv_getl_base. Tactic Definition CSubVGetL := ( Match Context With | [ H0: (csubv ?0 ?); H1: (getl ? ?0 (CHead ? (Bind Void) ?)) |- ? ] -> XDecomPose '(csubv_getl_conf_void ? ? H0 ? ? ? H1); Clear H0 | [ H0: (csubv ?0 ?); H1: (getl ? ?0 (CHead ? (Bind ?) ?)) |- ? ] -> XDecomPose '(csubv_getl_conf ? ? H0 ? ? ? ? H1); Clear H0 ).