lift_weight: bug fix

[helm.git] / matita / matita / lib / lambda-delta / reduction / tpr_tpr.ma

diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
index 4451ec892373030d917b7a11d4098653885409a8..da8a5507184680fbf2b2e48d1026ee8526dc1a27 100644 (file)
--- a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
@@ -33,8 +33,7 @@ lemma tpr_conf_bind_bind:
    ∃∃T0. 𝕓{I1} V12. T12 ⇒ T0 & 𝕓{I1} V22. T22 ⇒ T0.
 #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
 elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
-elim (IH … HT1 … HT2) -HT1 HT2 // #T #HT1 #HT2
-/3 width=5/
+elim (IH … HT1 … HT2) -HT1 HT2 IH /3 width=5/
 qed.
 
 lemma tpr_conf_bind_zeta:
@@ -62,12 +61,62 @@ lemma tpr_conf_flat_flat:
    ∃∃T0. 𝕗{I1} V12. T12 ⇒ T0 & 𝕗{I1} V22. T22 ⇒ T0.
 #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
 elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
-elim (IH … HT1 … HT2) -HT1 HT2 // #T #HT1 #HT2
-/3 width=5/
+elim (IH … HT1 … HT2) -HT1 HT2 /3 width=5/
 qed.
 
+lemma tpr_conf_flat_beta:
+   ∀V11,V12,T12,V22,W2,T21,T22. (
+      ∀T1. #T1 < #V11 + (#W2 + #T21 + 1) + 1 →
+      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+   ) →
+   V11 ⇒ V12 → V11 ⇒ V22 →
+   T21 ⇒ T22 → 𝕓{Abst} W2. T21 ⇒ T12 →
+   ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} V22. T22 ⇒ T0.
+#V11 #V12 #T12 #V22 #W2 #T21 #T22 #IH #HV1 #HV2 #HT1 #HT2
+elim (tpr_inv_abst1 … HT2) -HT2 #W1 #T1 #HW21 #HT21 #H destruct -T12;
+elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV12 #HV22
+elim (IH … HT21 … HT1) -HT21 HT1 IH /3 width=5/
+qed.
+(*
+lemma tpr_conf_flat_theta:
+   ∀V11,V12,T12,V2,V22,W21,W22,T21,T22. (
+      ∀T1. #T1 < #V11 + (#W21 + #T21 + 1) + 1 →
+      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+      ∃∃T0. T3 ⇒ T0 & T4 ⇒T0
+   ) →
+   V11 ⇒ V12 → V11 ⇒ V22 → ↑[O,1] V22 ≡ V2 →
+   W21 ⇒ W22 → T21 ⇒ T22 →  𝕓{Abbr} W21. T21 ⇒ T12 →
+   ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0.
+*)
+
 (* Confluence ***************************************************************)
+(*
+lemma tpr_conf_aux:
+   ∀T. (
+      ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+         ) →
+   ∀U1,T1,T2. U1 ⇒ T1 → U1 ⇒ T2 → U1 = T →
+   ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
+#T #IH  #U1 #T1 #T2 * -U1 T1
+[ #k1 #H1 #H2 destruct -T;
+  lapply (tpr_inv_sort1 … H1) -H1
+(* case 1: sort, sort *) 
+  #H1 destruct -T2 //
+| #i1 #H1 #H2 destruct -T;
+  lapply (tpr_inv_lref1 … H1) -H1
+(* case 2: lref, lref *) 
+  #H1 destruct -T2 //
+| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 #H1 #H2 destruct -T;
+  lapply (tpr_inv_bind1 … H1) -H1
+  [ 
 
+theorem tpr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 →
+                 ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
+#T @(tw_wf_ind … T) -T /3 width=6/
+qed.
+*)
 lemma tpr_conf_aux:
    ∀T. (
       ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
@@ -140,7 +189,7 @@ lemma tpr_conf_aux:
 (* case 27: bind, tau (excluded) *)
   | #V2 #T21 #T22 #_ #H1 #H2 destruct
   ]
-| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2 
+| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2
 (* case 28: flat, sort (excluded) *)
   [ #k2 #H1 #H2 destruct
 (* case 29: flat, lref (excluded) *)
@@ -152,9 +201,20 @@ lemma tpr_conf_aux:
     destruct -T I2 V21 T21 /3 width=7/
 (* case 32: flat, beta *)
   | #V21 #V22 #W2 #T21 #T22 #HV212 #HT212 #H1 #H2
-    destruct -I1 V21 T11 T; 
-  
-theorem pr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 →
-                 ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
-#T @(tw_wf_ind … T) -T /3 width=8/
-qed.
+    destruct -I1 V21 T11 T /3 width=8/ (**) (* slow *)
+(* case 33: flat, delta (excluded) *)
+  | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
+(* case 34: flat, theta *)
+  | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #H212 #HV222 #HW212 #HT212 #H1 #H2
+    destruct -I1 V21 T11 T //
+
+lemma tpr_conf_flat_theta:
+   ∀V11,V12,T12,V2,V22,W21,W22,T21,T22. (
+      ∀T1. #T1 < #V11 + (#W21 + #T21 + 1) + 1 →
+      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+      ∃∃T0. T3 ⇒ T0 & T4 ⇒T0
+   ) →
+   V11 ⇒ V12 → V11 ⇒ V22 → ↑[O,1] V22 ≡ V2 →
+   W21 ⇒ W22 → T21 ⇒ T22 →  𝕓{Abbr} W21. T21 ⇒ T12 →
+   ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0.
+