--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "paths/standard_precedence.ma".
+
+(* ALTERNATIVE STANDARD ORDER ***********************************************)
+
+(* Note: this is p < q *)
+definition slt: relation path ≝ TC … sprec.
+
+interpretation "standard 'less than' on paths"
+ 'lt p q = (slt p q).
+
+lemma slt_step_rc: ∀p,q. p ≺ q → p < q.
+/2 width=1/
+qed.
+
+lemma slt_nil: ∀c,p. ◊ < c::p.
+/2 width=1/
+qed.
+
+lemma slt_skip: dx::◊ < ◊.
+/2 width=1/
+qed.
+
+lemma slt_comp: ∀c,p,q. p < q → c::p < c::q.
+#c #p #q #H elim H -q /3 width=1/ /3 width=3/
+qed.
+
+theorem slt_trans: transitive … slt.
+/2 width=3/
+qed-.
+
+lemma slt_refl: ∀p. p < p.
+#p elim p -p /2 width=1/
+@(slt_trans … (dx::◊)) //
+qed.
(* *)
(**************************************************************************)
-include "subterms/delifting_substitution.ma".
-include "subterms/projections.ma".
+include "subterms/booleanize.ma".
include "paths/standard_order.ma".
(* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************)
(* *)
(**************************************************************************)
-include "paths/path.ma".
+include "paths/standard_precedence.ma".
(* STANDARD ORDER ************************************************************)
-(* Note: standard precedence relation on paths: p ≺ q
- to serve as base for the order relations: p < q and p ≤ q *)
-inductive sprec: relation path ≝
-| sprec_nil : ∀c,q. sprec (◊) (c::q)
-| sprec_rc : ∀p,q. sprec (dx::p) (rc::q)
-| sprec_sn : ∀p,q. sprec (rc::p) (sn::q)
-| sprec_comp: ∀c,p,q. sprec p q → sprec (c::p) (c::q)
-| sprec_skip: sprec (dx::◊) ◊
-.
-
-interpretation "standard 'precedes' on paths"
- 'prec p q = (sprec p q).
-
-lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
- ∃∃q0. p0 ≺ q0 & sn::q0 = q.
-#p #q * -p -q
-[ #c #q #p0 #H destruct
-| #p #q #p0 #H destruct
-| #p #q #p0 #H destruct
-| #c #p #q #Hpq #p0 #H destruct /2 width=3/
-| #p0 #H destruct
-]
-qed-.
-
-lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
-#p #q #H elim H -p -q // /2 width=1/
-[ #p #q * #H destruct
-| #p #q * #H destruct
-| #c #p #q #_ #IHpq * #H destruct /3 width=1/
-]
-qed-.
-
-(* Note: this is p < q *)
-definition slt: relation path ≝ TC … sprec.
-
-interpretation "standard 'less than' on paths"
- 'lt p q = (slt p q).
-
-lemma slt_step_rc: ∀p,q. p ≺ q → p < q.
-/2 width=1/
-qed.
-
-lemma slt_nil: ∀c,p. ◊ < c::p.
-/2 width=1/
-qed.
-
-lemma slt_skip: dx::◊ < ◊.
-/2 width=1/
-qed.
-
-lemma slt_comp: ∀c,p,q. p < q → c::p < c::q.
-#c #p #q #H elim H -q /3 width=1/ /3 width=3/
-qed.
-
-theorem slt_trans: transitive … slt.
-/2 width=3/
-qed-.
-
-lemma slt_refl: ∀p. p < p.
-#p elim p -p /2 width=1/
-@(slt_trans … (dx::◊)) //
-qed.
-
(* Note: this is p ≤ q *)
definition sle: relation path ≝ star … sprec.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "paths/path.ma".
+
+(* STANDARD PRECEDENCE ******************************************************)
+
+(* Note: standard precedence relation on paths: p ≺ q
+ to serve as base for the order relations: p < q and p ≤ q *)
+inductive sprec: relation path ≝
+| sprec_nil : ∀c,q. sprec (◊) (c::q)
+| sprec_rc : ∀p,q. sprec (dx::p) (rc::q)
+| sprec_sn : ∀p,q. sprec (rc::p) (sn::q)
+| sprec_comp: ∀c,p,q. sprec p q → sprec (c::p) (c::q)
+| sprec_skip: sprec (dx::◊) ◊
+.
+
+interpretation "standard 'precedes' on paths"
+ 'prec p q = (sprec p q).
+
+lemma sprec_inv_sn: ∀p,q. p ≺ q → ∀p0. sn::p0 = p →
+ ∃∃q0. p0 ≺ q0 & sn::q0 = q.
+#p #q * -p -q
+[ #c #q #p0 #H destruct
+| #p #q #p0 #H destruct
+| #p #q #p0 #H destruct
+| #c #p #q #Hpq #p0 #H destruct /2 width=3/
+| #p0 #H destruct
+]
+qed-.
+
+lemma sprec_fwd_in_whd: ∀p,q. p ≺ q → in_whd q → in_whd p.
+#p #q #H elim H -p -q // /2 width=1/
+[ #p #q * #H destruct
+| #p #q * #H destruct
+| #c #p #q #_ #IHpq * #H destruct /3 width=1/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "terms/relocating_substitution.ma".
+include "subterms/relocating_substitution.ma".
+
+(* BOOLEAN (EMPTY OR FULL) SUBSET *******************************************)
+
+let rec boolean b M on M ≝ match M with
+[ VRef i ⇒ {b}#i
+| Abst A ⇒ {b}𝛌.(boolean b A)
+| Appl B A ⇒ {b}@(boolean b B).(boolean b A)
+].
+
+interpretation "boolean subset (subterms)"
+ 'ProjectUp b M = (boolean b M).
+
+notation "hvbox( { term 46 b } ⇑ break term 46 M)"
+ non associative with precedence 46
+ for @{ 'ProjectUp $b $M }.
+
+lemma boolean_inv_vref: ∀j,b0,b,M. {b}⇑ M = {b0}#j → b = b0 ∧ M = #j.
+#j #b0 #b * normalize
+[ #i #H destruct /2 width=1/
+| #A #H destruct
+| #B #A #H destruct
+]
+qed-.
+
+lemma boolean_inv_abst: ∀U,b0,b,M. {b}⇑ M = {b0}𝛌.U →
+ ∃∃C. b = b0 & {b}⇑C = U & M = 𝛌.C.
+#U #b0 #b * normalize
+[ #i #H destruct
+| #A #H destruct /2 width=3/
+| #B #A #H destruct
+]
+qed-.
+
+lemma boolean_inv_appl: ∀W,U,b0,b,M. {b}⇑ M = {b0}@W.U →
+ ∃∃D,C. b = b0 & {b}⇑D = W & {b}⇑C = U & M = @D.C.
+#W #U #b0 #b * normalize
+[ #i #H destruct
+| #A #H destruct
+| #B #A #H destruct /2 width=5/
+]
+qed-.
+
+lemma boolean_lift: ∀b,h,M,d. {b}⇑ ↑[d, h] M = ↑[d, h] {b}⇑ M.
+#b #h #M elim M -M normalize //
+qed.
+
+lemma boolean_dsubst: ∀b,N,M,d. {b}⇑ [d ↙ N] M = [d ↙ {b}⇑ N] {b}⇑ M.
+#b #N #M elim M -M [2,3: normalize // ]
+#i #d elim (lt_or_eq_or_gt i d) #Hid
+[ >(sdsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
+| destruct normalize //
+| >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "subterms/carrier.ma".
+include "subterms/boolean.ma".
+
+(* BOOLEANIZE (EMPTY OR FILL) **********************************************)
+
+definition booleanize: bool → subterms → subterms ≝
+ λb,F. {b}⇑⇓F.
+
+interpretation "make boolean (subterms)"
+ 'ProjectSame b F = (booleanize b F).
+
+notation "hvbox( { term 46 b } ⇕ break term 46 F)"
+ non associative with precedence 46
+ for @{ 'ProjectSame $b $F }.
+
+lemma booleanize_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j →
+ ∃∃b1. b = b0 & F = {b1}#j.
+#j #b0 #b #F #H
+elim (boolean_inv_vref … H) -H #H0 #H
+elim (carrier_inv_vref … H) -H /2 width=2/
+qed-.
+
+lemma booleanize_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U →
+ ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T.
+#U #b0 #b #F #H
+elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
+elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
+qed-.
+
+lemma booleanize_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U →
+ ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
+#W #U #b0 #b #F #H
+elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
+elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
+qed-.
+(*
+lemma booleanize_lift: ∀b,h,F,d. {b}⇕ ↑[d, h] F = ↑[d, h] {b}⇕ F.
+#b #h #M elim M -M normalize //
+qed.
+
+lemma booleanize_dsubst: ∀b,G,F,d. {b}⇕ [d ↙ G] F = [d ↙ {b}⇕ G] {b}⇕ F.
+#b #N #M elim M -M [2,3: normalize // ]
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "terms/relocating_substitution.ma".
+include "subterms/relocating_substitution.ma".
+
+(* CARRIER (UNDERLYING TERM) ************************************************)
+
+let rec carrier F on F ≝ match F with
+[ SVRef _ i ⇒ #i
+| SAbst _ T ⇒ 𝛌.(carrier T)
+| SAppl _ V T ⇒ @(carrier V).(carrier T)
+].
+
+interpretation "carrier (subterms)"
+ 'ProjectDown F = (carrier F).
+
+notation "hvbox(⇓ term 46 F)"
+ non associative with precedence 46
+ for @{ 'ProjectDown $F }.
+
+lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j.
+#j * normalize
+[ #b #i #H destruct /2 width=2/
+| #b #T #H destruct
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U.
+#C * normalize
+[ #b #i #H destruct
+| #b #T #H destruct /2 width=4/
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C →
+ ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U.
+#D #C * normalize
+[ #b #i #H destruct
+| #b #T #H destruct
+| #b #V #T #H destruct /2 width=6/
+]
+qed-.
+
+lemma carrier_lift: ∀h,F,d. ⇓ ↑[d, h] F = ↑[d, h] ⇓F.
+#h #F elim F -F normalize //
+qed.
+
+lemma carrier_dsubst: ∀G,F,d. ⇓ [d ↙ G] F = [d ↙ ⇓G] ⇓F.
+#G #F elim F -F [2,3: normalize // ]
+#b #i #d elim (lt_or_eq_or_gt i d) #Hid
+[ >(sdsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
+| destruct normalize //
+| >(sdsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
+]
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "subterms/lift.ma".
-
-(* DELIFTING SUBSTITUTION ***************************************************)
-
-(* Policy: depth (level) metavariables: d, e (as for lift) *)
-let rec sdsubst G d F on F ≝ match F with
-[ SVRef b i ⇒ tri … i d ({b}#i) (↑[i] G) ({b}#(i-1))
-| SAbst b T ⇒ {b}𝛌. (sdsubst G (d+1) T)
-| SAppl b V T ⇒ {b}@ (sdsubst G d V). (sdsubst G d T)
-].
-
-interpretation "delifting substitution for subterms"
- 'DSubst G d F = (sdsubst G d F).
-
-lemma sdsubst_vref_lt: ∀b,i,d,G. i < d → [d ↙ G] {b}#i = {b}#i.
-normalize /2 width=1/
-qed.
-
-lemma sdsubst_vref_eq: ∀b,i,G. [i ↙ G] {b}#i = ↑[i]G.
-normalize //
-qed.
-
-lemma sdsubst_vref_gt: ∀b,i,d,G. d < i → [d ↙ G] {b}#i = {b}#(i-1).
-normalize /2 width=1/
-qed.
-
-theorem sdsubst_slift_le: ∀h,G,F,d1,d2. d2 ≤ d1 →
- [d2 ↙ ↑[d1 - d2, h] G] ↑[d1 + 1, h] F = ↑[d1, h] [d2 ↙ G] F.
-#h #G #F elim F -F
-[ #b #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
- [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
- >(sdsubst_vref_lt … Hid2) >(slift_vref_lt … Hid1) >slift_vref_lt /2 width=1/
- | destruct >sdsubst_vref_eq >slift_vref_lt /2 width=1/
- | >(sdsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
- [ >(slift_vref_lt … Hi1d1) >slift_vref_lt /2 width=1/
- | lapply (ltn_to_ltO … Hid2) #Hi
- >(slift_vref_ge … Hi1d1) >slift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
- ]
- ]
-| normalize #b #T #IHT #d1 #d2 #Hd21
- lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
-| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21
- >IHV -IHV // >IHT -IHT //
-]
-qed.
-
-theorem sdsubst_slift_be: ∀h,G,F,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
- [d2 ↙ G] ↑[d1, h + 1] F = ↑[d1, h] F.
-#h #G #F elim F -F
-[ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
- >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
- | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
- >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) -Hid1
- >sdsubst_vref_gt // /2 width=1/
- ]
-| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21
- >IHT -IHT // /2 width=1/
-| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21
- >IHV -IHV // >IHT -IHT //
-]
-qed.
-
-theorem sdsubst_slift_ge: ∀h,G,F,d1,d2. d1 + h ≤ d2 →
- [d2 ↙ G] ↑[d1, h] F = ↑[d1, h] [d2 - h ↙ G] F.
-#h #G #F elim F -F
-[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
- [ >(sdsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
- lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
- >(slift_vref_lt … Hid1) -Hid1 /2 width=1/
- | >(slift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
- ]
- | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
- >sdsubst_vref_eq >slift_vref_ge // >slift_slift_be // <plus_minus_m_m //
- | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
- lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
- lapply (ltn_to_ltO … Hid2h) #Hi
- >(sdsubst_vref_gt … Hid2h)
- >slift_vref_ge /2 width=1/ >slift_vref_ge /2 width=1/ -Hid1
- >sdsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
- ]
-| normalize #b #T #IHT #d1 #d2 #Hd12
- elim (le_inv_plus_l … Hd12) #_ #Hhd2
- >IHT -IHT /2 width=1/ <plus_minus //
-| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
- >IHV -IHV // >IHT -IHT //
-]
-qed.
-
-theorem sdsubst_sdsubst_ge: ∀G1,G2,F,d1,d2. d1 ≤ d2 →
- [d2 ↙ G2] [d1 ↙ G1] F = [d1 ↙ [d2 - d1 ↙ G2] G1] [d2 + 1 ↙ G2] F.
-#G1 #G2 #F elim F -F
-[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
- >(sdsubst_vref_lt … Hid1) >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
- | destruct >sdsubst_vref_eq >sdsubst_vref_lt /2 width=1/
- | >(sdsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
- [ lapply (ltn_to_ltO … Hid1) #Hi
- >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
- | destruct /2 width=1/
- | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
- >(sdsubst_vref_gt … Hid2) >sdsubst_vref_gt /2 width=1/
- >sdsubst_vref_gt // /2 width=1/
- ]
- ]
-| normalize #b #T #IHT #d1 #d2 #Hd12
- lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
-| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
- >IHV -IHV // >IHT -IHT //
-]
-qed.
-
-theorem sdsubst_sdsubst_lt: ∀G1,G2,F,d1,d2. d2 < d1 →
- [d2 ↙ [d1 - d2 -1 ↙ G1] G2] [d1 ↙ G1] F = [d1 - 1 ↙ G1] [d2 ↙ G2] F.
-#G1 #G2 #F #d1 #d2 #Hd21
-lapply (ltn_to_ltO … Hd21) #Hd1
->sdsubst_sdsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
-qed.
-
-definition sdsubstable_dx: predicate (relation subterms) ≝ λR.
- ∀G,F1,F2. R F1 F2 → ∀d. R ([d ↙ G] F1) ([d ↙ G] F2).
-(*
-definition sdsubstable: predicate (relation subterms) ≝ λR.
- ∀G1,G2. R G1 G2 → ∀F1,F2. R F1 F2 → ∀d. R ([d ↙ G1] F1) ([d ↙ G2] F2).
-
-lemma star_sdsubstable_dx: ∀R. sdsubstable_dx R → sdsubstable_dx (star … R).
-#R #HR #G #F1 #F2 #H elim H -F2 // /3 width=3/
-qed.
-
-lemma lstar_sdsubstable_dx: ∀S,R. (∀a. sdsubstable_dx (R a)) →
- ∀l. sdsubstable_dx (lstar S … R l).
-#S #R #HR #l #G #F1 #F2 #H
-@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
-qed.
-
-lemma star_sdsubstable: ∀R. reflexive ? R →
- sdsubstable R → sdsubstable (star … R).
-#R #H1R #H2 #G1 #G2 #H elim H -G2 /3 width=1/ /3 width=5/
-qed.
-*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "subterms/subterms.ma".
-
-(* RELOCATION FOR SUBTERMS **************************************************)
-
-let rec slift h d E on E ≝ match E with
-[ SVRef b i ⇒ {b}#(tri … i d i (i + h) (i + h))
-| SAbst b T ⇒ {b}𝛌.(slift h (d+1) T)
-| SAppl b V T ⇒ {b}@(slift h d V).(slift h d T)
-].
-
-interpretation "relocation for subterms" 'Lift h d E = (slift h d E).
-
-lemma slift_vref_lt: ∀b,d,h,i. i < d → ↑[d, h] {b}#i = {b}#i.
-normalize /3 width=1/
-qed.
-
-lemma slift_vref_ge: ∀b,d,h,i. d ≤ i → ↑[d, h] {b}#i = {b}#(i+h).
-#b #d #h #i #H elim (le_to_or_lt_eq … H) -H
-normalize // /3 width=1/
-qed.
-
-lemma slift_id: ∀E,d. ↑[d, 0] E = E.
-#E elim E -E
-[ #b #i #d elim (lt_or_ge i d) /2 width=1/
-| /3 width=1/
-| /3 width=1/
-]
-qed.
-
-lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E = {b0}#j.
-#b0 #j #d #Hjd #h * normalize
-[ #b #i elim (lt_or_eq_or_gt i d) #Hid
- [ >(tri_lt ???? … Hid) -Hid -Hjd //
- | #H destruct >tri_eq in Hjd; #H
- elim (plus_lt_false … H)
- | >(tri_gt ???? … Hid)
- lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
- elim (plus_lt_false … H)
- ]
-| #b #T #H destruct
-| #b #V #T #H destruct
-]
-qed.
-
-lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j →
- d + h ≤ j ∧ E = {b0}#(j-h).
-#b0 #j #d #Hdj #h * normalize
-[ #b #i elim (lt_or_eq_or_gt i d) #Hid
- [ >(tri_lt ???? … Hid) #H destruct
- lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
- elim (lt_refl_false … H)
- | #H -Hdj destruct /2 width=1/
- | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
- ]
-| #b #T #H destruct
-| #b #V #T #H destruct
-]
-qed-.
-
-lemma slift_inv_vref_be: ∀b0,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {b0}#j → ⊥.
-#b0 #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E
-lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
-elim (lt_refl_false … H)
-qed-.
-
-lemma slift_inv_vref_ge_plus: ∀b0,j,d,h. d + h ≤ j →
- ∀E. ↑[d, h] E = {b0}#j → E = {b0}#(j-h).
-#b0 #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/
-qed.
-
-lemma slift_inv_abst: ∀b0,U,d,h,E. ↑[d, h] E = {b0}𝛌.U →
- ∃∃T. ↑[d+1, h] T = U & E = {b0}𝛌.T.
-#b0 #U #d #h * normalize
-[ #b #i #H destruct
-| #b #T #H destruct /2 width=3/
-| #b #V #T #H destruct
-]
-qed-.
-
-lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U →
- ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T.
-#b0 #W #U #d #h * normalize
-[ #b #i #H destruct
-| #b #T #H destruct
-| #b #V #T #H destruct /2 width=5/
-]
-qed-.
-
-theorem slift_slift_le: ∀h1,h2,E,d1,d2. d2 ≤ d1 →
- ↑[d2, h2] ↑[d1, h1] E = ↑[d1 + h2, h1] ↑[d2, h2] E.
-#h1 #h2 #E elim E -E
-[ #b #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
- [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
- >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid2)
- >slift_vref_lt // /2 width=1/
- | >(slift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
- [ >(slift_vref_lt … Hid1) >(slift_vref_ge … Hid2)
- >slift_vref_lt // -d2 /2 width=1/
- | >(slift_vref_ge … Hid1) >slift_vref_ge /2 width=1/
- >slift_vref_ge // /2 width=1/
- ]
- ]
-| normalize #b #T #IHT #d1 #d2 #Hd21 >IHT // /2 width=1/
-| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21 >IHV >IHT //
-]
-qed.
-
-theorem slift_slift_be: ∀h1,h2,E,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
- ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1 + h2] E.
-#h1 #h2 #E elim E -E
-[ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
- >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
- | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
- >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) /2 width=1/
- ]
-| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21 >IHT // /2 width=1/
-| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21 >IHV >IHT //
-]
-qed.
-
-theorem slift_slift_ge: ∀h1,h2,E,d1,d2. d1 + h1 ≤ d2 →
- ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1] ↑[d2 - h1, h2] E.
-#h1 #h2 #E #d1 #d2 #Hd12
->(slift_slift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
-qed.
-
-(* Note: this is "∀h,d. injective … (slift h d)" *)
-theorem slift_inj: ∀h,E1,E2,d. ↑[d, h] E2 = ↑[d, h] E1 → E2 = E1.
-#h #E1 elim E1 -E1
-[ #b #i #E2 #d #H elim (lt_or_ge i d) #Hid
- [ >(slift_vref_lt … Hid) in H; #H
- >(slift_inv_vref_lt … Hid … H) -E2 -d -h //
- | >(slift_vref_ge … Hid) in H; #H
- >(slift_inv_vref_ge_plus … H) -E2 // /2 width=1/
- ]
-| normalize #b #T1 #IHT1 #E2 #d #H
- elim (slift_inv_abst … H) -H #T2 #HT12 #H destruct
- >(IHT1 … HT12) -IHT1 -T2 //
-| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d #H
- elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- >(IHV1 … HV12) -IHV1 -V2 >(IHT1 … HT12) -IHT1 -T2 //
-]
-qed-.
-
-theorem slift_inv_slift_le: ∀h1,h2,E1,E2,d1,d2. d2 ≤ d1 →
- ↑[d2, h2] E2 = ↑[d1 + h2, h1] E1 →
- ∃∃E. ↑[d1, h1] E = E2 & ↑[d2, h2] E = E1.
-#h1 #h2 #E1 elim E1 -E1
-[ #b #i #E2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
- [ >(slift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
- [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
- >(slift_inv_vref_lt … Hid2 … H) -E2 /3 width=3/
- | elim (slift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
- elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
- @(ex2_intro … ({b}#(i-h2))) [ /4 width=1/ ] -Hid1
- >slift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
- ]
- | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
- lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
- elim (le_inv_plus_l … Hdh2i) #Hd2i #_
- >(slift_vref_ge … Hid1) #H -Hid1
- >(slift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
- @(ex2_intro … ({b}#(i-h2))) (**) (* auto: needs some help here *)
- [ >slift_vref_ge // -Hd1i /3 width=1/
- | >slift_vref_ge // -Hd2i -Hd1i /3 width=1/
- ]
- ]
-| normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd21 #H
- elim (slift_inv_abst … H) -H >plus_plus_comm_23 #T2 #HT12 #H destruct
- elim (IHT1 … HT12) -IHT1 -HT12 /2 width=1/ -Hd21 #T #HT2 #HT1
- @(ex2_intro … ({b}𝛌.T)) normalize //
-| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd21 #H
- elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- elim (IHV1 … HV12) -IHV1 -HV12 // #V #HV2 #HV1
- elim (IHT1 … HT12) -IHT1 -HT12 // -Hd21 #T #HT2 #HT1
- @(ex2_intro … ({b}@V.T)) normalize //
-]
-qed-.
-
-theorem slift_inv_slift_be: ∀h1,h2,E1,E2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
- ↑[d2, h2] E2 = ↑[d1, h1 + h2] E1 → ↑[d1, h1] E1 = E2.
-#h1 #h2 #E1 elim E1 -E1
-[ #b #i #E2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
- >(slift_vref_lt … Hid1) #H >(slift_inv_vref_lt … Hid2 … H) -h2 -E2 -d2 /2 width=1/
- | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
- >(slift_vref_ge … Hid1) #H >(slift_inv_vref_ge_plus … H) -E2 /2 width=1/
- ]
-| normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H
- elim (slift_inv_abst … H) -H #T #HT12 #H destruct
- >(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
-| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H
- elim (slift_inv_appl … H) -H #V #T #HV12 #HT12 #H destruct
- >(IHV1 … HV12) -IHV1 -HV12 // >(IHT1 … HT12) -IHT1 -HT12 //
-]
-qed-.
-
-theorem slift_inv_slift_ge: ∀h1,h2,E1,E2,d1,d2. d1 + h1 ≤ d2 →
- ↑[d2, h2] E2 = ↑[d1, h1] E1 →
- ∃∃E. ↑[d1, h1] E = E2 & ↑[d2 - h1, h2] E = E1.
-#h1 #h2 #E1 #E2 #d1 #d2 #Hd12 #H
-elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
-lapply (sym_eq subterms … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
-elim (slift_inv_slift_le … Hd12 … H) -H -Hd12 /2 width=3/
-qed-.
-
-definition sliftable: predicate (relation subterms) ≝ λR.
- ∀h,F1,F2. R F1 F2 → ∀d. R (↑[d, h] F1) (↑[d, h] F2).
-
-definition sdeliftable_sn: predicate (relation subterms) ≝ λR.
- ∀h,G1,G2. R G1 G2 → ∀d,F1. ↑[d, h] F1 = G1 →
- ∃∃F2. R F1 F2 & ↑[d, h] F2 = G2.
-(*
-lemma star_sliftable: ∀R. sliftable R → sliftable (star … R).
-#R #HR #h #F1 #F2 #H elim H -F2 // /3 width=3/
-qed.
-
-lemma star_deliftable_sn: ∀R. sdeliftable_sn R → sdeliftable_sn (star … R).
-#R #HR #h #G1 #G2 #H elim H -G2 /2 width=3/
-#G #G2 #_ #HG2 #IHG1 #d #F1 #HFG1
-elim (IHG1 … HFG1) -G1 #F #HF1 #HFG
-elim (HR … HG2 … HFG) -G /3 width=3/
-qed-.
-
-lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) →
- ∀l. sliftable (lstar S … R l).
-#S #R #HR #l #h #F1 #F2 #H
-@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
-qed.
-
-lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) →
- ∀l. sdeliftable_sn (lstar S … R l).
-#S #R #HR #l #h #G1 #G2 #H
-@(lstar_ind_l ????????? H) -l -G1 /2 width=3/
-#a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1
-elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG
-elim (IHG2 … HFG) -G /3 width=3/
-qed-.
-*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "terms/term.ma".
-include "subterms/subterms.ma".
-
-(* PROJECTIONS **************************************************************)
-
-(* Note: the boolean subset of subterms *)
-let rec boolean b M on M ≝ match M with
-[ VRef i ⇒ {b}#i
-| Abst A ⇒ {b}𝛌.(boolean b A)
-| Appl B A ⇒ {b}@(boolean b B).(boolean b A)
-].
-
-interpretation "boolean subset (subterms)"
- 'ProjectUp b M = (boolean b M).
-
-notation "hvbox( { term 46 b } ⇑ break term 46 M)"
- non associative with precedence 46
- for @{ 'ProjectUp $b $M }.
-
-lemma boolean_inv_vref: ∀j,b0,b,M. {b}⇑ M = {b0}#j → b = b0 ∧ M = #j.
-#j #b0 #b * normalize
-[ #i #H destruct /2 width=1/
-| #A #H destruct
-| #B #A #H destruct
-]
-qed-.
-
-lemma boolean_inv_abst: ∀U,b0,b,M. {b}⇑ M = {b0}𝛌.U →
- ∃∃C. b = b0 & {b}⇑C = U & M = 𝛌.C.
-#U #b0 #b * normalize
-[ #i #H destruct
-| #A #H destruct /2 width=3/
-| #B #A #H destruct
-]
-qed-.
-
-lemma boolean_inv_appl: ∀W,U,b0,b,M. {b}⇑ M = {b0}@W.U →
- ∃∃D,C. b = b0 & {b}⇑D = W & {b}⇑C = U & M = @D.C.
-#W #U #b0 #b * normalize
-[ #i #H destruct
-| #A #H destruct
-| #B #A #H destruct /2 width=5/
-]
-qed-.
-
-(* Note: the carrier (underlying term) of a subset of subterms *)
-let rec carrier F on F ≝ match F with
-[ SVRef _ i ⇒ #i
-| SAbst _ T ⇒ 𝛌.(carrier T)
-| SAppl _ V T ⇒ @(carrier V).(carrier T)
-].
-
-interpretation "carrier (subterms)"
- 'ProjectDown F = (carrier F).
-
-notation "hvbox(⇓ term 46 F)"
- non associative with precedence 46
- for @{ 'ProjectDown $F }.
-
-lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j.
-#j * normalize
-[ #b #i #H destruct /2 width=2/
-| #b #T #H destruct
-| #b #V #T #H destruct
-]
-qed-.
-
-lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U.
-#C * normalize
-[ #b #i #H destruct
-| #b #T #H destruct /2 width=4/
-| #b #V #T #H destruct
-]
-qed-.
-
-lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C →
- ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U.
-#D #C * normalize
-[ #b #i #H destruct
-| #b #T #H destruct
-| #b #V #T #H destruct /2 width=6/
-]
-qed-.
-
-definition mk_boolean: bool → subterms → subterms ≝
- λb,F. {b}⇑⇓F.
-
-interpretation "make boolean (subterms)"
- 'ProjectSame b F = (mk_boolean b F).
-
-notation "hvbox( { term 46 b } ⇕ break term 46 F)"
- non associative with precedence 46
- for @{ 'ProjectSame $b $F }.
-
-lemma mk_boolean_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j →
- ∃∃b1. b = b0 & F = {b1}#j.
-#j #b0 #b #F #H
-elim (boolean_inv_vref … H) -H #H0 #H
-elim (carrier_inv_vref … H) -H /2 width=2/
-qed-.
-
-lemma mk_boolean_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U →
- ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T.
-#U #b0 #b #F #H
-elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
-elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
-qed-.
-
-lemma mk_boolean_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U →
- ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
-#W #U #b0 #b #F #H
-elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
-elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "subterms/relocation.ma".
+
+(* RELOCATING SUBSTITUTION **************************************************)
+
+(* Policy: depth (level) metavariables: d, e (as for lift) *)
+let rec sdsubst G d F on F ≝ match F with
+[ SVRef b i ⇒ tri … i d ({b}#i) (↑[i] G) ({b}#(i-1))
+| SAbst b T ⇒ {b}𝛌. (sdsubst G (d+1) T)
+| SAppl b V T ⇒ {b}@ (sdsubst G d V). (sdsubst G d T)
+].
+
+interpretation "relocating substitution for subterms"
+ 'DSubst G d F = (sdsubst G d F).
+
+lemma sdsubst_vref_lt: ∀b,i,d,G. i < d → [d ↙ G] {b}#i = {b}#i.
+normalize /2 width=1/
+qed.
+
+lemma sdsubst_vref_eq: ∀b,i,G. [i ↙ G] {b}#i = ↑[i]G.
+normalize //
+qed.
+
+lemma sdsubst_vref_gt: ∀b,i,d,G. d < i → [d ↙ G] {b}#i = {b}#(i-1).
+normalize /2 width=1/
+qed.
+
+theorem sdsubst_slift_le: ∀h,G,F,d1,d2. d2 ≤ d1 →
+ [d2 ↙ ↑[d1 - d2, h] G] ↑[d1 + 1, h] F = ↑[d1, h] [d2 ↙ G] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+ >(sdsubst_vref_lt … Hid2) >(slift_vref_lt … Hid1) >slift_vref_lt /2 width=1/
+ | destruct >sdsubst_vref_eq >slift_vref_lt /2 width=1/
+ | >(sdsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
+ [ >(slift_vref_lt … Hi1d1) >slift_vref_lt /2 width=1/
+ | lapply (ltn_to_ltO … Hid2) #Hi
+ >(slift_vref_ge … Hi1d1) >slift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
+ ]
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd21
+ lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21
+ >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_slift_be: ∀h,G,F,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+ [d2 ↙ G] ↑[d1, h + 1] F = ↑[d1, h] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
+ | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+ >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) -Hid1
+ >sdsubst_vref_gt // /2 width=1/
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21
+ >IHT -IHT // /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21
+ >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_slift_ge: ∀h,G,F,d1,d2. d1 + h ≤ d2 →
+ [d2 ↙ G] ↑[d1, h] F = ↑[d1, h] [d2 - h ↙ G] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
+ [ >(sdsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
+ lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
+ >(slift_vref_lt … Hid1) -Hid1 /2 width=1/
+ | >(slift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
+ ]
+ | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
+ >sdsubst_vref_eq >slift_vref_ge // >slift_slift_be // <plus_minus_m_m //
+ | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
+ lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
+ lapply (ltn_to_ltO … Hid2h) #Hi
+ >(sdsubst_vref_gt … Hid2h)
+ >slift_vref_ge /2 width=1/ >slift_vref_ge /2 width=1/ -Hid1
+ >sdsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd12
+ elim (le_inv_plus_l … Hd12) #_ #Hhd2
+ >IHT -IHT /2 width=1/ <plus_minus //
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
+ >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_sdsubst_ge: ∀G1,G2,F,d1,d2. d1 ≤ d2 →
+ [d2 ↙ G2] [d1 ↙ G1] F = [d1 ↙ [d2 - d1 ↙ G2] G1] [d2 + 1 ↙ G2] F.
+#G1 #G2 #F elim F -F
+[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
+ >(sdsubst_vref_lt … Hid1) >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
+ | destruct >sdsubst_vref_eq >sdsubst_vref_lt /2 width=1/
+ | >(sdsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
+ [ lapply (ltn_to_ltO … Hid1) #Hi
+ >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
+ | destruct /2 width=1/
+ | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
+ >(sdsubst_vref_gt … Hid2) >sdsubst_vref_gt /2 width=1/
+ >sdsubst_vref_gt // /2 width=1/
+ ]
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd12
+ lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
+ >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_sdsubst_lt: ∀G1,G2,F,d1,d2. d2 < d1 →
+ [d2 ↙ [d1 - d2 -1 ↙ G1] G2] [d1 ↙ G1] F = [d1 - 1 ↙ G1] [d2 ↙ G2] F.
+#G1 #G2 #F #d1 #d2 #Hd21
+lapply (ltn_to_ltO … Hd21) #Hd1
+>sdsubst_sdsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
+qed.
+
+definition sdsubstable_dx: predicate (relation subterms) ≝ λR.
+ ∀G,F1,F2. R F1 F2 → ∀d. R ([d ↙ G] F1) ([d ↙ G] F2).
+(*
+definition sdsubstable: predicate (relation subterms) ≝ λR.
+ ∀G1,G2. R G1 G2 → ∀F1,F2. R F1 F2 → ∀d. R ([d ↙ G1] F1) ([d ↙ G2] F2).
+
+lemma star_sdsubstable_dx: ∀R. sdsubstable_dx R → sdsubstable_dx (star … R).
+#R #HR #G #F1 #F2 #H elim H -F2 // /3 width=3/
+qed.
+*)
+lemma lstar_sdsubstable_dx: ∀S,R. (∀a. sdsubstable_dx (R a)) →
+ ∀l. sdsubstable_dx (lstar S … R l).
+#S #R #HR #l #G #F1 #F2 #H
+@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+qed.
+(*
+lemma star_sdsubstable: ∀R. reflexive ? R →
+ sdsubstable R → sdsubstable (star … R).
+#R #H1R #H2 #G1 #G2 #H elim H -G2 /3 width=1/ /3 width=5/
+qed.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "subterms/subterms.ma".
+
+(* RELOCATION FOR SUBTERMS **************************************************)
+
+let rec slift h d E on E ≝ match E with
+[ SVRef b i ⇒ {b}#(tri … i d i (i + h) (i + h))
+| SAbst b T ⇒ {b}𝛌.(slift h (d+1) T)
+| SAppl b V T ⇒ {b}@(slift h d V).(slift h d T)
+].
+
+interpretation "relocation for subterms" 'Lift h d E = (slift h d E).
+
+lemma slift_vref_lt: ∀b,d,h,i. i < d → ↑[d, h] {b}#i = {b}#i.
+normalize /3 width=1/
+qed.
+
+lemma slift_vref_ge: ∀b,d,h,i. d ≤ i → ↑[d, h] {b}#i = {b}#(i+h).
+#b #d #h #i #H elim (le_to_or_lt_eq … H) -H
+normalize // /3 width=1/
+qed.
+
+lemma slift_id: ∀E,d. ↑[d, 0] E = E.
+#E elim E -E
+[ #b #i #d elim (lt_or_ge i d) /2 width=1/
+| /3 width=1/
+| /3 width=1/
+]
+qed.
+
+lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E = {b0}#j.
+#b0 #j #d #Hjd #h * normalize
+[ #b #i elim (lt_or_eq_or_gt i d) #Hid
+ [ >(tri_lt ???? … Hid) -Hid -Hjd //
+ | #H destruct >tri_eq in Hjd; #H
+ elim (plus_lt_false … H)
+ | >(tri_gt ???? … Hid)
+ lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
+ elim (plus_lt_false … H)
+ ]
+| #b #T #H destruct
+| #b #V #T #H destruct
+]
+qed.
+
+lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j →
+ d + h ≤ j ∧ E = {b0}#(j-h).
+#b0 #j #d #Hdj #h * normalize
+[ #b #i elim (lt_or_eq_or_gt i d) #Hid
+ [ >(tri_lt ???? … Hid) #H destruct
+ lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
+ elim (lt_refl_false … H)
+ | #H -Hdj destruct /2 width=1/
+ | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
+ ]
+| #b #T #H destruct
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma slift_inv_vref_be: ∀b0,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {b0}#j → ⊥.
+#b0 #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E
+lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
+elim (lt_refl_false … H)
+qed-.
+
+lemma slift_inv_vref_ge_plus: ∀b0,j,d,h. d + h ≤ j →
+ ∀E. ↑[d, h] E = {b0}#j → E = {b0}#(j-h).
+#b0 #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/
+qed.
+
+lemma slift_inv_abst: ∀b0,U,d,h,E. ↑[d, h] E = {b0}𝛌.U →
+ ∃∃T. ↑[d+1, h] T = U & E = {b0}𝛌.T.
+#b0 #U #d #h * normalize
+[ #b #i #H destruct
+| #b #T #H destruct /2 width=3/
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U →
+ ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T.
+#b0 #W #U #d #h * normalize
+[ #b #i #H destruct
+| #b #T #H destruct
+| #b #V #T #H destruct /2 width=5/
+]
+qed-.
+
+theorem slift_slift_le: ∀h1,h2,E,d1,d2. d2 ≤ d1 →
+ ↑[d2, h2] ↑[d1, h1] E = ↑[d1 + h2, h1] ↑[d2, h2] E.
+#h1 #h2 #E elim E -E
+[ #b #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+ >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid2)
+ >slift_vref_lt // /2 width=1/
+ | >(slift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
+ [ >(slift_vref_lt … Hid1) >(slift_vref_ge … Hid2)
+ >slift_vref_lt // -d2 /2 width=1/
+ | >(slift_vref_ge … Hid1) >slift_vref_ge /2 width=1/
+ >slift_vref_ge // /2 width=1/
+ ]
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd21 >IHT // /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21 >IHV >IHT //
+]
+qed.
+
+theorem slift_slift_be: ∀h1,h2,E,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
+ ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1 + h2] E.
+#h1 #h2 #E elim E -E
+[ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
+ | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
+ >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) /2 width=1/
+ ]
+| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21 >IHT // /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21 >IHV >IHT //
+]
+qed.
+
+theorem slift_slift_ge: ∀h1,h2,E,d1,d2. d1 + h1 ≤ d2 →
+ ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1] ↑[d2 - h1, h2] E.
+#h1 #h2 #E #d1 #d2 #Hd12
+>(slift_slift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
+qed.
+
+(* Note: this is "∀h,d. injective … (slift h d)" *)
+theorem slift_inj: ∀h,E1,E2,d. ↑[d, h] E2 = ↑[d, h] E1 → E2 = E1.
+#h #E1 elim E1 -E1
+[ #b #i #E2 #d #H elim (lt_or_ge i d) #Hid
+ [ >(slift_vref_lt … Hid) in H; #H
+ >(slift_inv_vref_lt … Hid … H) -E2 -d -h //
+ | >(slift_vref_ge … Hid) in H; #H
+ >(slift_inv_vref_ge_plus … H) -E2 // /2 width=1/
+ ]
+| normalize #b #T1 #IHT1 #E2 #d #H
+ elim (slift_inv_abst … H) -H #T2 #HT12 #H destruct
+ >(IHT1 … HT12) -IHT1 -T2 //
+| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d #H
+ elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ >(IHV1 … HV12) -IHV1 -V2 >(IHT1 … HT12) -IHT1 -T2 //
+]
+qed-.
+
+theorem slift_inv_slift_le: ∀h1,h2,E1,E2,d1,d2. d2 ≤ d1 →
+ ↑[d2, h2] E2 = ↑[d1 + h2, h1] E1 →
+ ∃∃E. ↑[d1, h1] E = E2 & ↑[d2, h2] E = E1.
+#h1 #h2 #E1 elim E1 -E1
+[ #b #i #E2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
+ [ >(slift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
+ >(slift_inv_vref_lt … Hid2 … H) -E2 /3 width=3/
+ | elim (slift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
+ elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
+ @(ex2_intro … ({b}#(i-h2))) [ /4 width=1/ ] -Hid1
+ >slift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
+ ]
+ | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
+ lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
+ elim (le_inv_plus_l … Hdh2i) #Hd2i #_
+ >(slift_vref_ge … Hid1) #H -Hid1
+ >(slift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
+ @(ex2_intro … ({b}#(i-h2))) (**) (* auto: needs some help here *)
+ [ >slift_vref_ge // -Hd1i /3 width=1/
+ | >slift_vref_ge // -Hd2i -Hd1i /3 width=1/
+ ]
+ ]
+| normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd21 #H
+ elim (slift_inv_abst … H) -H >plus_plus_comm_23 #T2 #HT12 #H destruct
+ elim (IHT1 … HT12) -IHT1 -HT12 /2 width=1/ -Hd21 #T #HT2 #HT1
+ @(ex2_intro … ({b}𝛌.T)) normalize //
+| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd21 #H
+ elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IHV1 … HV12) -IHV1 -HV12 // #V #HV2 #HV1
+ elim (IHT1 … HT12) -IHT1 -HT12 // -Hd21 #T #HT2 #HT1
+ @(ex2_intro … ({b}@V.T)) normalize //
+]
+qed-.
+
+theorem slift_inv_slift_be: ∀h1,h2,E1,E2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
+ ↑[d2, h2] E2 = ↑[d1, h1 + h2] E1 → ↑[d1, h1] E1 = E2.
+#h1 #h2 #E1 elim E1 -E1
+[ #b #i #E2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(slift_vref_lt … Hid1) #H >(slift_inv_vref_lt … Hid2 … H) -h2 -E2 -d2 /2 width=1/
+ | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+ >(slift_vref_ge … Hid1) #H >(slift_inv_vref_ge_plus … H) -E2 /2 width=1/
+ ]
+| normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H
+ elim (slift_inv_abst … H) -H #T #HT12 #H destruct
+ >(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
+| normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H
+ elim (slift_inv_appl … H) -H #V #T #HV12 #HT12 #H destruct
+ >(IHV1 … HV12) -IHV1 -HV12 // >(IHT1 … HT12) -IHT1 -HT12 //
+]
+qed-.
+
+theorem slift_inv_slift_ge: ∀h1,h2,E1,E2,d1,d2. d1 + h1 ≤ d2 →
+ ↑[d2, h2] E2 = ↑[d1, h1] E1 →
+ ∃∃E. ↑[d1, h1] E = E2 & ↑[d2 - h1, h2] E = E1.
+#h1 #h2 #E1 #E2 #d1 #d2 #Hd12 #H
+elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
+lapply (sym_eq subterms … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
+elim (slift_inv_slift_le … Hd12 … H) -H -Hd12 /2 width=3/
+qed-.
+
+definition sliftable: predicate (relation subterms) ≝ λR.
+ ∀h,F1,F2. R F1 F2 → ∀d. R (↑[d, h] F1) (↑[d, h] F2).
+
+definition sdeliftable_sn: predicate (relation subterms) ≝ λR.
+ ∀h,G1,G2. R G1 G2 → ∀d,F1. ↑[d, h] F1 = G1 →
+ ∃∃F2. R F1 F2 & ↑[d, h] F2 = G2.
+(*
+lemma star_sliftable: ∀R. sliftable R → sliftable (star … R).
+#R #HR #h #F1 #F2 #H elim H -F2 // /3 width=3/
+qed.
+
+lemma star_deliftable_sn: ∀R. sdeliftable_sn R → sdeliftable_sn (star … R).
+#R #HR #h #G1 #G2 #H elim H -G2 /2 width=3/
+#G #G2 #_ #HG2 #IHG1 #d #F1 #HFG1
+elim (IHG1 … HFG1) -G1 #F #HF1 #HFG
+elim (HR … HG2 … HFG) -G /3 width=3/
+qed-.
+*)
+lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) →
+ ∀l. sliftable (lstar S … R l).
+#S #R #HR #l #h #F1 #F2 #H
+@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+qed.
+
+lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) →
+ ∀l. sdeliftable_sn (lstar S … R l).
+#S #R #HR #l #h #G1 #G2 #H
+@(lstar_ind_l ????????? H) -l -G1 /2 width=3/
+#a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1
+elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG
+elim (IHG2 … HFG) -G /3 width=3/
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "terms/lift.ma".
-
-(* DELIFTING SUBSTITUTION ***************************************************)
-
-(* Policy: depth (level) metavariables: d, e (as for lift) *)
-let rec dsubst N d M on M ≝ match M with
-[ VRef i ⇒ tri … i d (#i) (↑[i] N) (#(i-1))
-| Abst A ⇒ 𝛌. (dsubst N (d+1) A)
-| Appl B A ⇒ @ (dsubst N d B). (dsubst N d A)
-].
-
-interpretation "delifting substitution"
- 'DSubst N d M = (dsubst N d M).
-
-lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i.
-normalize /2 width=1/
-qed.
-
-lemma dsubst_vref_eq: ∀i,N. [i ↙ N] #i = ↑[i]N.
-normalize //
-qed.
-
-lemma dsubst_vref_gt: ∀i,d,N. d < i → [d ↙ N] #i = #(i-1).
-normalize /2 width=1/
-qed.
-
-theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 →
- [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M.
-#h #N #M elim M -M
-[ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
- [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
- >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
- | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/
- | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
- [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/
- | lapply (ltn_to_ltO … Hid2) #Hi
- >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
- ]
- ]
-| normalize #A #IHA #d1 #d2 #Hd21
- lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd21
- >IHB -IHB // >IHA -IHA //
-]
-qed.
-
-theorem dsubst_lift_be: ∀h,N,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
- [d2 ↙ N] ↑[d1, h + 1] M = ↑[d1, h] M.
-#h #N #M elim M -M
-[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
- >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
- | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
- >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1
- >dsubst_vref_gt // /2 width=1/
- ]
-| normalize #A #IHA #d1 #d2 #Hd12 #Hd21
- >IHA -IHA // /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21
- >IHB -IHB // >IHA -IHA //
-]
-qed.
-
-theorem dsubst_lift_ge: ∀h,N,M,d1,d2. d1 + h ≤ d2 →
- [d2 ↙ N] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ N] M.
-#h #N #M elim M -M
-[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
- [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
- lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
- >(lift_vref_lt … Hid1) -Hid1 /2 width=1/
- | >(lift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
- ]
- | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
- >dsubst_vref_eq >lift_vref_ge // >lift_lift_be // <plus_minus_m_m //
- | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
- lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
- lapply (ltn_to_ltO … Hid2h) #Hi
- >(dsubst_vref_gt … Hid2h)
- >lift_vref_ge /2 width=1/ >lift_vref_ge /2 width=1/ -Hid1
- >dsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
- ]
-| normalize #A #IHA #d1 #d2 #Hd12
- elim (le_inv_plus_l … Hd12) #_ #Hhd2
- >IHA -IHA /2 width=1/ <plus_minus //
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd12
- >IHB -IHB // >IHA -IHA //
-]
-qed.
-
-theorem dsubst_dsubst_ge: ∀N1,N2,M,d1,d2. d1 ≤ d2 →
- [d2 ↙ N2] [d1 ↙ N1] M = [d1 ↙ [d2 - d1 ↙ N2] N1] [d2 + 1 ↙ N2] M.
-#N1 #N2 #M elim M -M
-[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
- >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
- | destruct >dsubst_vref_eq >dsubst_vref_lt /2 width=1/
- | >(dsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
- [ lapply (ltn_to_ltO … Hid1) #Hi
- >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
- | destruct /2 width=1/
- | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
- >(dsubst_vref_gt … Hid2) >dsubst_vref_gt /2 width=1/
- >dsubst_vref_gt // /2 width=1/
- ]
- ]
-| normalize #A #IHA #d1 #d2 #Hd12
- lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd12
- >IHB -IHB // >IHA -IHA //
-]
-qed.
-
-theorem dsubst_dsubst_lt: ∀N1,N2,M,d1,d2. d2 < d1 →
- [d2 ↙ [d1 - d2 -1 ↙ N1] N2] [d1 ↙ N1] M = [d1 - 1 ↙ N1] [d2 ↙ N2] M.
-#N1 #N2 #M #d1 #d2 #Hd21
-lapply (ltn_to_ltO … Hd21) #Hd1
->dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
-qed.
-
-definition dsubstable_dx: predicate (relation term) ≝ λR.
- ∀N,M1,M2. R M1 M2 → ∀d. R ([d ↙ N] M1) ([d ↙ N] M2).
-
-definition dsubstable: predicate (relation term) ≝ λR.
- ∀N1,N2. R N1 N2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ N1] M1) ([d ↙ N2] M2).
-
-lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
-#R #HR #N #M1 #M2 #H elim H -M2 // /3 width=3/
-qed.
-
-lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
- ∀l. dsubstable_dx (lstar S … R l).
-#S #R #HR #l #N #M1 #M2 #H
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
-qed.
-
-lemma star_dsubstable: ∀R. reflexive ? R →
- dsubstable R → dsubstable (star … R).
-#R #H1R #H2 #N1 #N2 #H elim H -N2 /3 width=1/ /3 width=5/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "terms/term.ma".
-
-(* RELOCATION ***************************************************************)
-
-(* Policy: level metavariables : d, e
- height metavariables: h, k
-*)
-(* Note: indexes start at zero *)
-let rec lift h d M on M ≝ match M with
-[ VRef i ⇒ #(tri … i d i (i + h) (i + h))
-| Abst A ⇒ 𝛌. (lift h (d+1) A)
-| Appl B A ⇒ @(lift h d B). (lift h d A)
-].
-
-interpretation "relocation" 'Lift h d M = (lift h d M).
-
-lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i.
-normalize /3 width=1/
-qed.
-
-lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
-#d #h #i #H elim (le_to_or_lt_eq … H) -H
-normalize // /3 width=1/
-qed.
-
-lemma lift_id: ∀M,d. ↑[d, 0] M = M.
-#M elim M -M
-[ #i #d elim (lt_or_ge i d) /2 width=1/
-| /3 width=1/
-| /3 width=1/
-]
-qed.
-
-lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j.
-#j #d #Hjd #h * normalize
-[ #i elim (lt_or_eq_or_gt i d) #Hid
- [ >(tri_lt ???? … Hid) -Hid -Hjd //
- | #H destruct >tri_eq in Hjd; #H
- elim (plus_lt_false … H)
- | >(tri_gt ???? … Hid)
- lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
- elim (plus_lt_false … H)
- ]
-| #A #H destruct
-| #B #A #H destruct
-]
-qed.
-
-lemma lift_inv_vref_ge: ∀j,d. d ≤ j → ∀h,M. ↑[d, h] M = #j →
- d + h ≤ j ∧ M = #(j-h).
-#j #d #Hdj #h * normalize
-[ #i elim (lt_or_eq_or_gt i d) #Hid
- [ >(tri_lt ???? … Hid) #H destruct
- lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
- elim (lt_refl_false … H)
- | #H -Hdj destruct /2 width=1/
- | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
- ]
-| #A #H destruct
-| #B #A #H destruct
-]
-qed-.
-
-lemma lift_inv_vref_be: ∀j,d,h. d ≤ j → j < d + h → ∀M. ↑[d, h] M = #j → ⊥.
-#j #d #h #Hdj #Hjdh #M #H elim (lift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -M
-lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
-elim (lt_refl_false … H)
-qed-.
-
-lemma lift_inv_vref_ge_plus: ∀j,d,h. d + h ≤ j →
- ∀M. ↑[d, h] M = #j → M = #(j-h).
-#j #d #h #Hdhj #M #H elim (lift_inv_vref_ge … H) -H // -M /2 width=2/
-qed.
-
-lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
- ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
-#C #d #h * normalize
-[ #i #H destruct
-| #A #H destruct /2 width=3/
-| #B #A #H destruct
-]
-qed-.
-
-lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C →
- ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A.
-#D #C #d #h * normalize
-[ #i #H destruct
-| #A #H destruct
-| #B #A #H destruct /2 width=5/
-]
-qed-.
-
-theorem lift_lift_le: ∀h1,h2,M,d1,d2. d2 ≤ d1 →
- ↑[d2, h2] ↑[d1, h1] M = ↑[d1 + h2, h1] ↑[d2, h2] M.
-#h1 #h2 #M elim M -M
-[ #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
- [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
- >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid2)
- >lift_vref_lt // /2 width=1/
- | >(lift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
- [ >(lift_vref_lt … Hid1) >(lift_vref_ge … Hid2)
- >lift_vref_lt // -d2 /2 width=1/
- | >(lift_vref_ge … Hid1) >lift_vref_ge /2 width=1/
- >lift_vref_ge // /2 width=1/
- ]
- ]
-| normalize #A #IHA #d1 #d2 #Hd21 >IHA // /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd21 >IHB >IHA //
-]
-qed.
-
-theorem lift_lift_be: ∀h1,h2,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
- ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1 + h2] M.
-#h1 #h2 #M elim M -M
-[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
- >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
- | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
- >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) /2 width=1/
- ]
-| normalize #A #IHA #d1 #d2 #Hd12 #Hd21 >IHA // /2 width=1/
-| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 >IHB >IHA //
-]
-qed.
-
-theorem lift_lift_ge: ∀h1,h2,M,d1,d2. d1 + h1 ≤ d2 →
- ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1] ↑[d2 - h1, h2] M.
-#h1 #h2 #M #d1 #d2 #Hd12
->(lift_lift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
-qed.
-
-(* Note: this is "∀h,d. injective … (lift h d)" *)
-theorem lift_inj: ∀h,M1,M2,d. ↑[d, h] M2 = ↑[d, h] M1 → M2 = M1.
-#h #M1 elim M1 -M1
-[ #i #M2 #d #H elim (lt_or_ge i d) #Hid
- [ >(lift_vref_lt … Hid) in H; #H
- >(lift_inv_vref_lt … Hid … H) -M2 -d -h //
- | >(lift_vref_ge … Hid) in H; #H
- >(lift_inv_vref_ge_plus … H) -M2 // /2 width=1/
- ]
-| normalize #A1 #IHA1 #M2 #d #H
- elim (lift_inv_abst … H) -H #A2 #HA12 #H destruct
- >(IHA1 … HA12) -IHA1 -A2 //
-| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d #H
- elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
- >(IHB1 … HB12) -IHB1 -B2 >(IHA1 … HA12) -IHA1 -A2 //
-]
-qed-.
-
-theorem lift_inv_lift_le: ∀h1,h2,M1,M2,d1,d2. d2 ≤ d1 →
- ↑[d2, h2] M2 = ↑[d1 + h2, h1] M1 →
- ∃∃M. ↑[d1, h1] M = M2 & ↑[d2, h2] M = M1.
-#h1 #h2 #M1 elim M1 -M1
-[ #i #M2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
- [ >(lift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
- [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
- >(lift_inv_vref_lt … Hid2 … H) -M2 /3 width=3/
- | elim (lift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
- elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
- @(ex2_intro … (#(i-h2))) [ /4 width=1/ ] -Hid1
- >lift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
- ]
- | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
- lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
- elim (le_inv_plus_l … Hdh2i) #Hd2i #_
- >(lift_vref_ge … Hid1) #H -Hid1
- >(lift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
- @(ex2_intro … (#(i-h2))) (**) (* auto: needs some help here *)
- [ >lift_vref_ge // -Hd1i /3 width=1/
- | >lift_vref_ge // -Hd2i -Hd1i /3 width=1/
- ]
- ]
-| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd21 #H
- elim (lift_inv_abst … H) -H >plus_plus_comm_23 #A2 #HA12 #H destruct
- elim (IHA1 … HA12) -IHA1 -HA12 /2 width=1/ -Hd21 #A #HA2 #HA1
- @(ex2_intro … (𝛌.A)) normalize //
-| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd21 #H
- elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
- elim (IHB1 … HB12) -IHB1 -HB12 // #B #HB2 #HB1
- elim (IHA1 … HA12) -IHA1 -HA12 // -Hd21 #A #HA2 #HA1
- @(ex2_intro … (@B.A)) normalize //
-]
-qed-.
-
-theorem lift_inv_lift_be: ∀h1,h2,M1,M2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
- ↑[d2, h2] M2 = ↑[d1, h1 + h2] M1 → ↑[d1, h1] M1 = M2.
-#h1 #h2 #M1 elim M1 -M1
-[ #i #M2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
- [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
- >(lift_vref_lt … Hid1) #H >(lift_inv_vref_lt … Hid2 … H) -h2 -M2 -d2 /2 width=1/
- | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
- >(lift_vref_ge … Hid1) #H >(lift_inv_vref_ge_plus … H) -M2 /2 width=1/
- ]
-| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
- elim (lift_inv_abst … H) -H #A #HA12 #H destruct
- >(IHA1 … HA12) -IHA1 -HA12 // /2 width=1/
-| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
- elim (lift_inv_appl … H) -H #B #A #HB12 #HA12 #H destruct
- >(IHB1 … HB12) -IHB1 -HB12 // >(IHA1 … HA12) -IHA1 -HA12 //
-]
-qed-.
-
-theorem lift_inv_lift_ge: ∀h1,h2,M1,M2,d1,d2. d1 + h1 ≤ d2 →
- ↑[d2, h2] M2 = ↑[d1, h1] M1 →
- ∃∃M. ↑[d1, h1] M = M2 & ↑[d2 - h1, h2] M = M1.
-#h1 #h2 #M1 #M2 #d1 #d2 #Hd12 #H
-elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
-lapply (sym_eq term … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
-elim (lift_inv_lift_le … Hd12 … H) -H -Hd12 /2 width=3/
-qed-.
-
-definition liftable: predicate (relation term) ≝ λR.
- ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
-
-definition deliftable_sn: predicate (relation term) ≝ λR.
- ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
- ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
-
-lemma star_liftable: ∀R. liftable R → liftable (star … R).
-#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
-qed.
-
-lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
-#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
-#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
-elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
-elim (HR … HN2 … HMN) -N /3 width=3/
-qed-.
-
-lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
- ∀l. liftable (lstar S … R l).
-#S #R #HR #l #h #M1 #M2 #H
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
-qed.
-
-lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
- ∀l. deliftable_sn (lstar S … R l).
-#S #R #HR #l #h #N1 #N2 #H
-@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
-#a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
-elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
-elim (IHN2 … HMN) -N /3 width=3/
-qed-.
(* *)
(**************************************************************************)
-include "terms/delifting_substitution.ma".
+include "terms/relocating_substitution.ma".
(* MULTIPLICITY *************************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "terms/relocation.ma".
+
+(* RELOCATING SUBSTITUTION **************************************************)
+
+(* Policy: depth (level) metavariables: d, e (as for lift) *)
+let rec dsubst N d M on M ≝ match M with
+[ VRef i ⇒ tri … i d (#i) (↑[i] N) (#(i-1))
+| Abst A ⇒ 𝛌. (dsubst N (d+1) A)
+| Appl B A ⇒ @ (dsubst N d B). (dsubst N d A)
+].
+
+interpretation "relocating substitution"
+ 'DSubst N d M = (dsubst N d M).
+
+lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i.
+normalize /2 width=1/
+qed.
+
+lemma dsubst_vref_eq: ∀i,N. [i ↙ N] #i = ↑[i]N.
+normalize //
+qed.
+
+lemma dsubst_vref_gt: ∀i,d,N. d < i → [d ↙ N] #i = #(i-1).
+normalize /2 width=1/
+qed.
+
+theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 →
+ [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M.
+#h #N #M elim M -M
+[ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+ >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
+ | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/
+ | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
+ [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/
+ | lapply (ltn_to_ltO … Hid2) #Hi
+ >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
+ ]
+ ]
+| normalize #A #IHA #d1 #d2 #Hd21
+ lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd21
+ >IHB -IHB // >IHA -IHA //
+]
+qed.
+
+theorem dsubst_lift_be: ∀h,N,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+ [d2 ↙ N] ↑[d1, h + 1] M = ↑[d1, h] M.
+#h #N #M elim M -M
+[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
+ | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+ >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1
+ >dsubst_vref_gt // /2 width=1/
+ ]
+| normalize #A #IHA #d1 #d2 #Hd12 #Hd21
+ >IHA -IHA // /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21
+ >IHB -IHB // >IHA -IHA //
+]
+qed.
+
+theorem dsubst_lift_ge: ∀h,N,M,d1,d2. d1 + h ≤ d2 →
+ [d2 ↙ N] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ N] M.
+#h #N #M elim M -M
+[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
+ [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
+ lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
+ >(lift_vref_lt … Hid1) -Hid1 /2 width=1/
+ | >(lift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
+ ]
+ | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
+ >dsubst_vref_eq >lift_vref_ge // >lift_lift_be // <plus_minus_m_m //
+ | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
+ lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
+ lapply (ltn_to_ltO … Hid2h) #Hi
+ >(dsubst_vref_gt … Hid2h)
+ >lift_vref_ge /2 width=1/ >lift_vref_ge /2 width=1/ -Hid1
+ >dsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
+ ]
+| normalize #A #IHA #d1 #d2 #Hd12
+ elim (le_inv_plus_l … Hd12) #_ #Hhd2
+ >IHA -IHA /2 width=1/ <plus_minus //
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12
+ >IHB -IHB // >IHA -IHA //
+]
+qed.
+
+theorem dsubst_dsubst_ge: ∀N1,N2,M,d1,d2. d1 ≤ d2 →
+ [d2 ↙ N2] [d1 ↙ N1] M = [d1 ↙ [d2 - d1 ↙ N2] N1] [d2 + 1 ↙ N2] M.
+#N1 #N2 #M elim M -M
+[ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
+ >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
+ | destruct >dsubst_vref_eq >dsubst_vref_lt /2 width=1/
+ | >(dsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
+ [ lapply (ltn_to_ltO … Hid1) #Hi
+ >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
+ | destruct /2 width=1/
+ | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
+ >(dsubst_vref_gt … Hid2) >dsubst_vref_gt /2 width=1/
+ >dsubst_vref_gt // /2 width=1/
+ ]
+ ]
+| normalize #A #IHA #d1 #d2 #Hd12
+ lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12
+ >IHB -IHB // >IHA -IHA //
+]
+qed.
+
+theorem dsubst_dsubst_lt: ∀N1,N2,M,d1,d2. d2 < d1 →
+ [d2 ↙ [d1 - d2 -1 ↙ N1] N2] [d1 ↙ N1] M = [d1 - 1 ↙ N1] [d2 ↙ N2] M.
+#N1 #N2 #M #d1 #d2 #Hd21
+lapply (ltn_to_ltO … Hd21) #Hd1
+>dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
+qed.
+
+definition dsubstable_dx: predicate (relation term) ≝ λR.
+ ∀N,M1,M2. R M1 M2 → ∀d. R ([d ↙ N] M1) ([d ↙ N] M2).
+
+definition dsubstable: predicate (relation term) ≝ λR.
+ ∀N1,N2. R N1 N2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ N1] M1) ([d ↙ N2] M2).
+
+lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
+#R #HR #N #M1 #M2 #H elim H -M2 // /3 width=3/
+qed.
+
+lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
+ ∀l. dsubstable_dx (lstar S … R l).
+#S #R #HR #l #N #M1 #M2 #H
+@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+qed.
+
+lemma star_dsubstable: ∀R. reflexive ? R →
+ dsubstable R → dsubstable (star … R).
+#R #H1R #H2 #N1 #N2 #H elim H -N2 /3 width=1/ /3 width=5/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "terms/term.ma".
+
+(* RELOCATION ***************************************************************)
+
+(* Policy: level metavariables : d, e
+ height metavariables: h, k
+*)
+(* Note: indexes start at zero *)
+let rec lift h d M on M ≝ match M with
+[ VRef i ⇒ #(tri … i d i (i + h) (i + h))
+| Abst A ⇒ 𝛌. (lift h (d+1) A)
+| Appl B A ⇒ @(lift h d B). (lift h d A)
+].
+
+interpretation "relocation" 'Lift h d M = (lift h d M).
+
+lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i.
+normalize /3 width=1/
+qed.
+
+lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
+#d #h #i #H elim (le_to_or_lt_eq … H) -H
+normalize // /3 width=1/
+qed.
+
+lemma lift_id: ∀M,d. ↑[d, 0] M = M.
+#M elim M -M
+[ #i #d elim (lt_or_ge i d) /2 width=1/
+| /3 width=1/
+| /3 width=1/
+]
+qed.
+
+lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j.
+#j #d #Hjd #h * normalize
+[ #i elim (lt_or_eq_or_gt i d) #Hid
+ [ >(tri_lt ???? … Hid) -Hid -Hjd //
+ | #H destruct >tri_eq in Hjd; #H
+ elim (plus_lt_false … H)
+ | >(tri_gt ???? … Hid)
+ lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
+ elim (plus_lt_false … H)
+ ]
+| #A #H destruct
+| #B #A #H destruct
+]
+qed.
+
+lemma lift_inv_vref_ge: ∀j,d. d ≤ j → ∀h,M. ↑[d, h] M = #j →
+ d + h ≤ j ∧ M = #(j-h).
+#j #d #Hdj #h * normalize
+[ #i elim (lt_or_eq_or_gt i d) #Hid
+ [ >(tri_lt ???? … Hid) #H destruct
+ lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
+ elim (lt_refl_false … H)
+ | #H -Hdj destruct /2 width=1/
+ | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
+ ]
+| #A #H destruct
+| #B #A #H destruct
+]
+qed-.
+
+lemma lift_inv_vref_be: ∀j,d,h. d ≤ j → j < d + h → ∀M. ↑[d, h] M = #j → ⊥.
+#j #d #h #Hdj #Hjdh #M #H elim (lift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -M
+lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
+elim (lt_refl_false … H)
+qed-.
+
+lemma lift_inv_vref_ge_plus: ∀j,d,h. d + h ≤ j →
+ ∀M. ↑[d, h] M = #j → M = #(j-h).
+#j #d #h #Hdhj #M #H elim (lift_inv_vref_ge … H) -H // -M /2 width=2/
+qed.
+
+lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
+ ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
+#C #d #h * normalize
+[ #i #H destruct
+| #A #H destruct /2 width=3/
+| #B #A #H destruct
+]
+qed-.
+
+lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C →
+ ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A.
+#D #C #d #h * normalize
+[ #i #H destruct
+| #A #H destruct
+| #B #A #H destruct /2 width=5/
+]
+qed-.
+
+theorem lift_lift_le: ∀h1,h2,M,d1,d2. d2 ≤ d1 →
+ ↑[d2, h2] ↑[d1, h1] M = ↑[d1 + h2, h1] ↑[d2, h2] M.
+#h1 #h2 #M elim M -M
+[ #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+ >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid2)
+ >lift_vref_lt // /2 width=1/
+ | >(lift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
+ [ >(lift_vref_lt … Hid1) >(lift_vref_ge … Hid2)
+ >lift_vref_lt // -d2 /2 width=1/
+ | >(lift_vref_ge … Hid1) >lift_vref_ge /2 width=1/
+ >lift_vref_ge // /2 width=1/
+ ]
+ ]
+| normalize #A #IHA #d1 #d2 #Hd21 >IHA // /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd21 >IHB >IHA //
+]
+qed.
+
+theorem lift_lift_be: ∀h1,h2,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
+ ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1 + h2] M.
+#h1 #h2 #M elim M -M
+[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
+ | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
+ >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) /2 width=1/
+ ]
+| normalize #A #IHA #d1 #d2 #Hd12 #Hd21 >IHA // /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 >IHB >IHA //
+]
+qed.
+
+theorem lift_lift_ge: ∀h1,h2,M,d1,d2. d1 + h1 ≤ d2 →
+ ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1] ↑[d2 - h1, h2] M.
+#h1 #h2 #M #d1 #d2 #Hd12
+>(lift_lift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
+qed.
+
+(* Note: this is "∀h,d. injective … (lift h d)" *)
+theorem lift_inj: ∀h,M1,M2,d. ↑[d, h] M2 = ↑[d, h] M1 → M2 = M1.
+#h #M1 elim M1 -M1
+[ #i #M2 #d #H elim (lt_or_ge i d) #Hid
+ [ >(lift_vref_lt … Hid) in H; #H
+ >(lift_inv_vref_lt … Hid … H) -M2 -d -h //
+ | >(lift_vref_ge … Hid) in H; #H
+ >(lift_inv_vref_ge_plus … H) -M2 // /2 width=1/
+ ]
+| normalize #A1 #IHA1 #M2 #d #H
+ elim (lift_inv_abst … H) -H #A2 #HA12 #H destruct
+ >(IHA1 … HA12) -IHA1 -A2 //
+| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d #H
+ elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
+ >(IHB1 … HB12) -IHB1 -B2 >(IHA1 … HA12) -IHA1 -A2 //
+]
+qed-.
+
+theorem lift_inv_lift_le: ∀h1,h2,M1,M2,d1,d2. d2 ≤ d1 →
+ ↑[d2, h2] M2 = ↑[d1 + h2, h1] M1 →
+ ∃∃M. ↑[d1, h1] M = M2 & ↑[d2, h2] M = M1.
+#h1 #h2 #M1 elim M1 -M1
+[ #i #M2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
+ [ >(lift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
+ [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
+ >(lift_inv_vref_lt … Hid2 … H) -M2 /3 width=3/
+ | elim (lift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
+ elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
+ @(ex2_intro … (#(i-h2))) [ /4 width=1/ ] -Hid1
+ >lift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
+ ]
+ | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
+ lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
+ elim (le_inv_plus_l … Hdh2i) #Hd2i #_
+ >(lift_vref_ge … Hid1) #H -Hid1
+ >(lift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
+ @(ex2_intro … (#(i-h2))) (**) (* auto: needs some help here *)
+ [ >lift_vref_ge // -Hd1i /3 width=1/
+ | >lift_vref_ge // -Hd2i -Hd1i /3 width=1/
+ ]
+ ]
+| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd21 #H
+ elim (lift_inv_abst … H) -H >plus_plus_comm_23 #A2 #HA12 #H destruct
+ elim (IHA1 … HA12) -IHA1 -HA12 /2 width=1/ -Hd21 #A #HA2 #HA1
+ @(ex2_intro … (𝛌.A)) normalize //
+| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd21 #H
+ elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
+ elim (IHB1 … HB12) -IHB1 -HB12 // #B #HB2 #HB1
+ elim (IHA1 … HA12) -IHA1 -HA12 // -Hd21 #A #HA2 #HA1
+ @(ex2_intro … (@B.A)) normalize //
+]
+qed-.
+
+theorem lift_inv_lift_be: ∀h1,h2,M1,M2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
+ ↑[d2, h2] M2 = ↑[d1, h1 + h2] M1 → ↑[d1, h1] M1 = M2.
+#h1 #h2 #M1 elim M1 -M1
+[ #i #M2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+ [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+ >(lift_vref_lt … Hid1) #H >(lift_inv_vref_lt … Hid2 … H) -h2 -M2 -d2 /2 width=1/
+ | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+ >(lift_vref_ge … Hid1) #H >(lift_inv_vref_ge_plus … H) -M2 /2 width=1/
+ ]
+| normalize #A1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
+ elim (lift_inv_abst … H) -H #A #HA12 #H destruct
+ >(IHA1 … HA12) -IHA1 -HA12 // /2 width=1/
+| normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
+ elim (lift_inv_appl … H) -H #B #A #HB12 #HA12 #H destruct
+ >(IHB1 … HB12) -IHB1 -HB12 // >(IHA1 … HA12) -IHA1 -HA12 //
+]
+qed-.
+
+theorem lift_inv_lift_ge: ∀h1,h2,M1,M2,d1,d2. d1 + h1 ≤ d2 →
+ ↑[d2, h2] M2 = ↑[d1, h1] M1 →
+ ∃∃M. ↑[d1, h1] M = M2 & ↑[d2 - h1, h2] M = M1.
+#h1 #h2 #M1 #M2 #d1 #d2 #Hd12 #H
+elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
+lapply (sym_eq term … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
+elim (lift_inv_lift_le … Hd12 … H) -H -Hd12 /2 width=3/
+qed-.
+
+definition liftable: predicate (relation term) ≝ λR.
+ ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
+
+definition deliftable_sn: predicate (relation term) ≝ λR.
+ ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
+ ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
+
+lemma star_liftable: ∀R. liftable R → liftable (star … R).
+#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
+qed.
+
+lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
+#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
+#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
+elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
+elim (HR … HN2 … HMN) -N /3 width=3/
+qed-.
+
+lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
+ ∀l. liftable (lstar S … R l).
+#S #R #HR #l #h #M1 #M2 #H
+@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+qed.
+
+lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
+ ∀l. deliftable_sn (lstar S … R l).
+#S #R #HR #l #h #N1 #N2 #H
+@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
+#a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
+elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
+elim (IHN2 … HMN) -N /3 width=3/
+qed-.
(* *)
(**************************************************************************)
-include "terms/lift.ma".
+include "terms/relocation.ma".
(* SIZE *********************************************************************)
projects / helm.git / commitdiff