(****************************************************************************) (* *) (* 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 subst0_defs. Inductive subst1 [i:nat; v:T; t1:T] : T -> Prop := | subst1_refl : (subst1 i v t1 t1) | subst1_single : (t2:?) (subst0 i v t1 t2) -> (subst1 i v t1 t2). Hint subst1 : ld := Constructors subst1. Section subst1_props. (***************************************************) Theorem subst1_head: (v,u1,u2:?; i:?) (subst1 i v u1 u2) -> (k:?; t1,t2:?) (subst1 (s k i) v t1 t2) -> (subst1 i v (THead k u1 t1) (THead k u2 t2)). Proof. Intros until 1; XElim H; Clear u2. (* case 1: csubst1_refl *) Intros until 1; XElim H; Clear t2; XAuto. (* case 2: csubst1_single *) Intros until 2; XElim H0; Clear t3; XAuto. Qed. End subst1_props. Hints Resolve subst1_head : ld. Section subst1_gen_base. (************************************************) Lemma subst1_gen_sort: (v,x:?; i,n:?) (subst1 i v (TSort n) x) -> x = (TSort n). Proof. Intros; XElim H; Clear x; Intros; Try Subst0GenBase; XAuto. Qed. Lemma subst1_gen_lref: (v,x:?; i,n:?) (subst1 i v (TLRef n) x) -> x = (TLRef n) \/ n = i /\ x = (lift (S n) (0) v). Proof. Intros; XElim H; Clear x; Intros; Try Subst0GenBase; XAuto. Qed. Lemma subst1_gen_head: (k:?; v,u1,t1,x:?; i:?) (subst1 i v (THead k u1 t1) x) -> (EX u2 t2 | x = (THead k u2 t2) & (subst1 i v u1 u2) & (subst1 (s k i) v t1 t2) ). Proof. Intros; XElim H; Clear x; Intros; Try Subst0GenBase; XDEAuto 4. Qed. End subst1_gen_base. Tactic Definition Subst1GenBase := ( Match Context With | [ H: (subst1 ? ? (TSort ?) ?) |- ? ] -> XPoseClear H '(subst1_gen_sort ? ? ? ? H); Subst | [ H: (subst1 ? ? (TLRef ?) ?) |- ? ] -> XDecomPoseClear H '(subst1_gen_lref ? ? ? ? H); Subst | [ H: (subst1 ? ? (THead ? ? ?) ?) |- ? ] -> XDecomPoseClear H '(subst1_gen_head ? ? ? ? ? ? H); Subst ).