/3 width=3 by tc_lfxs_step_dx, lfxs_pair_refl, inj/
qed.
+lemma tc_lfxs_tc: ∀R,L1,L2,T,f. 𝐈⦃f⦄ → TC … (lexs cfull (cext2 R) f) L1 L2 →
+ L1 ⪤**[R, T] L2.
+#R #L1 #L2 #T #f #Hf #H elim H -L2
+[ elim (frees_total L1 T) | #L elim (frees_total L T) ]
+/5 width=7 by lexs_sdj, tc_lfxs_step_dx, sdj_isid_sn, inj, ex2_intro/
+qed.
+
(* Advanced eliminators *****************************************************)
lemma tc_lfxs_ind_sn: ∀R. c_reflexive … R →
--- /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/ext2_tc.ma".
+include "basic_2/relocation/lexs_tc.ma".
+include "basic_2/relocation/lex.ma".
+include "basic_2/static/lfeq_fqup.ma".
+include "basic_2/static/lfeq_lfeq.ma".
+include "basic_2/i_static/tc_lfxs_fqup.ma".
+
+(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
+
+(* Properties with generic extension of a context sensitive relation ********)
+
+lemma tc_lfxs_lex: ∀R. c_reflexive … R →
+ ∀L1,L2,T. L1 ⪤[LTC … R] L2 → L1 ⪤**[R, T] L2.
+#R #HR #L1 #L2 #T *
+/5 width=7 by tc_lfxs_tc, lexs_inv_tc_dx, lexs_co, ext2_inv_tc, ext2_refl/
+qed.
+
+lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R →
+ ∀L1,L. L1 ⪤[LTC … R] L → ∀L2,T. L ≡[T] L2 →
+ L1 ⪤**[R, T] L2.
+/3 width=3 by tc_lfxs_lex, tc_lfxs_step_dx, lfeq_fwd_lfxs/ qed.
+
+(* Inversion lemmas with generic extension of a context sensitive relation **)
+
+lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
+ lexs_frees_confluent (cext2 R) cfull →
+ s_rs_transitive_isid cfull (cext2 R) →
+ lfeq_transitive R →
+ ∀L1,L2,T. L1 ⪤**[R, T] L2 →
+ ∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2.
+#R #H1R #H2R #H3R #H4R #L1 #L2 #T #H
+@(tc_lfxs_ind_sn … H1R … H) -H -L2
+[ /4 width=3 by lfeq_refl, lex_refl, inj, ex2_intro/
+| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0
+ lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 // * #f1 #Hf1 #HL2
+ elim (lexs_sdj_split … ceq_ext … HL2 f0 ?) -HL2
+ [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ]
+ lapply (lexs_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H
+ elim (H2R … Hf1 … H) -H #f2 #Hf2 #Hf21
+ lapply (sle_lexs_trans … HL02 … Hf21) -f1 // #HL02
+ lapply (lexs_co ?? cfull (LTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1
+ /8 width=11 by lexs_inv_tc_dx, lexs_tc_dx, lexs_co, ext2_tc, ext2_refl, step, ex2_intro/ (**) (* full auto too slow *)
+]
+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/ext2_tc.ma".
-include "basic_2/relocation/lexs_tc.ma".
-include "basic_2/relocation/lex.ma".
-include "basic_2/static/lfeq_fqup.ma".
-include "basic_2/static/lfxs_lfxs.ma".
-include "basic_2/i_static/tc_lfxs_fqup.ma".
-
-(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
-
-lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
- (lexs_frees_confluent (cext2 R) cfull) →
- (∀f. 𝐈⦃f⦄ → s_rs_transitive … (cext2 R) (λ_.lexs cfull (cext2 R) f)) →
- ∀L1,L2,T. L1 ⪤**[R, T] L2 →
- ∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2.
-#R #H1R #H2R #H3R #L1 #L2 #T #H
-@(tc_lfxs_ind_sn … H1R … H) -H -L2
-[ /4 width=3 by lfeq_refl, lex_refl, inj, ex2_intro/
-| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0
- lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 * #f1 #Hf1 #HL2
- elim (lexs_sdj_split … ceq_ext … HL2 f0 ?) -HL2
- [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ]
- lapply (lexs_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H
- elim (H2R … Hf1 … H) -H #f2 #Hf2 #Hf21
- lapply (sle_lexs_trans … HL02 … Hf21) -f1 // #HL02
- lapply (lexs_co ?? cfull (LTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1
- lapply (lexs_inv_tc_dx … HL1) -HL1 /2 width=1 by ext2_refl/ #HL1
- lapply (step ????? HL1 … HL0) -L #HL10
- lapply (lexs_tc_dx … H3R … HL10) -HL10 // #HL10
- lapply (lexs_co … cfull (cext2 (LTC … R)) … HL10) -HL10 /2 width=1 by ext2_tc/ #HL10
- /3 width=5 by ex2_intro/
-]
-qed-.
Transitive … (lexs RN RP f).
/2 width=9 by lexs_trans_gen/ qed-.
+theorem lexs_trans_id_cfull: ∀R1,R2,R3,L1,L,f. L1 ⪤*[R1, cfull, f] L → 𝐈⦃f⦄ →
+ ∀L2. L ⪤*[R2, cfull, f] L2 → L1 ⪤*[R3, cfull, f] L2.
+#R1 #R2 #R3 #L1 #L #f #H elim H -L1 -L -f
+[ #f #Hf #L2 #H >(lexs_inv_atom1 … H) -L2 // ]
+#f #I1 #I #K1 #K #HK1 #_ #IH #Hf #L2 #H
+[ elim (isid_inv_next … Hf) | lapply (isid_inv_push … Hf ??) ] -Hf [5: |*: // ] #Hf
+elim (lexs_inv_push1 … H) -H #I2 #K2 #HK2 #_ #H destruct
+/3 width=1 by lexs_push/
+qed-.
+
(* Basic_2A1: includes: lpx_sn_conf *)
theorem lexs_conf (RN1) (RP1) (RN2) (RP2):
∀L,f.
(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
+definition s_rs_transitive_isid: relation (relation3 lenv bind bind) ≝ λRN,RP.
+ ∀f. 𝐈⦃f⦄ → s_rs_transitive … RP (λ_.lexs RN RP f).
+
(* Properties with transitive closure ***************************************)
lemma lexs_tc_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP →
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)) →
+theorem lexs_tc_step_dx: ∀RN,RP. s_rs_transitive_isid RN RP →
∀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
(* 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)) →
+lemma lexs_tc_dx: ∀RN,RP. s_rs_transitive_isid RN RP →
∀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/
(* Basic properties *********************************************************)
-lemma fqu_lref_S: ∀b,I,G,L,V,i. ⦃G, L.ⓑ{I}V, #⫯i⦄ ⊐[b] ⦃G, L, #i⦄.
+lemma fqu_sort: ∀b,I,G,L,s. ⦃G, L.ⓘ{I}, ⋆s⦄ ⊐[b] ⦃G, L, ⋆s⦄.
+/2 width=1 by fqu_drop/ qed.
+
+lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G, L.ⓘ{I}, #⫯i⦄ ⊐[b] ⦃G, L, #i⦄.
+/2 width=1 by fqu_drop/ qed.
+
+lemma fqu_gref: ∀b,I,G,L,l. ⦃G, L.ⓘ{I}, §l⦄ ⊐[b] ⦃G, L, §l⦄.
/2 width=1 by fqu_drop/ qed.
(* Basic inversion lemmas ***************************************************)
interpretation
"degree-based ranged equivalence (local environment)"
'StarEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2).
-(*
-definition lfdeq_transitive: predicate (relation3 lenv term term) ≝
- λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≛[h, o, T1] L2 → R L1 T1 T2.
-*)
+
(* Basic properties ***********************************************************)
lemma frees_tdeq_conf_lexs: ∀h,o,f,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → ∀T2. T1 ≛[h, o] T2 →
"syntactic equivalence on referred entries (local environment)"
'LazyEqSn T L1 L2 = (lfeq T L1 L2).
-(***************************************************)
+(* Basic_2A1: uses: lleq_transitive *)
+definition lfeq_transitive: predicate (relation3 lenv term term) ≝
+ λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2.
-axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L →
- ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
+(* Basic_properties *********************************************************)
+
+lemma lfxs_transitive_lfeq: ∀R. lfxs_transitive ceq R R → lfeq_transitive R.
+/2 width=5 by/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfeq_transitive_inv_lfxs: ∀R. lfeq_transitive R → lfxs_transitive ceq R R.
+/2 width=3 by/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+(* Basic_2A1: was: llpx_sn_lrefl *)
+(* Note: this should have been lleq_fwd_llpx_sn *)
+lemma lfeq_fwd_lfxs: ∀R. c_reflexive … R →
+ ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤*[R, T] L2.
+#R #HR #L1 #L2 #T * #f #Hf #HL12
+/4 width=7 by lexs_co, cext2_co, ex2_intro/
+qed-.
(* Basic_2A1: removed theorems 10:
lleq_ind lleq_fwd_lref
--- /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/lfxs_lfxs.ma".
+include "basic_2/static/lfeq.ma".
+
+(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
+
+(* Advanced forward lemmas **************************************************)
+
+(* Note: the proof should may invoke lfeq_transitive_inv_lfxs *)
+lemma lfeq_lfxs_trans: ∀R. c_reflexive … R → lfeq_transitive R →
+ ∀L1,L,T. L1 ≡[T] L →
+ ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
+/3 width=9 by lfxs_trans_gen/ qed-.
∀L1. L0 ⪤*[RP1, T0] L1 → ∀L2. L0 ⪤*[RP2, T0] L2 →
∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+definition lfxs_confluent: relation … ≝
+ λR1,R2.
+ ∀K1,K,V1. K1 ⪤*[R1, V1] K → ∀V. R1 K1 V1 V →
+ ∀K2. K ⪤*[R2, V] K2 → K ⪤*[R2, V1] K2.
+
+definition lfxs_transitive: relation3 ? (relation3 ?? term) ? ≝
+ λR1,R2,R3.
+ ∀K1,K,V1. K1 ⪤*[R1, V1] K →
+ ∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2.
+
(* Basic inversion lemmas ***************************************************)
lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⪤*[R, T] Y2 → Y2 = ⋆.
]
qed-.
+theorem lfxs_trans_gen: ∀R1,R2,R3.
+ c_reflexive … R1 → c_reflexive … R2 →
+ lfxs_confluent R1 R2 → lfxs_transitive R1 R2 R3 →
+ ∀L1,T,L. L1 ⪤*[R1, T] L →
+ ∀L2. L ⪤*[R2, T] L2 → L1 ⪤*[R3, T] L2.
+#R1 #R2 #R3 #H1R #H2R #H3R #H4R #L1 #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L1 T) -L1 -T
+#G0 #L0 #T0 #IH #G #L1 * *
+[ #s #HG #HL #HT #L #H1 #L2 #H2 destruct
+ elim (lfxs_inv_sort … H1) -H1 *
+ [ #H1 #H0 destruct
+ >(lfxs_inv_atom_sn … H2) -L2 //
+ | #I1 #I #K1 #K #HK1 #H1 #H0 destruct
+ elim (lfxs_inv_sort_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct
+ /4 width=3 by lfxs_sort, fqu_fqup/
+ ]
+| * [ | #i ] #HG #HL #HT #L #H1 #L2 #H2 destruct
+ [ elim (lfxs_inv_zero … H1) -H1 *
+ [ #H1 #H0 destruct
+ >(lfxs_inv_atom_sn … H2) -L2 //
+ | #I #K1 #K #V1 #V #HK1 #H1 #H0 #H destruct
+ elim (lfxs_inv_zero_pair_sn … H2) -H2 #K2 #V2 #HK2 #HV2 #H destruct
+ /4 width=7 by lfxs_pair, fqu_fqup, fqu_lref_O/
+ | #f1 #I #K1 #K #Hf1 #HK1 #H1 #H0 destruct
+ elim (lfxs_inv_zero_unit_sn … H2) -H2 #f2 #K2 #Hf2 #HK2 #H destruct
+ /5 width=8 by lfxs_unit, lexs_trans_id_cfull, lexs_eq_repl_back, isid_inv_eq_repl/
+ ]
+ | elim (lfxs_inv_lref … H1) -H1 *
+ [ #H1 #H0 destruct
+ >(lfxs_inv_atom_sn … H2) -L2 //
+ | #I1 #I #K1 #K #HK1 #H1 #H0 destruct
+ elim (lfxs_inv_lref_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct
+ /4 width=3 by lfxs_lref, fqu_fqup/
+ ]
+ ]
+| #l #HG #HL #HT #L #H1 #L2 #H2 destruct
+ elim (lfxs_inv_gref … H1) -H1 *
+ [ #H1 #H0 destruct
+ >(lfxs_inv_atom_sn … H2) -L2 //
+ | #I1 #I #K1 #K #HK1 #H1 #H0 destruct
+ elim (lfxs_inv_gref_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct
+ /4 width=3 by lfxs_gref, fqu_fqup/
+ ]
+| #p #I #V1 #T1 #HG #HL #HT #L #H1 #L2 #H2 destruct
+ elim (lfxs_inv_bind … V1 V1 … H1) -H1 // #H1V #H1T
+ elim (lfxs_inv_bind … V1 V1 … H2) -H2 // #H2V #H2T
+ /3 width=4 by lfxs_bind/
+| #I #V1 #T1 #HG #HL #HT #L #H1 #L2 #H2 destruct
+ elim (lfxs_inv_flat … H1) -H1 #H1V #H1T
+ elim (lfxs_inv_flat … H2) -H2 #H2V #H2T
+ /3 width=3 by lfxs_flat/
+]
+qed-.
+
(* Negated inversion lemmas *************************************************)
(* Basic_2A1: uses: nllpx_sn_inv_bind nllpx_sn_inv_bind_O *)
class "water"
[ { "iterated static typing" * } {
[ { "iterated extension on referred entries" * } {
- [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
+ [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ]
}
]
}
}
]
[ { "syntactic equivalence on referred entries" * } {
- [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" * ]
+ [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ]
}
]
[ { "generic extension on referred entries" * } {
projects / helm.git / commitdiff