From 44927f6b05adef73df12ff1b85f79f99698709d3 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 26 May 2014 17:08:40 +0000
Subject: [PATCH] new definition of llor gives a long awaited lemma :), but
 introduces an axiom :(

---
 .../llor.ma => etc/llor/llor.etc}             |  0
 .../llor_alt.ma => etc/llor/llor_alt.etc}     |  0
 .../lleq_llor.ma}                             | 33 +++++++++---------
 .../basic_2/substitution/llpx_sn_llor.ma      | 34 +++++++++++++++++++
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  6 ++--
 5 files changed, 54 insertions(+), 19 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution/llor.ma => etc/llor/llor.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{substitution/llor_alt.ma => etc/llor/llor_alt.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/{etc/llor/lleq_llor.etc => substitution/lleq_llor.ma} (66%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_llor.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor_alt.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/llor/llor_alt.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_llor.ma
similarity index 66%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc
rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_llor.ma
index a180d1124..80bc596f2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_llor.ma
@@ -12,24 +12,25 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/llor.ma".
+include "basic_2/substitution/llor.ma".
 include "basic_2/substitution/lleq_alt.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
 (* Properties on poinwise union for local environments **********************)
-
-lemma llor_lleq_O: ∀T,L1,L2,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → |L2| = |L| → L2 ⋕[T, yinj 0] L.
-#T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 #T #Hn #L2 #L #H #HL12 #HL2 elim (llor_inv_alt … H) // destruct
-#HL1 #IHT @lleq_intro_alt //
-#I2 #I #K2 #K #V2 #V #i #_ #HnT #HLK2 #HLK lapply (ldrop_fwd_length_lt2 … HLK)
-#Hi elim (ldrop_O1_lt L1 i) //
-#I1 #K1 #V1 #HLK1 elim (IHT … HLK1 HLK) >HL1 >HL2 <minus_n_n -IHT -HLK1 -HLK
-[
-| * #I0 #K0 #V0 #_ #HLK0 lapply (ldrop_mono … HLK0 … HLK2) -HLK0 -HLK2
-  #H1 #H2 #H3 #_ destruct
-    
-
-
- 
+(*
+lemma llor_lleq_O: ∀R,L1,L2,T. llpx_sn R 0 T L1 L2 →
+                   ∀L. L1 ⩖[T] L2 ≡ L → L2 ≡[T, 0] L.
+#R #L1 #L2 #T #H1 #L #H2
+elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1
+elim H2 -H2 #_ #HL1 #IH2
+@lleq_intro_alt // #I2 #I #K2 #K #V2 #V #i #Hi #HnT #HLK2 #HLK
+lapply (ldrop_fwd_length_lt2 … HLK) #HiL
+elim (ldrop_O1_lt (Ⓕ) L1 i) // -HiL #I1 #K1 #V1 #HLK1
+elim (IH1 … HLK1 HLK2) // -IH1
+[ #H #_ destruct
+  elim (IH2 … HLK1 HLK2 HLK) * /2 width=1 by conj/
+  #H elim HnT -HnT
+| #H @HnT -HnT
+]
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_llor.ma
new file mode 100644
index 000000000..a22618f1c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_llor.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/relocation/lpx_sn_alt.ma".
+include "basic_2/substitution/llor.ma".
+include "basic_2/substitution/lleq_alt.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* Inversion lemmas on poinwise union for local environments ****************)
+
+lemma llpx_sn_llor_fwd_sn: ∀R. (∀L. reflexive … (R L)) →
+                           ∀L1,L2,T. llpx_sn R 0 T L1 L2 →
+                           ∀L. L1 ⩖[T] L2 ≡ L → lpx_sn R L1 L.
+#R #HR #L1 #L2 #T #H1 #L #H2
+elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1
+elim H2 -H2 #_ #HL1 #IH2
+@lpx_sn_intro_alt // #I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
+lapply (ldrop_fwd_length_lt2 … HLK) #HiL
+elim (ldrop_O1_lt (Ⓕ) L2 i) // -HiL -HL1 -HL12 #I2 #K2 #V2 #HLK2
+elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * [ /2 width=1 by conj/ ]
+#HnT #H1 #H2 elim (IH1 … HnT … HLK1 HLK2) -IH1 -HnT -HLK1 -HLK2 /2 width=1 by conj/
+qed-.
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 54cb06e9f..b97ddd853 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
@@ -211,15 +211,15 @@ table {
    [ { "substitution" * } {
         [ { "lazy equivalence" * } {
              [ "fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )" "fleq_fleq" * ]
-             [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ]
+             [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
           }
         ]
         [ { "lazy pointwise extension of a relation" * } {
-             [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ]
+             [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" + "llpx_sn_llor" * ]
           }
         ]
         [ { "pointwise union for local environments" * } {
-             [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_alt" * ]
+             [ "llor ( ? ⩖[?] ? ≡ ? )" * ]
           }
         ]
         [ { "context-sensitive exclusion from free variables" * } {
-- 
2.39.2