X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Freducibility%2Ftpr.ma;h=57a619fa58a54589ac69103355d9f9fa3488ac69;hb=7e6643f9ce7ae87e9241aeac5b6d828e9d47fb63;hp=db2c8c69f3b3ed5af2d86173bc337891cdfbcc8c;hpb=f75be90562ddd964ef7ed43b956eb908f3133e3a;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
index db2c8c69f..57a619fa5 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
@@ -28,9 +28,9 @@ inductive tpr: relation term ≝
              tpr V1 V2 → tpr T1 T2 → ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T →
              tpr (𝕓{I} V1. T1) (𝕓{I} V2. T)
 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
-             tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
+             tpr V1 V2 → ⇑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
              tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2)
-| tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 →
+| tpr_zeta : ∀V,T,T1,T2. ⇑[0,1] T1 ≡ T → tpr T1 T2 →
              tpr (𝕔{Abbr} V. T) T2
 | tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2
 .
@@ -42,19 +42,19 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
-                             𝕓{I} V1. T1 ⇒  𝕓{I} V2. T2.
-/2/ qed.
+                            𝕓{I} V1. T1 ⇒  𝕓{I} V2. T2.
+/2 width=3/ qed.
 
 (* Basic_1: was by definition: pr0_refl *)
 lemma tpr_refl: ∀T. T ⇒ T.
 #T elim T -T //
-#I elim I -I /2/
+#I elim I -I /2 width=1/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
 fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}.
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
 [ //
 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
@@ -67,21 +67,21 @@ qed.
 
 (* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
 lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
-/2/ qed.
+/2 width=3/ qed-.
 
 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
                         (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
                                     ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
                                     U2 = 𝕓{I} V2. T
                         ) ∨
-                        ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-#U1 #U2 * -U1 U2
+                        ∃∃T. ⇑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
+#U1 #U2 * -U1 -U2
 [ #J #I #V #T #H destruct
 | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
-| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
+| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
+| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/
 | #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
 ]
 qed.
@@ -91,8 +91,8 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
                                  ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
                                  U2 = 𝕓{I} V2. T
                      ) ∨
-                     ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-/2/ qed.
+                     ∃∃T. ⇑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
+/2 width=3/ qed-.
 
 (* Basic_1: was pr0_gen_abbr *)
 lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
@@ -100,10 +100,10 @@ lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
                                  ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
                                  U2 = 𝕓{Abbr} V2. T
                       ) ∨
-                      ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
+                      ∃∃T. ⇑[0,1] T ≡ T1 & T ⇒ U2.
 #V1 #T1 #U2 #H
 elim (tpr_inv_bind1 … H) -H * /3 width=7/
-qed.
+qed-.
 
 fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 →
                         ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
@@ -112,20 +112,19 @@ fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0
                                                U0 = 𝕔{Abst} W. T1 &
                                                U2 = 𝕔{Abbr} V2. T2 & I = Appl
                          | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
-                                               ↑[0,1] V2 ≡ V &
+                                               ⇑[0,1] V2 ≡ V &
                                                U0 = 𝕔{Abbr} W1. T1 &
                                                U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
                                                I = Appl
                          |                     (U0 ⇒ U2 ∧ I = Cast).
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
 [ #I #J #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
+| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/
 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H
-  destruct -J V1 T0 /3 width=12/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/
 | #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
-| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
+| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
 ]
 qed.
 
@@ -136,12 +135,12 @@ lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
                                             U0 = 𝕔{Abst} W. T1 &
                                             U2 = 𝕔{Abbr} V2. T2 & I = Appl
                       | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
-                                            ↑[0,1] V2 ≡ V &
+                                            ⇑[0,1] V2 ≡ V &
                                             U0 = 𝕔{Abbr} W1. T1 &
                                             U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
                                             I = Appl
                       |                     (U0 ⇒ U2 ∧ I = Cast).
-/2/ qed.
+/2 width=3/ qed-.
 
 (* Basic_1: was pr0_gen_appl *)
 lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
@@ -151,12 +150,26 @@ lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
                                             U0 = 𝕔{Abst} W. T1 &
                                             U2 = 𝕔{Abbr} V2. T2
                       | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
-                                            ↑[0,1] V2 ≡ V &
+                                            ⇑[0,1] V2 ≡ V &
                                             U0 = 𝕔{Abbr} W1. T1 &
                                             U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
 #V1 #U0 #U2 #H
 elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
-qed.
+qed-.
+
+(* Note: the main property of simple terms *)
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. 𝕔{Appl} V1. T1 ⇒ U → 𝕊[T1] →
+                            ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 &
+                                     U = 𝕔{Appl} V2. T2.
+#V1 #T1 #U #H #HT1
+elim (tpr_inv_appl1 … H) -H *
+[ /2 width=5/
+| #V2 #W #W1 #W2 #_ #_ #H #_ destruct
+  elim (simple_inv_bind … HT1)
+| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
+  elim (simple_inv_bind … HT1)
+]
+qed-.
 
 (* Basic_1: was: pr0_gen_cast *)
 lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 →
@@ -167,30 +180,30 @@ elim (tpr_inv_flat1 … H) -H * /3 width=5/
 [ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
 | #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
 ]
-qed.
+qed-.
 
 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
                         ∨∨           T1 = #i
-                         | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
+                         | ∃∃V,T,T0. ⇑[O,1] T0 ≡ T & T0 ⇒ #i &
                                      T1 = 𝕔{Abbr} V. T
                          | ∃∃V,T.    T ⇒ #i & T1 = 𝕔{Cast} V. T.
-#T1 #T2 * -T1 T2
-[ #I #i #H destruct /2/
+#T1 #T2 * -T1 -T2
+[ #I #i #H destruct /2 width=1/
 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
-| #V #T1 #T2 #HT12 #i #H destruct /3/
+| #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
 ]
 qed.
 
 lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
                      ∨∨           T1 = #i
-                      | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
+                      | ∃∃V,T,T0. ⇑[O,1] T0 ≡ T & T0 ⇒ #i &
                                   T1 = 𝕔{Abbr} V. T
                       | ∃∃V,T.    T ⇒ #i & T1 = 𝕔{Cast} V. T.
-/2/ qed.
+/2 width=3/ qed-.
 
 (* Basic_1: removed theorems 3:
             pr0_subst0_back pr0_subst0_fwd pr0_subst0