+ advances on nv ...
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/cpms_aaa.ma".
+include "basic_2/dynamic/nv.ma".
+
+(* NATIVE VALIDITY FOR TERMS ************************************************)
+
+(* Forward lemmas on atomic arity assignment for terms **********************)
+
+(* Basic_2A1: uses: snv_fwd_aaa *)
+lemma nv_fwd_aaa (a) (h): ∀G,L,T. ⦃G, L⦄ ⊢ T ![a, h] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A.
+#a #h #G #L #T #H elim H -G -L -T
+[ /2 width=2 by aaa_sort, ex_intro/
+| #I #G #L #V #_ * /3 width=2 by aaa_zero, ex_intro/
+| #I #G #L #K #_ * /3 width=2 by aaa_lref, ex_intro/
+| #p * #G #L #V #T #_ #_ * #B #HV * #A #HA
+ /3 width=2 by aaa_abbr, aaa_abst, ex_intro/
+| #n #p #G #L #V #W #T0 #U0 #_ #_ #_ #HVW #HTU0 * #B #HV * #X #HT
+ lapply (cpms_aaa_conf … HV … HVW) -HVW #H1W
+ lapply (cpms_aaa_conf … HT … HTU0) -HTU0 #H
+ elim (aaa_inv_abst … H) -H #B0 #A #H2W #HU #H destruct
+ lapply (aaa_mono … H2W … H1W) -W #H destruct
+ /3 width=4 by aaa_appl, ex_intro/
+| #G #L #U #T #U0 #_ #_ #HU0 #HTU0 * #B #HU * #A #HT
+ lapply (cpms_aaa_conf … HU … HU0) -HU0 #HU0
+ lapply (cpms_aaa_conf … HT … HTU0) -HTU0 #H
+ lapply (aaa_mono … H … HU0) -U0 #H destruct
+ /3 width=3 by aaa_cast, ex_intro/
+]
+qed-.
-(* Properties on subclosure *************************************************)
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
-lemma snv_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+include "basic_2/s_computation/fqus_fqup.ma".
+include "basic_2/dynamic/nv_drops.ma".
+
+(* NATIVE VALIDITY FOR TERMS ************************************************)
+
+(* Properties with supclosure ***********************************************)
+
+(* Basic_2A1: uses: snv_fqu_conf *)
+lemma nv_fqu_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h].
+#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
[ #I1 #G1 #L1 #V1 #H
- elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
- lapply (drop_inv_O2 … H) -H #H destruct //
-|2: *
-|5,6: /3 width=8 by snv_inv_lift/
-]
-[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
-|2,4: * #G1 #L1 #V1 #T1 #H
- [1,3: elim (snv_inv_appl … H) -H //
- |2,4: elim (snv_inv_cast … H) -H //
+ elim (nv_inv_zero … H) -H #I2 #L2 #V2 #HV2 #H destruct //
+| * [ #p #I1 | * ] #G1 #L1 #V1 #T1 #H
+ [ elim (nv_inv_bind … H) -H //
+ | elim (nv_inv_appl … H) -H //
+ | elim (nv_inv_cast … H) -H //
+ ]
+| #p #I1 #G1 #L1 #V1 #T1 #H
+ elim (nv_inv_bind … H) -H //
+| #p #I1 #G1 #L1 #V1 #T1 #H destruct
+| * #G1 #L1 #V1 #T1 #H
+ [ elim (nv_inv_appl … H) -H //
+ | elim (nv_inv_cast … H) -H //
]
+| #I1 #G1 #L1 #T1 #U1 #HTU1 #HU
+ /4 width=7 by nv_inv_lifts, drops_refl, drops_drop/
]
qed-.
-lemma snv_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_inv_gen … H) -H [|*]
-/2 width=5 by snv_fqu_conf/
+(* Basic_2A1: uses: snv_fquq_conf *)
+lemma nv_fquq_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h].
+#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [|*]
+/2 width=5 by nv_fqu_conf/
qed-.
-lemma snv_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
- ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-/3 width=5 by fqup_strap1, snv_fqu_conf/
+(* Basic_2A1: uses: snv_fqup_conf *)
+lemma nv_fqup_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h].
+#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+/3 width=5 by fqup_strap1, nv_fqu_conf/
qed-.
-lemma snv_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
- ⦃G1, L1⦄ ⊢ T1 ¡[h, o] → ⦃G2, L2⦄ ⊢ T2 ¡[h, o].
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_gen … H) -H [|*]
-/2 width=5 by snv_fqup_conf/
+(* Basic_2A1: uses: snv_fqus_conf *)
+lemma nv_fqus_conf (a) (h): ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ⦃G1, L1⦄ ⊢ T1 ![a, h] → ⦃G2, L2⦄ ⊢ T2 ![a, h].
+#a #h #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_fqup … H) -H [|*]
+/2 width=5 by nv_fqup_conf/
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/fsb_aaa.ma".
+include "basic_2/dynamic/nv_aaa.ma".
+
+(* NATIVE VALIDITY FOR TERMS ************************************************)
+
+(* Forward lemmas with strongly rst-normalizing closures ********************)
+
+(* Basic_2A1: uses: snv_fwd_fsb *)
+lemma nv_fwd_fsb (a) (h) (o): ∀G,L,T. ⦃G, L⦄ ⊢ T ![a, h] → ≥[h, o] 𝐒⦃G, L, T⦄.
+#a #h #o #G #L #T #H elim (nv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/
+qed-.
-nv.ma nv_drops.ma
+nv.ma nv_drops.ma nv_fqus.ma nv_aaa.ma nv_fsb.ma
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/static/da_aaa.ma".
-include "basic_2/computation/scpds_aaa.ma".
-include "basic_2/dynamic/snv.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* Forward lemmas on atomic arity assignment for terms **********************)
-
-lemma snv_fwd_aaa: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A.
-#h #o #G #L #T #H elim H -G -L -T
-[ /2 width=2 by aaa_sort, ex_intro/
-| #I #G #L #K #V #i #HLK #_ * /3 width=6 by aaa_lref, ex_intro/
-| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2 by aaa_abbr, aaa_abst, ex_intro/
-| #a #G #L #V #W0 #T #U0 #d #_ #_ #HVW0 #HTU0 * #B #HV * #X #HT
- lapply (scpds_aaa_conf … HV … HVW0) -HVW0 #HW0
- lapply (scpds_aaa_conf … HT … HTU0) -HTU0 #H
- elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
- lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4 by aaa_appl, ex_intro/
-| #G #L #U #T #U0 #_ #_ #HU0 #HTU0 * #B #HU * #A #HT
- lapply (scpds_aaa_conf … HU … HU0) -HU0 #HU0
- lapply (scpds_aaa_conf … HT … HTU0) -HTU0 #H
- lapply (aaa_mono … H … HU0) -U0 #H destruct /3 width=3 by aaa_cast, ex_intro/
-]
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma snv_fwd_da: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ∃d. ⦃G, L⦄ ⊢ T ▪[h, o] d.
-#h #o #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_da/
-qed-.
-
-lemma snv_fwd_lstas: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] →
- ∀d. ∃U. ⦃G, L⦄ ⊢ T •*[h, d] U.
-#h #o #G #L #T #H #d elim (snv_fwd_aaa … H) -H
-#A #HT elim (aaa_lstas h … HT d) -HT /2 width=2 by ex_intro/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/fsb_aaa.ma".
-include "basic_2/dynamic/snv_aaa.ma".
-
-(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
-
-(* forward lemmas on "qrst" strongly normalizing closures *********************)
-
-lemma snv_fwd_fsb: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, o] → ⦥[h, o] ⦃G, L, T⦄.
-#h #o #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/
-qed-.
(*
[ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
*)
- [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" (* + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" *) * ]
+ [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" "nv_fqus" + "nv_aaa" + "snv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ]
}
]
}
projects / helm.git / commitdiff