(****************************************************************************) (* *) (* The formal system \lambda\delta *) (* *) (* Author: Ferruccio Guidi *) (* *) (* This file is distributed under the terms of the *) (* GNU General Public License Version 2 *) (* *) (****************************************************************************) Require lift_props. Require subst0_defs. Section dnf_dec. (********************************************************) Lemma dnf_dec2: (t:?; d:?) ((w:?) (EX v | (subst0 d w t (lift (1) d v)))) \/ (EX v | t = (lift (1) d v)). Proof. XElim t; Intros. (* case 1: TSort *) Right; EApply ex_intro; Rewrite lift_sort; XAuto. (* case 2: TLRef n *) Apply (lt_eq_gt_e n d); Intros; Subst. (* case 2.1: n < d *) Right; EApply ex_intro; Rewrite lift_lref_lt; XAuto. (* case 2.2: n = d *) Left; Intros; EApply ex_intro; Rewrite lift_free; Simpl; XAuto. (* case 2.3: n > d *) Right; EApply ex_intro; Rewrite lift_lref_gt; XAuto. (* case 3: THead k *) XDecomPoseClear H '(H d); XDecomPoseClear H0 '(H0 (s k d)); Subst. (* case 3.1: subst0_both *) Left; Intros; XDecomPoseClear H '(H w); XDecomPoseClear H1 '(H1 w). EApply ex_intro; Rewrite lift_head; XDEAuto 3. (* case 3.2: subst0_snd *) Left; Intros; XDecomPoseClear H1 '(H1 w). EApply ex_intro; Rewrite lift_head; XDEAuto 3. (* case 3.3: subst0_fst *) Left; Intros; XDecomPoseClear H '(H w). EApply ex_intro; Rewrite lift_head; XDEAuto 3. (* case 3.4: lift *) Right; EApply ex_intro; Rewrite lift_head; XDEAuto 3. Qed. Lemma dnf_dec: (w,t:?; d:?) (EX v | (subst0 d w t (lift (1) d v)) \/ t = (lift (1) d v) ). Proof. Intros. XDecomPose '(dnf_dec2 t d); Subst; [ Idtac | XDEAuto 3 ]. XDecomPoseClear H '(H w); XDEAuto 3. Qed. End dnf_dec.