- lambda_delta: strong normalization of simply typed terms closed!

- star.ma: transitive closure: support for reverse elimination

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 4341a5a94a6d81219405893f98d49c9b21f7d85d..5ea230f9b91af1b7d17eda7d453a2779ea36a605 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
@@ -28,12 +28,16 @@ interpretation "context-sensitive parallel computation (term)"
 lemma cprs_ind: ∀L,T1. ∀R:predicate term. R T1 →
                 (∀T,T2. L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → R T → R T2) →
                 ∀T2. L ⊢ T1 ➡* T2 → R T2.
-#L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
+#L #T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
 qed-.
 
-axiom cprs_ind_dx: ∀L,T2. ∀R:predicate term. R T2 →
+lemma cprs_ind_dx: ∀L,T2. ∀R:predicate term. R T2 →
                    (∀T1,T. L ⊢ T1 ➡ T → L ⊢ T ➡* T2 → R T → R T1) →
                    ∀T1. L ⊢ T1 ➡* T2 → R T1.
+#L #T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx … HT2 IHT2 … HT12) //
+qed-.
 
 (* Basic properties *********************************************************)
 

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 2f8486cc26d70f2b557428f87b0927010e2867ac..feaedbf76bfd6be07b00496a2b065845f9cffe6b 100644 (file)
--- 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
@@ -20,6 +20,7 @@ include "basic_2/computation/cprs_tstc.ma".
 
 (* Vector form of forward lemmas involving same top term constructor ********)
 
+(* Basic_1: was just: nf2_iso_appls_lref *)
 lemma cprs_fwd_cnf_vector: ∀L,T.  𝐒[T] → L ⊢ 𝐍[T] → ∀Vs,U. L ⊢ ⒶVs.T ➡* U → ⒶVs.T ≃ U.
 #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cprs_fwd_cnf … H2T) ] (**) (* /2 width=3 by cprs_fwd_cnf/ does not work *)
 #V #Vs #IHVs #U #H

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma
new file mode 100644 (file)
index 0000000..375d645
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr_vector.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/computation/csn_cpr.ma".
+include "basic_2/computation/csn_vector.ma".
+
+(* Advanced forward lemmas **************************************************)
+
+lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T.
+#L #T #Vs elim Vs -Vs /2 width=1/
+#V #Vs #IHVs #HVs
+lapply (csn_fwd_pair_sn … HVs) #HV
+lapply (csn_fwd_flat_dx … HVs) -HVs #HVs
+elim (IHVs HVs) -IHVs -HVs /3 width=1/
+qed-.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
index 00de73f528cc89cf85672740d583628754ac7439..3aa7170f50da7ca220c06e2c529fa290cf4636b6 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
@@ -28,11 +28,9 @@ lemma csn_applv_cnf: ∀L,T. 𝐒[T] → L ⊢ 𝐍[T] →
 #V #Vs #IHV #H
 elim (csnv_inv_cons … H) -H #HV #HVs
 @csn_appl_simple_tstc // -HV /2 width=1/ -IHV -HVs
-[ #X #H #H0
-  lapply (cprs_fwd_cnf_vector … H) -H // -H1T -H2T #H
-  elim (H0 ?) -H0 //
-| -L -V elim Vs -Vs //
-]
+#X #H #H0
+lapply (cprs_fwd_cnf_vector … H) -H // -H1T -H2T #H
+elim (H0 ?) -H0 //
 qed.
 
 (* Basic_1: was: sn3_appls_beta *)
@@ -44,12 +42,10 @@ lemma csn_applv_beta: ∀L,W. L ⊢ ⬇* W →
 lapply (csn_fwd_pair_sn … H1T) #HV0
 lapply (csn_fwd_flat_dx … H1T) #H2T
 @csn_appl_simple_tstc // -HV0 /2 width=1/ -IHV -H2T
-[ #X #H #H0
-  elim (cprs_fwd_beta_vector … H) -H #H
-  [ -H1T elim (H0 ?) -H0 //
-  | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
-  ]
-| -H1T elim Vs -Vs //
+#X #H #H0
+elim (cprs_fwd_beta_vector … H) -H #H
+[ -H1T elim (H0 ?) -H0 //
+| -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
 ]
 qed.
 
@@ -64,12 +60,10 @@ lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
   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 //
+  #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/
   ]
 ]
 qed.
@@ -102,12 +96,10 @@ lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W →
 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_tau_vector … H) -H #H
