- more properties on strongly normalizing terms ...

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
index e71d2bd3e694e178da1a76e489579bd3d8dff816..81c179293619714cc0b0ad5ebb3831683c9ce780 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cr.ma
@@ -20,6 +20,20 @@ include "Basic_2/computation/csn_vector.ma".
 
 (* Advanced properties ******************************************************)
 (*
+
+(* Basic_1: was only: sn3_appl_appls *)
+lemma csn_appl_appls_simple_tstc: ∀L,Vs,V,T1. L ⊢ ⬇* V → L ⊢ ⬇* T1 →
+                                  (∀T2. L ⊢ ⒶVs.T1 ➡* T2 → (ⒶVs.T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) →
+                                  𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1.
+#L *
+[ #V #T1 #HV
+  @csn_appl_simple_tstc //
+| #V0 #Vs #V #T1 #HV #H1T1 #H2T1 #H3T1
+  @csn_appl_simple_tstc // -HV
+  [ @H2T1
+]
+qed.
+
 lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
                        ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
 #L #V1s #V2s * -V1s -V2s /2 width=1/

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma
index 77ae2f9dbe2d2f0782176cde521a3d0e1efed1e5..98ee1843748ffedabb3571c06618a45f0449d9f9 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Basic_2/grammar/tstc_tstc.ma".
 include "Basic_2/reducibility/lcpr_cpr.ma".
 include "Basic_2/computation/cprs_cprs.ma".
 include "Basic_2/computation/csn_lift.ma".
@@ -117,3 +118,30 @@ qed.
 lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
                       ∀L,V,T. L ⊢ ⬇* ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T.
 /2 width=5/ qed.
+
+(* Basic_1: was only: sn3_appl_appl *)
+lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1.
+                            L ⊢ ⬇* T1 →
+                            (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) →
+                            𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
+#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csn_intro #X #HL #H
+elim (cpr_inv_appl1_simple … HL ?) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (eq_false_inv_tpair_sn … H) -H
+[ -IHT1 #HV0
+  @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
+  @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
+  #T2 #HLT12 #HT12
+  @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
+  @H2T1 -H2T1 // -HLT12 /2 width=1/
+| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
+  elim (tstc_dec T1 T0) #H2T10
+  [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
+    #T2 #HLT02 #HT02
+    @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
+  | -IHT1 -H3T1 -H1T10
+    @H2T1 -H2T1 /2 width=1/
+  ]
+]
+qed.

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma
index de29660f091fce6b658cd481f0722119643c3c41..1326a8bb482d556adf75daa324d495250180b580 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma
@@ -78,7 +78,6 @@ elim (eq_false_inv_tpair_sn … H2) -H2
 ]
 qed.
 
-(* Basic_1: was only: sn3_appl_appl *)
 lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1.
                        (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) →
                        𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
@@ -92,19 +91,8 @@ elim (eq_false_inv_tpair_dx … H2) -H2
   @IHT1 -IHT1 // /2 width=1/
 | -HLT10 * #H #HV0 destruct
   @IHV -IHV // -HT1 /2 width=1/ -HV0
-  #T2 #HLT02 #HT02 
+  #T2 #HLT02 #HT02
   @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
   @IHT1 -IHT1 // -HLT02 /2 width=1/
 ]
 qed.
-
-(* Basic_1: was only: sn3_appl_appls *)
-lemma csn_appl_appls_simple: ∀L,V. L ⊢ ⬇* V → ∀Vs,T1.
-                             (∀T2. L ⊢ ⒶVs.T1 ➡ T2 → (ⒶVs.T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) →
-                             𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1.
-#L #V #HV #Vs elim Vs -Vs
-[ @csn_appl_simple //
-| #V0 #Vs #_ #T1 #HT1 #_
-  @csn_appl_simple // -HV @HT1
-]
-qed.

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
deleted file mode 100644 (file)
index 5b90bd1..0000000
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
+++ /dev/null
@@ -1,78 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/grammar/term_simple.ma".
-
-(* HOMOMORPHIC TERMS ********************************************************)
-
-inductive thom: relation term ≝
-   | thom_atom: ∀I. thom (⓪{I}) (⓪{I})
-   | thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2)
-   | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝐒[T1] → 𝐒[T2] →
-                thom (ⓐV1. T1) (ⓐV2. T2)
-.
-
-interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma thom_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1.
-#T1 #T2 #H elim H -T1 -T2 /2 width=1/
-qed.
-
-lemma thom_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2.
-#T1 #T2 #H elim H -T1 -T2 // /2 width=1/
-qed.
-
-lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
-/3 width=2/ qed.
-
-lemma simple_thom_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒[T1] → 𝐒[T2].
-#T1 #T2 #H elim H -T1 -T2 //
-#V1 #V2 #T1 #T2 #H
-elim (simple_inv_bind … H)
-qed. (**) (* remove from index *)
-
-lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒[T2] → 𝐒[T1].
-/3 width=3/ qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 →
-                         ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
-#T1 #T2 * -T1 -T2
-[ #J #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
-| #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct
-]
-qed.
-
-lemma thom_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 →
-                      ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
-/2 width=5/ qed-.
-
-fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
-                         ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] &
-                                  I = Appl & T2 = ⓐW2. U2.
-#T1 #T2 * -T1 -T2
-[ #J #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
-| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/
-]
-qed.
-
-lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
-                      ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] &
-                               I = Appl & T2 = ⓐW2. U2.
-/2 width=4/ qed-.

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tshf.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tshf.ma
new file mode 100644 (file)
index 0000000..364a530
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tshf.ma
@@ -0,0 +1,78 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/grammar/term_simple.ma".
+
+(* SAME HEAD TERM FORMS *****************************************************)
+
+inductive tshf: relation term ≝
+   | tshf_atom: ∀I. tshf (⓪{I}) (⓪{I})
+   | tshf_abst: ∀V1,V2,T1,T2. tshf (ⓛV1. T1) (ⓛV2. T2)
+   | tshf_appl: ∀V1,V2,T1,T2. tshf T1 T2 → 𝐒[T1] → 𝐒[T2] →
+                tshf (ⓐV1. T1) (ⓐV2. T2)
+.
+
+interpretation "same head form (term)" 'napart T1 T2 = (tshf T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tshf_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1.
+#T1 #T2 #H elim H -T1 -T2 /2 width=1/
+qed.
+
+lemma tshf_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2.
+#T1 #T2 #H elim H -T1 -T2 // /2 width=1/
+qed.
+
+lemma tshf_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
+/3 width=2/ qed.
+
+lemma simple_tshf_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒[T1] → 𝐒[T2].
+#T1 #T2 #H elim H -T1 -T2 //
+#V1 #V2 #T1 #T2 #H
+elim (simple_inv_bind … H)
+qed. (**) (* remove from index *)
+
+lemma simple_tshf_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒[T2] → 𝐒[T1].
+/3 width=3/ qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact tshf_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 →
+                         ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
+#T1 #T2 * -T1 -T2
+[ #J #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
+| #V1 #V2 #T1 #T2 #H_ #_ #_ #I #W1 #U1 #H destruct
+]
+qed.
+
+lemma tshf_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 →
+                      ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
+/2 width=5/ qed-.
+
+fact tshf_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
+                         ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] &
+                                  I = Appl & T2 = ⓐW2. U2.
+#T1 #T2 * -T1 -T2
+[ #J #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
+| #V1 #V2 #T1 #T2 #HT12 #HT1 #HT2 #I #W1 #U1 #H destruct /2 width=5/
+]
+qed.
+
+lemma tshf_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
+                      ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] &
+                               I = Appl & T2 = ⓐW2. U2.
+/2 width=4/ qed-.

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma
index 26bb95386f0d758edf2028002b212c105301e34d..9c91d59f97e7bc21c813bd4e6dfe5f1f35f95f57 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/term.ma".
+include "Basic_2/grammar/term_simple.ma".
 
 (* SAME TOP TERM CONSTRUCTOR ************************************************)
 
