From aff2f21cec89cf343297ae6bd720fc6573a3aba1 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 30 Nov 2017 11:11:27 +0000
Subject: [PATCH] work in progress with fle ...

---
 .../lambdadelta/basic_2/static/fle.ma         | 51 +++++++++---------
 .../lambdadelta/basic_2/static/fle_fle.ma     | 53 ++++++++++++++++++-
 .../lambdadelta/basic_2/static/fle_fqup.ma    | 53 ++++++++++++-------
 3 files changed, 109 insertions(+), 48 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma
index 1ba1b6c01..1a0a83d6b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma
@@ -14,38 +14,37 @@
 
 include "ground_2/relocation/rtmap_id.ma".
 include "basic_2/notation/relations/subseteq_4.ma".
+include "basic_2/syntax/voids_length.ma".
 include "basic_2/static/frees.ma".
 
 (* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
 
-definition fle: bi_relation lenv term ≝ λL1,T1,L2,T2.
-                ∃∃f1,f2. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f1 ⊆ f2.
+inductive fle (T2) (L2) (T1): predicate lenv ≝
+| fle_intro: ∀f1,f2,L1,n. ⓧ*[n]L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 →
+             |L1| = |L2| → ⫱*[n]f1 ⊆ f2 → fle T2 L2 T1 (ⓧ*[n]L1)
+.
 
 interpretation "free variables inclusion (restricted closure)"
-   'SubSetEq L1 T1 L2 T2 = (fle L1 T1 L2 T2).
+   'SubSetEq L1 T1 L2 T2 = (fle T2 L2 T1 L1).
 
 (* Basic properties *********************************************************)
 
-lemma fle_sort: ∀L1,L2,s1,s2. ⦃L1, ⋆s1⦄ ⊆ ⦃L2, ⋆s2⦄.
-/3 width=5 by frees_sort, sle_refl, ex3_2_intro/ qed.
-
-lemma fle_gref: ∀L1,L2,l1,l2. ⦃L1, §l1⦄ ⊆ ⦃L2, §l2⦄.
-/3 width=5 by frees_gref, sle_refl, ex3_2_intro/ qed.
-
-lemma fle_bind: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
-                ∀I1,I2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ →
-                ∀p. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄.
-#L1 #L2 #V1 #V2 * #f1 #g1 #HV1 #HV2 #Hfg1 #I1 #I2 #T1 #T2 * #f2 #g2 #Hf2 #Hg2 #Hfg2 #p
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
-/4 width=12 by frees_bind, monotonic_sle_sor, sle_tl, ex3_2_intro/
-qed.
-
-lemma fle_flat: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
-                ∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
-                ∀I1,I2. ⦃L1, ⓕ{I1}V1.T1⦄ ⊆ ⦃L2, ⓕ{I2}V2.T2⦄.
-#L1 #L2 #V1 #V2 * #f1 #g1 #HV1 #HV2 #Hfg1 #T1 #T2 * #f2 #g2 #Hf2 #Hg2 #Hfg2 #I1 #I2
-elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_
-elim (sor_isfin_ex g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
-/3 width=12 by frees_flat, monotonic_sle_sor, ex3_2_intro/
-qed.
+lemma fle_sort: ∀L1,L2. |L1| = |L2| → ∀s1,s2. ⦃L1, ⋆s1⦄ ⊆ ⦃L2, ⋆s2⦄.
+/3 width=5 by frees_sort, sle_refl, fle_intro/ qed.
+
+lemma fle_gref: ∀L1,L2. |L1| = |L2| → ∀l1,l2. ⦃L1, §l1⦄ ⊆ ⦃L2, §l2⦄.
+/3 width=5 by frees_gref, sle_refl, fle_intro/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact fle_inv_voids_sn_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
+                           ∀K1,n. |K1| = |L2| → L1 = ⓧ*[n]K1 →
+                           ∃∃f1,f2. ⓧ*[n]K1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n]f1 ⊆ f2.
+#L1 #L2 #T1 #T2 * -L1 #f1 #f2 #L1 #n #Hf1 #Hf2 #HL12 #Hf12 #Y #x #HY #H destruct
+elim (voids_inj_length … H) // -H -HL12 -HY #H1 #H2 destruct
+/2 width=5 by ex3_2_intro/
+qed-.
+
+lemma fle_inv_voids_sn: ∀L1,L2,T1,T2,n. ⦃ⓧ*[n]L1, T1⦄ ⊆ ⦃L2, T2⦄ → |L1| = |L2| →
+                        ∃∃f1,f2. ⓧ*[n]L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & ⫱*[n]f1 ⊆ f2.
+/2 width=3 by fle_inv_voids_sn_aux/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma
index 77b284b11..e756b43f7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fle.ma
@@ -13,13 +13,62 @@
 (**************************************************************************)
 
 include "basic_2/static/frees_frees.ma".
-include "basic_2/static/fle.ma".
+include "basic_2/static/fle_fqup.ma".
 
 (* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
 
-(* Main properties **********************************************************)
+(* Advanced inversion lemmas ************************************************)
+
+lemma fle_inv_voids_sn_frees_dx: ∀L1,L2,T1,T2,n. ⦃ⓧ*[n]L1, T1⦄ ⊆ ⦃L2, T2⦄ →
+                                 |L1| = |L2| → ∀f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 →
+                                 ∃∃f1. ⓧ*[n]L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 & ⫱*[n]f1 ⊆ f2.
+#L1 #L2 #T1 #T2 #n #H #HL12 #f2 #Hf2
+elim (fle_inv_voids_sn … H HL12) -H -HL12 #f1 #g2 #Hf1 #Hg2 #Hfg
+lapply (frees_mono … Hg2 … Hf2) -Hg2 -Hf2 #Hfg2
+lapply (sle_eq_repl_back2 … Hfg … Hfg2) -g2
+/2 width=3 by ex2_intro/
+qed-.
 
+(* Main properties **********************************************************)
+(*
 theorem fle_trans: bi_transitive … fle.
 #L1 #L #T1 #T * #f1 #f #HT1 #HT #Hf1 #L2 #T2 * #g #f2 #Hg #HT2 #Hf2
 /5 width=8 by frees_mono, sle_trans, sle_eq_repl_back2, ex3_2_intro/
 qed-.
+*)
+theorem fle_bind_sn: ∀L1,L2,V1,T1,T. ⦃L1, V1⦄ ⊆ ⦃L2, T⦄ → ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2, T⦄ →
+                     ∀p,I. ⦃L1, ⓑ{p,I}V1.T1⦄ ⊆ ⦃L2, T⦄.
+#L1 #L2 #V1 #T1 #T * -L1 #f1 #x #L1 #n1 #Hf1 #Hx #HL12 #Hf1x
+>voids_succ #H #p #I
+elim (fle_inv_voids_sn_frees_dx … H … Hx) -H // #f2 #Hf2
+<tls_xn #Hf2x
+elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+/4 width=9 by fle_intro, frees_bind_void, sor_inv_sle, sor_tls/
+qed.
+
+theorem fle_flat_sn: ∀L1,L2,V1,T1,T. ⦃L1, V1⦄ ⊆ ⦃L2, T⦄ → ⦃L1, T1⦄ ⊆ ⦃L2, T⦄ →
+                     ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ⊆ ⦃L2, T⦄.
+#L1 #L2 #V1 #T1 #T * -L1 #f1 #x #L1 #n1 #Hf1 #Hx #HL12 #Hf1x #H #I
+elim (fle_inv_voids_sn_frees_dx … H … Hx) -H // #f2 #Hf2 #Hf2x
+elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_
+/4 width=9 by fle_intro, frees_flat, sor_inv_sle, sor_tls/
+qed.
+(*
+lemma fle_bind: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
+                ∀I1,I2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ →
+                ∀p. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄.
+#L1 #L2 #V1 #V2 * #f1 #g1 #HV1 #HV2 #Hfg1 #I1 #I2 #T1 #T2 * #f2 #g2 #Hf2 #Hg2 #Hfg2 #p
+elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+/4 width=12 by frees_bind, monotonic_sle_sor, sle_tl, ex3_2_intro/
+qed.
+
+lemma fle_flat: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
+                ∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
+                ∀I1,I2. ⦃L1, ⓕ{I1}V1.T1⦄ ⊆ ⦃L2, ⓕ{I2}V2.T2⦄.
+#L1 #L2 #V1 #V2 * #f1 #g1 #HV1 #HV2 #Hfg1 #T1 #T2 * #f2 #g2 #Hf2 #Hg2 #Hfg2 #I1 #I2
+elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_
+elim (sor_isfin_ex g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
+/3 width=12 by frees_flat, monotonic_sle_sor, ex3_2_intro/
+qed.
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma
index 23e460341..aeed5c146 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/fle_fqup.ma
@@ -18,31 +18,44 @@ include "basic_2/static/fle.ma".
 (* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
 
 (* Advanced properties ******************************************************)
-
+(*
 lemma fle_refl: bi_reflexive … fle.
 #L #T elim (frees_total L T) /2 width=5 by sle_refl, ex3_2_intro/
 qed.
-
-lemma fle_bind_sn: ∀p,I,L,V,T. ⦃L, V⦄ ⊆ ⦃L, ⓑ{p,I}V.T⦄.
-#p #I #L #V #T
-elim (frees_total L V) #f1 #Hf1
-elim (frees_total (L.ⓑ{I}V) T) #f2 #Hf2
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-/3 width=6 by frees_bind, sor_inv_sle_sn, ex3_2_intro/
+*)
+lemma fle_bind_dx_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
+                      ∀p,I,T2. ⦃L1, V1⦄ ⊆ ⦃L2, ⓑ{p,I}V2.T2⦄.
+#L1 #L2 #V1 #V2 * -L1 #f1 #g1 #L1 #n #Hf1 #Hg1 #HL12 #Hfg1 #p #I #T2
+elim (frees_total (L2.ⓧ) T2) #g2 #Hg2
+elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+/4 width=8 by fle_intro, frees_bind_void, sor_inv_sle_sn, sle_trans/
 qed.
+(*
+lemma fle_bind_dx_dx: ∀L1,L2,T1,T2. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2.ⓧ, T2⦄ →
+                      ∀p,I,V2. ⦃L1.ⓧ, T1⦄ ⊆ ⦃L2, ⓑ{p,I}V2.T2⦄.
+#L1 #L2 #T1 #T2 * -L1 #f2 #g2 #L1 #n #Hf2 #Hg2 #HL12 #Hfg2 #p #I #V2
+elim (frees_total L2 V2) #g1 #Hg1
+elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+@(fle_intro … g … Hf2) /2 width=5 by frees_bind_void/
+@(sle_trans … Hfg1) @(sor_inv_sle_sn … Hg)
+
 
-lemma fle_flat_sn: ∀I,L,V,T. ⦃L, V⦄ ⊆ ⦃L, ⓕ{I}V.T⦄.
-#I #L #V #T
-elim (frees_total L V) #f1 #Hf1
-elim (frees_total L T) #f2 #Hf2
-elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_
-/3 width=6 by frees_flat, sor_inv_sle_sn, ex3_2_intro/
+
+/4 width=8 by fle_intro, frees_bind_void, sor_inv_sle_dx, sle_trans/
+qed.
+*)
+lemma fle_flat_dx_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
+                      ∀I,T2. ⦃L1, V1⦄ ⊆ ⦃L2, ⓕ{I}V2.T2⦄.
+#L1 #L2 #V1 #V2 * -L1 #f1 #g1 #L1 #n #Hf1 #Hg1 #HL12 #Hfg1 #I #T2
+elim (frees_total L2 T2) #g2 #Hg2
+elim (sor_isfin_ex g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
+/4 width=8 by fle_intro, frees_flat, sor_inv_sle_sn, sle_trans/
 qed.
 
-lemma fle_flat_dx: ∀I,L,V,T. ⦃L, T⦄ ⊆ ⦃L, ⓕ{I}V.T⦄.
-#I #L #V #T
-elim (frees_total L V) #f1 #Hf1
-elim (frees_total L T) #f2 #Hf2
-elim (sor_isfin_ex f1 f2) /2 width=3 by frees_fwd_isfin/ #f #Hf #_
-/3 width=6 by frees_flat, sor_inv_sle_dx, ex3_2_intro/
+lemma fle_flat_dx_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
+                      ∀I,V2. ⦃L1, T1⦄ ⊆ ⦃L2, ⓕ{I}V2.T2⦄.
+#L1 #L2 #T1 #T2 * -L1 #f2 #g2 #L1 #n #Hf2 #Hg2 #HL12 #Hfg2 #I #V2
+elim (frees_total L2 V2) #g1 #Hg1
+elim (sor_isfin_ex g1 g2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_
+/4 width=8 by fle_intro, frees_flat, sor_inv_sle_dx, sle_trans/
 qed.
-- 
2.39.2