some restyling ...

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / relocation / lifts.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
index 060f3b8057d843e509201ed69a526d62895c6f01..4ec47cc91e47a93787cc259b65cc02b62541d386 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts.ma
@@ -24,7 +24,7 @@ include "static_2/syntax/term.ma".
 *)
 inductive lifts: rtmap → relation term ≝
 | lifts_sort: ∀f,s. lifts f (⋆s) (⋆s)
-| lifts_lref: ∀f,i1,i2. @⦃i1, f⦄ ≘ i2 → lifts f (#i1) (#i2)
+| lifts_lref: ∀f,i1,i2. @⦃i1,f⦄ ≘ i2 → lifts f (#i1) (#i2)
 | lifts_gref: ∀f,l. lifts f (§l) (§l)
 | lifts_bind: ∀f,p,I,V1,V2,T1,T2.
               lifts f V1 V2 → lifts (⫯f) T1 T2 →
@@ -56,6 +56,10 @@ definition deliftable2_bi: predicate (relation term) ≝
                            λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≘ U1 →
                            ∀T2. ⬆*[f] T2 ≘ U2 → R T1 T2.
 
+definition liftable2_dx: predicate (relation term) ≝
+                         λR. ∀T1,T2. R T1 T2 → ∀f,U2. ⬆*[f] T2 ≘ U2 →
+                         ∃∃U1. ⬆*[f] T1 ≘ U1 & R U1 U2.
+
 definition deliftable2_dx: predicate (relation term) ≝
                            λR. ∀U1,U2. R U1 U2 → ∀f,T2. ⬆*[f] T2 ≘ U2 →
                            ∃∃T1. ⬆*[f] T1 ≘ U1 & R T1 T2.
@@ -76,7 +80,7 @@ lemma lifts_inv_sort1: ∀f,Y,s. ⬆*[f] ⋆s ≘ Y → Y = ⋆s.
 /2 width=4 by lifts_inv_sort1_aux/ qed-.
 
 fact lifts_inv_lref1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀i1. X = #i1 →
-                          ∃∃i2. @⦃i1, f⦄ ≘ i2 & Y = #i2.
+                          ∃∃i2. @⦃i1,f⦄ ≘ i2 & Y = #i2.
 #f #X #Y * -f -X -Y
 [ #f #s #x #H destruct
 | #f #i1 #i2 #Hi12 #x #H destruct /2 width=3 by ex2_intro/
@@ -89,7 +93,7 @@ qed-.
 (* Basic_1: was: lift1_lref *)
 (* Basic_2A1: includes: lift_inv_lref1 lift_inv_lref1_lt lift_inv_lref1_ge *)
 lemma lifts_inv_lref1: ∀f,Y,i1. ⬆*[f] #i1 ≘ Y →
-                       ∃∃i2. @⦃i1, f⦄ ≘ i2 & Y = #i2.
+                       ∃∃i2. @⦃i1,f⦄ ≘ i2 & Y = #i2.
 /2 width=3 by lifts_inv_lref1_aux/ qed-.
 
 fact lifts_inv_gref1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀l. X = §l → Y = §l.
@@ -158,7 +162,7 @@ lemma lifts_inv_sort2: ∀f,X,s. ⬆*[f] X ≘ ⋆s → X = ⋆s.
 /2 width=4 by lifts_inv_sort2_aux/ qed-.
 
 fact lifts_inv_lref2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀i2. Y = #i2 →
-                          ∃∃i1. @⦃i1, f⦄ ≘ i2 & X = #i1.
+                          ∃∃i1. @⦃i1,f⦄ ≘ i2 & X = #i1.
 #f #X #Y * -f -X -Y
 [ #f #s #x #H destruct
 | #f #i1 #i2 #Hi12 #x #H destruct /2 width=3 by ex2_intro/
@@ -171,7 +175,7 @@ qed-.
 (* Basic_1: includes: lift_gen_lref lift_gen_lref_lt lift_gen_lref_false lift_gen_lref_ge *)
 (* Basic_2A1: includes: lift_inv_lref2 lift_inv_lref2_lt lift_inv_lref2_be lift_inv_lref2_ge lift_inv_lref2_plus *)
 lemma lifts_inv_lref2: ∀f,X,i2. ⬆*[f] X ≘ #i2 →
-                       ∃∃i1. @⦃i1, f⦄ ≘ i2 & X = #i1.
+                       ∃∃i1. @⦃i1,f⦄ ≘ i2 & X = #i1.
 /2 width=3 by lifts_inv_lref2_aux/ qed-.
 
 fact lifts_inv_gref2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀l. Y = §l → X = §l.
@@ -230,7 +234,7 @@ lemma lifts_inv_flat2: ∀f:rtmap. ∀I,V2,T2,X. ⬆*[f] X ≘ ⓕ{I}V2.T2 →
 
 lemma lifts_inv_atom1: ∀f,I,Y. ⬆*[f] ⓪{I} ≘ Y →
                        ∨∨ ∃∃s. I = Sort s & Y = ⋆s
-                        | ∃∃i,j. @⦃i, f⦄ ≘ j & I = LRef i & Y = #j
+                        | ∃∃i,j. @⦃i,f⦄ ≘ j & I = LRef i & Y = #j
                         | ∃∃l. I = GRef l & Y = §l.
 #f * #n #Y #H
 [ lapply (lifts_inv_sort1 … H)
@@ -241,7 +245,7 @@ qed-.
 
 lemma lifts_inv_atom2: ∀f,I,X. ⬆*[f] X ≘ ⓪{I} →
                        ∨∨ ∃∃s. X = ⋆s & I = Sort s
-                        | ∃∃i,j. @⦃i, f⦄ ≘ j & X = #i & I = LRef j
+                        | ∃∃i,j. @⦃i,f⦄ ≘ j & X = #i & I = LRef j
                         | ∃∃l. X = §l & I = GRef l.
 #f * #n #X #H
 [ lapply (lifts_inv_sort2 … H)
@@ -333,6 +337,11 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma liftable2_sn_dx (R): symmetric … R → liftable2_sn R → liftable2_dx R.
+#R #H2R #H1R #T1 #T2 #HT12 #f #U2 #HTU2
+elim (H1R … T1 … HTU2) -H1R /3 width=3 by ex2_intro/
+qed-.
+
 lemma deliftable2_sn_dx (R): symmetric … R → deliftable2_sn R → deliftable2_dx R.
 #R #H2R #H1R #U1 #U2 #HU12 #f #T2 #HTU2
 elim (H1R … U1 … HTU2) -H1R /3 width=3 by ex2_intro/
@@ -365,7 +374,7 @@ elim (IHV1 f) -IHV1 #V2 #HV12
 ]
 qed-.
 
-lemma lifts_push_zero (f): ⬆*[⫯f]#O ≘ #0.
+lemma lifts_push_zero (f): ⬆*[⫯f]#0 ≘ #0.
 /2 width=1 by lifts_lref/ qed.
 
 lemma lifts_push_lref (f) (i1) (i2): ⬆*[f]#i1 ≘ #i2 → ⬆*[⫯f]#(↑i1) ≘ #(↑i2).