From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 4 Apr 2017 17:14:20 +0000 (+0000)
Subject: advances non lfsx ...
X-Git-Tag: make_still_working~464
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d0e3208d69d24a9dc9e066e381f1601bc8e109be;p=helm.git

advances non lfsx ...
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma
index 51596c44e..2311f424c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma
@@ -45,56 +45,27 @@ lemma lfsx_intro: ∀h,o,G,L1,T.
                   (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) →
                   G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄.
 /5 width=1 by lfdeq_sym, SN_intro/ qed.
-(*
+
+(* Basic_2A1: was: lsx_sort *)
 lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄.
 #h #o #G #L1 #s @lfsx_intro
 #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H *
 [ #H1 #H2 destruct //
-| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct 
-  @lfdeq_sort 
+| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
+  /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort_gen, frees_inv_sort/
+]
 qed.
 
-lemma lfsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬈*[h, o, §p, l] L.
-#h #o #G #L1 #l #p @lfsx_intro
-#L2 #HL12 #H elim H -H
-/3 width=4 by lfpx_fwd_length, lfdeq_gref/
+(* Basic_2A1: was: lsx_gref *)
+lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄.
+#h #o #G #L1 #s @lfsx_intro
+#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H *
+[ #H1 #H2 destruct //
+| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct
+  /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref_gen, frees_inv_gref/
+]
 qed.
 
-(* Basic forward lemmas *****************************************************)
-
-lemma lfsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L →
-                       G ⊢ ⬈*[h, o, V, l] L.
-#h #o #a #I #G #L #V #T #l #H @(lfsx_ind … H) -L
-#L1 #_ #IHL1 @lfsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=4 by lfdeq_fwd_bind_sn/
-qed-.
-
-lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
-                       G ⊢ ⬈*[h, o, V, l] L.
-#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
-#L1 #_ #IHL1 @lfsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/
-qed-.
-
-lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
-                       G ⊢ ⬈*[h, o, T, l] L.
-#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
-#L1 #_ #IHL1 @lfsx_intro
-#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/
-qed-.
-
-lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L →
-                       G ⊢ ⬈*[h, o, V, l] L.
-#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
-                    G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L.
-/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-.
-
-(* Basic_2A1: removed theorems 5:
-              lsx_atom lsx_sort lsx_gref lsx_ge_up lsx_ge
-*)
+(* Basic_2A1: removed theorems 2:
+              lsx_ge_up lsx_ge
 *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma
new file mode 100644
index 000000000..5ea3071b0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/static/lfdeq_lfdeq.ma".
+include "basic_2/rt_transition/lfpx_lfdeq.ma".
+include "basic_2/rt_computation/lfsx.ma".
+
+(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+
+axiom pippo: ∀h,o,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 →
+             ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L & L ≡[h, o, V] L2.
+
+(* Advanced properties ******************************************************)
+
+lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ →
+                        ∀L2. L1 ≡[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄.
+#h #o #G #L1 #T #H @(lfsx_ind … H) -L1
+#L1 #_ #IHL1 #L2 #HL12 @lfsx_intro
+#L #HL2 #HnL2 elim (lfdeq_lfpx_trans … HL2 … HL12) -HL2
+/4 width=5 by lfdeq_repl/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+(* Basic_2A1: was: lsx_fwd_bind_sn *)
+lemma lfsx_fwd_bind_sn: ∀h,o,p,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ →
+                        G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄.
+#h #o #p #I #G #L #V #T #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #H #HnL12 elim (pippo … o p I … T H) -H
+/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_bind_sn/
+qed-.
+(*
+lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+                       G ⊢ ⬈*[h, o, V, l] L.
+#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/
+qed-.
+
+lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+                       G ⊢ ⬈*[h, o, T, l] L.
+#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L
+#L1 #_ #IHL1 @lfsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/
+qed-.
+
+lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L →
+                       G ⊢ ⬈*[h, o, V, l] L.
+#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L →
+                    G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L.
+/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-.
+*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma
index 71b1c0d4f..c42edd196 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma
@@ -42,6 +42,10 @@ theorem lfdeq_canc_sn: ∀h,o,T. left_cancellable … (lfdeq h o T).
 theorem lfdeq_canc_dx: ∀h,o,T. right_cancellable … (lfdeq h o T).
 /3 width=3 by lfdeq_trans, lfdeq_sym/ qed-.
 
+theorem lfdeq_repl: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 →
+                    ∀K1. L1 ≡[h, o, T] K1 → ∀K2. L2 ≡[h, o, T] K2 → K1 ≡[h, o, T] K2.
+/3 width=3 by lfdeq_canc_sn, lfdeq_trans/ qed-.
+
 (* Advanced properies on negated lazy equivalence *****************************)
 
 (* Note: auto works with /4 width=8/ so lfdeq_canc_sn is preferred ************) 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index f754e46de..1d7781d7e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -89,6 +89,14 @@ lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) →
 #R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/
 qed-.
 
+lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2.
+                 (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → 𝐈⦃f⦄) → 
+                 (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≡ f) → 
+                 L1 ⦻*[R1, T1] L2 → L1 ⦻*[R2, T2] L2.
+#R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 *
+/4 width=7 by lexs_co_isid, ex2_intro/
+qed-.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⦻*[R, T] Y2 → Y2 = ⋆.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 5019e8956..68759e53b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -113,6 +113,7 @@ table {
              [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
              [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
 *)
+             [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfsx" * ]
              [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
              [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
              [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]