The static type of <W>.T is now the static type of T.
This allows to prove that each valid term has a static type as
expected!
+++ /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/reducibility/ypr.ma".
-
-(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
-
-definition yprs: ∀h. sd h → bi_relation lenv term ≝
- λh,g. bi_TC … (ypr h g).
-
-interpretation "hyper parallel computation (closure)"
- 'YPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 →
- (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → R L T → R L2 T2) →
- ∀L2,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L2 T2.
-/3 width=7 by bi_TC_star_ind/ qed-.
-
-lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 →
- (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → R L T → R L1 T1) →
- ∀L1,T1. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L1 T1.
-/3 width=7 by bi_TC_star_ind_dx/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g).
-/2 width=1/ qed.
-
-lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ →
- h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ →
- h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
-/2 width=4/ 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/unfold/csups.ma".
-include "basic_2/computation/yprs.ma".
-
-(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
-
-(* Properties on iterated supclosure ****************************************)
-
-lemma csups_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ →
- h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 /3 width=1/ /3 width=4/
-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/xprs_cprs.ma".
-include "basic_2/computation/yprs.ma".
-
-(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************)
-
-(* Properties on extended parallel computation for terms ********************)
-
-lemma xprs_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 →
- h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(xprs_ind … H) -T2 // /3 width=4/
-qed.
-
-lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄.
-/3 width=1/ 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/yprs.ma".
-
-(* HYPER PARALLEL COMPUTATION ON TERMS **************************************)
-
-theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g).
-/2 width=4/ 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/substitution/csup.ma".
-include "basic_2/computation/yprs.ma".
-
-(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************)
-
-inductive ysteps (h) (g) (L1) (T1) (L2) (T2): Prop ≝
-| ysteps_intro: h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → (L1 = L2 → T1 = T2 → ⊥) →
- ysteps h g L1 T1 L2 T2
-.
-
-interpretation "iterated step of hyper parallel computation (closure)"
- 'YPRedStepStar h g L1 T1 L2 T2 = (ysteps h g L1 T1 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma ssta_ysteps: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U →
- h ⊢ ⦃L, T⦄ •⭃*[g] ⦃L, U⦄.
-#h #g #L #T #U #l #HTU
-@ysteps_intro /3 width=2/ #_ #H destruct
-elim (ssta_inv_refl … HTU)
-qed.
-
-lemma csup_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ →
- h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 #H
-lapply (csup_fwd_cw … H) #H1
-@ysteps_intro /3 width=1/ -H #H2 #H3 destruct
-elim (lt_refl_false … H1)
-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/yprs_csups.ma".
-include "basic_2/computation/ysteps.ma".
-
-(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************)
-
-(* Properties on iterated supclosure ****************************************)
-
-lemma csups_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ →
- h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 #H
-lapply (csups_fwd_cw … H) #H1
-@ysteps_intro /2 width=1/ -H #H2 #H3 destruct
-elim (lt_refl_false … H1)
-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/static/ssta.ma".
+include "basic_2/dynamic/snv.ma".
+
+(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
+
+(* Properties on stratified static type assignment for terms ****************)
+
+lemma snv_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃U,l. ⦃h, L⦄ ⊢ T •[g, l] U.
+#h #g #L #T #H elim H -L -T
+[ #L #k elim (deg_total h g k) /3 width=3/
+| * #L #K #V #i #HLK #_ * #W #l0 #HVW
+ [ elim (lift_total W 0 (i+1)) /3 width=8/
+ | elim (lift_total V 0 (i+1)) /3 width=8/
+ ]
+| #a #I #L #V #T #_ #_ #_ * /3 width=3/
+| #a #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/
+| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *)
+]
+qed-.
+(*
+fact snv_ssta_conf_aux: ∀h,g,L,T. (
+ ∀L0,T1,U1,l1. ⦃h, L0⦄ ⊢ T1 •[g, l1] U1 →
+ ∀T2,U2,l2. ⦃h, L0⦄ ⊢ T2 •[g, l2] U2 →
+ L0 ⊢ T1 ⬌* T2 → ⦃h, L0⦄ ⊩ T1 :[g] → ⦃h, L0⦄ ⊩ T2 :[g] →
+ #{L0, T1} < #{L ,T} →
+ l1 = l2 ∧ L0 ⊢ U1 ⬌* U2
+ ) → (
+ ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
+ ∀U0. ⦃h, L0⦄ ⊢ T0 •➡*[g] U0 →
+ #{L0, T0} < #{L ,T} →
+ ⦃h, L0⦄ ⊩ U0 :[g]
+ ) →
+ ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
+ ∀U0,l. ⦃h, L⦄ ⊢ T0 •[g, l + 1] U0 →
+ L0 = L → T0 = T → ⦃h, L0⦄ ⊩ U0 :[g].
+#h #g #L #T #IH2 #IH1 #L0 #T0 * -L0 -T0
+[
+|
+|
+| #a #L0 #V #W #W0 #T0 #V0 #l0 #HV #HT0 #HVW #HW0 #HTV0 #X #l #H #H1 #H2 destruct
+ elim (ssta_inv_appl1 … H) -H #U0 #HTU0 #H destruct
+ lapply (IH1 … HT0 U0 ? ?) // [ /3 width=2/ ] -HTU0 #HU0
+ @(snv_appl … HV HU0 HVW HW0) -HV -HU0 -HVW -HW0
+| #L0 #W #T0 #W0 #l0 #HW #HT0 #HTW0 #HW0 #X #l #H #H1 #H2 destruct
+ elim (ssta_inv_cast1 … H) -H <minus_plus_m_m #V #U0 #HWV #HTU0 #H destruct
+ elim (ssta_mono … HTU0 … HTW0) -HTU0 #H1 #H2
+ lapply (injective_plus_l … H1) -H1 #H1 destruct
+(* elim (ssta_fwd_correct … HTW0) <minus_plus_m_m #X0 #HWX0 *)
+ lapply (IH1 … HT0 W0 ? ?) -IH1 -HT0 // [ /3 width=2/ ] -HTW0 #HW0
+ @(snv_cast … HV HW0)
+
+ HVW HW0) -HV -HU0 -HVW -HW0
+*)
fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T1 →
∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A.
-#L #T @(cw_wf_ind … L T) -L -T #L #T #IH
+#L #T @(fw_ind … L T) -L -T #L #T #IH
#L1 #T1 #A * -L1 -T1 -A
[ -IH #L1 #k #H1 #H2 #L2 #_ #T2 #H destruct
>(tpr_inv_atom1 … H) -H //
| #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct
>(tpr_inv_atom1 … H) -T2
- lapply (ldrop_pair2_fwd_cw … HLK1 (#i)) #HKV1
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/
(* Basic_1: was: pr0_confluence *)
theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 →
∃∃T. T1 ➡ T & T2 ➡ T.
-#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/
+#T @(tw_ind … T) -T /3 width=6 by tpr_conf_aux/
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/substitution/csup.ma".
-include "basic_2/reducibility/xpr.ma".
-
-(* HYPER PARALLEL REDUCTION ON CLOSURES *************************************)
-
-inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
-| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2
-| ypr_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2
-| ypr_csup: ∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2
-.
-
-interpretation
- "hyper parallel reduction (closure)"
- 'YPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g).
-/2 width=1/ qed.
-
-lemma xpr_ypr: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡[g] T2 → h ⊢ ⦃L, T1⦄ •⥸[g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 * /2 width=1/ /2 width=2/
-qed.
projects / helm.git / commitdiff