--- /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( ⫱ * [ term 46 L , break term 46 K ] term 46 f )"
+ non associative with precedence 46
+ for @{ 'DropPreds $L $K $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 "basic_2/relocation/drops_weight.ma".
+include "basic_2/s_computation/fqup_weight.ma".
+include "basic_2/s_computation/fqus_fqup.ma".
+include "basic_2/static/frees.ma".
+
+corec lemma sle_refl: ∀f. f ⊆ f.
+#f cases (pn_split f) * #g #H
+[ @(sle_push … H H) | @(sle_next … H H) ] -H //
+qed.
+
+lemma sle_inv_tl1: ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ⫯f2.
+#f1 elim (pn_split f1) * #g #H destruct
+/2 width=5 by sle_next, sle_weak/
+qed-.
+
+axiom sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
+ ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≡ ⫱*[n]f.
+
+axiom sor_sle1: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
+ ∀g. g ⊆ f1 → g ⊆ f.
+
+axiom sor_sle2: ∀f1,f2,f. f1 ⋓ f2 ≡ f →
+ ∀g. g ⊆ f2 → g ⊆ f.
+
+lemma fqus_inv_refl_atom3: ∀I,G,L,X. ⦃G, L, ⓪{I}⦄ ⊐* ⦃G, L, X⦄ → ⓪{I} = X.
+#I #G #L #X #H elim (fqus_inv_fqup … H) -H [2: * // ]
+#H lapply (fqup_fwd_fw … H) -H
+#H elim (lt_le_false … H) -H /2 width=1 by monotonic_le_plus_r/
+qed-.
+
+axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0.
+
+axiom fqus_split_fqu: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ (∧∧ G1 = G2 & L1 = L2 & T1 = T2) ∨
+ ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊐ ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄.
+
+axiom fqus_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & ⋆ = L2 & ⓪{I} = T2.
+
+axiom fqus_inv_sort1: ∀G1,G2,L1,L2,T2,s. ⦃G1, L1, ⋆s⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L1 = L2 & ⋆s = T2.
+
+axiom fqus_inv_zero1: ∀I,G1,G2,L1,L2,V1,T2. ⦃G1, L1.ⓑ{I}V1, #0⦄ ⊐* ⦃G2, L2, T2⦄ →
+ (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #0 = T2) ∨ ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄.
+
+axiom fqus_inv_lref1: ∀I,G1,G2,L1,L2,V1,T2,i. ⦃G1, L1.ⓑ{I}V1, #⫯i⦄ ⊐* ⦃G2, L2, T2⦄ →
+ (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #(⫯i) = T2) ∨ ⦃G1, L1, #i⦄ ⊐* ⦃G2, L2, T2⦄.
+
+axiom fqus_inv_gref1: ∀G1,G2,L1,L2,T2,l. ⦃G1, L1, §l⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∧∧ G1 = G2 & L1 = L2 & §l = T2.
+
+axiom fqus_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓑ{p,I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2
+ | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄
+ | ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐* ⦃G2, L2, T2⦄.
+
+axiom fqus_inv_flat1: ∀I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓕ{I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+ ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2
+ | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄
+ | ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄.
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+lemma frees_drops_sle: ∀f1,G,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
+ ∀L2,T2. ⦃G, L1, T1⦄ ⊐* ⦃G, L2, T2⦄ →
+ ∀I,n. ⬇*[n] L1 ≡ L2.ⓑ{I}T2 →
+ ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ ⫱*[⫯n] f1.
+#f1 #G #L1 #T1 #H elim H -f1 -L1 -T1
+[ #f1 #J #Hf1 #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_atom1 … H12) -H12 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+| #f1 #J #L1 #V1 #s #_ #_ #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_sort1 … H12) -H12 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+| #f1 #J #L1 #V1 #Hf1 #IH #L2 #T2 #H12
+ elim (fqus_inv_zero1 … H12) -H12 [ * | #H12 #I * ]
+ [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+ | -IH -H12 #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
+ #H destruct /3 width=3 by sle_refl, ex2_intro/
+ | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+ #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/
+ ]
+| #f1 #J #L1 #V1 #i #Hf1 #IH #L2 #T2 #H12
+ elim (fqus_inv_lref1 … H12) -H12 [ * | #H12 #I * ]
+ [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+ | -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
+ #H destruct <(fqus_inv_refl_atom3 … H12) -H12 /2 width=3 by sle_refl, ex2_intro/
+ | -Hf1 #I #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+ #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/
+ ]
+| #f1 #J #L1 #V1 #l #_ #_ #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_gref1 … H12) -H12 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+| #f1V #f1T #f1 #p #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_bind1 … H12) -H12 [ * |*: #H12 ]
+ [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+ | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12
+ /4 width=6 by sor_tls, sor_sle1, ex2_intro/
+ | -IHV elim (IHT … H12 I (⫯n)) -IHT -H12 /2 width=1 by drops_drop/ -HL12
+ <tls_xn /4 width=6 by ex2_intro, sor_tls, sor_sle2/
+ ]
+| #f1V #f1T #f1 #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12
+ elim (fqus_inv_flat1 … H12) -H12 [ * |*: #H12 ]
+ [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct
+ lapply (drops_fwd_lw … HL12) -HL12 #HL12
+ elim (lt_le_false … HL12) -HL12 //
+ | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12
+ /4 width=6 by sor_tls, sor_sle1, ex2_intro/
+ | -IHV elim (IHT … H12 … HL12) -IHT -H12 -HL12
+ /4 width=6 by ex2_intro, sor_tls, sor_sle2/
+ ]
+]
+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/rt_transition/lfpr_lfpr.ma".
+
+(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************)
+
+definition lfxs_confluent_R: relation2 … ≝
+ λRP1,RP2.
+ ∀L0,T0,T1. RP1 L0 T0 T1 → ∀T2. RP2 L0 T0 T2 →
+ ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
+ ∃∃L. L1 ⦻*[RP2, T1] L & L2 ⦻*[RP1, T2] L.
+
+(* Main properties **********************************************************)
+
+fact lfpr_conf_cpr_atom_atom:
+ ∀h,I,G,L0. (
+ ∀L,T. ⦃G, L0, ⓪{I}⦄ ⊐+ ⦃G, L, T⦄ →
+ ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 →
+ ∀L1. ⦃G, L⦄ ⊢ ➡[h, T] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h, T] L2 →
+ ∃∃K0. ⦃G, L1⦄ ⊢ ➡[h, T1] K0 & ⦃G, L2⦄ ⊢ ➡[h, T2] K0
+ ) →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h, ⓪{I}] L2 →
+ ∃∃L. ⦃G, L1⦄ ⊢ ➡[h, ⓪{I}] L & ⦃G, L2⦄ ⊢ ➡[h, ⓪{I}] L.
+#h #I #G * [ | #K0 #J #V0 cases I -I [ | * | ] ]
+[ #_ #L1 #HL01 #L2 #HL02
+ lapply (lfpr_inv_atom_sn … HL01) -HL01 #H destruct
+ lapply (lfpr_inv_atom_sn … HL02) -HL02 #H destruct
+ /2 width=3 by ex2_intro/
+| #s #IH #L1 #HL01 #L2 #HL02
+ elim (lfxs_inv_sort_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
+ elim (lfxs_inv_sort_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
+ elim (IH … HK01 … HK02) -IH -HK01 -HK02
+ /3 width=5 by lfpr_sort, fqu_fqup, fqu_drop, ex2_intro/
+| #IH #L1 #HL01 #L2 #HL02
+ elim (lfpr_inv_zero_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct
+ elim (lfpr_inv_zero_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct
+ elim (cpr_conf_lfpr … HV01 … HV02 … HK01 … HK02) #V #HV1 #HV2
+ elim (IH … HV01 … HV02 … HK01 … HK02) -IH -HV01 -HV02 -HK01 -HK02
+ /3 width=5 by lfpr_zero, fqu_fqup, fqu_drop, ex2_intro/
+| #i #IH #L1 #HL01 #L2 #HL02
+ elim (lfxs_inv_lref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
+ elim (lfxs_inv_lref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
+ elim (IH … HK01 … HK02) -IH -HK01 -HK02
+ /3 width=5 by lfpr_lref, fqu_fqup, fqu_drop, ex2_intro/
+| #l #IH #L1 #HL01 #L2 #HL02
+ elim (lfxs_inv_gref_pair_sn … HL01) -HL01 #K1 #V1 #HK01 #H destruct
+ elim (lfxs_inv_gref_pair_sn … HL02) -HL02 #K2 #V2 #HK02 #H destruct
+ elim (IH … HK01 … HK02) -IH -HK01 -HK02
+ /3 width=5 by lfpr_gref, fqu_fqup, fqu_drop, ex2_intro/
+]
+qed-.
+
+theorem lfpr_conf_cpr: ∀h,G. lfxs_confluent_R (cpm 0 h G) (cpm 0 h G).
+#h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ]
+[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpr_inv_atom1_drops … H1) -H1
+ elim (cpr_inv_atom1_drops … H2) -H2
+ [ #H2 #H1 destruct
+ /3 width=7 by lfpr_conf_cpr_atom_atom/
+ | * #K0 #V0 #V2 * [2: #i2 ] #HLK0 #HV02 #HVT2 #H2 #H1 destruct
+
+(*
+
+theorem lpr_conf: ∀G. confluent … (lpr G).
+/3 width=6 by lpx_sn_conf, cpr_conf_lpr/
+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/lfxs_lfxs.ma".
+include "basic_2/static/frees_frees.ma".
+
+(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
+
+theorem lfxs_conf: ∀R. R_confluent_lfxs R R R R →
+ ∀T. confluent … (lfxs R T).
+#R #H1R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
+lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
+lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
+elim (lexs_conf … HL01 … HL02)
--- /dev/null
+include "basic_2/notation/functions/droppreds_3.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+axiom pred_minus: ∀x,y. y < x → ⫰(x - y) = x - ⫯y.
+
+(*
+axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0.
+
+lemma le_succ_trans: ∀m,n. ⫯m ≤ n → m ≤ n.
+/2 width=1 by lt_to_le/ qed-.
+*)
+
+lemma tls_pred: ∀f,n. 0 < n → ⫱*[n] f = ⫱ ⫱*[⫰n] f.
+#f #n #Hn >tls_S >S_pred //
+qed-.
+
+definition ltls (f): lenv → lenv → rtmap ≝ λL,K. ⫱*[|L|-|K|] f.
+
+interpretation "ltls (rtmap)" 'DropPreds L K f = (ltls f L K).
+
+lemma ltls_refl: ∀f,L1,L2. |L1| ≤ |L2| → ⫱*[L1, L2] f = f.
+#f #L1 #L2 #HL12 whd in ⊢ (??%?); >(eq_minus_O … HL12) -HL12 //
+qed.
+
+lemma ltls_pair2: ∀f,I,L1,L2,V. |L2| < |L1| → ⫱⫱*[L1, L2.ⓑ{I}V] f = ⫱*[L1, L2] f.
+#f #I #L1 #L2 #V #HL12 whd in ⊢ (??(?%)%); <pred_minus // <tls_pred //
+/2 width=1 by lt_plus_to_minus_r/
+qed-.
+
+lemma ltls_pair1_push: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ↑f = ⫱*[L1, L2] f.
+#f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m //
+qed.
+
+lemma ltls_pair1_next: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ⫯f = ⫱*[L1, L2] f.
+#f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m //
+qed.
+
+lemma ltls_sle_pair: ∀f1,f2,L1,L2. ⫱*[L2, L1] f2 ⊆ ⫱*[L1, L2] f1 →
+ ∀I,V1. ⫱*[L2, L1.ⓑ{I}V1] f2 ⊆ ⫱*[L1.ⓑ{I}V1, L2] ⫯f1.
+#f1 #f2 #L1 #L2 elim (lt_or_ge (|L1|) (|L2|))
+[ #HL12 >ltls_refl in ⊢ (??%→?); /2 width=1 by lt_to_le/
+ #Hf21 #I #V1 >ltls_refl in ⊢ (??%); //
+ <(ltls_pair2 … I … V1 HL12) in Hf21; -HL12 /2 width=1 by sle_inv_tl1/
+| #HL21 >ltls_refl // #Hf21 #I #V1 >ltls_refl /2 width=1 by le_S/
+ >ltls_pair1_next //
+]
+qed.
include "ground_2/relocation/rtmap_sand.ma".
include "ground_2/relocation/rtmap_sor.ma".
-include "basic_2/grammar/lenv_weight.ma".
include "basic_2/relocation/lexs.ma".
(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
/2 width=9 by lexs_trans_gen/ qed-.
(* Basic_2A1: includes: lpx_sn_conf *)
-theorem lexs_conf: ∀RN1,RP1,RN2,RP2.
- lexs_confluent RN1 RN2 RN1 RP1 RN2 RP2 →
- lexs_confluent RP1 RP2 RN1 RP1 RN2 RP2 →
- ∀f. confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f).
-#RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L0 generalize in match f; -f
-@(f_ind … lw … L0) -L0 #x #IH *
-[ #_ #f #X1 #H1 #X2 #H2 -x
- >(lexs_inv_atom1 … H1) -X1
- >(lexs_inv_atom1 … H2) -X2 /2 width=3 by lexs_atom, ex2_intro/
-| #L0 #I #V0 #Hx #f elim (pn_split f) *
- #g #H #X1 #H1 #X2 #H2 destruct
- [ elim (lexs_inv_push1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
- elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
- elim (IH … HL01 … HL02) -IH // #L #HL1 #HL2
- elim (HRP … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lexs_push, ex2_intro/
- | elim (lexs_inv_next1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
- elim (lexs_inv_next1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
- elim (IH … HL01 … HL02) -IH // #L #HL1 #HL2
- elim (HRN … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lexs_next, ex2_intro/
+theorem lexs_conf (RN1) (RP1) (RN2) (RP2): lexs_confluent RN1 RN2 RN1 RP1 RN2 RP2 →
+ lexs_confluent RP1 RP2 RN1 RP1 RN2 RP2 →
+ ∀f. confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f).
+#RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L0
+generalize in match f; -f elim L0 -L0
+[ #f #L1 #HL01 #L2 #HL02 -HRN -HRP
+ lapply (lexs_inv_atom1 … HL01) -HL01 #H destruct
+ lapply (lexs_inv_atom1 … HL02) -HL02 #H destruct
+ /2 width=3 by ex2_intro/
+| #K0 #I #V0 #IH #f #L1 #HL01 #L2 #HL02
+ elim (pn_split f) * #g #H destruct
+ [ elim (lexs_inv_push1 … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct
+ elim (lexs_inv_push1 … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct
+ elim (IH … HK01 … HK02) -IH #K #HK1 #HK2
+ elim (HRP … HV01 … HV02 … HK01 … HK02) -HRP -HRN -K0 -V0
+ /3 width=5 by lexs_push, ex2_intro/
+ | elim (lexs_inv_next1 … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct
+ elim (lexs_inv_next1 … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct
+ elim (IH … HK01 … HK02) -IH #K #HK1 #HK2
+ elim (HRN … HV01 … HV02 … HK01 … HK02) -HRN -HRP -K0 -V0
+ /3 width=5 by lexs_next, ex2_intro/
]
]
qed-.
⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, ⋆s] L2.ⓑ{I}V2.
/2 width=1 by lfxs_sort/ qed.
-lemma lfpr_zero: ∀h,I,G,L1,L2,V.
- ⦃G, L1⦄ ⊢ ➡[h, V] L2 → ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, #0] L2.ⓑ{I}V.
+lemma lfpr_zero: ∀h,I,G,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 →
+ ⦃G, L1⦄ ⊢ V1 ➡[h] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #0] L2.ⓑ{I}V2.
/2 width=1 by lfxs_zero/ qed.
lemma lfpr_lref: ∀h,I,G,L1,L2,V1,V2,i.
lemma lfpr_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ➡[h, ⓪{I}] ⋆ → Y1 = ⋆.
/2 width=3 by lfxs_inv_atom_dx/ qed-.
+lemma lfpr_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ➡[h, ⋆s] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+/2 width=1 by lfxs_inv_sort/ qed-.
+
lemma lfpr_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ➡[h, #0] Y2 →
(Y1 = ⋆ ∧ Y2 = ⋆) ∨
∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 &
Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
/2 width=1 by lfxs_inv_lref/ qed-.
+lemma lfpr_inv_gref: ∀h,G,Y1,Y2,l. ⦃G, Y1⦄ ⊢ ➡[h, §l] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+/2 width=1 by lfxs_inv_gref/ qed-.
+
lemma lfpr_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 →
⦃G, L1⦄ ⊢ ➡[h, V] L2 ∧ ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V.
/2 width=2 by lfxs_inv_bind/ qed-.
(* Advanced inversion lemmas ************************************************)
+lemma lfpr_inv_sort_pair_sn: ∀h,I,G,Y2,L1,V1,s. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, ⋆s] Y2 →
+ ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & Y2 = L2.ⓑ{I}V2.
+/2 width=2 by lfxs_inv_sort_pair_sn/ qed-.
+
+lemma lfpr_inv_sort_pair_dx: ∀h,I,G,Y1,L2,V2,s. ⦃G, Y1⦄ ⊢ ➡[h, ⋆s] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & Y1 = L1.ⓑ{I}V1.
+/2 width=2 by lfxs_inv_sort_pair_dx/ qed-.
+
lemma lfpr_inv_zero_pair_sn: ∀h,I,G,Y2,L1,V1. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #0] Y2 →
∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h] V2 &
Y2 = L2.ⓑ{I}V2.
∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & Y1 = L1.ⓑ{I}V1.
/2 width=2 by lfxs_inv_lref_pair_dx/ qed-.
+lemma lfpr_inv_gref_pair_sn: ∀h,I,G,Y2,L1,V1,l. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, §l] Y2 →
+ ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & Y2 = L2.ⓑ{I}V2.
+/2 width=2 by lfxs_inv_gref_pair_sn/ qed-.
+
+lemma lfpr_inv_gref_pair_dx: ∀h,I,G,Y1,L2,V2,l. ⦃G, Y1⦄ ⊢ ➡[h, §l] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & Y1 = L1.ⓑ{I}V1.
+/2 width=2 by lfxs_inv_gref_pair_dx/ qed-.
+
(* Basic forward lemmas *****************************************************)
lemma lfpr_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T.
/4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
qed-.
-theorem cpr_conf_lfpr: ∀h,G. lfxs_confluent (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G).
+theorem cpr_conf_lfpr: ∀h,G. R_confluent_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G).
#h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ]
[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
elim (cpr_inv_atom1_drops … H1) -H1
#h #G #L0 #T0 #T1 #HT01 #L1 #HL01
elim (cpr_conf_lfpr … HT01 T0 … L0 … HL01) /2 width=3 by ex2_intro/
qed-.
-
-(* Main properties **********************************************************)
-
-(*
-
-theorem lpr_conf: ∀G. confluent … (lpr G).
-/3 width=6 by lpx_sn_conf, cpr_conf_lpr/
-qed-.
-
-*)
lemma lfpx_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ⬈[h, ⓪{I}] ⋆ → Y1 = ⋆.
/2 width=3 by lfxs_inv_atom_dx/ qed-.
+lemma lfpx_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+/2 width=1 by lfxs_inv_sort/ qed-.
+
lemma lfpx_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ⬈[h, #0] Y2 →
(Y1 = ⋆ ∧ Y2 = ⋆) ∨
∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 &
Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
/2 width=1 by lfxs_inv_lref/ qed-.
+lemma lfpx_inv_gref: ∀h,G,Y1,Y2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+/2 width=1 by lfxs_inv_gref/ qed-.
+
lemma lfpx_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 →
⦃G, L1⦄ ⊢ ⬈[h, V] L2 ∧ ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V.
/2 width=2 by lfxs_inv_bind/ qed-.
(* Advanced inversion lemmas ************************************************)
+lemma lfpx_inv_sort_pair_sn: ∀h,I,G,Y2,L1,V1,s. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, ⋆s] Y2 →
+ ∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y2 = L2.ⓑ{I}V2.
+/2 width=2 by lfxs_inv_sort_pair_sn/ qed-.
+
+lemma lfpx_inv_sort_pair_dx: ∀h,I,G,Y1,L2,V2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y1 = L1.ⓑ{I}V1.
+/2 width=2 by lfxs_inv_sort_pair_dx/ qed-.
+
lemma lfpx_inv_zero_pair_sn: ∀h,I,G,Y2,L1,V1. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, #0] Y2 →
∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 &
Y2 = L2.ⓑ{I}V2.
∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 & Y1 = L1.ⓑ{I}V1.
/2 width=2 by lfxs_inv_lref_pair_dx/ qed-.
+lemma lfpx_inv_gref_pair_sn: ∀h,I,G,Y2,L1,V1,l. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, §l] Y2 →
+ ∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & Y2 = L2.ⓑ{I}V2.
+/2 width=2 by lfxs_inv_gref_pair_sn/ qed-.
+
+lemma lfpx_inv_gref_pair_dx: ∀h,I,G,Y1,L2,V2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & Y1 = L1.ⓑ{I}V1.
+/2 width=2 by lfxs_inv_gref_pair_dx/ qed-.
+
(* Basic forward lemmas *****************************************************)
lemma lfpx_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T.
interpretation "generic extension on referred entries (local environment)"
'RelationStar R T L1 L2 = (lfxs R T L1 L2).
-definition lfxs_confluent: relation4 (relation3 lenv term term)
- (relation3 lenv term term) … ≝
- λR1,R2,RP1,RP2.
- ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
- ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
- ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+definition R_confluent_lfxs: relation4 (relation3 lenv term term)
+ (relation3 lenv term term) … ≝
+ λR1,R2,RP1,RP2.
+ ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+ ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 →
+ ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
(* Basic properties ***********************************************************)
#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/
qed-.
+lemma pippo: ∀R1,R2,RP1,RP2. R_confluent_lfxs R1 R2 RP1 RP2 →
+ lexs_confluent R1 R2 RP1 cfull RP2 cfull.
+#R1 #R2 #RP1 #RP2 #HR #f #L0 #T0 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02
+
(* Basic inversion lemmas ***************************************************)
lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆.
#R #I #Y1 * /2 width=4 by lexs_inv_atom2/
qed-.
+lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+#R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2
+[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
+| lapply (frees_inv_sort … H1) -H1 #Hf
+ elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
+ elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct
+ /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/
+]
+qed-.
+
lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 →
(Y1 = ⋆ ∧ Y2 = ⋆) ∨
∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 &
]
qed-.
+lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 →
+ (Y1 = ⋆ ∧ Y2 = ⋆) ∨
+ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 &
+ Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2.
+#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2
+[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/
+| lapply (frees_inv_gref … H1) -H1 #Hf
+ elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct
+ elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct
+ /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/
+]
+qed-.
+
lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 →
L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2.
#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf
(* Advanced inversion lemmas ************************************************)
+lemma lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 →
+ ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2.
+#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H *
+[ #H destruct
+| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1.
+#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H *
+[ #_ #H destruct
+| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 →
∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 &
Y2 = L2.ⓑ{I}V2.
]
qed-.
+lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 →
+ ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2.
+#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H *
+[ #H destruct
+| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
+lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 →
+ ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1.
+#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H *
+[ #_ #H destruct
+| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/
+]
+qed-.
+
(* Basic forward lemmas *****************************************************)
lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2.
projects / helm.git / commitdiff