+++ /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/substitution/lpx_sn.ma".
-
-(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
-
-(* Properties on transitive_closure *****************************************)
-
-lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) →
- ∀L1,L2. lpx_sn (LTC … R) L1 L2 →
- TC … (lpx_sn R) L1 L2.
-#R #HR #L1 #L2 #H elim H -L1 -L2
-/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/
-qed-.
-
-(* Inversion lemmas on transitive closure ***********************************)
-
-lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) →
- ∀S:relation lenv.
- S (⋆) (⋆) → (
- ∀I,K1,K2,V1,V2.
- TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 →
- S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
- ) →
- ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2.
-#R #HR #S #IH1 #IH2 #L2 elim L2 -L2
-[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X //
-| #L2 #I #V2 #IHL2 #X #H
- elim (TC_lpx_sn_inv_pair2 … H) // -H -HR
- #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/
-]
-qed-.
-
-lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. c_rs_transitive … R (λ_. lpx_sn R) →
- ∀L1,L2. TC … (lpx_sn R) L1 L2 →
- lpx_sn (LTC … R) L1 L2.
-/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ 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/static/lfeq.ma".
+*)
+include "basic_2/static/lfxs_lfxs.ma".
+include "basic_2/i_static/tc_lfxs_fqup.ma".
+
+include "basic_2/notation/relations/lazyeqsn_3.ma".
+
+definition ceq_ext: relation3 lenv bind bind ≝
+ cext2 (λL,T1,T2. T1 = T2).
+
+definition lfeq: relation3 term lenv lenv ≝
+ lfxs (λL,T1,T2. T1 = T2).
+
+interpretation
+ "syntactic equivalence on referred entries (local environment)"
+ 'LazyEqSn T L1 L2 = (lfeq T L1 L2).
+
+axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L →
+ ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
+
+axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2.
+(*
+#R #L #I1 #I2 * -I1 -I2
+[ /2 width=1 by ext2_unit, inj/
+| #I #V1 #V2 #HV12
+*)
+
+
+(*
+lemma pippo: ∀RN,RP. (∀L. reflexive … (RP L)) →
+ ∀f,L1,L2. L1 ⪤*[LTC … RN, RP, f] L2 →
+ TC … (lexs RN RP f) L1 L2.
+#RN #RP #HRP #f #L1 #L2 #H elim H -f -L1 -L2
+[ /2 width=1 by lexs_atom, inj/ ]
+#f #I1 #I2 #L1 #L2 #HL12 #HI12 #IH
+[ @step [3:
+*)
+
+axiom lexs_frees_confluent_LTC_sn: ∀RN,RP. lexs_frees_confluent RN RP →
+ lexs_frees_confluent (LTC … RN) RP.
+(*
+#RN #RP #HR #f1 #L1 #T #Hf1 #L2 #H
+*)
+(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
+
+lemma pippo: ∀R. (∀L. reflexive … (R L)) →
+ (lexs_frees_confluent (cext2 R) cfull) →
+ ∀L1,L2,T. L1 ⪤**[R, T] L2 →
+ ∃∃L. L1 ⪤*[LTC … R, T] L & L ≡[T] L2.
+#R #H1R #H2R #L1 #L2 #T #H
+@(tc_lfxs_ind_sn … H1R … H) -H -L2
+[ /4 width=5 by lfxs_refl, inj, ex2_intro/
+| #L0 #L2 #_ #HL02 * #L * #f1 #Hf1 #HL1 #HL0
+ lapply (lexs_co ??? cfull … (cext2_inv_LTC R) … HL1) -HL1 // #HL1
+ lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 #HL2
+ elim (lexs_frees_confluent_LTC_sn … H2R … Hf1 … HL1) #f2 #Hf2 #Hf21
+ lapply (lfxs_inv_frees … HL2 … Hf2) -HL2 #HL2
+ elim (lexs_sle_split … ceq_ext … HL2 … Hf21) -HL2
+ [ #L0 #HL0 #HL02
+ |*: /2 width=1 by ext2_refl/
+ ]
+ lapply (sle_lexs_trans … HL0 … Hf21) -Hf21 // #H
+ elim (H2R … Hf2 … H) -H #f0 #Hf0 #Hf02
+ lapply (sle_lexs_trans … HL02 … Hf02) -f2 // #HL02
+ @(ex2_intro … L0)
+ [ @(ex2_intro … Hf1)
+ | @(ex2_intro … HL02) //
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ⪤ [ break term 46 R ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'Relation $R $L1 $L2 }.
(* Properties with context-sensitive equivalence for terms ******************)
-lemma ceq_lift_sn: d_liftable2_sn … liftsb ceq.
+lemma ceq_lift_sn: d_liftable2_sn … liftsb ceq_ext.
+#K #I1 #I2 #H <(ceq_ext_inv_eq … H) -I2
/2 width=3 by ex2_intro/ qed-.
-lemma ceq_inv_lift_sn: d_deliftable2_sn … liftsb ceq.
+lemma ceq_inv_lift_sn: d_deliftable2_sn … liftsb ceq_ext.
+#L #J1 #J2 #H <(ceq_ext_inv_eq … H) -J2
/2 width=3 by ex2_intro/ qed-.
(* Note: d_deliftable2_sn cfull does not hold *)
∀b,f,I,K2. ⬇*[b, f] L2 ≡ K2.ⓘ{I} → 𝐔⦃f⦄ →
∀f1. f ~⊚ ⫯f1 ≡ f2 →
∃∃K1. ⬇*[b, f] L1 ≡ K1.ⓘ{I} & K1 ≡[f1] K2.
-#f2 #L1 #L2 #HL12 #b #f #I #K1 #HLK1 #Hf #f1 #Hf2
-elim (lexs_drops_trans_next … HL12 … HLK1 Hf … Hf2) -f2 -L2 -Hf
+#f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2
+elim (lexs_drops_trans_next … HL12 … HLK2 Hf … Hf2) -f2 -L2 -Hf
+#I1 #K1 #HLK1 #HK12 #H <(ceq_ext_inv_eq … H) -I2
/2 width=3 by ex2_intro/
qed-.
∀b,f,I,K1. ⬇*[b, f] L1 ≡ K1.ⓘ{I} → 𝐔⦃f⦄ →
∀f1. f ~⊚ ⫯f1 ≡ f2 →
∃∃K2. ⬇*[b, f] L2 ≡ K2.ⓘ{I} & K1 ≡[f1] K2.
-#f2 #L1 #L2 #HL12 #b #f #I #K1 #HLK1 #Hf #f1 #Hf2
+#f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2
elim (lreq_drops_trans_next … (lreq_sym … HL12) … HLK1 … Hf2) // -f2 -L1 -Hf
/3 width=3 by lreq_sym, ex2_intro/
qed-.
∀b,f,I,L1. ⬇*[b, f] L1.ⓘ{I} ≡ K1 →
∀f2. f ~⊚ f1 ≡ ⫯f2 →
∃∃L2. ⬇*[b, f] L2.ⓘ{I} ≡ K2 & L1 ≡[f2] L2 & L1.ⓘ{I} ≡[f] L2.ⓘ{I}.
-#f1 #K1 #K2 #HK12 #b #f #I #L1 #HLK1 #f2 #Hf2
+#f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1
-/2 width=6 by cfull_lift_sn, ceq_lift_sn, ex3_intro/ qed-.
+/2 width=6 by cfull_lift_sn, ceq_lift_sn/
+#I2 #L2 #HLK2 #HL12 #H >(ceq_ext_inv_eq … H) -I1
+/2 width=4 by ex3_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/notation/relations/relation_3.ma".
+include "basic_2/relocation/lexs.ma".
+
+(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION ON TERMS ***************)
+
+(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *)
+definition lex: (lenv → relation bind) → relation lenv ≝
+ λR,L1,L2. ∃∃f. 𝐈⦃f⦄ & L1 ⪤*[cfull, R, f] L2.
+
+interpretation "generic extension (local environment)"
+ 'Relation R L1 L2 = (lex R L1 L2).
(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
-(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *)
inductive lexs (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝
| lexs_atom: ∀f. lexs RN RP f (⋆) (⋆)
| lexs_next: ∀f,I1,I2,L1,L2.
--- /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/lib/star.ma".
+include "basic_2/relocation/lexs.ma".
+
+(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
+
+(* Properties with transitive closure ***************************************)
+
+lemma lexs_tc_refl: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+ ∀f. reflexive … (TC … (lexs RN RP f)).
+/3 width=1 by lexs_refl, TC_reflexive/ qed.
+
+lemma lexs_tc_next_sn: ∀RN,RP. (∀L. reflexive … (RN L)) →
+ ∀f,I2,L1,L2. TC … (lexs RN RP f) L1 L2 → ∀I1. RN L1 I1 I2 →
+ TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
+#RN #RP #HRN #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
+/3 width=3 by lexs_next, TC_strap, inj/
+qed.
+
+lemma lexs_tc_next_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+ ∀f,I1,I2,L1. (LTC … RN) L1 I1 I2 → ∀L2. L1 ⪤*[RN, RP, f] L2 →
+ TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
+#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
+/4 width=5 by lexs_refl, lexs_next, step, inj/
+qed.
+
+lemma lexs_tc_push_sn: ∀RN,RP. (∀L. reflexive … (RP L)) →
+ ∀f,I2,L1,L2. TC … (lexs RN RP f) L1 L2 → ∀I1. RP L1 I1 I2 →
+ TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
+#RN #RP #HRP #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
+/3 width=3 by lexs_push, TC_strap, inj/
+qed.
+
+lemma lexs_tc_push_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+ ∀f,I1,I2,L1. (LTC … RP) L1 I1 I2 → ∀L2. L1 ⪤*[RN, RP, f] L2 →
+ TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
+#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
+/4 width=5 by lexs_refl, lexs_push, step, inj/
+qed.
+
+lemma lexs_tc_inj_sn: ∀RN,RP,f,L1,L2. L1 ⪤*[RN, RP, f] L2 → L1 ⪤*[LTC … RN, RP, f] L2.
+#RN #RP #f #L1 #L2 #H elim H -f -L1 -L2
+/3 width=1 by lexs_push, lexs_next, inj/
+qed.
+
+lemma lexs_tc_inj_dx: ∀RN,RP,f,L1,L2. L1 ⪤*[RN, RP, f] L2 → L1 ⪤*[RN, LTC … RP, f] L2.
+#RN #RP #f #L1 #L2 #H elim H -f -L1 -L2
+/3 width=1 by lexs_push, lexs_next, inj/
+qed.
+
+(* Main properties with transitive closure **********************************)
+
+theorem lexs_tc_next: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+ ∀f,I1,I2,L1. (LTC … RN) L1 I1 I2 → ∀L2. TC … (lexs RN RP f) L1 L2 →
+ TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
+#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
+/4 width=5 by lexs_tc_next_sn, lexs_tc_refl, trans_TC/
+qed.
+
+theorem lexs_tc_push: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+ ∀f,I1,I2,L1. (LTC … RP) L1 I1 I2 → ∀L2. TC … (lexs RN RP f) L1 L2 →
+ TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}).
+#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2
+/4 width=5 by lexs_tc_push_sn, lexs_tc_refl, trans_TC/
+qed.
+
+(* Basic_2A1: uses: TC_lpx_sn_ind *)
+theorem lexs_tc_step_dx: ∀RN,RP. (∀f. 𝐈⦃f⦄ → s_rs_transitive … RP (λ_.lexs RN RP f)) →
+ ∀f,L1,L. L1 ⪤*[RN, RP, f] L → 𝐈⦃f⦄ →
+ ∀L2. L ⪤*[RN, LTC … RP, f] L2 → L1⪤* [RN, LTC … RP, f] L2.
+#RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L
+[ #f #_ #Y #H -HRP >(lexs_inv_atom1 … H) -Y // ]
+#f #I1 #I #L1 #L #HL1 #HI1 #IH #Hf #Y #H
+[ elim (isid_inv_next … Hf) -Hf //
+| lapply (isid_inv_push … Hf ??) -Hf [3: |*: // ] #Hf
+ elim (lexs_inv_push1 … H) -H #I2 #L2 #HL2 #HI2 #H destruct
+ @lexs_push [ /2 width=1 by/ ] -L2 -IH
+ @(TC_strap … HI1) -HI1
+ @(HRP … HL1) // (**) (* auto fails *)
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: TC_lpx_sn_inv_lpx_sn_LTC *)
+lemma lexs_tc_dx: ∀RN,RP. (∀f. 𝐈⦃f⦄ → s_rs_transitive … RP (λ_.lexs RN RP f)) →
+ ∀f. 𝐈⦃f⦄ → ∀L1,L2. TC … (lexs RN RP f) L1 L2 → L1 ⪤*[RN, LTC … RP, f] L2.
+#RN #RP #HRP #f #Hf #L1 #L2 #H @(TC_ind_dx ??????? H) -L1
+/3 width=3 by lexs_tc_step_dx, lexs_tc_inj_dx/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lexs_inv_tc_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+ ∀f,L1,L2. L1 ⪤*[LTC … RN, RP, f] L2 → TC … (lexs RN RP f) L1 L2.
+#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
+/2 width=1 by lexs_tc_next, lexs_tc_push_sn, lexs_atom, inj/
+qed-.
+
+(* Basic_2A1: uses: lpx_sn_LTC_TC_lpx_sn *)
+lemma lexs_inv_tc_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) →
+ ∀f,L1,L2. L1 ⪤*[RN, LTC … RP, f] L2 → TC … (lexs RN RP f) L1 L2.
+#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2
+/2 width=1 by lexs_tc_push, lexs_tc_next_sn, lexs_atom, inj/
+qed-.
(**************************************************************************)
include "basic_2/notation/relations/lazyeqsn_3.ma".
-include "basic_2/syntax/ext2.ma".
+include "basic_2/syntax/lenv_ceq.ma".
include "basic_2/relocation/lexs.ma".
(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************)
(* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *)
-definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq cfull.
+definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq_ext cfull.
interpretation
"ranged equivalence (local environment)"
(* Basic_2A1: includes: lreq_refl *)
lemma lreq_refl: ∀f. reflexive … (lreq f).
-/3 width=1 by lexs_refl, ext2_refl/ qed.
+/2 width=1 by lexs_refl/ qed.
(* Basic_2A1: includes: lreq_sym *)
lemma lreq_sym: ∀f. symmetric … (lreq f).
-/3 width=1 by lexs_sym, ext2_sym/ qed-.
+/3 width=2 by lexs_sym, cext2_sym/ qed-.
(* Basic inversion lemmas ***************************************************)
(* Basic_2A1: includes: lreq_inv_pair1 *)
lemma lreq_inv_next1: ∀g,J,K1,Y. K1.ⓘ{J} ≡[⫯g] Y →
∃∃K2. K1 ≡[g] K2 & Y = K2.ⓘ{J}.
-#g #J #K1 #Y #H elim (lexs_inv_next1 … H) -H /2 width=3 by ex2_intro/
+#g #J #K1 #Y #H
+elim (lexs_inv_next1 … H) -H #Z #K2 #HK12 #H1 #H2 destruct
+<(ceq_ext_inv_eq … H1) -Z /2 width=3 by ex2_intro/
qed-.
(* Basic_2A1: includes: lreq_inv_zero1 lreq_inv_succ1 *)
(* Basic_2A1: includes: lreq_inv_pair2 *)
lemma lreq_inv_next2: ∀g,J,X,K2. X ≡[⫯g] K2.ⓘ{J} →
∃∃K1. K1 ≡[g] K2 & X = K1.ⓘ{J}.
-#g #J #X #K2 #H elim (lexs_inv_next2 … H) -H /2 width=3 by ex2_intro/
+#g #J #X #K2 #H
+elim (lexs_inv_next2 … H) -H #Z #K1 #HK12 #H1 #H2 destruct
+<(ceq_ext_inv_eq … H1) -J /2 width=3 by ex2_intro/
qed-.
(* Basic_2A1: includes: lreq_inv_zero2 lreq_inv_succ2 *)
(* Basic_2A1: includes: lreq_inv_pair *)
lemma lreq_inv_next: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≡[⫯f] L2.ⓘ{I2} →
L1 ≡[f] L2 ∧ I1 = I2.
-/2 width=1 by lexs_inv_next/ qed-.
+#f #I1 #I2 #L1 #L2 #H elim (lexs_inv_next … H) -H
+/3 width=3 by ceq_ext_inv_eq, conj/
+qed-.
(* Basic_2A1: includes: lreq_inv_succ *)
lemma lreq_inv_push: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≡[↑f] L2.ⓘ{I2} → L1 ≡[f] L2.
(* *)
(**************************************************************************)
+include "basic_2/syntax/ceq_ext_ceq_ext.ma".
include "basic_2/relocation/lexs_lexs.ma".
(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************)
(* Main properties **********************************************************)
theorem lreq_trans: ∀f. Transitive … (lreq f).
-/2 width=3 by lexs_trans/ qed-.
+/3 width=5 by lexs_trans, ceq_ext_trans/ qed-.
theorem lreq_canc_sn: ∀f. left_cancellable … (lreq f).
/3 width=3 by lexs_canc_sn, lreq_trans, lreq_sym/ 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/syntax/lenv_ceq.ma".
+
+(* CONTEXT-DEPENDENT SYNTACTIC EQUIVALENCE FOR BINDERS **********************)
+
+(* Main properties **********************************************************)
+
+theorem ceq_ext_trans: ∀L1,I1,I. ceq_ext L1 I1 I →
+ ∀L2,I2. ceq_ext L2 I I2 → ∀L3. ceq_ext L3 I1 I2.
+#L1 #I1 #I * -I1 -I //
+#I1 #V1 #V #HV1 #L2 #Z #H elim (ext2_inv_pair_sn … H) -H //
+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/lib/star.ma".
+include "basic_2/syntax/ext2.ma".
+
+(* EXTENSION TO BINDERS OF A RELATION FOR TERMS *****************************)
+
+(* Properties with transitive closure ***************************************)
+
+lemma ext2_tc_pair: ∀R,I,V1,V2. TC … R V1 V2 →
+ TC … (ext2 R) (BPair I V1) (BPair I V2).
+#R #I #V1 #V2 #H elim H -H -V2
+/3 width=3 by ext2_pair, step, inj/
+qed.
+
+lemma ext2_tc_inj: ∀R,I1,I2. ext2 R I1 I2 → ext2 (TC … R) I1 I2.
+#R #I1 #I2 * -I1 -I2
+/3 width=1 by ext2_unit, ext2_pair, inj/
+qed.
+
+(* Main properties with transitive closure **********************************)
+
+theorem ext2_tc_step: ∀R,I1,I. ext2 (TC … R) I1 I →
+ ∀I2. ext2 R I I2 → ext2 (TC … R) I1 I2.
+#R #I1 #I * -I1 -I
+[ #I #Z #H >(ext2_inv_unit_sn … H) -Z /2 width=1 by ext2_unit/
+| #I #V1 #V #HV1 #Z #H
+ elim (ext2_inv_pair_sn … H) -H #V2 #HV2 #H destruct
+ /3 width=3 by ext2_pair, step/
+]
+qed-.
+
+(* Advanced properties with transitive closure ******************************)
+
+lemma ext2_tc: ∀R,I1,I2. TC … (ext2 R) I1 I2 → ext2 (TC … R) I1 I2.
+#R #I1 #I2 #H elim H -I2
+/2 width=3 by ext2_tc_step, ext2_tc_inj/
+qed.
+
+(* Advanced inversion lemmas with transitive closure ************************)
+
+lemma ext2_inv_tc: ∀R,I1,I2. ext2 (TC … R) I1 I2 → TC … (ext2 R) I1 I2.
+#R #I1 #I2 * -I1 -I2
+/3 width=1 by ext2_tc_pair, ext2_unit, inj/
+qed-.
definition cfull: relation3 lenv bind bind ≝ λL,I1,I2. ⊤.
-definition ceq: relation3 lenv bind bind ≝ λL. eq ….
+definition ceq: relation3 lenv term term ≝ λL. eq ….
(* Basic properties *********************************************************)
--- /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/lenv_ext2.ma".
+
+(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********)
+
+definition ceq_ext: lenv → relation bind ≝
+ cext2 ceq.
+
+(* Basic properties *********************************************************)
+
+lemma ceq_ext_refl (L): reflexive … (ceq_ext L).
+/2 width=1 by ext2_refl/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ceq_ext_inv_eq: ∀L,I1,I2. ceq_ext L I1 I2 → I1 = I2.
+#L #I1 #I2 * -I1 -I2 //
+qed-.
}
]
[ { "generic entrywise extension" * } {
- [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_length" + "lexs_lexs" * ]
+ [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
}
]
}
}
]
[ { "binders for local environments" * } {
- [ "ext2" "ext2_ext2" * ]
+ [ "ext2" "ext2_tc" + "ext2_ext2" * ]
[ "bind" "bind_weight" * ]
}
]
projects / helm.git / commitdiff