(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require cnt_defs. Require sty0_props. Require sty1_defs. Section sty1_props. (*****************************************************) Hints Resolve sty1_sing : ld. Lemma sty1_lift: (g:?; e:?; t1,t2:?) (sty1 g e t1 t2) -> (c:?; h,d:?) (drop h d c e) -> (sty1 g c (lift h d t1) (lift h d t2)). Proof. Intros until 1; XElim H; Clear t2; Intros; XDEAuto 4. Qed. (* Note: existential theorem applied backward here *) Lemma sty1_correct: (g:?; c:?; t1, t:?) (sty1 g c t1 t) -> (EX t2 | (sty0 g c t t2)). Proof. Intros until 1; XElim H; Clear t; Intros; EApply sty0_correct; XDEAuto 2. Qed. Lemma sty1_abbr: (g:?; c,d:?; v:?; i:?) (getl i c (CHead d (Bind Abbr) v)) -> (w:?) (sty1 g d v w) -> (sty1 g c (TLRef i) (lift (S i) (0) w)). Proof. Intros until 2; XElim H0; Clear w; Intros; Try GetLDrop; XDEAuto 3. Qed. Lemma sty1_cast2: (g:?; c:?; t1,t2:?) (sty1 g c t1 t2) -> (v1,v2:?) (sty0 g c v1 v2) -> (EX v2 | (sty1 g c v1 v2) & (sty1 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v2 t2)) ). Proof. Intros until 1; XElim H; Clear t2; Intros. (* case 1: sty1_sty0 *) XDEAuto 5. (* case 1: sty1_sing *) XDecomPoseClear H0 '(H0 ? ? H2); Clear H2 H v2. XDecomPose '(sty1_correct ? ? ? ? H3). XDEAuto 5. Qed. Hints Resolve sty1_trans sty1_abbr sty1_lift : ld. Lemma sty1_cnt: (g:?; c:?; t1,t:?) (sty0 g c t1 t) -> (EX t2 | (sty1 g c t1 t2) & (cnt t2)). Proof. Intros until 1; XElim H; Clear c t1 t; Intros. (* case 1: sty0_sort *) XDEAuto 3. (* case 2: sty0_abbr *) XDecompose H1; XDEAuto 4. (* case 3: sty0_abst *) XDecompose H1; GetLDrop; XDEAuto 7. (* case 4: sty0_bind *) XDecompose H0; XDEAuto 4. (* case 5: sty0_appl *) XDecompose H0; XDEAuto 4. (* case 6: sty0_cast *) XDecompose H2; Clear H0 H1. XDecomPoseClear H '(sty1_cast2 ? ? ? ? H3 ? ? H); Clear H3. XDEAuto 3. Qed. End sty1_props. Hints Resolve sty1_abbr sty1_lift: ld.