# xoa ########################################################################
-xoa: $(TARGETS)
+xoa: $(XOA_TARGETS)
$(XOA_TARGETS): $(XOA_CONF)
@echo " EXEC $(XOA) $(XOA_CONF)"
@printf ' ]\n' >> $$@
@printf ' class "cyan" [ "sizes"\n' >> $$@
@printf ' [ "files" "$$(V1)" ]\n' >> $$@
- @printf ' [ "bytes" "$$(V2)" ]\n' >> $$@
+ @printf ' [ "characters" "$$(V2)" ]\n' >> $$@
@printf ' [ * ]\n' >> $$@
@printf ' ]\n' >> $$@
@printf ' class "green" [ "propositions"\n' >> $$@
(* *)
(**************************************************************************)
+include "basic_2/static/lsubss.ma".
include "basic_2/reducibility/xpr.ma".
(*
include "basic_2/reducibility/cnf.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/reducibility/xpr_lsubss.ma".
+include "basic_2/computation/xprs.ma".
+
+(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************)
+
+(* Properties on lenv ref for stratified type assignment ********************)
+
+lemma lsubss_xprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡*[g] T2.
+#h #g #L1 #L2 #HL12 #T1 #T2 #H @(xprs_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT1
+lapply (lsubss_xpr_trans … HL12 … HT2) -L2 /2 width=3/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/static/ssta.ma".
include "basic_2/dynamic/snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
| #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} < #{L ,T} → ⦃h, L0⦄ ⊩ U0 :[g]
) →
∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] →
- ∀U0,l. ⦃h, L⦄ ⊢ T0 •[g, l + 1] U0 →
+ ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 →
L0 = L → T0 = T → ⦃h, L0⦄ ⊩ U0 :[g].
-#h #g #L #T #IH2 #IH1 #L0 #T0 * -L0 -T0
+#h #g #L #T #IH1 #L0 #T0 * -L0 -T0
[
|
|
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
-*)
+| #L0 #W #T0 #W0 #l0 #_ #HT0 #_ #_ #U0 #l #H #H1 #H2 destruct -W0
+ lapply (ssta_inv_cast1 … H) -H #HTU0
+ lapply (IH1 … HT0 U0 ? ?) -IH1 -HT0 // -W /3 width=2/
qed.
lemma fw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}.
-#I #L #V #T normalize in ⊢ (? % %); //
+normalize in ⊢ (?→?→?→?→?%%); //
qed.
lemma fw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}.
-#I #L #V #T normalize in ⊢ (? % %); //
+normalize in ⊢ (?→?→?→?→?%%); //
qed.
lemma fw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}.
-#I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
+normalize in ⊢ (?→?→?→?→?→?→?%%); /2 width=1/
qed.
-lemma fw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T.
- #{L.ⓑ{I2}V2, T} < #{L, ②{I1}V1.ⓑ{a2,I2}V2.T}.
-#a2 #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
+lemma fw_tpair_sn_sn_shift: ∀I,I1,I2,L,V1,V2,T.
+ #{L.ⓑ{I}V1, T} < #{L, ②{I1}V1.②{I2}V2.T}.
+normalize in ⊢ (?→?→?→?→?→?→?→?%%); /3 width=1/
+qed.
+
+lemma fw_tpair_sn_dx_shift: ∀I,I1,I2,L,V1,V2,T.
+ #{L.ⓑ{I}V2, T} < #{L, ②{I1}V1.②{I2}V2.T}.
+normalize in ⊢ (?→?→?→?→?→?→?→?%%); /2 width=1/
qed.
(* Basic_1: removed theorems 6:
non associative with precedence 45
for @{ 'StaticType $h $g $l $L $T1 $T2 }.
-notation "hvbox( h ⊢ break term 46 L1 • ≃ [ g ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'CCongS $h $g $L1 $L2 }.
-
notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )"
non associative with precedence 45
for @{ 'CrSubEqS $h $g $L1 $L2 }.
non associative with precedence 45
for @{ 'NativeValid $h $g $L $T }.
+notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqV $h $g $L1 $L2 }.
+
notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
non associative with precedence 45
for @{ 'NativeType $h $L $T1 $T2 }.
--- /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/lsubss_ssta.ma".
+include "basic_2/reducibility/xpr.ma".
+
+(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
+
+(* Properties on lenv ref for stratified type assignment ********************)
+
+lemma lsubss_xpr_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡[g] T2.
+#h #g #L1 #L2 #HL12 #T1 #T2 * [ | #l ] #HT12
+[ lapply (lsubss_fwd_lsubs2 … HL12) -HL12 /3 width=3/
+| /3 width=4/
+]
+qed-.
(* sort degree specification *)
record sd (h:sh): Type[0] ≝ {
- deg : relation nat; (* degree of the sort *)
- deg_total: ∀k. ∃l. deg k l; (* functional relation axioms *)
+ deg : relation nat; (* degree of the sort *)
+ deg_total: ∀k. ∃l. deg k l; (* functional relation axioms *)
deg_mono : ∀k,l1,l2. deg k l1 → deg k l2 → l1 = l2;
- deg_next : ∀k,l. deg k l → deg (next h k) (l - 1); (* compatibility condition *)
- deg_prev : ∀k,l. deg (next h k) (l + 1) → deg k (l + 2)
+ deg_next : ∀k,l. deg k l → deg (next h k) (l - 1) (* compatibility condition *)
}.
(* Notable specifications ***************************************************)
| #H1 @deg_SO_zero * #l #H2 destruct
@H1 -H1 @(ex_intro … (S l)) /2 width=1/ (**) (* explicit constructor *)
]
-| #K0 #l0 #H
- <(deg_SO_inv_pos … H) -H >plus_n_2
- @deg_SO_pos >iter_SO /2 width=1/ (**) (* explicit constructor: iter_SO is needed *)
]
qed.
(* Basic properties *********************************************************)
+lemma deg_pred: ∀h,g,k,l. deg h g (next h k) (l + 1) → deg h g k (l + 2).
+#h #g #k #l #H1
+elim (deg_total h g k) #l0 #H0
+lapply (deg_next … H0) #H2
+lapply (deg_mono … H1 H2) -H1 -H2 #H
+<(associative_plus l 1 1) >H <plus_minus_m_m // /2 width=3 by transitive_le/
+qed.
+
lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
#h #k #l <plus_n_Sm <plus_n_Sm //
qed.
(* *)
(**************************************************************************)
-include "basic_2/substitution/frsup.ma".
include "basic_2/unfold/frsupp.ma".
(* STAR-ITERATED RESTRICTED SUPCLOSURE **************************************)
lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
| -Hd21 normalize in Hde12;
lapply (lt_to_le_to_lt 0 … Hde12) // #He2
- lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/
+ lapply (le_plus_to_minus_r … Hde12) -Hde12
+ /3 width=5 by ltpss_dx_tpss2_lt, tpss_weak/ (**) (* /3 width=5/ used to work *)
]
]
qed.
<key name="ex">6 4</key>
<key name="ex">6 6</key>
<key name="ex">6 7</key>
+ <key name="ex">7 4</key>
<key name="ex">7 7</key>
<key name="or">3</key>
<key name="or">4</key>
interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
+(* multiple existental quantifier (7, 4) *)
+
+inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
(* multiple existental quantifier (7, 7) *)
inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }.
+(* multiple existental quantifier (7, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }.
+
(* multiple existental quantifier (7, 7) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
projects / helm.git / commitdiff