interpretation "context-free parallel computation (closure)"
'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2).
+(* Basic eliminators ********************************************************)
+
+lemma fprs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 →
+ (∀L,L2,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → R L T → R L2 T2) →
+ ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L2 T2.
+/3 width=7 by bi_TC_star_ind/ qed-.
+
+lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 →
+ (∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → R L T → R L1 T1) →
+ ∀L1,T1. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L1 T1.
+/3 width=7 by bi_TC_star_ind_dx/ qed-.
+
(* Basic properties *********************************************************)
lemma fprs_refl: bi_reflexive … fprs.
--- /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/reducibility/fpr_cpr.ma".
+include "basic_2/computation/cprs.ma".
+include "basic_2/computation/fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Properties on context-sensitive parallel computation for terms ***********)
+
+lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄.
+#L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/
+qed.
+(*
+(* Advanced propertis *******************************************************)
+
+lamma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
+ ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄.
+#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I
+elim (fpr_inv_all … H) /3 width=4/
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lamma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2.
+ ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ →
+ ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2.
+* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H
+elim (fpr_inv_all … H) -H #L #HL1 #H #HL2
+[ elim (cpr_inv_abbr1 … H) -H *
+ [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/
+ | #T #_ #_ #H destruct
+ ]
+| elim (cpr_inv_abst1 … H Abst V2) -H
+ #V #T #HV1 #_ #H destruct /3 width=4/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lamma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ →
+ ∃∃K2,V2. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ &
+ ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ &
+ L2 = K2.ⓑ{I}V2.
+#I1 #K1 #X #V1 #T1 #T2 #H
+elim (fpr_fwd_pair1 … H) -H #I2 #K2 #V2 #HT12 #H destruct
+elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/
+qed-.
+
+lamma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ →
+ ∃∃K1,V1. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ &
+ ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ &
+ L1 = K1.ⓑ{I}V1.
+#I2 #X #K2 #V2 #T1 #T2 #H
+elim (fpr_fwd_pair3 … H) -H #I1 #K1 #V1 #HT12 #H destruct
+elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/
+qed-.
+*)
(* Basic properties *********************************************************)
-lemma cpc_refl: ∀L,T. L ⊢ T ⬌ T.
+lemma cpc_refl: ∀L. reflexive … (cpc L).
/2 width=1/ qed.
-lemma cpc_sym: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → L ⊢ T2 ⬌ T1.
+lemma cpc_sym: ∀L. symmetric … (cpc L).
#L #T1 #T2 * /2 width=1/
qed.
-lemma cpc_cpr: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → ∃∃T. L ⊢ T1 ➡ T & L ⊢ T2 ➡ T.
+(* Basic forward lemmas *****************************************************)
+
+lemma cpc_fwd_cpr: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → ∃∃T. L ⊢ T1 ➡ T & L ⊢ T2 ➡ T.
#L #T1 #T2 * /2 width=3/
qed.
⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
- ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T)
+ ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ W ⬌* U → snv h g L (ⓝW.T)
.
interpretation "stratified native validity (term)"
(* Basic inversion lemmas ***************************************************)
-lemma snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
- ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g].
+fact snv_inv_lref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀i. X = #i →
+ ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g].
+#h #g #L #X * -L -X
+[ #L #k #i #H destruct
+| #I #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/
+| #a #I #L #V #T #_ #_ #i #H destruct
+| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #i #H destruct
+| #L #W #T #U #l #_ #_ #_ #_ #i #H destruct
+]
+qed.
+
+lemma snv_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊩ #i :[g] →
+ ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g].
+/2 width=3/ qed-.
+
+fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T →
+ ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g].
#h #g #L #X * -L -X
[ #L #k #a #I #V #T #H destruct
| #I0 #L #K #V0 #i #_ #_ #a #I #V #T #H destruct
⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g].
/2 width=4/ qed-.
-lemma snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T →
- ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
- ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
- ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U.
+fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T →
+ ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
+ ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
+ ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U.
#h #g #L #X * -L -X
[ #L #k #V #T #H destruct
| #I #L #K #V0 #i #_ #_ #V #T #H destruct
⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U.
/2 width=3/ qed-.
+
+fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T →
+ ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] &
+ L ⊢ W ⬌* U & ⦃h, L⦄ ⊢ T •[g, l + 1] U.
+#h #g #L #X * -L -X
+[ #L #k #W #T #H destruct
+| #I #L #K #V #i #_ #_ #W #T #H destruct
+| #a #I #L #V #T0 #_ #_ #W #T #H destruct
+| #a #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #W #T #H destruct
+| #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HWU0 #W #T #H destruct /2 width=4/
+]
+qed.
+
+lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊩ ⓝW.T :[g] →
+ ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] &
+ L ⊢ W ⬌* U & ⦃h, L⦄ ⊢ T •[g, l + 1] U.
+/2 width=3/ qed-.
lapply (xprs_aaa … HT … HTU) -HTU #H
elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct
lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/
-| #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT
- lapply (aaa_cpcs_mono … HUW A … HW) -HUW /2 width=7/ -HTU #H destruct /3 width=3/
+| #L #W #T #U #l #_ #_ #HTU #HWU * #B #HW * #A #HT
+ lapply (aaa_cpcs_mono … HWU … HW A ?) -HWU /2 width=7/ -HTU #H destruct /3 width=3/
]
qed-.
| #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct
elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW
- lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/
+ lapply (cpcs_inv_lift … HLK … HVW0 … HVW ?) // -W /3 width=4/
]
qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: pc3_refl *)
-lemma cpcs_refl: ∀L,T. L ⊢ T ⬌* T.
+lemma cpcs_refl: ∀L. reflexive … (cpcs L).
/2 width=1/ qed.
-lemma cpcs_sym: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → L ⊢ T2 ⬌* T1.
+(* Basic_1: was: pc3_s *)
+lemma cpcs_sym: ∀L. symmetric … (cpcs L).
/3 width=1/ qed.
lemma cpcs_strap1: ∀L,T1,T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2.
lemma cpcs_cpr_dx: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ⬌* T2.
/3 width=1/ qed.
+lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2.
+/3 width=1/ qed.
+
(* Basic_1: was: pc3_pr2_x *)
lemma cpcs_cpr_sn: ∀L,T1,T2. L ⊢ T2 ➡ T1 → L ⊢ T1 ⬌* T2.
/3 width=1/ qed.
+lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2.
+/3 width=1/ qed.
+
lemma cpcs_cpr_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2.
/3 width=3/ qed.
lemma cpcs_cpr_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
/3 width=3/ qed.
+lemma cpr_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
+/3 width=3/ qed-.
+
(* Basic_1: was: pc3_pr2_u2 *)
lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
/3 width=3/ qed.
-(* Basic_1: was: pc3_s *)
-lemma cprs_comm: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → L ⊢ T2 ⬌* T1.
-#L #T1 #T2 #H @(cpcs_ind … H) -T2 // /3 width=3/
-qed.
-
(* Basic_1: removed theorems 9:
clear_pc3_trans pc3_ind_left
pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
/2 width=3/ qed.
theorem cpcs_canc_sn: ∀L,T,T1,T2. L ⊢ T ⬌* T1 → L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_trans, cprs_comm/ qed. (**) (* /3 width=3/ is too slow *)
+/3 width=3 by cpcs_trans, cpcs_sym/ qed. (**) (* /3 width=3/ is too slow *)
theorem cpcs_canc_dx: ∀L,T,T1,T2. L ⊢ T1 ⬌* T → L ⊢ T2 ⬌* T → L ⊢ T1 ⬌* T2.
-/3 width=3 by cpcs_trans, cprs_comm/ qed. (**) (* /3 width=3/ is too slow *)
+/3 width=3 by cpcs_trans, cpcs_sym/ qed. (**) (* /3 width=3/ is too slow *)
lemma cpcs_abbr1: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV1 ⊢ T1 ⬌* T2 →
L ⊢ ⓓ{a}V1. T1 ⬌* ⓓ{a}V2. T2.
#L #T1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /3 width=3/
qed.
-lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2.
-/3 width=1/ qed.
-
(* Basic_1: was: pc3_pr3_x *)
lemma cpcs_cprs_sn: ∀L,T1,T2. L ⊢ T2 ➡* T1 → L ⊢ T1 ⬌* T2.
#L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /3 width=3/
qed.
-lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2.
-/3 width=1/ qed.
-
lemma cpcs_cprs_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2.
#L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /2 width=3/
qed.
-lemma cpcs_cpr_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2.
-/3 width=3/ qed-.
-
lemma cpcs_cprs_strap2: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
#L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /width=1/ /2 width=3/
qed.
-lemma cpcs_cpr_strap2: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-/3 width=3/ qed-.
-
lemma cpcs_cprs_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
#L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /2 width=3/
qed.
-lemma cpcs_cpr_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
-/3 width=3/ qed-.
-
(* Basic_1: was: pc3_pr3_conf *)
lemma cpcs_cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
#L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /width=1/ /2 width=3/
qed.
-lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2.
-/3 width=3/ qed-.
-
(* Basic_1: was: pc3_pr3_t *)
(* Basic_1: note: pc3_pr3_t should be renamed *)
lemma cprs_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
lemma cpr_cprs_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2.
/3 width=3 by step, cprs_div/ qed-.
-
-lemma cpr_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2.
-/3 width=5 by step, cprs_div/ qed-.
(* Basic properties *********************************************************)
-lemma lfpcs_refl: ∀L. ⦃L⦄ ⬌* ⦃L⦄.
+lemma lfpcs_refl: reflexive … lfpcs.
/2 width=1/ qed.
+lemma lfprs_sym: symmetric … lfpcs.
+/3 width=1/ qed.
+
lemma lfpcs_strap1: ∀L1,L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
/2 width=3/ qed.
lemma lfpcs_lfpr_conf: ∀L1,L. ⦃L⦄ ➡ ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
/3 width=3/ qed.
-
-lemma lfprs_comm: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ⦃L2⦄ ⬌* ⦃L1⦄.
-#L1 #L2 #H @(lfpcs_ind … H) -L2 // /3 width=3/
-qed.
/2 width=3/ qed.
theorem lfpcs_canc_sn: ∀L,L1,L2. ⦃L⦄ ⬌* ⦃L1⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
-/3 width=3 by lfpcs_trans, lfprs_comm/ qed.
+/3 width=3 by lfpcs_trans, lfprs_sym/ qed.
theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
-/3 width=3 by lfpcs_trans, lfprs_comm/ qed.
+/3 width=3 by lfpcs_trans, lfprs_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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CPConvStar $L1 $L2 }.
+
+include "basic_2/grammar/lenv_px_sn.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************)
+
+definition lcpcs: relation lenv ≝ lpx_sn … cpcs.
+
+interpretation "context-sensitive parallel equivalence (local environment)"
+ 'CPConvStar L1 L2 = (lcpcs L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lcpcs_inv_atom1: ∀L2. ⋆ ⊢ ⬌* L2 → L2 = ⋆.
+/2 width=2 by lpx_sn_inv_atom1/ qed-.
+
+lemma lcpcs_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ⬌* L2 →
+ ∃∃K2,V2. K1 ⊢ ⬌* K2 & K1 ⊢ V1 ⬌* V2 & L2 = K2. ⓑ{I} V2.
+/2 width=1 by lpx_sn_inv_pair1/ qed-.
+
+lemma lcpcs_inv_atom2: ∀L1. L1 ⊢ ⬌* ⋆ → L1 = ⋆.
+/2 width=2 by lpx_sn_inv_atom2/ qed-.
+
+lemma lcpcs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ⬌* K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ⬌* K2 & K1 ⊢ V1 ⬌* V2 & L1 = K1. ⓑ{I} V1.
+/2 width=1 by lpx_sn_inv_pair2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lcpcs_fwd_length: ∀L1,L2. L1 ⊢ ⬌* L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ 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/reducibility/ltpr.ma".
+include "basic_2/equivalence/lcpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************)
+
+(* Properties on context-free parallel reduction for local environments *****)
+
+lemma ltpr_lcpcs: ∀L1,L2. L1 ➡ L2 → L1 ⊢ ⬌* L2.
+#L1 #L2 #H elim H -L1 -L2 // /4 width=1/
+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/grammar/lenv_length.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **********)
+
+inductive lpx_sn (R:lenv→relation term): relation lenv ≝
+| lpx_sn_stom: lpx_sn R (⋆) (⋆)
+| lpx_sn_pair: ∀I,K1,K2,V1,V2.
+ lpx_sn R K1 K2 → R K1 V1 V2 → lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
+.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+#R #L1 #L2 * -L1 -L2
+[ #J #K1 #V1 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 →
+ ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
+#R #L1 #L2 * -L1 -L2
+[ #J #K2 #V2 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) →
+ ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L1 -L2 normalize //
+qed-.
non associative with precedence 45
for @{ 'StaticType $h $g $l $L $T1 $T2 }.
+notation "hvbox( h ⊢ break term 46 L1 • ≃ [ g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CCongS $h $g $L1 $L2 }.
+
notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )"
non associative with precedence 45
for @{ 'CrSubEqS $h $g $L1 $L2 }.
non associative with precedence 45
for @{ 'PConv $L $T1 $T2 }.
-notation "hvbox( ⦃ L1 ⦄ ⬌ ⦃ L2 ⦄ )"
+notation "hvbox( ⦃ L1 ⦄ ⬌ break ⦃ L2 ⦄ )"
non associative with precedence 45
for @{ 'FocalizedPConv $L1 $L2 }.
+notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConv $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }.
+
(* Equivalence **************************************************************)
notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )"
non associative with precedence 45
for @{ 'PConvStar $L $T1 $T2 }.
-notation "hvbox( ⦃ L1 ⦄ ⬌ * ⦃ L2 ⦄ )"
+notation "hvbox( ⦃ L1 ⦄ ⬌ * break ⦃ L2 ⦄ )"
non associative with precedence 45
for @{ 'FocalizedPConvStar $L1 $L2 }.
-notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
+notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ * break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ * break ⦃ L2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPConvStarAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ * break ⦃ L2 , break T2 ⦄ )"
non associative with precedence 45
- for @{ 'CPConvStar $L1 $L2 }.
+ for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }.
(* Dynamic typing ***********************************************************)
(* *)
(**************************************************************************)
-include "basic_2/static/aaa_ltpss_sn.ma".
-include "basic_2/reducibility/ltpr_aaa.ma".
include "basic_2/reducibility/cpr_aaa.ma".
include "basic_2/reducibility/cfpr_cpr.ma".
(**************************************************************************)
include "basic_2/unfold/ltpss_sn_alt.ma".
-include "basic_2/reducibility/ltpr.ma".
include "basic_2/reducibility/cpr_tpss.ma".
include "basic_2/reducibility/cpr_cpr.ma".
include "basic_2/reducibility/cfpr_ltpss.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************)
+(* Properties on context-sensitive parallel reduction for terms *************)
+
+lemma cpr_fpr: ∀L,T1,T2. L ⊢ T1 ➡ T2 → ⦃L, T1⦄ ➡ ⦃L, T2⦄.
+/2 width=4/ qed.
+
(* Advanced propertis *******************************************************)
lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
include "basic_2/unfold/ltpss_sn_alt.ma".
include "basic_2/static/ssta_ltpss_dx.ma".
-(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
(* Properties about sn parallel unfold **************************************)
definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop
≝ λA,B,R. ∀x,y. R x y x y.
+definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
+ ∀a1,a2,b1,b2. R a2 b2 a1 b1 → R a1 b1 a2 b2.
+
definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
∀a1,a,b1,b. R a1 b1 a b →
∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.
P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
∀a2. TC … R a1 a2 → P a2.
#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/
-qed.
+qed-.
inductive TC_dx (A:Type[0]) (R:relation A): A → A → Prop ≝
|inj_dx: ∀a,c. R a c → TC_dx A R a c
#A #B #S #R #HSR #b #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/
qed.
-inductive bi_TC (A,B:Type[0]) (R:bi_relation A B) (a:A) (b:B): A → B → Prop ≝
+inductive bi_TC (A,B:Type[0]) (R:bi_relation A B) (a:A) (b:B): relation2 A B ≝
|bi_inj : ∀c,d. R a b c d → bi_TC A B R a b c d
|bi_step: ∀c,d,e,f. bi_TC A B R a b c d → R c d e f → bi_TC A B R a b e f.
+lemma bi_TC_strap: ∀A,B. ∀R:bi_relation A B. ∀a1,a,a2,b1,b,b2.
+ R a1 b1 a b → bi_TC … R a b a2 b2 → bi_TC … R a1 b1 a2 b2.
+#A #B #R #a1 #a #a2 #b1 #b #b2 #HR #H elim H -a2 -b2 /2 width=4/ /3 width=4/
+qed.
+
lemma bi_TC_reflexive: ∀A,B,R. bi_reflexive A B R →
bi_reflexive A B (bi_TC … R).
/2 width=1/ qed.
-lemma bi_TC_strap: ∀A,B. ∀R:bi_relation A B. ∀a1,a,a2,b1,b,b2.
- R a1 b1 a b → bi_TC … R a b a2 b2 → bi_TC … R a1 b1 a2 b2.
-#A #B #R #a1 #a #a2 #b1 #b #b2 #HR #H elim H -a2 -b2 /2 width=4/ /3 width=4/
+inductive bi_TC_dx (A,B:Type[0]) (R:bi_relation A B): bi_relation A B ≝
+ |bi_inj_dx : ∀a1,a2,b1,b2. R a1 b1 a2 b2 → bi_TC_dx A B R a1 b1 a2 b2
+ |bi_step_dx : ∀a1,a,a2,b1,b,b2. R a1 b1 a b → bi_TC_dx A B R a b a2 b2 →
+ bi_TC_dx A B R a1 b1 a2 b2.
+
+lemma bi_TC_dx_strap: ∀A,B. ∀R: bi_relation A B.
+ ∀a1,a,a2,b1,b,b2. bi_TC_dx A B R a1 b1 a b →
+ R a b a2 b2 → bi_TC_dx A B R a1 b1 a2 b2.
+#A #B #R #a1 #a #a2 #b1 #b #b2 #H1 elim H1 -a -b /3 width=4/
+qed.
+
+lemma bi_TC_to_bi_TC_dx: ∀A,B. ∀R: bi_relation A B.
+ ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 →
+ bi_TC_dx … R a1 b1 a2 b2.
+#A #B #R #a1 #a2 #b1 #b2 #H12 elim H12 -a2 -b2 /2 width=4/
+qed.
+
+lemma bi_TC_dx_to_bi_TC: ∀A,B. ∀R: bi_relation A B.
+ ∀a1,a2,b1,b2. bi_TC_dx … R a1 b1 a2 b2 →
+ bi_TC … R a1 b1 a2 b2.
+#A #b #R #a1 #a2 #b1 #b2 #H12 elim H12 -a1 -a2 -b1 -b2 /2 width=4/
+qed.
+
+fact bi_TC_ind_dx_aux: ∀A,B,R,a2,b2. ∀P:relation2 A B.
+ (∀a1,b1. R a1 b1 a2 b2 → P a1 b1) →
+ (∀a1,a,b1,b. R a1 b1 a b → bi_TC … R a b a2 b2 → P a b → P a1 b1) →
+ ∀a1,a,b1,b. bi_TC … R a1 b1 a b → a = a2 → b = b2 → P a1 b1.
+#A #B #R #a2 #b2 #P #H1 #H2 #a1 #a #b1 #b #H1
+elim (bi_TC_to_bi_TC_dx ??????? H1) -a1 -a -b1 -b
+[ #a1 #x #b1 #y #H1 #Hx #Hy destruct /2 width=1/
+| #a1 #a #x #b1 #b #y #H1 #H #IH #Hx #Hy destruct /3 width=5/
+]
+qed-.
+
+lemma bi_TC_ind_dx: ∀A,B,R,a2,b2. ∀P:relation2 A B.
+ (∀a1,b1. R a1 b1 a2 b2 → P a1 b1) →
+ (∀a1,a,b1,b. R a1 b1 a b → bi_TC … R a b a2 b2 → P a b → P a1 b1) →
+ ∀a1,b1. bi_TC … R a1 b1 a2 b2 → P a1 b1.
+#A #B #R #a2 #b2 #P #H1 #H2 #a1 #b1 #H12
+@(bi_TC_ind_dx_aux ?????? H1 H2 … H12) //
+qed-.
+
+lemma bi_TC_symmetric: ∀A,B,R. bi_symmetric A B R →
+ bi_symmetric A B (bi_TC … R).
+#A #B #R #HR #a1 #a2 #b1 #b2 #H21
+@(bi_TC_ind_dx ?????????? H21) -a2 -b2 /3 width=1/ /3 width=4/
qed.
lemma bi_TC_transitive: ∀A,B,R. bi_transitive A B (bi_TC … R).
lemma bi_TC_Conf3: ∀A,B,C,S,R. bi_Conf3 A B C S R → bi_Conf3 A B C S (bi_TC … R).
#A #B #C #S #R #HSR #c #a1 #b1 #Hab1 #a2 #b2 #H elim H -a2 -b2 /2 width=4/
qed.
+
+lemma bi_TC_star_ind: ∀A,B,R. bi_reflexive A B R → ∀a1,b1. ∀P:relation2 A B.
+ P a1 b1 → (∀a,a2,b,b2. bi_TC … R a1 b1 a b → R a b a2 b2 → P a b → P a2 b2) →
+ ∀a2,b2. bi_TC … R a1 b1 a2 b2 → P a2 b2.
+#A #B #R #HR #a1 #b1 #P #H1 #IH #a2 #b2 #H12 elim H12 -a2 -b2 /3 width=5/
+qed-.
+
+lemma bi_TC_star_ind_dx: ∀A,B,R. bi_reflexive A B R →
+ ∀a2,b2. ∀P:relation2 A B. P a2 b2 →
+ (∀a1,a,b1,b. R a1 b1 a b → bi_TC … R a b a2 b2 → P a b → P a1 b1) →
+ ∀a1,b1. bi_TC … R a1 b1 a2 b2 → P a1 b1.
+#A #B #R #HR #a2 #b2 #P #H2 #IH #a1 #b1 #H12
+@(bi_TC_ind_dx … P ? IH … H12) /3 width=5/
+qed-.
projects / helm.git / commitdiff