- pts: we restored the former hierarchy

- nat: we added a missing lemma
- lambda_delta: subject reduction continues ...

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
index af3b3496b7c4a48415016f3833e424f5844715c8..e3dee1e0bac03c0764bf5854c1b1a9fdc3d25160 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma
@@ -41,6 +41,22 @@ lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
 @transitive_le [3: @IHL |2: /2 width=2/ | skip ]
 qed.
 
+lemma cw_tpair_sn: ∀I,L,V,T. #[L, V] < #[L, ②{I}V.T].
+#I #L #V #T normalize in ⊢ (? % %); //
+qed.
+
+lemma cw_tpair_dx: ∀I,L,V,T. #[L, T] < #[L, ②{I}V.T].
+#I #L #V #T normalize in ⊢ (? % %); //
+qed.
+
+lemma cw_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/
+qed.
+
+lemma cw_tpair_dx_sn_shift: ∀I1,I2,L,V1,V2,T. #[L.ⓑ{I2}V2, T] < #[L, ②{I1}V1.②{I2}V2.T].
+#I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
+qed.
+
 (* Basic_1: removed theorems 6:
             flt_thead_sx flt_thead_dx flt_arith0 flt_arith1 flt_arith2 flt_trans
 *)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma
index 00050032d0a9df6634fbc02d4c112d506d75ff4d..e567df2089e41a6a04319311d1c9d09f387cbc5c 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma
@@ -38,6 +38,6 @@ axiom tw_wf_ind: ∀R:predicate term.
 
 (* Basic_1: removed theorems 11:
             wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
-                 weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
+            weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
             removed local theorems 1: q_ind
 *)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index ce9a370e29af537dfad8993acb1ab9983a693a1a..9ec72083a6797ee46de0eb4806147bc16696e723 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -308,8 +308,16 @@ notation "hvbox( L ⊢ break term 90 T1 ⬌ break T2 )"
    non associative with precedence 45
    for @{ 'PConv $L $T1 $T2 }.
 
+notation "hvbox( T1 ⬌ break T2 )"
+   non associative with precedence 45
+   for @{ 'PConv $T1 $T2 }.
+
 (* Equivalence **************************************************************)
 
 notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )"
    non associative with precedence 45
    for @{ 'PConvStar $L $T1 $T2 }.
+
+notation "hvbox( T1 ⬌* break T2 )"
+   non associative with precedence 45
+   for @{ 'PConvStar $T1 $T2 }.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
new file mode 100644 (file)
index 0000000..b4f73c9
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ltpr_ldrop.ma".
+include "basic_2/static/aaa_ltps.ma".
+include "basic_2/static/lsuba_aaa.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+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
+#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_fw … HLK1 (#i)) #HKV1
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
+  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/
+| #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
+  elim (tpr_inv_abbr1 … H) -H *
+  [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
+    lapply (tps_lsubs_conf … HT02 (L2.ⓓV2) ?) -HT02 /2 width=1/ #HT02
+    lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
+    lapply (IH … HA … (L2.ⓓV2) … HT10) -IH -HA -HT10 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
+  | -B #T #HT1 #HTX
+    elim (lift_total X 0 1) #X1 #HX1
+    lapply (tpr_lift … HTX … HT1 … HX1) -T #HTX1
+    lapply (IH … HA … (L2.ⓓV1) … HTX1) /width=5/ -T1 /2 width=1/ -L1 #HA
+    @(aaa_inv_lift … HA … HX1) /2 width=1/
+  ]
+| #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct
+  elim (tpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+  lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB
+  lapply (IH … HA … (L2.ⓛV2) … HT12) -IH -HA -HT12 /width=5/ -T1 /2 width=1/
+| #L1 #V1 #T1 #B #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
+  elim (tpr_inv_appl1 … H) -H *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
+    lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ /2 width=3/
+  | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
+    elim (aaa_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
+    lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
+    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
+  | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
+    elim (aaa_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
+    lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
+    lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
+    lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
+    @(aaa_abbr … HW2) -HW2
+    @(aaa_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
+  ]
+| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
+  elim (tpr_inv_cast1 … H) -H
+  [ * #V2 #T2 #HV12 #HT12 #H destruct
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
+    lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
+  | -HV1 #HT1X
+     lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/
+  ]
+]
+qed.
+
+lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ➡ L2 →
+                         ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A.
+/2 width=9/ qed.
+
+lemma aaa_ltpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ➡ L2 → L2 ⊢ T ÷ A.
+/2 width=5/ qed.
+
+lemma aaa_tpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. T1 ➡ T2 → L ⊢ T2 ÷ A.
+/2 width=5/ qed.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma
index 2d62640ad6ec2321bf6e6da7149f2ed18a3b6456..b243338eed0a7b0fde39f49457c3b46411d11fcd 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma
@@ -45,3 +45,28 @@ lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 
   /3 width=4/
 ]
 qed.
+
+lemma aaa_inv_lift: ∀L2,T2,A. L2 ⊢ T2 ÷ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
+                    ∀T1. ⇧[d, e] T1 ≡ T2 → L1 ⊢ T1 ÷ A.
+#L2 #T2 #A #H elim H -L2 -T2 -A
+[ #L2 #k #L1 #d #e #_ #T1 #H
+  >(lift_inv_sort2 … H) -H //
+| #I #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #d #e #HL21 #T1 #H
+  elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+  [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/
+  | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/
+  ]
+| #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+  elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  /4 width=4/
+| #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+  elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  /4 width=4/
+| #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  /3 width=4/
+| #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  /3 width=4/
+]
+qed-.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
index 3dfc3563906caeb81ffd56ea44b0221bd07869b2..4550fde4b9aa92f01f0da5d187acca6ec3614a82 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_weight.ma".
+include "basic_2/grammar/cl_weight.ma".
 include "basic_2/grammar/lsubs.ma".
 include "basic_2/substitution/lift.ma".
 
@@ -187,6 +187,13 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
 ]
 qed-. 
 
+lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
+                          ∀T. #[K, V] < #[L, T].
+#I #L #K #V #d #e #H #T
+lapply (ldrop_fwd_lw … H) -H #H
+@(le_to_lt_to_lt … H) -H /3 width=1/
+qed-.
+
 lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e.
                                ⇩[0, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
 #L1 elim L1 -L1

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 44c3119fae1fad9be401452f9c4a667eb813a050..31d5ced7f7c64ac7dfa03ee8b6f96c65ad12a09b 100644 (file)
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -374,6 +374,9 @@ theorem lt_plus_to_minus_r: ∀a,b,c. a + b < c → a < c - b.
 #a #b #c #H @le_plus_to_minus_r //
 qed.
 
+lemma lt_plus_Sn_r: ∀a,x,n. a < a + x + (S n).
+/2 width=1/ qed.
+
 theorem lt_S_S_to_lt: ∀n,m:nat. S n < S m → n < m.
 (* demo *)
 /2/ qed-.
@@ -780,4 +783,3 @@ lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
 lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
 #i #n #m #leni #lemi normalize (cases (leb n m)) 
 normalize // qed.
-

diff --git a/matita/matita/lib/basics/pts.ma b/matita/matita/lib/basics/pts.ma
index 237c0c2b39df57203c487e401de78b77673d13ce..446305ecf4e76299535171930827f01bd704e37f 100644 (file)
--- a/matita/matita/lib/basics/pts.ma
+++ b/matita/matita/lib/basics/pts.ma
@@ -19,4 +19,3 @@ universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
 universe constraint Type[3] < Type[4].
 universe constraint Type[4] < Type[5].
-universe constraint Type[5] < Type[6].