- firs theorems on native type assignment

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / cprs_cprs.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
index 518c2bd07295a88765cbe26ed0a2785cfaf8971e..85b391d2dde8f8f2b58a5f216bd2465a99f47df4 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
@@ -21,8 +21,16 @@ include "basic_2/computation/cprs_lcpr.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma cprs_abbr_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 →
-                    L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+lemma cprs_abst_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2.
+                    L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2.
+#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HT12) -T2
+[ /3 width=2/
+| /3 width=6 by cprs_strap1, cpr_abst/ (**) (* /3 width=6/ is too slow *)
+]
+qed.
+
+lemma cprs_abbr1_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 →
+                     L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
 #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1
 [ /3 width=5/
 | #T1 #T #HT1 #_ #IHT1
@@ -30,8 +38,8 @@ lemma cprs_abbr_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 
 ]
 qed.
 
-lemma cpr_abbr: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 →
-                L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+lemma cpr_abbr1: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 →
+                 L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
 /3 width=1/ qed.
 
 lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 →
@@ -88,13 +96,40 @@ lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 
 @(cprs_trans … IHV1) -IHV1 /2 width=1/ 
 qed.
 
-lemma cprs_abbr: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 →
-                 L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2.
+                 L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2.
+#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HV12) -V2
+[ lapply (cprs_lsubs_conf … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
+| #V0 #V2 #_ #HV02 #IHV01
+  @(cprs_trans … IHV01) -V1 /2 width=2/
+]
+qed.
+
+lemma cprs_abbr1: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 →
+                  L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
 #L #V1 #T1 #T2 #HT12 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
 #V #V2 #_ #HV2 #IHV1
 @(cprs_trans … IHV1) -IHV1 /2 width=1/
 qed.
 
+lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 →
+                     L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+#L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1
+[ /2 width=1/
+| #T1 #T #HT1 #_ #IHT1
+  lapply (lcpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1
+  @(cprs_trans … IHT1) -IHT1 /2 width=1/
+]
+qed.
+
+lemma cprs_abbr2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 →
+                  L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+#L #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12
+lapply (IHV1 T1 T1 ?) -IHV1 // #HV1
+@(cprs_trans … HV1) -HV1 /2 width=1/
+qed.
+
 (* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
 lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
                        ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.