-  [ -H1T elim (H0 ?) -H0 //
-  | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
-  ]
-| -H1T elim Vs -Vs //
+#X #H #H0
+elim (cprs_fwd_tau_vector … H) -H #H
+[ -H1T elim (H0 ?) -H0 //
+| -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
 ]
 qed.
 

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
index 7dab76e2307c7e6a16d1592ee5b4ba6f897720a2..a8663d8ba7138e98830de9c1048d0ef95229c4bd 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
@@ -17,41 +17,14 @@ include "basic_2/computation/csn.ma".
 
 (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
 
-inductive csnv (L:lenv): predicate (list term) ≝
-| csnv_nil: csnv L ◊
-| csn_cons: ∀Ts,T. L  ⊢ ⬇* T → csnv L Ts → csnv L (T :: Ts)
-.
+definition csnv: lenv → predicate (list term) ≝
+                 λL. all … (csn L).
 
 interpretation
    "context-sensitive strong normalization (term vector)"
    'SN L Ts = (csnv L Ts).
 
-(* Basic properties *********************************************************)
-
-lemma all_csnv: ∀L,Vs. all … (csn L) Vs → L ⊢ ⬇* Vs.
-#L #Vs elim Vs -Vs //
-#V #Vs #IHVs * /3 width=1/ 
-qed.
-
 (* Basic inversion lemmas ***************************************************)
 
-fact csnv_inv_cons_aux: ∀L,Ts. L ⊢ ⬇* Ts → ∀U,Us. Ts = U :: Us →
-                        L ⊢ ⬇* U ∧ L ⊢ ⬇* Us.
-#L #Ts * -Ts
-[ #U #Us #H destruct
-| #Ts #T #HT #HTs #U #Us #H destruct /2 width=1/
-]
-qed.
-
 lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
-/2 width=3/ qed-.
-
-include "basic_2/computation/csn_cpr.ma".
-
-lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T.
-#L #T #Vs elim Vs -Vs /2 width=1/
-#V #Vs #IHVs #HVs
-lapply (csn_fwd_pair_sn … HVs) #HV
-lapply (csn_fwd_flat_dx … HVs) -HVs #HVs
-elim (IHVs HVs) -IHVs -HVs /3 width=1/
-qed-.
+normalize // qed-.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma
index c2ad0f835f63504ab3c054b646db776c75adce88..7b4923bbe6b3a60530fc9731d3d55130f1c3c87e 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/list.ma".
-include "basic_2/grammar/term.ma".
+include "basic_2/grammar/term_simple.ma".
 
 (* TERMS ********************************************************************)
 
@@ -25,3 +25,9 @@ let rec applv Vs T on Vs ≝
 
 interpretation "application o vevtor (term)"
    'SnApplV Vs T = (applv Vs T).
+
+(* properties concerning simple terms ***************************************)
+
+lemma applv_simple: ∀T,Vs.  𝐒[T] -> 𝐒[ⒶVs.T].
+#T * //
+qed.

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index cae3766b1d008bf2b41c9ecb50360ea9ce00ec44..bac2e771c23672b73fa9d936dc5fac913d3ac461 100644 (file)
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -153,3 +153,41 @@ lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
                    ∀a2. TC … R a1 a2 → P a2.
 #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/
 qed.
+
+inductive TC_dx (A:Type[0]) (R:relation A): A → A → Prop ≝
+  |inj_dx: ∀a,c. R a c → TC_dx A R a c
+  |step_dx : ∀a,b,c. R a b → TC_dx A R b c → TC_dx A R a c.
+
+lemma TC_dx_strap: ∀A. ∀R: relation A.
+                   ∀a,b,c. TC_dx A R a b → R b c → TC_dx A R a c.
+#A #R #a #b #c #Hab elim Hab -a -b /3 width=3/
+qed.
+
+lemma TC_to_TC_dx: ∀A. ∀R: relation A.
+                   ∀a1,a2. TC … R a1 a2 → TC_dx … R a1 a2.
+#A #R #a1 #a2 #Ha12 elim Ha12 -a2 /2 width=3/
+qed.
+
+lemma TC_dx_to_TC: ∀A. ∀R: relation A.
+                   ∀a1,a2. TC_dx … R a1 a2 → TC … R a1 a2.
+#A #R #a1 #a2 #Ha12 elim Ha12 -a1 -a2 /2 width=3/
+qed.
+
+fact TC_star_ind_dx_aux: ∀A,R. reflexive A R →
+                         ∀a2. ∀P:predicate A. P a2 →
+                         (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
+                         ∀a1,a. TC … R a1 a → a = a2 → P a1.
+#A #R #HR #a2 #P #Ha2 #H #a1 #a #Ha1
+elim (TC_to_TC_dx ???? Ha1) -a1 -a
+[ #a #c #Hac #H destruct /3 width=4/
+| #a #b #c #Hab #Hbc #IH #H destruct /3 width=4/
+]
+qed-.
+
+lemma TC_star_ind_dx: ∀A,R. reflexive A R →
+                      ∀a2. ∀P:predicate A. P a2 →
+                      (∀a1,a. R a1 a → TC … R a a2 → P a → P a1) →
+                      ∀a1. TC … R a1 a2 → P a1.
+#A #R #HR #a2 #P #Ha2 #H #a1 #Ha12
+@(TC_star_ind_dx_aux … HR … Ha2 H … Ha12) //
+qed-.