*)
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 →
λ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.
+
(* Basic inversion lemmas ***************************************************)
fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → ∀s. X = ⋆s → 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/
(* 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.
/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/
(* 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.
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)
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)
(* 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/
+qed-.
+
lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≘ T2).
#T1 #T2 #f1 #H elim H -T1 -T2 -f1
/4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/
]
qed-.
+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).
+#f1 #i1 #i2 #H
+elim (lifts_inv_lref1 … H) -H #j #Hij #H destruct
+/3 width=7 by lifts_lref, at_push/
+qed.
+
lemma lifts_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i).
#l elim l -l /2 width=1 by lifts_lref/
qed.