@@ -23,17 +23,6 @@ inductive tstc: relation term ≝
 
 interpretation "same top constructor (term)" 'Iso T1 T2 = (tstc T1 T2).
 
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: iso_refl *)
-lemma tstc_refl: ∀T. T ≃ T.
-#T elim T -T //
-qed.
-
-lemma tstc_sym: ∀T1,T2. T1 ≃ T2 → T2 ≃ T1.
-#T1 #T2 #H elim H -T1 -T2 //
-qed.
-
 (* Basic inversion lemmas ***************************************************)
 
 fact tstc_inv_atom1_aux: ∀T1,T2. T1 ≃ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}.
@@ -78,6 +67,47 @@ lemma tstc_inv_pair2: ∀I,T1,W2,U2. T1 ≃ ②{I}W2.U2 →
                       ∃∃W1,U1. T1 = ②{I}W1. U1.
 /2 width=5/ qed-.
 
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: iso_refl *)
+lemma tstc_refl: ∀T. T ≃ T.
+#T elim T -T //
+qed.
+
+lemma tstc_sym: ∀T1,T2. T1 ≃ T2 → T2 ≃ T1.
+#T1 #T2 #H elim H -T1 -T2 //
+qed.
+
+lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2).
+* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ]
+[ elim (item2_eq_dec I1 I2) #HI12
+  [ destruct /2 width=1/
+  | @or_intror #H
+    elim (tstc_inv_pair1 … H) -H #V #T #H destruct /2 width=1/
+  ]
+| @or_intror #H
+  lapply (tstc_inv_atom1 … H) -H #H destruct
+| @or_intror #H
+  lapply (tstc_inv_atom2 … H) -H #H destruct
+| elim (item0_eq_dec I1 I2) #HI12
+  [ destruct /2 width=1/
+  | @or_intror #H
+    lapply (tstc_inv_atom2 … H) -H #H destruct /2 width=1/
+  ]
+]
+qed.
+
+axiom simple_inv_pair: ∀I,V,T.  𝐒[②{I}V.T] → ∃J. I = Flat2 J.
+
+lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≃ T2 → 𝐒[T1] → 𝐒[T2].
+#T1 #T2 * -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #H
+elim (simple_inv_pair … H) -H #J #H destruct //
+qed. (**) (* remove from index *)
+
+lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒[T2] → 𝐒[T1].
+/3 width=3/ qed-.
+
 (* Basic_1: removed theorems 2:
             iso_flats_lref_bind_false iso_flats_flat_bind_false
 *)

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
index 2497ea27365ebf67b3ef278c24e4cb1acae0db6d..90598b1e7905bcf8639d2fdffc83841f1dcf4272 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma
@@ -12,12 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/grammar/thom.ma".
+include "Basic_2/grammar/tshf.ma".
 include "Basic_2/reducibility/tpr.ma".
 
 (* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
 
-definition twhnf: predicate term ≝ NF … tpr thom.
+definition twhnf: predicate term ≝ NF … tpr tshf.
 
 interpretation
    "context-free weak head normality (term)"
@@ -25,32 +25,32 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma twhnf_inv_thom: ∀T. 𝐖𝐇𝐍[T] → T ≈ T.
+lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍[T] → T ≈ T.
 normalize /2 width=1/
 qed-.
 
 (* Basic properties *********************************************************)
 
-lemma tpr_thom: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2.
+lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2.
 #T1 #T2 #H elim H -T1 -T2 //
 [ #I #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H
-  elim (thom_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
+  elim (tshf_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
   lapply (IHT12 HT1U2) -IHT12 -HT1U2 #HUT2
-  lapply (simple_thom_repl_dx … HUT2 HT1) /2 width=1/
+  lapply (simple_tshf_repl_dx … HUT2 HT1) /2 width=1/
 | #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
-  elim (thom_inv_flat1 … H) -H #W2 #U2 #_ #H
+  elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #H
   elim (simple_inv_bind … H)
 | #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H
-  elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct //
+  elim (tshf_inv_bind1 … H) -H #W2 #U2 #H destruct //
 | #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
-  elim (thom_inv_flat1 … H) -H #U1 #U2 #_ #H
+  elim (tshf_inv_flat1 … H) -H #U1 #U2 #_ #H
   elim (simple_inv_bind … H)
 | #V #T #T1 #T2 #_ #_ #_ #H
-  elim (thom_inv_bind1 … H) -H #W2 #U2 #H destruct
+  elim (tshf_inv_bind1 … H) -H #W2 #U2 #H destruct
 | #V #T1 #T2 #_ #_ #H
-  elim (thom_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct
+  elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct
 ]
 qed.
 
-lemma twhnf_thom: ∀T. T ≈ T → 𝐖𝐇𝐍[T].
+lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍[T].
 /2 width=1/ qed.