From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 14 Mar 2012 15:39:49 +0000 (+0000)
Subject: - property S4 of strongly normalizing term proved!
X-Git-Tag: make_still_working~1856
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bbac36729dab046d61019081c1523af06d876103;p=helm.git

- property S4 of strongly normalizing term proved!
---

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index b360bb20d..5370377e6 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -250,11 +250,9 @@ pr2/clen pr2_gen_ctail
 pr2/fwd pr2_gen_void
 pr2/props pr2_ctail
 pr2/subst1 pr2_gen_cabbr
-
-pr3/fwd pr3_gen_lref
 pr3/fwd pr3_gen_void
-pr3/fwd pr3_gen_bind
 pr3/pr1 pr3_pr1
+
 pr3/pr3 pr3_strip
 pr3/props pr3_thin_dx
 pr3/props pr3_head_1
@@ -270,8 +268,6 @@ sn3/props sn3_shift
 sn3/props sn3_change
 sn3/props sn3_gen_def
 sn3/props sn3_cdelta
-sn3/props sn3_appl_lref
-sn3/props sn3_appl_abbr
 sn3/props sn3_appl_appls
 sn3/props sn3_appls_lref
 sn3/props sns3_lifts
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
index ed6ee27e3..a91c9d8b5 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
@@ -82,7 +82,7 @@ elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
 #W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
 qed-.
 
-(* Basic_1: removed theorems 5:
-   clear_pr3_trans pr3_cflat
+(* Basic_1: removed theorems 6:
+   clear_pr3_trans pr3_cflat pr3_gen_bind
    pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
 *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
index 5ee21be85..32dcb2ce9 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma
@@ -19,6 +19,25 @@ include "basic_2/computation/cprs.ma".
 
 (* Advanced inversion lemmas ************************************************)
 
+(* Basic_1: was: pr3_gen_lref *)
+lemma cprs_inv_lref1: ∀L,T2,i. L ⊢ #i ➡* T2 →
+                      T2 = #i ∨
+                      ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 &
+                                 K ⊢ V1 ➡* T1 &
+                                 ⇧[0, i + 1] T1 ≡ T2 &
+                                 i < |L|.
+#L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1/
+#T #T2 #_ #HT2 *
+[ #H destruct
+  elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/
+  * #K #V1 #T1 #HLK #HVT1 #HT12 #Hi
+  @or_intror @(ex4_3_intro … HLK … HT12) // /3 width=3/ (**) (* explicit constructors *)
+| * #K #V1 #T1 #HLK #HVT1 #HT1 #Hi
+  lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+  elim (cpr_inv_lift … H0LK … HT1 … HT2) -H0LK -T /4 width=6/
+]
+qed-.
+
 (* Basic_1: was: pr3_gen_abst *)
 lemma cprs_inv_abst1: ∀I,W,L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡* U2 →
                       ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 &
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma
index 6969f7c60..c7f49d1cf 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma
@@ -35,6 +35,18 @@ elim (cprs_inv_appl1 … H) -H *
 ]
 qed-.
 
+(* Note: probably this is an inversion lemma *)
+lemma cprs_fwd_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
+                      ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+                      ∀U. L ⊢ #i ➡* U →
+                      #i ≃ U ∨ L ⊢ V2 ➡* U.
+#L #K #V1 #i #HLK #V2 #HV12 #U #H
+elim (cprs_inv_lref1 … H) -H /2 width=1/
+* #K0 #V0 #U0 #HLK0 #HVU0 #HU0 #_
+lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/
+qed-.
+
 lemma cprs_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡* U →
                       ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨
                       L ⊢ ⓓV. ⓐV2. T ➡* U.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma
index 4b65a08df..d12a9f498 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma
@@ -44,6 +44,31 @@ elim (cprs_inv_appl1 … H) -H *
 ]
 qed-.
 
+lemma cprs_fwd_delta_vector: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
+                             ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+                             ∀Vs,U. L ⊢ ⒶVs.#i ➡* U →
+                             ⒶVs.#i ≃ U ∨ L ⊢ ⒶVs.V2 ➡* U.
+#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=4 by cprs_fwd_delta/
+#V #Vs #IHVs #U #H -K -V1
+elim (cprs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
+| #V0 #W0 #T0 #HV0 #HT0 #HU
+  elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (tstc_inv_bind_appls_simple … HT0 ?) //
+  | @or_intror -i (**) (* explicit constructor *)
+    @(cprs_trans … HU) -U
+    @(cprs_strap1 … (ⓐV0.ⓛW0.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=1/
+  ]
+| #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
+  elim (IHVs … HT0) -IHVs -HT0 #HT0
+  [ elim (tstc_inv_bind_appls_simple … HT0 ?) //
+  | @or_intror -i (**) (* explicit constructor *)
+    @(cprs_trans … HU) -U
+    @(cprs_strap1 … (ⓐV0.ⓓV3.T0)) [ /2 width=1/ ] -V -V2 -Vs /3 width=3/
+  ]
+]
+qed-.
+
 (* Basic_1: was: pr3_iso_appls_abbr *)
 lemma cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
                              ∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡* U →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
index 2890fb9b1..5552c6fb7 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
@@ -82,7 +82,8 @@ qed.
 lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T.
 /2 width=5/ qed-.
 
-(* Basic_1: removed theorems 7:
-            sn3_gen_cflat sn3_cflat sn3_appl_cast sn3_appl_beta
+(* Basic_1: removed theorems 9:
+            sn3_gen_cflat sn3_cflat
+	    sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr
             sn3_bind sn3_appl_bind sn3_appls_bind
 *)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma
index c185ef2c6..5f5465b4f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma
@@ -52,6 +52,27 @@ lapply (csn_fwd_flat_dx … H1T) #H2T
 ]
 qed.
 
+lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
+                       ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+                       ∀Vs.L ⊢ ⬇* (ⒶVs. V2) → L ⊢ ⬇* (ⒶVs. #i).
+#L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
+[ #H
+  lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
+  lapply (csn_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=4/
+| #V #Vs #IHV #H1T
+  lapply (csn_fwd_pair_sn … H1T) #HV
+  lapply (csn_fwd_flat_dx … H1T) #H2T
+  @csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T
+  [ #X #H #H0
+    elim (cprs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
+    [ -H1T elim (H0 ?) -H0 //
+    | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
+    ]
+  | -L -K -V -V1 -V2 elim Vs -Vs //
+  ]
+]
+qed.
+
 (* Basic_1: was: sn3_appls_abbr *) 
 lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
                        ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V →
@@ -93,7 +114,7 @@ theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T).
 @mk_acr //
 [
 | /2 width=1/
-|
+| /2 width=6/
 | #L #V1 #V2 #HV12 #V #T #H #HVT
   @(csn_applv_theta … HV12) -HV12 //
   @(csn_abbr) //