X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_fqup.ma;h=217534a142f83b7786b580e98040f7eba90986be;hp=9bbc83a891bcd3c61874299e509d5bc0fb126d16;hb=222044da28742b24584549ba86b1805a87def070;hpb=86d7622f88247d83b2c366a722d2994a4af91929

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
index 9bbc83a89..217534a14 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -20,7 +20,7 @@ include "basic_2/static/lsubf_lsubr.ma".
 (* Advanced properties ******************************************************)
 
 (* Note: this replaces lemma 1400 concluding the "big tree" theorem *)
-lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f.
+lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≘ f.
 #L #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L T) -L -T
 #G0 #L0 #T0 #IH #G #L * *
 [ /3 width=2 by frees_sort, ex_intro/
@@ -51,8 +51,8 @@ qed-.
 
 (* Advanced main properties *************************************************)
 
-theorem frees_bind_void: ∀f1,L,V. L ⊢ 𝐅*⦃V⦄ ≡ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅*⦃T⦄ ≡ f2 →
-                         ∀f. f1 ⋓ ⫱f2 ≡ f → ∀p,I. L ⊢ 𝐅*⦃ⓑ{p,I}V.T⦄ ≡ f.
+theorem frees_bind_void: ∀f1,L,V. L ⊢ 𝐅*⦃V⦄ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅*⦃T⦄ ≘ f2 →
+                         ∀f. f1 ⋓ ⫱f2 ≘ f → ∀p,I. L ⊢ 𝐅*⦃ⓑ{p,I}V.T⦄ ≘ f.
 #f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
 elim (frees_total (L.ⓑ{I}V) T) #f0 #Hf0
 lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
@@ -70,7 +70,7 @@ elim (pn_split f2) * #g2 #H destruct
   lapply (sor_comm … Hz) -Hz #Hz
   lapply (sor_mono … f Hz ?) // -Hz #H
   lapply (sor_inv_sle_sn … Hf) -Hf #Hf
-  lapply (frees_eq_repl_back … Hf0 (⫯f) ?) /2 width=5 by eq_next/ -z #Hf0
+  lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by eq_next/ -z #Hf0
   @(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
   /2 width=1 by sor_sle_dx/
 ]
@@ -78,8 +78,8 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma frees_inv_bind_void: ∀f,p,I,L,V,T. L ⊢ 𝐅*⦃ⓑ{p,I}V.T⦄ ≡ f →
-                           ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓧ ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
+lemma frees_inv_bind_void: ∀f,p,I,L,V,T. L ⊢ 𝐅*⦃ⓑ{p,I}V.T⦄ ≘ f →
+                           ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≘ f1 & L.ⓧ ⊢ 𝐅*⦃T⦄ ≘ f2 & f1 ⋓ ⫱f2 ≘ f.
 #f #p #I #L #V #T #H
 elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
 elim (frees_total (L.ⓧ) T) #f0 #Hf0
@@ -99,3 +99,52 @@ elim (pn_split f0) * #g0 #H destruct
   /2 width=3 by sor_comm_23_idem/
 ]
 qed-.
+
+lemma frees_ind_void: ∀Q:relation3 ….
+                      (
+                         ∀f,L,s. 𝐈⦃f⦄ →  Q L (⋆s) f
+                      ) → (
+                         ∀f,i. 𝐈⦃f⦄ →  Q (⋆) (#i) (⫯*[i]↑f)
+                      ) → (
+                         ∀f,I,L,V.
+                         L ⊢ 𝐅*⦃V⦄ ≘ f →  Q L V f→ Q (L.ⓑ{I}V) (#O) (↑f) 
+                      ) → (
+                         ∀f,I,L. 𝐈⦃f⦄ →  Q (L.ⓤ{I}) (#O) (↑f)
+                      ) → (
+                         ∀f,I,L,i.
+                         L ⊢ 𝐅*⦃#i⦄ ≘ f →  Q L (#i) f → Q (L.ⓘ{I}) (#(↑i)) (⫯f)
+                      ) → (
+                         ∀f,L,l. 𝐈⦃f⦄ →  Q L (§l) f
+                      ) → (
+                         ∀f1,f2,f,p,I,L,V,T.
+                         L ⊢ 𝐅*⦃V⦄ ≘ f1 → L.ⓧ ⊢𝐅*⦃T⦄≘ f2 → f1 ⋓ ⫱f2 ≘ f →
+                         Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ{p,I}V.T) f
+                      ) → (
+                         ∀f1,f2,f,I,L,V,T.
+                         L ⊢ 𝐅*⦃V⦄ ≘ f1 → L ⊢𝐅*⦃T⦄ ≘ f2 → f1 ⋓ f2 ≘ f →
+                         Q L V f1 → Q L T f2 → Q L (ⓕ{I}V.T) f
+                      ) →
+                      ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≘ f →  Q L T f.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
+@(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * *
+[ #s #HG #HL #HT #f #H destruct -IH
+  lapply (frees_inv_sort … H) -H /2 width=1 by/
+| cases L -L
+  [ #i #HG #HL #HT #f #H destruct -IH
+    elim (frees_inv_atom … H) -H #g #Hg #H destruct /2 width=1 by/
+  | #L #I * [ cases I -I #I [ | #V ] | #i ] #HG #HL #HT #f #H destruct
+    [ elim (frees_inv_unit … H) -H #g #Hg #H destruct /2 width=1 by/
+    | elim (frees_inv_pair … H) -H #g #Hg #H destruct
+      /4 width=2 by fqu_fqup, fqu_lref_O/
+    | elim (frees_inv_lref … H) -H #g #Hg #H destruct
+      /4 width=2 by fqu_fqup/
+    ]
+  ]
+| #l #HG #HL #HT #f #H destruct -IH
+  lapply (frees_inv_gref … H) -H /2 width=1 by/
+| #p #I #V #T #HG #HL #HT #f #H destruct
+  elim (frees_inv_bind_void … H) -H /3 width=7 by/
+| #I #V #T #HG #HL #HT #f #H destruct
+  elim (frees_inv_flat … H) -H /3 width=7 by/
+]
+qed-.