--- /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 "basic_2/syntax/bind.ma".
+include "basic_2/relocation/lifts.ma".
+
+(* GENERIC RELOCATION FOR BINDERS *******************************************)
+
+definition liftsb: rtmap → relation bind ≝
+ λf. ext2 (lifts f).
+
+interpretation "uniform relocation (binder for local environments)"
+ 'RLiftStar i I1 I2 = (liftsb (uni i) I1 I2).
+
+interpretation "generic relocation (binder for local environments)"
+ 'RLiftStar f I1 I2 = (liftsb f I1 I2).
+
+(* Basic_inversion lemmas **************************************************)
+
+lemma liftsb_inv_unit_sn: ∀f,I,Z2. ⬆*[f] BUnit I ≡ Z2 → Z2 = BUnit I.
+/2 width=2 by ext2_inv_unit_sn/ qed-.
+
+lemma liftsb_inv_pair_sn: ∀f:rtmap. ∀Z2,I,V1. ⬆*[f] BPair I V1 ≡ Z2 →
+ ∃∃V2. ⬆*[f] V1 ≡ V2 & Z2 = BPair I V2.
+/2 width=1 by ext2_inv_pair_sn/ qed-.
+
+lemma liftsb_inv_unit_dx: ∀f,I,Z1. ⬆*[f] Z1 ≡ BUnit I → Z1 = BUnit I.
+/2 width=2 by ext2_inv_unit_dx/ qed-.
+
+lemma liftsb_inv_pair_dx: ∀f:rtmap. ∀Z1,I,V2. ⬆*[f] Z1 ≡ BPair I V2 →
+ ∃∃V1. ⬆*[f] V1 ≡ V2 & Z1 = BPair I V1.
+/2 width=1 by ext2_inv_pair_dx/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma liftsb_eq_repl_back: ∀I1,I2. eq_repl_back … (λf. ⬆*[f] I1 ≡ I2).
+#I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/
+qed-.
+
+lemma liftsb_refl: ∀f. 𝐈⦃f⦄ → reflexive … (liftsb f).
+/3 width=1 by lifts_refl, ext2_refl/ qed.
+
+lemma liftsb_total: ∀I1,f. ∃I2. ⬆*[f] I1 ≡ I2.
+* [2: #I #T1 #f elim (lifts_total T1 f) ]
+/3 width=2 by ext2_unit, ext2_pair, ex_intro/
+qed-.
+
+lemma liftsb_split_trans: ∀f,I1,I2. ⬆*[f] I1 ≡ I2 →
+ ∀f1,f2. f2 ⊚ f1 ≡ f →
+ ∃∃I. ⬆*[f1] I1 ≡ I & ⬆*[f2] I ≡ I2.
+#f #I1 #I2 * -I1 -I2 /2 width=3 by ext2_unit, ex2_intro/
+#I #V1 #V2 #HV12 #f1 #f2 #Hf elim (lifts_split_trans … HV12 … Hf) -f
+/3 width=3 by ext2_pair, ex2_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma liftsb_fwd_isid: ∀f,I1,I2. ⬆*[f] I1 ≡ I2 → 𝐈⦃f⦄ → I1 = I2.
+#f #I1 #I2 * -I1 -I2 /3 width=3 by lifts_fwd_isid, eq_f2/
+qed-.
(* Advanced proprerties *****************************************************)
(* Basic_2A1: includes: lift_inj *)
-lemma lifts_inj: ∀f,T1,U. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2.
+lemma lifts_inj: ∀f. is_inj2 … (lifts f).
#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝 … f)
/3 width=6 by lifts_div3, lifts_fwd_isid/
qed-.
(* Basic_2A1: includes: lift_mono *)
-lemma lifts_mono: ∀f,T,U1. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.
+lemma lifts_mono: ∀f,T. is_mono … (lifts f T).
#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝 … f)
/3 width=6 by lifts_conf, lifts_fwd_isid/
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 "basic_2/relocation/lifts_lifts.ma".
+include "basic_2/relocation/lifts_bind.ma".
+
+(* GENERIC RELOCATION FOR BINDERS *******************************************)
+
+(* Main properties **********************************************************)
+
+theorem liftsb_div3: ∀f2,I,I2. ⬆*[f2] I2 ≡ I → ∀f,I1. ⬆*[f] I1 ≡ I →
+ ∀f1. f2 ⊚ f1 ≡ f → ⬆*[f1] I1 ≡ I2.
+#f2 #I #I2 * -I -I2 #I [2: #V #V2 #HV2 ] #f #I1 #H
+[ elim (liftsb_inv_pair_dx … H) | lapply (liftsb_inv_unit_dx … H) ] -H
+/3 width=6 by lifts_div3, ext2_pair, ext2_unit/
+qed-.
+
+theorem liftsb_trans: ∀f1,I1,I. ⬆*[f1] I1 ≡ I → ∀f2,I2. ⬆*[f2] I ≡ I2 →
+ ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] I1 ≡ I2.
+#f1 #I1 #I * -I1 -I #I1 [2: #V1 #V #HV1 ] #f2 #I2 #H
+[ elim (liftsb_inv_pair_sn … H) | lapply (liftsb_inv_unit_sn … H) ] -H
+/3 width=6 by lifts_trans, ext2_pair, ext2_unit/
+qed-.
liftsv f (T1 @ T1s) (T2 @ T2s)
.
-interpretation "uniform relocation (vector)"
+interpretation "uniform relocation (term vector)"
'RLiftStar i T1s T2s = (liftsv (uni i) T1s T2s).
-interpretation "generic relocation (vector)"
+interpretation "generic relocation (term vector)"
'RLiftStar f T1s T2s = (liftsv f T1s T2s).
(* Basic inversion lemmas ***************************************************)
--- /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 "basic_2/syntax/bind_weight.ma".
+include "basic_2/relocation/lifts_weight.ma".
+include "basic_2/relocation/lifts_bind.ma".
+
+(* GENERIC RELOCATION FOR BINDERS *******************************************)
+
+(* Forward lemmas with weight for binders ***********************************)
+
+lemma liftsb_fwd_bw: ∀f,I1,I2. ⬆*[f] I1 ≡ I2 → ♯{I1} = ♯{I2}.
+#f #I1 #I2 * -I1 -I2 /2 width=2 by lifts_fwd_tw/
+qed-.
| BPair: bind2 → term → bind
.
+inductive ext2 (R:relation term): relation bind ≝
+| ext2_unit: ∀I. ext2 R (BUnit I) (BUnit I)
+| ext2_pair: ∀I,V1,V2. R V1 V2 → ext2 R (BPair I V1) (BPair I V2)
+.
+
+(* Basic_inversion lemmas **************************************************)
+
+fact ext2_inv_unit_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
+ ∀I. Z1 = BUnit I → Z2 = BUnit I.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
+#J #H destruct //
+qed-.
+
+lemma ext2_inv_unit_sn: ∀R,I,Z2. ext2 R (BUnit I) Z2 → Z2 = BUnit I.
+/2 width=4 by ext2_inv_unit_sn_aux/ qed-.
+
+fact ext2_inv_pair_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
+ ∀I,V1. Z1 = BPair I V1 →
+ ∃∃V2. R V1 V2 & Z2 = BPair I V2.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
+#J #W1 #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma ext2_inv_pair_sn: ∀R,Z2,I,V1. ext2 R (BPair I V1) Z2 →
+ ∃∃V2. R V1 V2 & Z2 = BPair I V2.
+/2 width=3 by ext2_inv_pair_sn_aux/ qed-.
+
+fact ext2_inv_unit_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
+ ∀I. Z2 = BUnit I → Z1 = BUnit I.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ]
+#J #H destruct //
+qed-.
+
+lemma ext2_inv_unit_dx: ∀R,I,Z1. ext2 R Z1 (BUnit I) → Z1 = BUnit I.
+/2 width=4 by ext2_inv_unit_dx_aux/ qed-.
+
+fact ext2_inv_pair_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 →
+ ∀I,V2. Z2 = BPair I V2 →
+ ∃∃V1. R V1 V2 & Z1 = BPair I V1.
+#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ]
+#J #W2 #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma ext2_inv_pair_dx: ∀R,Z1,I,V2. ext2 R Z1 (BPair I V2) →
+ ∃∃V1. R V1 V2 & Z1 = BPair I V1.
+/2 width=3 by ext2_inv_pair_dx_aux/ qed-.
+
(* Basic properties ********************************************************)
lemma eq_bind_dec: ∀I1,I2:bind. Decidable (I1 = I2).
* #I1 [2: #V1 ] * #I2 [2,4: #V2 ]
-[ elim (eq_bind2_dec I1 I2) #HI
- [ elim (eq_term_dec V1 V2) #HV /2 width=1 by or_introl/ ]
- @or_intror #H destruct /2 width=1 by/
-| @or_intror #H destruct
-| @or_intror #H destruct
-| elim (eq_bind1_dec I1 I2) #HI /2 width=1 by or_introl/
- @or_intror #H destruct /2 width=1 by/
+[1: elim (eq_bind2_dec I1 I2) #HI
+ [ elim (eq_term_dec V1 V2) #HV ]
+|4: elim (eq_bind1_dec I1 I2) #HI
]
+/2 width=1 by or_introl/
+@or_intror #H destruct /2 width=1 by/
+qed-.
+
+lemma ext2_refl: ∀R. reflexive … R → reflexive … (ext2 R).
+#R #HR * /2 width=1 by ext2_pair/
+qed.
+
+lemma ext2_sym: ∀R. symmetric … R → symmetric … (ext2 R).
+#R #HR #T1 #T2 * /3 width=1 by ext2_unit, ext2_pair/
qed-.
(* *)
(**************************************************************************)
-include "basic_2/syntax/term.ma".
-
-(* BINDERS FOR LOCAL ENVIRONMENTS ******************************************)
-
include "basic_2/syntax/term_weight.ma".
include "basic_2/syntax/bind.ma".
projects / helm.git / commitdiff