- basics: bug fix in Conf3, it was not generic enough

- lambda_delta: subject reduction of static typestarted ...

diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma
new file mode 100644 (file)
index 0000000..162fa38
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltps.ma
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ltps_ldrop.ma".
+include "basic_2/static/aaa_lift.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Properties about parallel substitution ***********************************)
+
+(* Note: lemma 500 *)
+lemma aaa_ltps_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶ L2 →
+                         ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A.
+#L1 #T1 #A #H elim H -L1 -T1 -A
+[ #L1 #k #L2 #d #e #_ #T2 #H
+  >(tps_inv_sort1 … H) -H //
+| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #L2 #d #e #HL12 #T2 #H
+  elim (tps_inv_lref1 … H) -H
+  [ #H destruct
+    elim (lt_or_ge i d) #Hdi
+    [ elim (ltps_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+      elim (ltps_inv_tps11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct
+      /3 width=8/
+    | elim (lt_or_ge i (d + e)) #Hide
+      [ elim (ltps_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+        elim (ltps_inv_tps21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct
+        /3 width=8/
+      | -Hdi
+        lapply (ltps_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide #HLK2
+        /3 width=8/
+      ]
+    ]
+  | * #K2 #V2 #Hdi #Hide #HLK2 #HVT2
+    elim (ltps_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+    elim (ltps_inv_tps21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct
+    lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct
+    lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /3 width=7/
+  ]
+| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
+  elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/
+| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
+  elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/
+| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
+  elim (tps_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
+| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
+  elim (tps_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
+]
+qed.
+
+lemma aaa_ltps_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2,d,e. L1 [d, e] ▶ L2 → L2 ⊢ T ÷ A.
+/2 width=7/ qed.
+
+lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ÷ A.
+/2 width=7/ qed.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma
new file mode 100644 (file)
index 0000000..171dd6b
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ltpss.ma".
+include "basic_2/static/aaa_ltps.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Properties about parallel unfold *****************************************)
+
+lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ÷ A.
+#L1 #T #A #HT #L2 #d #e #HL12
+@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=5/
+qed.
+
+lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ÷ A.
+#L #T1 #A #HT1 #T2 #d #e #HT12
+@(TC_Conf3 … HT1 ? HT12) /2 width=5/
+qed.
+
+lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
+                           ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A.
+/3 width=5/ qed.

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index a82f314f698e9dc23fb479c56848c83b586d2654..ff190e5e3c2d2fb1ef7b952638e85e5f4f011f6e 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -11,7 +11,7 @@
 
 include "basics/logic.ma".
 
-(********** preducates *********)
+(********** predicates *********)
 
 definition predicate: Type[0] → Type[0]
 ≝ λA.A→Prop.
@@ -20,6 +20,9 @@ definition predicate: Type[0] → Type[0]
 definition relation : Type[0] → Type[0]
 ≝ λA.A→A→Prop. 
 
+definition relation2 : Type[0] → Type[0] → Type[0]
+≝ λA,B.A→B→Prop.
+
 definition reflexive: ∀A.∀R :relation A.Prop
 ≝ λA.λR.∀x:A.R x x.
 

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index bff1aaeef80042a2ae2e838317d0c5ed5c858a58..8fd32c2e1f3092ade0b5a40208b3afb2641c2f54 100644 (file)
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -192,9 +192,9 @@ lemma TC_star_ind_dx: ∀A,R. reflexive A R →
 @(TC_star_ind_dx_aux … HR … Ha2 H … Ha12) //
 qed-.
 
-definition Conf3: ∀A. relation A → relation A → Prop ≝ λA,S,R.
-                  ∀a,a1. S a1 a → ∀a2. R a1 a2 → S a2 a.
+definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
+                  ∀b,a1. S a1 b → ∀a2. R a1 a2 → S a2 b.
 
-lemma TC_Conf3: ∀A,S,R. Conf3 A S R → Conf3 A S (TC … R).
-#A #S #R #HSR #a #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/
+lemma TC_Conf3: ∀A,B,S,R. Conf3 A B S R → Conf3 A B S (TC … R).
+#A #B #S #R #HSR #b #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/
 qed.