-lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 →
-|t1| + ∥t2∥ = ∥t1∥ + |t2|.
-#L1 #L2 #t1 #H elim H -L1 -L2 -t1
-[ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H
- #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 //
-| #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize
+(* Inversion lemmas on equivalence ******************************************)
-lemma drop_conf_div: ∀I1,L,K,V1,m1. ⬇[m1] L ≡ K.ⓑ{I1}V1 →
- ∀I2,V2,m2. ⬇[m2] L ≡ K.ⓑ{I2}V2 →
- ∧∧ m1 = m2 & I1 = I2 & V1 = V2.
-#I1 #L #K #V1 #m1 #HLK1 #I2 #V2 #m2 #HLK2
-elim (yle_split m1 m2) #H
-elim (yle_inv_plus_sn … H) -H #m #Hm
-[ lapply (drop_conf_ge … HLK1 … HLK2 … Hm ?)
-| lapply (drop_conf_ge … HLK2 … HLK1 … Hm ?)
-] -HLK1 -HLK2 // #HK
-lapply (drop_fwd_length … HK) #H
-elim (discr_yplus_x_xy … H) -H
-[1,3: #H elim (ylt_yle_false (|K.ⓑ{I1}V1|) (∞)) // ]
-#H destruct
-lapply (drop_inv_O2 … HK) -HK #H destruct
-/2 width=1 by and3_intro/
+lemma drop_O1_inj: ∀i,L1,L2,K. ⬇[i] L1 ≡ K → ⬇[i] L2 ≡ K → L1 ⩬[i, ∞] L2.
+#i @(ynat_ind … i) -i
+[ #L1 #L2 #K #H <(drop_inv_O2 … H) -K #H <(drop_inv_O2 … H) -L1 //
+| #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 //
+ lapply (drop_fwd_length … HLK1)
+ <(drop_fwd_length … HLK2) [ /4 width=5 by drop_inv_drop1, lreq_succ/ ]
+ #H [ elim (ysucc_inv_O_sn … H) | elim (ysucc_inv_O_dx … H) ]
+| #L1 #L2 #K #H1 lapply (drop_fwd_Y2 … H1) -H1
+ #H elim (ylt_yle_false … H) //
+]
qed-.
#K1 #V1 #HK1 #_ #_ lapply (drop_fwd_length_lt2 … HK1) -I -K1 -V1
#H elim (ylt_yle_false … H) -H //
qed-.
+
+lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 →
+|t1| + ∥t2∥ = ∥t1∥ + |t2|.
+#L1 #L2 #t1 #H elim H -L1 -L2 -t1
+[ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H
+ #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 //
+| #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize
+
+lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
+ ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2.
+#K2 #i @(ynat_ind … i) -i
+[ /3 width=3 by lreq_O2, ex2_intro/
+| #i #IHi #Y >yplus_succ2 #Hi
+ elim (drop_O1_lt (Ⓕ) Y 0) [2: >Hi // ]
+ #I #L1 #V #H lapply (drop_inv_O2 … H) -H #H destruct
+ >length_pair in Hi; #H lapply (ysucc_inv_inj … H) -H
+ #HL1K2 elim (IHi L1) -IHi // -HL1K2
+ /3 width=5 by lreq_pair, drop_drop, ex2_intro/
+| #L1 >yplus_Y2 #H elim (ylt_yle_false (|L1|) (∞)) //
+]
+qed-.
+++ /dev/null
-definition dropable_dx: predicate (relation lenv) ≝
- λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 →
- ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2.
-
-lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
-#R #HR #L1 #L2 #H elim H -L2
-[ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2
- /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2
- #K #HLK #HK2 elim (IHL1 … HLK) -L
- /3 width=5 by step, ex2_intro/
-]
-qed-.
-
-
-fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
- l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2.
-#R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k
-[ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H
- /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/
-| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H
- #K1 #V1 #HK12 #HV12 #H destruct
- /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/
-| #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H
- #L1 #V1 #HL12 #HV12 #H destruct
- elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/
-| #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H)
-]
-qed-.
-
-lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R).
-/2 width=5 by lpx_sn_dropable_aux/ qed-.
-
-lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 →
- ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 →
- ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2.
-#R #L1 #L2 #H elim H -L1 -L2
-[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
- [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
- | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
- /3 width=5 by drop_drop_lt, ex3_2_intro/
- ]
-]
-qed-.
-
-lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 →
- ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 →
- ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2.
-#R #L1 #L2 #H elim H -L1 -L2
-[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H
- [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/
- | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10
- /3 width=5 by drop_drop_lt, ex3_2_intro/
- ]
-]
-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 "ground_2/ynat/ynat_plus.ma".
-include "basic_2/grammar/lreq.ma".
-
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
-
-(* Main properties **********************************************************)
-
-theorem lreq_trans: ∀f. Transitive … (lreq f).
-#f #L1 #L2 #H elim H -L1 -L2 -l -m
-[ #l #m #X #H lapply (lreq_inv_atom1 … H) -H
- #H destruct //
-| #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (lreq_inv_zero1 … H) -H
- #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_zero/
-| #I #L1 #L #V #m #_ #IHL1 #X #H elim (lreq_inv_pair1 … H) -H //
- #L2 #HL2 #H destruct /3 width=1 by lreq_pair/
-| #I1 #I #L1 #L #V1 #V #l #m #_ #IHL1 #X #H elim (lreq_inv_succ1 … H) -H //
- #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lreq_succ/
-]
-qed-.
-
-theorem lreq_canc_sn: ∀l,m,L,L1,L2. L ⩬[l, m] L1 → L ⩬[l, m] L2 → L1 ⩬[l, m] L2.
-/3 width=3 by lreq_trans, lreq_sym/ qed-.
-
-theorem lreq_canc_dx: ∀l,m,L,L1,L2. L1 ⩬[l, m] L → L2 ⩬[l, m] L → L1 ⩬[l, m] L2.
-/3 width=3 by lreq_trans, lreq_sym/ qed-.
-
-theorem lreq_join: ∀L1,L2,l,i. L1 ⩬[l, i] L2 →
- ∀m. L1 ⩬[i+l, m] L2 → L1 ⩬[l, i+m] L2.
-#L1 #L2 #l #i #H elim H -L1 -L2 -l -i //
-[ #I #L1 #L2 #V #m #_ #IHL12 #m #H
- lapply (lreq_inv_succ … H ?) -H // >ypred_succ /3 width=1 by lreq_pair/
-| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #m #H
- lapply (lreq_inv_succ … H ?) -H // >yplus_succ2 >ypred_succ /3 width=1 by lreq_succ/
-]
-qed-.
(**************************************************************************)
include "basic_2/notation/relations/rdropstar_4.ma".
-include "basic_2/grammar/lenv.ma".
+include "basic_2/relocation/lreq.ma".
include "basic_2/relocation/lifts.ma".
(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
∀f1. f ⊚ f1 ≡ f2 →
∃∃K2. R f1 K1 K2 & ⬇*[c, f] L2 ≡ K2.
+definition dropable_dx: predicate (rtmap → relation lenv) ≝
+ λR. ∀L1,L2,f2. R f2 L1 L2 →
+ ∀K2,c,f. ⬇*[c, f] L2 ≡ K2 → 𝐔⦃f⦄ →
+ ∀f1. f ⊚ f1 ≡ f2 →
+ ∃∃K1. ⬇*[c, f] L1 ≡ K1 & R f1 K1 K2.
+
+definition dedropable_sn: predicate (rtmap → relation lenv) ≝
+ λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀K2,f1. R f1 K1 K2 →
+ ∀f2. f ⊚ f1 ≡ f2 →
+ ∃∃L2. R f2 L1 L2 & ⬇*[c, f] L2 ≡ K2 & L1 ≡[f] L2.
+
(* Basic inversion lemmas ***************************************************)
fact drops_inv_atom1_aux: ∀X,Y,c,f. ⬇*[c, f] X ≡ Y → X = ⋆ →
(* Basic forward lemmas *****************************************************)
+(* Basic_1: includes: drop_gen_refl *)
+(* Basic_2A1: includes: drop_inv_O2 *)
+lemma drops_fwd_isid: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2.
+#L1 #L2 #c #f #H elim H -L1 -L2 -f //
+[ #I #L1 #L2 #V #f #_ #_ #H elim (isid_inv_next … H) //
+| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/
+]
+qed-.
+
fact drops_fwd_drop2_aux: ∀X,Y,c,f2. ⬇*[c, f2] X ≡ Y → ∀I,K,V. Y = K.ⓑ{I}V →
∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[c, f] X ≡ K.
#X #Y #c #f2 #H elim H -X -Y -f2
]
qed-.
-(* Basic_1: includes: drop_S *)
-(* Basic_2A1: includes: drop_fwd_drop2 *)
lemma drops_fwd_drop2: ∀I,X,K,V,c,f2. ⬇*[c, f2] X ≡ K.ⓑ{I}V →
∃∃f1,f. 𝐈⦃f1⦄ & f2 ⊚ ⫯f1 ≡ f & ⬇*[c, f] X ≡ K.
/2 width=5 by drops_fwd_drop2_aux/ qed-.
/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/
qed-.
-(* Basic_1: includes: drop_gen_refl *)
-(* Basic_2A1: includes: drop_inv_O2 *)
-lemma drops_fwd_isid: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2.
-#L1 #L2 #c #f #H elim H -L1 -L2 -f //
-[ #I #L1 #L2 #V #f #_ #_ #H elim (isid_inv_next … H) //
-| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/
-]
-qed-.
+(* Basic_1: was: drop_S *)
+(* Basic_2A1: was: drop_fwd_drop2 *)
+lemma drops_isuni_fwd_drop2: ∀I,X,K,V,c,f. 𝐔⦃f⦄ → ⬇*[c, f] X ≡ K.ⓑ{I}V → ⬇*[c, ⫯f] X ≡ K.
+/3 width=7 by drops_after_fwd_drop2, after_isid_isuni/ qed-.
(* Basic_2A1: removed theorems 14:
drops_inv_nil drops_inv_cons d1_liftable_liftables
--- /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/drops.ma".
+
+(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Properties on context sensitive equivalence for terms ********************)
+
+lemma ceq_lift: d_liftable2 ceq.
+/2 width=3 by ex2_intro/ qed-.
+
+lemma ceq_inv_lift: d_deliftable2_sn ceq.
+/2 width=3 by ex2_intro/ qed-.
+
+(* Note: cfull_inv_lift does not hold *)
+lemma cfull_lift: d_liftable2 cfull.
+#K #T1 #T2 #_ #L #c #f #_ #U1 #_ -K -T1 -c
+elim (lifts_total T2 f) /2 width=3 by ex2_intro/
+qed-.
(**************************************************************************)
include "basic_2/relocation/lifts_lifts.ma".
-include "basic_2/relocation/drops.ma".
+include "basic_2/relocation/drops_weight.ma".
(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
]
qed-.
+theorem drops_conf_div: ∀L,K,f1. ⬇*[Ⓣ,f1] L ≡ K → ∀f2. ⬇*[Ⓣ,f2] L ≡ K →
+ 𝐔⦃f1⦄ → 𝐔⦃f2⦄ → f1 ≗ f2.
+#L #K #f1 #H elim H -L -K -f1
+[ #f1 #Hf1 #f2 #Hf2 elim (drops_inv_atom1 … Hf2) -Hf2
+ /3 width=1 by isid_inv_eq_repl/
+| #I #L #K #V #f1 #Hf1 #IH #f2 elim (pn_split f2) *
+ #g2 #H2 #Hf2 #HU1 #HU2 destruct
+ [ elim (drops_inv_skip1 … Hf2) -IH -HU1 -Hf2 #Y2 #X2 #HY2 #_ #H destruct
+ lapply (drops_fwd_isid … HY2 ?) -HY2 /2 width=3 by isuni_inv_push/ -HU2
+ #H destruct elim (drops_inv_x_pair_xy … Hf1)
+ | /4 width=5 by drops_inv_drop1, isuni_inv_next, eq_next/
+ ]
+| #I #L #K #V #W #f1 #Hf1 #_ #IH #f2 elim (pn_split f2) *
+ #g2 #H2 #Hf2 #HU1 #HU2 destruct
+ [ elim (drops_inv_skip1 … Hf2) -Hf2 #Y2 #X2 #HY2 #_ #H destruct -Hf1
+ /4 width=5 by isuni_fwd_push, eq_push/
+ | lapply (drops_inv_drop1 … Hf2) -Hf2 -IH -HU2 #Hg2
+ lapply (drops_fwd_isid … Hf1 ?) -Hf1 /2 width=3 by isuni_inv_push/ -HU1
+ #H destruct elim (drops_inv_x_pair_xy … Hg2)
+ ]
+]
+qed-.
+
(* Advanced properties ******************************************************)
(* Basic_2A1: includes: drop_mono *)
lapply (drops_trans … H1 … H2 … Hf) -L -Hf
#H elim (drops_inv_skip2 … H) -H /2 width=5 by ex3_2_intro/
qed-.
+
+(* Basic_2A1: includes: drops_conf_div *)
+lemma drops_conf_div_pair: ∀I1,I2,L,K,V1,V2,f1,f2.
+ ⬇*[Ⓣ,f1] L ≡ K.ⓑ{I1}V1 → ⬇*[Ⓣ,f2] L ≡ K.ⓑ{I2}V2 →
+ 𝐔⦃f1⦄ → 𝐔⦃f2⦄ → ∧∧ f1 ≗ f2 & I1 = I2 & V1 = V2.
+#I1 #I2 #L #K #V1 #V2 #f1 #f2 #Hf1 #Hf2 #HU1 #HU2
+lapply (drops_isuni_fwd_drop2 … Hf1) // #H1
+lapply (drops_isuni_fwd_drop2 … Hf2) // #H2
+lapply (drops_conf_div … H1 … H2 ??) /2 width=3 by isuni_next/ -H1 -H2 -HU1 -HU2 #H
+lapply (eq_inv_nn … H ????) -H [5: |*: // ] #H12
+lapply (drops_eq_repl_back … Hf1 … H12) -Hf1 #H0
+lapply (drops_mono … H0 … Hf2) -L #H
+destruct /2 width=1 by and3_intro/
+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/drops.ma".
+
+(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Properties on general entrywise extension of context-sensitive relations *)
+
+(* Basic_2A1: includes: lpx_sn_deliftable_dropable *)
+lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP →
+ dropable_sn (lexs RN RP).
+#RN #RP #HN #HP #L1 #K1 #c #f #H elim H -L1 -K1 -f
+[ #f #Hf #X #f2 #H #f1 #Hf2 >(lexs_inv_atom1 … H) -X
+ /4 width=3 by lexs_atom, drops_atom, ex2_intro/
+| #I #L1 #K1 #V1 #f #_ #IH #X #f2 #H #f1 #Hf2 elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ]
+ #g2 #Hg2 #H2 destruct elim (lexs_inv_next1 … H) -H
+ #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2
+ /3 width=3 by drops_drop, ex2_intro/
+| #I #L1 #K1 #V1 #W1 #f #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (after_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ]
+ #g1 #g2 #Hg2 #H1 #H2 destruct
+ [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H
+ #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2
+ [ elim (HP … HV12 … HLK … HWV) | elim (HN … HV12 … HLK … HWV) ] -V1
+ /3 width=5 by lexs_next, lexs_push, drops_skip, ex2_intro/
+]
+qed-.
+
+(* Basic_2A1: includes: lpx_sn_liftable_dedropable *)
+lemma lexs_liftable_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
+ d_liftable2 RN → d_liftable2 RP → dedropable_sn (lexs RN RP).
+#RN #RP #H1RN #H1RP #H2RN #H2RP #L1 #K1 #c #f #H elim H -L1 -K1 -f
+[ #f #Hf #X #f1 #H #f2 #Hf2 >(lexs_inv_atom1 … H) -X
+ /4 width=4 by drops_atom, lexs_atom, ex3_intro/
+| #I #L1 #K1 #V1 #f #_ #IHLK1 #K2 #f1 #HK12 #f2 #Hf2
+ elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct
+ elim (IHLK1 … HK12 … Hg2) -K1
+ /3 width=6 by drops_drop, lexs_next, ex3_intro/
+| #I #L1 #K1 #V1 #W1 #f #HLK1 #HWV1 #IHLK1 #X #f1 #H #f2 #Hf2
+ elim (after_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
+ [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H #K2 #W2 #HK12 #HW12 #H destruct
+ [ elim (H2RP … HW12 … HLK1 … HWV1) | elim (H2RN … HW12 … HLK1 … HWV1) ] -W1
+ elim (IHLK1 … HK12 … Hg2) -K1
+ /3 width=6 by drops_skip, lexs_next, lexs_push, ex3_intro/
+]
+qed-.
+
+fact lexs_dropable_aux: ∀RN,RP,L2,K2,c,f. ⬇*[c, f] L2 ≡ K2 → 𝐔⦃f⦄ →
+ ∀L1,f2. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f ⊚ f1 ≡ f2 →
+ ∃∃K1. ⬇*[c, f] L1 ≡ K1 & K1 ⦻*[RN, RP, f1] K2.
+#RN #RP #L2 #K2 #c #f #H elim H -L2 -K2 -f
+[ #f #Hf #_ #X #f2 #H #f1 #Hf2 lapply (lexs_inv_atom2 … H) -H
+ #H destruct /4 width=3 by lexs_atom, drops_atom, ex2_intro/
+| #I #L2 #K2 #V2 #f #_ #IH #Hf #X #f2 #HX #f1 #Hf2
+ elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct
+ elim (lexs_inv_next2 … HX) -HX #L1 #V1 #HL12 #HV12 #H destruct
+ elim (IH … HL12 … Hg2) -L2 -V2 -g2
+ /3 width=3 by drops_drop, isuni_inv_next, ex2_intro/
+| #I #L2 #K2 #V2 #W2 #f #_ #HWV2 #IH #Hf #X #f2 #HX #f1 #Hf2
+ elim (after_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct
+ [ elim (lexs_inv_push2 … HX) | elim (lexs_inv_next2 … HX) ] -HX #L1 #V1 #HL12 #HV12 #H destruct
+ elim (IH … HL12 … Hg2) -L2 -g2 /2 width=3 by isuni_fwd_push/ #K1 #HLK1 #HK12
+ lapply (isuni_inv_push … Hf ??) -Hf [3,6: |*: // ] #Hf
+ lapply (lifts_fwd_isid … HWV2 … Hf) #H destruct -HWV2
+ lapply (drops_fwd_isid … HLK1 … Hf) #H destruct -HLK1
+ /4 width=5 by lexs_next, lexs_push, drops_refl, isid_push, ex2_intro/
+]
+qed-.
+
+(* Basic_2A1: includes: lpx_sn_dropable *)
+lemma lexs_dropable: ∀RN,RP. dropable_dx (lexs RN RP).
+/2 width=5 by lexs_dropable_aux/ qed-.
+
+(* Basic_2A1: includes: lpx_sn_drop_conf *)
+lemma lexs_drops_conf_next: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP →
+ ∀L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 →
+ ∀I,K1,V1,c,f. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V1 →
+ ∀f1. f ⊚ ⫯f1 ≡ f2 →
+ ∃∃K2,V2. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[RN, RP, f1] K2 & RN K1 V1 V2.
+#RN #RP #HRN #HRP #L1 #L2 #f2 #HL12 #I #K1 #V1 #c #f #HLK1 #f1 #Hf2
+elim (lexs_deliftable_dropable … HRN HRP … HLK1 … HL12 … Hf2) -L1 -f2 -HRN -HRP
+#X #HX #HLK2 elim (lexs_inv_next1 … HX) -HX
+#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+lemma lexs_drops_conf_push: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP →
+ ∀L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 →
+ ∀I,K1,V1,c,f. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V1 →
+ ∀f1. f ⊚ ↑f1 ≡ f2 →
+ ∃∃K2,V2. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[RN, RP, f1] K2 & RP K1 V1 V2.
+#RN #RP #HRN #HRP #L1 #L2 #f2 #HL12 #I #K1 #V1 #c #f #HLK1 #f1 #Hf2
+elim (lexs_deliftable_dropable … HRN HRP … HLK1 … HL12 … Hf2) -L1 -f2 -HRN -HRP
+#X #HX #HLK2 elim (lexs_inv_push1 … HX) -HX
+#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+(* Basic_2A1: includes: lpx_sn_drop_trans *)
+lemma lexs_drops_trans_next: ∀RN,RP,L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 →
+ ∀I,K2,V2,c,f. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V2 → 𝐔⦃f⦄ →
+ ∀f1. f ⊚ ⫯f1 ≡ f2 →
+ ∃∃K1,V1. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[RN, RP, f1] K2 & RN K1 V1 V2.
+#RN #RP #L1 #L2 #f2 #HL12 #I #K1 #V1 #c #f #HLK1 #Hf #f1 #Hf2
+elim (lexs_dropable … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf
+#X #HLK1 #HX elim (lexs_inv_next2 … HX) -HX
+#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+lemma lexs_drops_trans_push: ∀RN,RP,L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 →
+ ∀I,K2,V2,c,f. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V2 → 𝐔⦃f⦄ →
+ ∀f1. f ⊚ ↑f1 ≡ f2 →
+ ∃∃K1,V1. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[RN, RP, f1] K2 & RP K1 V1 V2.
+#RN #RP #L1 #L2 #f2 #HL12 #I #K1 #V1 #c #f #HLK1 #Hf #f1 #Hf2
+elim (lexs_dropable … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf
+#X #HLK1 #HX elim (lexs_inv_push2 … HX) -HX
+#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/
+qed-.
+
+lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
+ d_liftable2 RN → d_liftable2 RP →
+ ∀K1,K2,f1. K1 ⦻*[RN, RP, f1] K2 →
+ ∀I,L1,V1,c,f. ⬇*[c,f] L1.ⓑ{I}V1 ≡ K1 →
+ ∀f2. f ⊚ f1 ≡ ⫯f2 →
+ ∃∃L2,V2. ⬇*[c,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RN L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2.
+#RN #RP #H1RN #H1RP #H2RN #H2RP #K1 #K2 #f1 #HK12 #I #L1 #V1 #c #f #HLK1 #f2 #Hf2
+elim (lexs_liftable_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
+#X #HX #HLK2 #H1L12 elim (lexs_inv_next1 … HX) -HX
+#L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/
+qed-.
+
+lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. reflexive ? (RP L)) →
+ d_liftable2 RN → d_liftable2 RP →
+ ∀K1,K2,f1. K1 ⦻*[RN, RP, f1] K2 →
+ ∀I,L1,V1,c,f. ⬇*[c,f] L1.ⓑ{I}V1 ≡ K1 →
+ ∀f2. f ⊚ f1 ≡ ↑f2 →
+ ∃∃L2,V2. ⬇*[c,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RP L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2.
+#RN #RP #H1RN #H1RP #H2RN #H2RP #K1 #K2 #f1 #HK12 #I #L1 #V1 #c #f #HLK1 #f2 #Hf2
+elim (lexs_liftable_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP
+#X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX
+#L2 #V2 #H2L12 #HV12 #H destruct /2 width=6 by ex4_2_intro/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/drops.ma".
-include "basic_2/relocation/lreq_lreq.ma".
+include "basic_2/relocation/drops_ceq.ma".
+include "basic_2/relocation/drops_lexs.ma".
(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-definition dedropable_sn: predicate (rtmap → relation lenv) ≝
- λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀K2,f1. R f1 K1 K2 →
- ∀f2. f ⊚ f1 ≡ f2 →
- ∃∃L2. R f2 L1 L2 & ⬇*[c, f] L2 ≡ K2 & L1 ≡[f] L2.
+(* Properties on ranged equivalence for local environments ******************)
-(* Properties on equivalence ************************************************)
-
-lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (LTC … R).
-#R #HR #L1 #K1 #c #f #HLK1 #K2 #f1 #H elim H -K2
-[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -K1 -f1
- /3 width=4 by inj, ex3_intro/
-| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
- #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -K -f1
- /3 width=6 by lreq_trans, step, ex3_intro/
-]
-qed-.
-(*
-lemma lreq_drop_trans_be: ∀L1,L2,l,k. L1 ⩬[l, k] L2 →
- ∀I,K2,W,c,i. ⬇[c, 0, i] L2 ≡ K2.ⓑ{I}W →
- l ≤ i → ∀k0. i + ⫯k0 = l + k →
- ∃∃K1. K1 ⩬[0, k0] K2 & ⬇[c, 0, i] L1 ≡ K1.ⓑ{I}W.
-#L1 #L2 #l #k #H elim H -L1 -L2 -l -k
-[ #l #k #J #K2 #W #c #i #H
- elim (drop_inv_atom1 … H) -H #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J #K2 #W #c #i #_ #_ #k0
- >yplus_succ2 #H elim (ysucc_inv_O_dx … H)
-| #I #L1 #L2 #V #k #HL12 #IHL12 #J #K2 #W #c #i #H #_ >yplus_O1 #k0 #H0
- elim (drop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ]
- [ destruct
- /2 width=3 by drop_pair, ex2_intro/
- | lapply (ylt_inv_O1 … Hi) #H <H in H0; -H
- >yplus_succ1 #H lapply (ysucc_inv_inj … H) -H <(yplus_O1 k)
- #H0 elim (IHL12 … HLK1 … H0) -IHL12 -HLK1 -H0 //
- /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-| #I1 #I2 #L1 #L2 #V1 #V2 #l #k #_ #IHL12 #J #K2 #W #c #i #HLK2 #Hli #k0
- elim (yle_inv_succ1 … Hli) -Hli
- #Hli #Hi <Hi >yplus_succ1 >yplus_succ1 #H lapply (ysucc_inv_inj … H) -H
- #H0 lapply (drop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O1/
- #HLK1 elim (IHL12 … HLK1 … H0) -IHL12 -HLK1 -H0
- /4 width=3 by ylt_O1, drop_drop_lt, ex2_intro/
-]
+lemma lreq_dedropable: dedropable_sn lreq.
+@lexs_liftable_dedropable
+/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl/
qed-.
-lemma lreq_drop_conf_be: ∀L1,L2,l,k. L1 ⩬[l, k] L2 →
- ∀I,K1,W,c,i. ⬇[c, 0, i] L1 ≡ K1.ⓑ{I}W →
- l ≤ i → ∀k0. i + ⫯k0 = l + k →
- ∃∃K2. K1 ⩬[0, k0] K2 & ⬇[c, 0, i] L2 ≡ K2.ⓑ{I}W.
-#L1 #L2 #l #k #HL12 #I #K1 #W #c #i #HLK1 #Hli #k0 #H0
-elim (lreq_drop_trans_be … (lreq_sym … HL12) … HLK1 … H0) // -L1 -Hli -H0
-/3 width=3 by lreq_sym, ex2_intro/
+lemma lreq_dropable: ∀RN,RP. dropable_dx (lexs RN RP).
+@lexs_dropable qed-.
+
+(* Basic_2A1: includes: lreq_drop_trans_be *)
+lemma lreq_drops_trans_next: ∀L1,L2,f2. L1 ≡[f2] L2 →
+ ∀I,K2,V,c,f. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V → 𝐔⦃f⦄ →
+ ∀f1. f ⊚ ⫯f1 ≡ f2 →
+ ∃∃K1. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V & K1 ≡[f1] K2.
+#L1 #L2 #f2 #HL12 #I #K1 #V #c #f #HLK1 #Hf #f1 #Hf2
+elim (lexs_drops_trans_next … HL12 … HLK1 Hf … Hf2) -L2 -f2 -Hf
+/2 width=3 by ex2_intro/
qed-.
-lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
- ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2.
-#K2 #i @(ynat_ind … i) -i
-[ /3 width=3 by lreq_O2, ex2_intro/
-| #i #IHi #Y >yplus_succ2 #Hi
- elim (drop_O1_lt (Ⓕ) Y 0) [2: >Hi // ]
- #I #L1 #V #H lapply (drop_inv_O2 … H) -H #H destruct
- >length_pair in Hi; #H lapply (ysucc_inv_inj … H) -H
- #HL1K2 elim (IHi L1) -IHi // -HL1K2
- /3 width=5 by lreq_pair, drop_drop, ex2_intro/
-| #L1 >yplus_Y2 #H elim (ylt_yle_false (|L1|) (∞)) //
-]
+(* Basic_2A1: includes: lreq_drop_conf_be *)
+lemma lreq_drops_conf_next: ∀L1,L2,f2. L1 ≡[f2] L2 →
+ ∀I,K1,V,c,f. ⬇*[c,f] L1 ≡ K1.ⓑ{I}V → 𝐔⦃f⦄ →
+ ∀f1. f ⊚ ⫯f1 ≡ f2 →
+ ∃∃K2. ⬇*[c,f] L2 ≡ K2.ⓑ{I}V & K1 ≡[f1] K2.
+#L1 #L2 #f2 #HL12 #I #K1 #V #c #f #HLK1 #Hf #f1 #Hf2
+elim (lreq_drops_trans_next … (lreq_sym … HL12) … HLK1 … Hf2) // -L1 -f2 -Hf
+/3 width=3 by lreq_sym, ex2_intro/
qed-.
-(* Inversion lemmas on equivalence ******************************************)
-
-lemma drop_O1_inj: ∀i,L1,L2,K. ⬇[i] L1 ≡ K → ⬇[i] L2 ≡ K → L1 ⩬[i, ∞] L2.
-#i @(ynat_ind … i) -i
-[ #L1 #L2 #K #H <(drop_inv_O2 … H) -K #H <(drop_inv_O2 … H) -L1 //
-| #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 //
- lapply (drop_fwd_length … HLK1)
- <(drop_fwd_length … HLK2) [ /4 width=5 by drop_inv_drop1, lreq_succ/ ]
- #H [ elim (ysucc_inv_O_sn … H) | elim (ysucc_inv_O_dx … H) ]
-| #L1 #L2 #K #H1 lapply (drop_fwd_Y2 … H1) -H1
- #H elim (ylt_yle_false … H) //
-]
+lemma drops_lreq_trans_next: ∀K1,K2,f1. K1 ≡[f1] K2 →
+ ∀I,L1,V,c,f. ⬇*[c,f] L1.ⓑ{I}V ≡ K1 →
+ ∀f2. f ⊚ f1 ≡ ⫯f2 →
+ ∃∃L2. ⬇*[c,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V≡[f]L2.ⓑ{I}V.
+#K1 #K2 #f1 #HK12 #I #L1 #V #c #f #HLK1 #f2 #Hf2
+elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -K1 -f1
+/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl, ex3_intro/
qed-.
(**************************************************************************)
include "ground_2/lib/lstar.ma".
+include "basic_2/relocation/lreq_lreq.ma".
include "basic_2/relocation/drops.ma".
(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
]
qed-.
+
+lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (LTC … R).
+#R #HR #L1 #L2 #f2 #H elim H -L2
+[ #L2 #HL12 #K2 #c #f #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -L2 -f2 -Hf
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IHL1 #K2 #c #f #HLK2 #Hf #f1 #Hf2 elim (HR … HL2 … HLK2 … Hf … Hf2) -HR -L2
+ #K #HLK #HK2 elim (IHL1 … HLK … Hf … Hf2) -L -f2 -Hf
+ /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (LTC … R).
+#R #HR #L1 #K1 #c #f #HLK1 #K2 #f1 #H elim H -K2
+[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -K1 -f1
+ /3 width=4 by inj, ex3_intro/
+| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
+ #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -K -f1
+ /3 width=6 by lreq_trans, step, ex3_intro/
+]
+qed-.
qed-.
(* Basic_2A1: includes: drop_fwd_lw_lt *)
-(* Note: 𝐈⦃t⦄ → ⊥ is ∥l∥ < |L| *)
lemma drops_fwd_lw_lt: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 →
(𝐈⦃f⦄ → ⊥) → ♯{L2} < ♯{L1}.
#L1 #L2 #f #H elim H -L1 -L2 -f
#I #L #K #V #c #f #HLK lapply (drops_fwd_lw … HLK) -HLK
normalize in ⊢ (%→?→?%%); /3 width=3 by le_to_lt_to_lt/
qed-.
+
+(* Advanced inversion lemma *************************************************)
+
+lemma drops_inv_x_pair_xy: ∀I,L,V,c,f. ⬇*[c,f] L ≡ L.ⓑ{I}V → ⊥.
+#I #L #V #c #f #H lapply (drops_fwd_lw … H) -c -f
+/2 width=4 by lt_le_false/ (**) (* full auto is a bit slow: 19s *)
+qed-.
(* *)
(**************************************************************************)
-include "ground_2/relocation/trace_sor.ma".
-include "ground_2/relocation/trace_isun.ma".
+include "ground_2/relocation/rtmap_sor.ma".
include "basic_2/notation/relations/freestar_3.ma".
include "basic_2/grammar/lenv.ma".
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-inductive frees: relation3 lenv term trace ≝
-| frees_atom: ∀I. frees (⋆) (⓪{I}) (◊)
-| frees_sort: ∀I,L,V,s,t. frees L (⋆s) t →
- frees (L.â\93\91{I}V) (â\8b\86s) (â\92» @ t)
-| frees_zero: ∀I,L,V,t. frees L V t →
- frees (L.â\93\91{I}V) (#0) (â\93\89 @ t)
-| frees_lref: ∀I,L,V,i,t. frees L (#i) t →
- frees (L.â\93\91{I}V) (#⫯i) (â\92» @ t)
-| frees_gref: ∀I,L,V,p,t. frees L (§p) t →
- frees (L.â\93\91{I}V) (§p) (â\92» @ t)
-| frees_bind: ∀I,L,V,T,t1,t2,t,b,a. frees L V t1 → frees (L.ⓑ{I}V) T (b @ t2) →
- t1 ⋓ t2 ≡ t → frees L (ⓑ{a,I}V.T) t
-| frees_flat: ∀I,L,V,T,t1,t2,t. frees L V t1 → frees L T t2 →
- t1 ⋓ t2 ≡ t → frees L (ⓕ{I}V.T) t
+inductive frees: relation3 lenv term rtmap ≝
+| frees_atom: ∀I,f. 𝐈⦃f⦄ → frees (⋆) (⓪{I}) f
+| frees_sort: ∀I,L,V,s,f. frees L (⋆s) f →
+ frees (L.â\93\91{I}V) (â\8b\86s) (â\86\91f)
+| frees_zero: ∀I,L,V,f. frees L V f →
+ frees (L.â\93\91{I}V) (#0) (⫯f)
+| frees_lref: ∀I,L,V,i,f. frees L (#i) f →
+ frees (L.â\93\91{I}V) (#⫯i) (â\86\91f)
+| frees_gref: ∀I,L,V,p,f. frees L (§p) f →
+ frees (L.â\93\91{I}V) (§p) (â\86\91f)
+| frees_bind: ∀I,L,V,T,a,f1,f2,f. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
+ f1 ⋓ ⫱f2 ≡ f → frees L (ⓑ{a,I}V.T) f
+| frees_flat: ∀I,L,V,T,f1,f2,f. frees L V f1 → frees L T f2 →
+ f1 ⋓ f2 ≡ f → frees L (ⓕ{I}V.T) f
.
interpretation
"context-sensitive free variables (term)"
'FreeStar L T t = (frees L T t).
-(* Basic forward lemmas *****************************************************)
+(* Basic inversion lemmas ***************************************************)
-fact frees_fwd_sort_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = ⋆x → 𝐔⦃t⦄.
-#L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/
-[ #_ #L #V #t #_ #_ #x #H destruct
-| #_ #L #_ #i #t #_ #_ #x #H destruct
-| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct
-| #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct
+fact frees_inv_sort_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x → 𝐈⦃f⦄.
+#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
+[ #_ #L #V #f #_ #_ #x #H destruct
+| #_ #L #_ #i #f #_ #_ #x #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
]
qed-.
-lemma frees_fwd_sort: ∀L,t,s. L ⊢ 𝐅*⦃⋆s⦄ ≡ t → 𝐔⦃t⦄.
-/2 width=5 by frees_fwd_sort_aux/ qed-.
+lemma frees_inv_sort: ∀L,s,f. L ⊢ 𝐅*⦃⋆s⦄ ≡ f → 𝐈⦃f⦄.
+/2 width=5 by frees_inv_sort_aux/ qed-.
-fact frees_fwd_gref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = §x → 𝐔⦃t⦄.
-#L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/
-[ #_ #L #V #t #_ #_ #x #H destruct
-| #_ #L #_ #i #t #_ #_ #x #H destruct
-| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct
-| #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct
+fact frees_inv_gref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x → 𝐈⦃f⦄.
+#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
+[ #_ #L #V #f #_ #_ #x #H destruct
+| #_ #L #_ #i #f #_ #_ #x #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
]
qed-.
-lemma frees_fwd_gref: ∀L,t,p. L ⊢ 𝐅*⦃§p⦄ ≡ t → 𝐔⦃t⦄.
-/2 width=5 by frees_fwd_gref_aux/ qed-.
-
-(* Basic inversion lemmas ***************************************************)
+lemma frees_inv_gref: ∀L,p,f. L ⊢ 𝐅*⦃§p⦄ ≡ f → 𝐈⦃f⦄.
+/2 width=5 by frees_inv_gref_aux/ qed-.
-fact frees_inv_zero_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → X = #0 →
- (L = ⋆ ∧ t = ◊) ∨
- ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u.
-#L #X #t * -L -X -t
+fact frees_inv_zero_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → X = #0 →
+ (L = ⋆ ∧ 𝐈⦃f⦄) ∨
+ ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
+#L #X #f * -L -X -f
[ /3 width=1 by or_introl, conj/
-| #I #L #V #s #t #_ #H destruct
+| #I #L #V #s #f #_ #H destruct
| /3 width=7 by ex3_4_intro, or_intror/
-| #I #L #V #i #t #_ #H destruct
-| #I #L #V #p #t #_ #H destruct
-| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #H destruct
-| #I #L #V #T #t1 #t2 #t #_ #_ #_ #H destruct
+| #I #L #V #i #f #_ #H destruct
+| #I #L #V #p #f #_ #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #H destruct
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #H destruct
]
qed-.
-lemma frees_inv_zero: ∀L,t. L ⊢ 𝐅*⦃#0⦄ ≡ t →
- (L = ⋆ ∧ t = ◊) ∨
- ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u.
+lemma frees_inv_zero: ∀L,f. L ⊢ 𝐅*⦃#0⦄ ≡ f →
+ (L = ⋆ ∧ 𝐈⦃f⦄) ∨
+ ∃∃I,K,V,g. K ⊢ 𝐅*⦃V⦄ ≡ g & L = K.ⓑ{I}V & f = ⫯g.
/2 width=3 by frees_inv_zero_aux/ qed-.
-fact frees_inv_lref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀j. X = #(⫯j) →
- (L = ⋆ ∧ t = ◊) ∨
- ∃∃I,K,V,u. K ⊢ 𝐅*⦃#j⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u.
-#L #X #t * -L -X -t
+fact frees_inv_lref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀j. X = #(⫯j) →
+ (L = ⋆ ∧ 𝐈⦃f⦄) ∨
+ ∃∃I,K,V,g. K ⊢ 𝐅*⦃#j⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
+#L #X #f * -L -X -f
[ /3 width=1 by or_introl, conj/
-| #I #L #V #s #t #_ #j #H destruct
-| #I #L #V #t #_ #j #H destruct
-| #I #L #V #i #t #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
-| #I #L #V #p #t #_ #j #H destruct
-| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #j #H destruct
-| #I #L #V #T #t1 #t2 #t #_ #_ #_ #j #H destruct
+| #I #L #V #s #f #_ #j #H destruct
+| #I #L #V #f #_ #j #H destruct
+| #I #L #V #i #f #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
+| #I #L #V #p #f #_ #j #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #j #H destruct
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #j #H destruct
]
qed-.
-lemma frees_inv_lref: ∀L,i,t. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ t →
- (L = ⋆ ∧ t = ◊) ∨
- ∃∃I,K,V,u. K ⊢ 𝐅*⦃#i⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u.
+lemma frees_inv_lref: ∀L,i,f. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f →
+ (L = ⋆ ∧ 𝐈⦃f⦄) ∨
+ ∃∃I,K,V,g. K ⊢ 𝐅*⦃#i⦄ ≡ g & L = K.ⓑ{I}V & f = ↑g.
/2 width=3 by frees_inv_lref_aux/ qed-.
+
+fact frees_inv_bind_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T,a. X = ⓑ{a,I}V.T →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
+#L #X #f * -L -X -f
+[ #I #f #_ #J #W #U #b #H destruct
+| #I #L #V #s #f #_ #J #W #U #b #H destruct
+| #I #L #V #f #_ #J #W #U #b #H destruct
+| #I #L #V #i #f #_ #J #W #U #b #H destruct
+| #I #L #V #p #f #_ #J #W #U #b #H destruct
+| #I #L #V #T #a #f1 #f2 #f #HV #HT #Hf #J #W #U #b #H destruct /2 width=5 by ex3_2_intro/
+| #I #L #V #T #f1 #f2 #f #_ #_ #_ #J #W #U #b #H destruct
+]
+qed-.
+
+lemma frees_inv_bind: ∀I,L,V,T,a,f. L ⊢ 𝐅*⦃ⓑ{a,I}V.T⦄ ≡ f →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L.ⓑ{I}V ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ ⫱f2 ≡ f.
+/2 width=4 by frees_inv_bind_aux/ qed-.
+
+fact frees_inv_flat_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = ⓕ{I}V.T →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
+#L #X #f * -L -X -f
+[ #I #f #_ #J #W #U #H destruct
+| #I #L #V #s #f #_ #J #W #U #H destruct
+| #I #L #V #f #_ #J #W #U #H destruct
+| #I #L #V #i #f #_ #J #W #U #H destruct
+| #I #L #V #p #f #_ #J #W #U #H destruct
+| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #J #W #U #H destruct
+| #I #L #V #T #f1 #f2 #f #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma frees_inv_flat: ∀I,L,V,T,f. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f →
+ ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
+/2 width=4 by frees_inv_flat_aux/ qed-.
+
+(* Basic properties ********************************************************)
+
+lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
+#L #T #f1 #H elim H -L -T -f1
+[ /3 width=3 by frees_atom, isid_eq_repl_back/
+| #I #L #V #s #f1 #_ #IH #f2 #Hf12
+ elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_sort/
+| #I #L #V #f1 #_ #IH #f2 #Hf12
+ elim (eq_inv_nx … Hf12) -Hf12 /3 width=3 by frees_zero/
+| #I #L #V #i #f1 #_ #IH #f2 #Hf12
+ elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_lref/
+| #I #L #V #p #f1 #_ #IH #f2 #Hf12
+ elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_gref/
+| /3 width=7 by frees_bind, sor_eq_repl_back3/
+| /3 width=7 by frees_flat, sor_eq_repl_back3/
+]
+qed-.
+
+lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
+#L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
+qed-.
+
+lemma frees_sort_gen: ∀L,s,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃⋆s⦄ ≡ f.
+#L elim L -L
+/4 width=3 by frees_eq_repl_back, frees_sort, frees_atom, eq_push_inv_isid/
+qed.
+
+lemma frees_gref_gen: ∀L,p,f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃§p⦄ ≡ f.
+#L elim L -L
+/4 width=3 by frees_eq_repl_back, frees_gref, frees_atom, eq_push_inv_isid/
+qed.
include "basic_2/notation/relations/relationstar_5.ma".
include "basic_2/grammar/lenv.ma".
-(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
≝ λA,B,C,D,E.A→B→C→D→E→Prop.
+++ /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/lexs.ma".
-include "basic_2/relocation/drops.ma".
-
-(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
-
-(* Basic_2A1: includes: lpx_sn_deliftable_dropable *)
-lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP →
- dropable_sn (lexs RN RP).
-#RN #RP #HN #HP #L1 #K1 #c #f #H elim H -L1 -K1 -f
-[ #f #Hf #X #f2 #H #f1 #Hf2 >(lexs_inv_atom1 … H) -X
- /4 width=3 by lexs_atom, drops_atom, ex2_intro/
-| #I #L1 #K1 #V1 #f #_ #IH #X #f2 #H #f1 #Hf2 elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ]
- #g2 #Hg2 #H2 destruct elim (lexs_inv_next1 … H) -H
- #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2
- /3 width=3 by drops_drop, ex2_intro/
-| #I #L1 #K1 #V1 #W1 #f #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (after_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ]
- #g1 #g2 #Hg2 #H1 #H2 destruct
- [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H
- #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2
- [ elim (HP … HV12 … HLK … HWV) | elim (HN … HV12 … HLK … HWV) ] -V1
- /3 width=5 by lexs_next, lexs_push, drops_skip, ex2_intro/
-]
-qed-.
-(*
-lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
- d_liftable2 R → dedropable_sn (lpx_sn R).
-#R #H1R #H2R #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m
-[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H
- /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/
-| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
- #K2 #V2 #HK12 #HV12 #H destruct
- lapply (lpx_sn_fwd_length … HK12)
- #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *)
- /3 width=1 by lpx_sn_pair, lreq_O2/
-| #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
- /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/
-| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H
- elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
- elim (H2R … HW12 … HLK1 … HWV1) -W1
- elim (IHLK1 … HK12) -K1
- /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/
-]
-qed-.
-*)
-include "ground_2/relocation/trace_isun.ma".
-
-lemma lpx_sn_dropable: ∀R,L2,K2,c,t. ⬇*[c, t] L2 ≡ K2 → 𝐔⦃t⦄ →
- ∀L1,u2. lpx_sn R u2 L1 L2 → ∀u1. t ⊚ u1 ≡ u2 →
- ∃∃K1. ⬇*[c, t] L1 ≡ K1 & lpx_sn R u1 K1 K2.
-#R #L2 #K2 #c #t #H elim H -L2 -K2 -t
-[ #t #Ht #_ #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom2 … H) -H
- #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu
- /4 width=3 by drops_atom, lpx_sn_atom, ex2_intro/
-| #I #L2 #K2 #V2 #t #_ #IH #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H
- #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu
- #u #H #Hu destruct elim (IH … HL … Hu) -L2 /3 width=3 by drops_drop, isun_inv_false, ex2_intro/
-| #I #L2 #K2 #V2 #W2 #t #_ #HWV #IHLK #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H
- #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu
- #y1 #y #x2 #H1 #H2 #Hu destruct lapply (isun_inv_true … Ht) -Ht
- #Ht elim (IHLK … HL … Hu) -L2 -Hu /2 width=1 by isun_id/
- #K1 #HLK1 #HK12 lapply (lifts_fwd_isid … HWV ?) // -HWV
- #H destruct lapply (drops_fwd_isid … HLK1 ?) //
- #H destruct
- @ex2_intro
- [
- | @(drops_skip … HLK1)
- | @(lpx_sn_pair … HK12 … HV)
-
-
- lapply (drops_fwd_isid … HLK1 ?) // -HLK1
- 2:
-
-
-
-
- elim (HR … HV … HLK … HWV) -V1
- elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/
-
-
-]
-qed-.
include "basic_2/grammar/lenv_length.ma".
include "basic_2/relocation/lexs.ma".
-(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
(* Forward lemmas on length for local environments **************************)
include "basic_2/grammar/lenv_weight.ma".
include "basic_2/relocation/lexs.ma".
-(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
(* Main properties **********************************************************)
]
qed-.
-theorem lexs_canc_sx: ∀RN,RP,f. Transitive … (lexs RN RP f) →
+theorem lexs_canc_sn: ∀RN,RP,f. Transitive … (lexs RN RP f) →
symmetric … (lexs RN RP f) →
left_cancellable … (lexs RN RP f).
/3 width=3 by/ 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/lexs_lexs.ma".
+include "basic_2/relocation/lreq.ma".
+
+(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************)
+
+(* Main properties **********************************************************)
+
+theorem lreq_trans: ∀f. Transitive … (lreq f).
+/2 width=3 by lexs_trans/ qed-.
+
+theorem lreq_canc_sn: ∀f. left_cancellable … (lreq f).
+/3 width=3 by lexs_canc_sn, lreq_trans, lreq_sym/ qed-.
+
+theorem lreq_canc_dx: ∀f. right_cancellable … (lreq f).
+/3 width=3 by lexs_canc_dx, lreq_trans, lreq_sym/ qed-.
+
+theorem lreq_join: ∀L1,L2,f1. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 →
+ ∀f. f1 ⋓ f2 ≡ f → L1 ≡[f] L2.
+/2 width=5 by lexs_join/ qed-.
+
+theorem lreq_meet: ∀L1,L2,f1. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 →
+ ∀f. f1 ⋒ f2 ≡ f → L1 ≡[f] L2.
+/2 width=5 by lexs_meet/ 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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( 𝐔 ⦃ term 46 f ⦄ )"
- non associative with precedence 45
- for @{ 'IsUniform $f }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( 𝐔 ⦃ term 46 f ⦄ )"
+ non associative with precedence 45
+ for @{ 'IsUniform $f }.
include "ground_2/notation/relations/rafter_3.ma".
include "ground_2/relocation/rtmap_istot.ma".
+include "ground_2/relocation/rtmap_isuni.ma".
(* RELOCATION MAP ***********************************************************)
lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄.
/3 width=4 by after_fwd_isid2, after_fwd_isid1, conj/ qed-.
+(* Properties on isuni ******************************************************)
+
+lemma after_isid_isuni: ∀f1,f2. 𝐈⦃f2⦄ → 𝐔⦃f1⦄ → f1 ⊚ ⫯f2 ≡ ⫯f1.
+#f1 #f2 #Hf2 #H elim H -H
+/5 width=7 by isid_after_dx, after_eq_repl_back_2, after_next, after_push, eq_push_inv_isid/
+qed.
+
(* Forward lemmas on at *****************************************************)
lemma after_at_fwd: ∀i,i1,f. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f →
--- /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 "ground_2/notation/relations/isuniform_1.ma".
+include "ground_2/relocation/rtmap_isid.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+inductive isuni: predicate rtmap ≝
+| isuni_isid: ∀f. 𝐈⦃f⦄ → isuni f
+| isuni_next: ∀f. isuni f → ∀g. ⫯f = g → isuni g
+.
+
+interpretation "test for uniformity (rtmap)"
+ 'IsUniform f = (isuni f).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma isuni_inv_push: ∀g. 𝐔⦃g⦄ → ∀f. ↑f = g → 𝐈⦃f⦄.
+#g * -g /2 width=3 by isid_inv_push/
+#f #_ #g #H #x #Hx destruct elim (discr_push_next … Hx)
+qed-.
+
+lemma isuni_inv_next: ∀g. 𝐔⦃g⦄ → ∀f. ⫯f = g → 𝐔⦃f⦄.
+#g * -g #f #Hf
+[ #x #Hx elim (isid_inv_next … Hf … Hx)
+| #g #H #x #Hx destruct /2 width=1 by injective_push/
+]
+qed-.
+
+(* basic forward lemmas *****************************************************)
+
+lemma isuni_fwd_push: ∀g. 𝐔⦃g⦄ → ∀f. ↑f = g → 𝐔⦃f⦄.
+/3 width=3 by isuni_inv_push, isuni_isid/ qed-.
(* Basic properties *********************************************************)
+corec lemma sand_eq_repl_back1: ∀f2,f. eq_repl_back … (λf1. f1 ⋒ f2 ≡ f).
+#f2 #f #f1 * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x #Hx
+try cases (eq_inv_px … Hx … H1) try cases (eq_inv_nx … Hx … H1) -g1
+/3 width=7 by sand_pp, sand_np, sand_pn, sand_nn/
+qed-.
+
+lemma sand_eq_repl_fwd1: ∀f2,f. eq_repl_fwd … (λf1. f1 ⋒ f2 ≡ f).
+#f2 #f @eq_repl_sym /2 width=3 by sand_eq_repl_back1/
+qed-.
+
+corec lemma sand_eq_repl_back2: ∀f1,f. eq_repl_back … (λf2. f1 ⋒ f2 ≡ f).
+#f1 #f #f2 * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx
+try cases (eq_inv_px … Hx … H2) try cases (eq_inv_nx … Hx … H2) -g2
+/3 width=7 by sand_pp, sand_np, sand_pn, sand_nn/
+qed-.
+
+lemma sand_eq_repl_fwd2: ∀f1,f. eq_repl_fwd … (λf2. f1 ⋒ f2 ≡ f).
+#f1 #f @eq_repl_sym /2 width=3 by sand_eq_repl_back2/
+qed-.
+
+corec lemma sand_eq_repl_back3: ∀f1,f2. eq_repl_back … (λf. f1 ⋒ f2 ≡ f).
+#f1 #f2 #f * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx
+try cases (eq_inv_px … Hx … H0) try cases (eq_inv_nx … Hx … H0) -g
+/3 width=7 by sand_pp, sand_np, sand_pn, sand_nn/
+qed-.
+
+lemma sand_eq_repl_fwd3: ∀f1,f2. eq_repl_fwd … (λf. f1 ⋒ f2 ≡ f).
+#f1 #f2 @eq_repl_sym /2 width=3 by sand_eq_repl_back3/
+qed-.
+
corec lemma sand_refl: ∀f. f ⋒ f ≡ f.
#f cases (pn_split f) * #g #H
[ @(sand_pp … H H H) | @(sand_nn … H H H) ] -H //
(* Basic properties *********************************************************)
+corec lemma sor_eq_repl_back1: ∀f2,f. eq_repl_back … (λf1. f1 ⋓ f2 ≡ f).
+#f2 #f #f1 * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0 #x #Hx
+try cases (eq_inv_px … Hx … H1) try cases (eq_inv_nx … Hx … H1) -g1
+/3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/
+qed-.
+
+lemma sor_eq_repl_fwd1: ∀f2,f. eq_repl_fwd … (λf1. f1 ⋓ f2 ≡ f).
+#f2 #f @eq_repl_sym /2 width=3 by sor_eq_repl_back1/
+qed-.
+
+corec lemma sor_eq_repl_back2: ∀f1,f. eq_repl_back … (λf2. f1 ⋓ f2 ≡ f).
+#f1 #f #f2 * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx
+try cases (eq_inv_px … Hx … H2) try cases (eq_inv_nx … Hx … H2) -g2
+/3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/
+qed-.
+
+lemma sor_eq_repl_fwd2: ∀f1,f. eq_repl_fwd … (λf2. f1 ⋓ f2 ≡ f).
+#f1 #f @eq_repl_sym /2 width=3 by sor_eq_repl_back2/
+qed-.
+
+corec lemma sor_eq_repl_back3: ∀f1,f2. eq_repl_back … (λf. f1 ⋓ f2 ≡ f).
+#f1 #f2 #f * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf #H #H2 #H0 #x #Hx
+try cases (eq_inv_px … Hx … H0) try cases (eq_inv_nx … Hx … H0) -g
+/3 width=7 by sor_pp, sor_np, sor_pn, sor_nn/
+qed-.
+
+lemma sor_eq_repl_fwd3: ∀f1,f2. eq_repl_fwd … (λf. f1 ⋓ f2 ≡ f).
+#f1 #f2 @eq_repl_sym /2 width=3 by sor_eq_repl_back3/
+qed-.
+
corec lemma sor_refl: ∀f. f ⋓ f ≡ f.
#f cases (pn_split f) * #g #H
[ @(sor_pp … H H H) | @(sor_nn … H H H) ] -H //
class "grass"
[ { "multiple relocation" * } {
[ { "" * } {
- [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
- [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
+ [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
+ [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" "" "nstream_sand" "" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
(*
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
projects / helm.git / commitdiff