non associative with precedence 45
for @{ 'PSubstStar $L $T1 $d $e $T2 }.
-(* Reduction ****************************************************************)
+(* Reducibility *************************************************************)
+
+notation "hvbox( ℝ [ T ] )"
+ non associative with precedence 45
+ for @{ 'Reducible $T }.
+
+notation "hvbox( L ⊢ ℝ [ T ] )"
+ non associative with precedence 45
+ for @{ 'Reducible $L $T }.
+
+notation "hvbox( 𝕀 [ T ] )"
+ non associative with precedence 45
+ for @{ 'NotReducible $T }.
+
+notation "hvbox( L ⊢ 𝕀 [ T ] )"
+ non associative with precedence 45
+ for @{ 'NotReducible $L $T }.
+
+notation "hvbox( ℕ [ T ] )"
+ non associative with precedence 45
+ for @{ 'Normal $T }.
+
+notation "hvbox( L ⊢ ℕ [ T ] )"
+ non associative with precedence 45
+ for @{ 'Normal $L $T }.
notation "hvbox( T1 ⇒ break T2 )"
non associative with precedence 45
notation "hvbox( L1 ⊢ ⇒* break L2 )"
non associative with precedence 45
for @{ 'CPRedStar $L1 $L2 }.
+
+notation "hvbox( ⇓ T )"
+ non associative with precedence 45
+ for @{ 'SN $T }.
+
+notation "hvbox( L ⊢ ⇓ T )"
+ non associative with precedence 45
+ for @{ 'SN $L $T }.
--- /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/cl_shift.ma".
+include "Basic_2/unfold/tpss.ma".
+include "Basic_2/reducibility/tpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Basic_1: includes: pr2_delta1 *)
+definition cpr: lenv → relation term ≝
+ λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫* T2.
+
+interpretation
+ "context-sensitive parallel reduction (term)"
+ 'PRed L T1 T2 = (cpr L T1 T2).
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was by definition: pr2_free *)
+lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
+/2/ qed.
+
+lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 ⇒ T2.
+/3 width=5/ qed.
+
+lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
+/2/ qed.
+
+(* Note: new property *)
+(* Basic_1: was only: pr2_thin_dx *)
+lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
+ L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
+qed.
+
+lemma cpr_cast: ∀L,V,T1,T2.
+ L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2.
+#L #V #T1 #T2 * /3/
+qed.
+
+(* Note: it does not hold replacing |L1| with |L2| *)
+(* Basic_1: was only: pr2_change *)
+lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 →
+ ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ⇒ T2.
+#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
+lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 HL12 /3/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_1: was: pr2_gen_csort *)
+lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
+#T1 #T2 * #T #HT normalize #HT2
+<(tpss_inv_refl_O2 … HT2) -HT2 //
+qed.
+
+(* Basic_1: was: pr2_gen_sort *)
+lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k.
+#L #T2 #k * #X #H
+>(tpr_inv_atom1 … H) -H #H
+>(tpss_inv_sort1 … H) -H //
+qed.
+
+(* Basic_1: was: pr2_gen_cast *)
+lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → (
+ ∃∃V2,T2. L ⊢ V1 ⇒ V2 & L ⊢ T1 ⇒ T2 &
+ U2 = 𝕔{Cast} V2. T2
+ ) ∨ L ⊢ T1 ⇒ U2.
+#L #V1 #T1 #U2 * #X #H #HU2
+elim (tpr_inv_cast1 … H) -H /3/
+* #V #T #HV1 #HT1 #H destruct -X;
+elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/
+qed.
+
+(* Basic_1: removed theorems 5:
+ pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
+ Basic_1: removed local theorems 3:
+ pr2_free_free pr2_free_delta pr2_delta_delta
+*)
+
+(*
+pr2/fwd pr2_gen_appl
+pr2/fwd pr2_gen_abbr
+*)
--- /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/tpr_tpr.ma".
+include "Basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 →
+ L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12
+@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *)
+qed.
+
+(* Basic_1: was only: pr2_gen_cbind *)
+lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 →
+ L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
+elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
+lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
+lapply (tpss_tps … HT0) -HT0 #HT0
+@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2/ ] (**) (* /3 width=5/ is too slow *)
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2.
+#L elim L -L
+[ /2/
+| normalize /3/
+].
+qed.
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: pr2_confluence *)
+theorem cpr_conf: ∀L,U0,T1,T2. L ⊢ U0 ⇒ T1 → L ⊢ U0 ⇒ T2 →
+ ∃∃T. L ⊢ T1 ⇒ T & L ⊢ T2 ⇒ T.
+#L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2
+elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2
+elim (tpr_tpss_ltpr ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1
+elim (tpr_tpss_ltpr ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2
+elim (tpss_conf_eq … HU1 … HU2) -U /3 width=5/
+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/unfold/tpss_lift.ma".
+include "Basic_2/reducibility/tpr_lift.ma".
+include "Basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma cpr_cdelta: ∀L,K,V1,W1,W2,i.
+ ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫* W1 →
+ ↑[0, i + 1] W1 ≡ W2 → L ⊢ #i ⇒ W2.
+#L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12
+@ex2_1_intro [2: // | skip | @tpss_subst /2 width=6/ ] (**) (* /4 width=6/ is too slow *)
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was: pr2_gen_lref *)
+lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
+ T2 = #i ∨
+ ∃∃K,V1,T1. ↓[0, i] L ≡ K. 𝕓{Abbr} V1 &
+ K ⊢ V1 [0, |L| - i - 1] ≫* T1 &
+ ↑[0, i + 1] T1 ≡ T2 &
+ i < |L|.
+#L #T2 #i * #X #H
+>(tpr_inv_atom1 … H) -H #H
+elim (tpss_inv_lref1 … H) -H /2/
+* /3 width=6/
+qed.
+
+(* Basic_1: was: pr2_gen_abst *)
+lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
+ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
+/2/ qed.
+
+(* Relocation properties ****************************************************)
+
+(* Basic_1: was: pr2_lift *)
+lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K →
+ ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀T2,U2. ↑[d, e] T2 ≡ U2 →
+ K ⊢ T1 ⇒ T2 → L ⊢ U1 ⇒ U2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 * #T #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1
+elim (lt_or_ge (|K|) d) #HKd
+[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 T HLK [ /2/ | /3/ ]
+| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 T HLK // /3/
+]
+qed.
+
+(* Basic_1: was: pr2_gen_lift *)
+lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K →
+ ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ⇒ U2 →
+ ∃∃T2. ↑[d, e] T2 ≡ U2 & K ⊢ T1 ⇒ T2.
+#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
+elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
+elim (lt_or_ge (|L|) d) #HLd
+[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U HLK [ /5/ | /2/ ]
+| elim (lt_or_ge (|L|) (d + e)) #HLde
+ [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U HLK // [ /5/ | /2/ ]
+ | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U HLK // /5/
+ ]
+]
+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/tpr_tpss.ma".
+include "Basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Unfold properties ********************************************************)
+
+(* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *)
+(* Basic_1: was only: pr2_subst1 *)
+lemma cpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L2 ⊢ T1 ⇒ T2 →
+ ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
+ ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
+#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1
+elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U #HU1 #HTU
+elim (tpss_conf_eq … HT2 … HTU) -T /3/
+qed.
+
+lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 ⇒ L2 →
+ ∃∃T. L2 ⊢ T1 ⇒ T & T2 ⇒ T.
+#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
+>(ltpr_fwd_length … HL12) in HT2 #HT2
+elim (tpr_tpss_ltpr … HL12 … HT2) -L1 HT2 /3/
+qed.
+
+lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 →
+ ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
+ ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 ⇒ U2.
+#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1
+elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2
+elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U2 #HU12 #HTU2
+lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is 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/unfold/ltpss.ma".
+include "Basic_2/reducibility/ltpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+definition lcpr: relation lenv ≝
+ λL1,L2. ∃∃L. L1 ⇒ L & L [0, |L|] ≫* L2
+.
+
+interpretation
+ "context-sensitive parallel reduction (environment)"
+ 'CPRed L1 L2 = (lcpr L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lcpr_refl: ∀L. L ⊢ ⇒ L.
+/2/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ⇒ L2 → L2 = ⋆.
+#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 //
+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/tpr.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+inductive ltpr: relation lenv ≝
+| ltpr_stom: ltpr (⋆) (⋆)
+| ltpr_pair: ∀K1,K2,I,V1,V2.
+ ltpr K1 K2 → V1 ⇒ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
+.
+
+interpretation
+ "context-free parallel reduction (environment)"
+ 'PRed L1 L2 = (ltpr L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltpr_refl: ∀L:lenv. L ⇒ L.
+#L elim L -L /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ⇒ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 L2
+[ //
+| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
+]
+qed.
+
+(* Basic_1: was: wcpr0_gen_sort *)
+lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆.
+/2/ qed.
+
+fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+ ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+#L1 #L2 * -L1 L2
+[ #K1 #I #V1 #H destruct
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
+]
+qed.
+
+(* Basic_1: was: wcpr0_gen_head *)
+lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 →
+ ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+/2/ qed.
+
+fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆.
+#L1 #L2 * -L1 L2
+[ //
+| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
+]
+qed.
+
+lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆.
+/2/ qed.
+
+fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ⇒ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
+ ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
+#L1 #L2 * -L1 L2
+[ #K2 #I #V2 #H destruct
+| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/
+]
+qed.
+
+lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 →
+ ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
+/2/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|.
+#L1 #L2 #H elim H -H L1 L2; normalize //
+qed.
+
+(* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
--- /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/tpr_lift.ma".
+include "Basic_2/reducibility/ltpr.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Basic_1: was: wcpr0_ldrop *)
+lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 →
+ ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2.
+#L1 #K1 #d #e #H elim H -H L1 K1 d e
+[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
+| #K1 #I #V1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
+ elim (IHLK1 … HL12) -IHLK1 HL12 /3/
+| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
+ elim (tpr_inv_lift … HV12 … HWV1) -HV12 HWV1;
+ elim (IHLK1 … HL12) -IHLK1 HL12 /3 width=5/
+]
+qed.
+
+(* Basic_1: was: wcpr0_ldrop_back *)
+lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 →
+ ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2.
+#L1 #K1 #d #e #H elim H -H L1 K1 d e
+[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
+| #K1 #I #V1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
+ elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct -X;
+ elim (lift_total W2 d e) #V2 #HWV2
+ lapply (tpr_lift … HW12 … HWV1 … HWV2) -HW12 HWV1;
+ elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
+]
+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/substitution/tps_lift.ma".
+include "Basic_2/reducibility/trf.ma".
+include "Basic_2/reducibility/tpr.ma".
+
+(* CONTEXT-FREE NORMAL TERMS ************************************************)
+
+definition tnf: term → Prop ≝
+ NF … tpr (eq …).
+
+interpretation
+ "context-free normality (term)"
+ 'Normal T = (tnf T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma tnf_inv_abst: ∀V,T. ℕ[𝕔{Abst}V.T] → ℕ[V] ∧ ℕ[T].
+#V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 //
+| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 //
+]
+qed.
+
+lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
+#V1 #T1 #HVT1 @and3_intro
+[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 //
+| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 //
+| generalize in match HVT1 -HVT1; elim T1 -T1 * // * #W1 #U1 #_ #_ #H
+ [ elim (lift_total V1 0 1) #V2 #HV12
+ lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2/ -HV12 #H destruct
+ | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2/ #H destruct
+]
+qed.
+
+axiom tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False.
+
+axiom tnf_inv_cast: ∀V,T. ℕ[𝕔{Cast}V.T] → False.
+
+(* Basic properties *********************************************************)
+
+lemma tpr_tif_eq: ∀T1,T2. T1 ⇒ T2 → 𝕀[T1] → T1 = T2.
+#T1 #T2 #H elim H -T1 T2
+[ //
+| * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
+ [ elim (tif_inv_appl … H) -H #HV1 #HT1 #_
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ | elim (tif_inv_cast … H)
+ ]
+| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+ elim (tif_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| * #V1 #V2 #T1 #T #T2 #_ #_ #HT2 #IHV1 #IHT1 #H
+ [ -HT2 IHV1 IHT1; elim (tif_inv_abbr … H)
+ | <(tps_inv_refl_SO2 … HT2 ?) -HT2 //
+ elim (tif_inv_abst … H) -H #HV1 #HT1
+ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
+ ]
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (tif_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+| #V1 #T1 #T2 #T #_ #_ #_ #H
+ elim (tif_inv_abbr … H)
+| #V1 #T1 #T #_ #_ #H
+ elim (tif_inv_cast … H)
+]
+qed.
+
+theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1].
+/2/ qed.
+
+(* Note: this property is unusual *)
+theorem tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False.
+#T1 #H elim H -T1
+[ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2/
+| #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/
+| #V #T #_ #IHV #H elim (tnf_inv_appl … H) -H /2/
+| #V #T #H elim (tnf_inv_abbr … H)
+| #V #T #H elim (tnf_inv_cast … H)
+| #V #W #T #H elim (tnf_inv_appl … H) -H #_ #_ #H
+ elim (simple_inv_bind … H)
+]
+qed.
+
+theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1].
+/2/ qed.
+
+lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[𝕔{Abst}V.T].
+/4 width=1/ qed.
+
+lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[𝕔{Appl}V.T].
+/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/substitution/tps.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Basic_1: includes: pr0_delta1 *)
+inductive tpr: relation term ≝
+| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
+| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
+ tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+| tpr_beta : ∀V1,V2,W,T1,T2.
+ tpr V1 V2 → tpr T1 T2 →
+ tpr (𝕔{Appl} V1. 𝕔{Abst} W. T1) (𝕔{Abbr} V2. T2)
+| tpr_delta: ∀I,V1,V2,T1,T2,T.
+ tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T →
+ tpr (𝕓{I} V1. T1) (𝕓{I} V2. T)
+| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
+ tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
+ tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2)
+| tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 →
+ tpr (𝕔{Abbr} V. T) T2
+| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2
+.
+
+interpretation
+ "context-free parallel reduction (term)"
+ 'PRed T1 T2 = (tpr T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
+ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+/2/ qed.
+
+(* Basic_1: was by definition: pr0_refl *)
+lemma tpr_refl: ∀T. T ⇒ T.
+#T elim T -T //
+#I elim I -I /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}.
+#U1 #U2 * -U1 U2
+[ //
+| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
+| #V #T #T1 #T2 #_ #_ #k #H destruct
+| #V #T1 #T2 #_ #k #H destruct
+]
+qed.
+
+(* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
+lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
+/2/ qed.
+
+fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+ (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+ ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
+ U2 = 𝕓{I} V2. T
+ ) ∨
+ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
+#U1 #U2 * -U1 U2
+[ #J #I #V #T #H destruct
+| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
+| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
+| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
+| #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
+]
+qed.
+
+lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
+ (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+ ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
+ U2 = 𝕓{I} V2. T
+ ) ∨
+ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
+/2/ qed.
+
+(* Basic_1: was pr0_gen_abbr *)
+lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
+ (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+ ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
+ U2 = 𝕓{Abbr} V2. T
+ ) ∨
+ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
+#V1 #T1 #U2 #H
+elim (tpr_inv_bind1 … H) -H * /3 width=7/
+qed.
+
+fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 →
+ ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
+ U2 = 𝕗{I} V2. T2
+ | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
+ U0 = 𝕔{Abst} W. T1 &
+ U2 = 𝕔{Abbr} V2. T2 & I = Appl
+ | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
+ ↑[0,1] V2 ≡ V &
+ U0 = 𝕔{Abbr} W1. T1 &
+ U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
+ I = Appl
+ | (U0 ⇒ U2 ∧ I = Cast).
+#U1 #U2 * -U1 U2
+[ #I #J #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/
+| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/
+| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H
+ destruct -J V1 T0 /3 width=12/
+| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
+| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
+]
+qed.
+
+lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
+ ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
+ U2 = 𝕗{I} V2. T2
+ | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
+ U0 = 𝕔{Abst} W. T1 &
+ U2 = 𝕔{Abbr} V2. T2 & I = Appl
+ | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
+ ↑[0,1] V2 ≡ V &
+ U0 = 𝕔{Abbr} W1. T1 &
+ U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
+ I = Appl
+ | (U0 ⇒ U2 ∧ I = Cast).
+/2/ qed.
+
+(* Basic_1: was pr0_gen_appl *)
+lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
+ ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
+ U2 = 𝕔{Appl} V2. T2
+ | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
+ U0 = 𝕔{Abst} W. T1 &
+ U2 = 𝕔{Abbr} V2. T2
+ | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
+ ↑[0,1] V2 ≡ V &
+ U0 = 𝕔{Abbr} W1. T1 &
+ U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
+#V1 #U0 #U2 #H
+elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
+qed.
+
+(* Basic_1: was: pr0_gen_cast *)
+lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 →
+ (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2)
+ ∨ T1 ⇒ U2.
+#V1 #T1 #U2 #H
+elim (tpr_inv_flat1 … H) -H * /3 width=5/
+[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
+| #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
+]
+qed.
+
+fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
+ ∨∨ T1 = #i
+ | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
+ T1 = 𝕔{Abbr} V. T
+ | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
+#T1 #T2 * -T1 T2
+[ #I #i #H destruct /2/
+| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
+| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
+| #V #T1 #T2 #HT12 #i #H destruct /3/
+]
+qed.
+
+lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
+ ∨∨ T1 = #i
+ | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
+ T1 = 𝕔{Abbr} V. T
+ | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
+/2/ qed.
+
+(* Basic_1: removed theorems 3:
+ pr0_subst0_back pr0_subst0_fwd pr0_subst0
+ Basic_1: removed local theorems: 1: pr0_delta_tau
+*)
--- /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/tps_lift.ma".
+include "Basic_2/reducibility/tpr.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Relocation properties ****************************************************)
+
+(* Basic_1: was: pr0_lift *)
+lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
+ ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2.
+#T1 #T2 #H elim H -H T1 T2
+[ * #i #d #e #U1 #HU1 #U2 #HU2
+ lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1
+ [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
+ | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
+ | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct -U2 //
+ ]
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
+ elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/
+| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
+ elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
+ elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/
+| #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+ elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
+ elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2;
+ elim (lift_total T2 (d + 1) e) #U2 #HTU2
+ @tpr_delta
+ [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *)
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
+ elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
+ elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2;
+ elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X;
+ elim (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // /3/
+| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20
+ elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
+ elim (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // /3 width=6/
+| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2
+ elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/
+]
+qed.
+
+(* Basic_1: was: pr0_gen_lift *)
+lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
+ ∀d,e,U1. ↑[d, e] U1 ≡ T1 →
+ ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2.
+#T1 #T2 #H elim H -H T1 T2
+[ * #i #d #e #U1 #HU1
+ [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/
+ | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/
+ | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct -U1 /2/
+ ]
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
+ elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
+ elim (IHV12 … HV01) -IHV12 HV01;
+ elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
+| #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
+ elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
+ elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
+ elim (IHV12 … HV01) -IHV12 HV01;
+ elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
+| #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
+ elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X;
+ elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12
+ elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12
+ elim (tps_inv_lift1_le … HT20 … HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
+ @ex2_1_intro [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *)
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX
+ elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
+ elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
+ elim (IHV12 … HV01) -IHV12 HV01 #V3 #HV32 #HV03
+ elim (IHW12 … HW01) -IHW12 HW01 #W3 #HW32 #HW03
+ elim (IHT12 … HT01) -IHT12 HT01 #T3 #HT32 #HT03
+ elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2
+ @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *)
+| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX
+ elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X;
+ elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1
+ elim (IHT12 … HT1) -IHT12 HT1 /3 width=5/
+| #V #T1 #T2 #_ #IHT12 #d #e #X #HX
+ elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X;
+ elim (IHT12 … HT01) -IHT12 HT01 /3/
+]
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 →
+ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
+#U1 #U2 * -U1 U2
+[ #I #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1;
+ <(tps_inv_refl_SO2 … HT2 ? ? ?) -HT2 T /2 width=5/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
+| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T2 #_ #V0 #T0 #H destruct
+]
+qed.
+
+(* Basic_1: was pr0_gen_abst *)
+lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
+ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
+/2/ 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/tpr_tpss.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Confluence lemmas ********************************************************)
+
+fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ⇒ X & 𝕒{I} ⇒ X.
+/2/ qed.
+
+fact tpr_conf_flat_flat:
+ ∀I,V0,V1,T0,T1,V2,T2. (
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
+ ∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0.
+#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/
+qed.
+
+fact tpr_conf_flat_beta:
+ ∀V0,V1,T1,V2,W0,U0,T2. (
+ ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 →
+ U0 ⇒ T2 → 𝕔{Abst} W0. U0 ⇒ T1 →
+ ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X.
+#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
+elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1;
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/
+qed.
+
+(* basic-1: was:
+ pr0_cong_upsilon_refl pr0_cong_upsilon_zeta
+ pr0_cong_upsilon_cong pr0_cong_upsilon_delta
+*)
+fact tpr_conf_flat_theta:
+ ∀V0,V1,T1,V2,V,W0,W2,U0,U2. (
+ ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V →
+ W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 →
+ ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X.
+#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
+elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2
+elim (lift_total VV 0 1) #VVV #HVV
+lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
+elim (tpr_inv_abbr1 … H) -H *
+(* case 1: delta *)
+[ -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1;
+ elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2
+ elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2
+ elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1
+ @ex2_1_intro
+ [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
+ |1:skip
+ |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/
+ ] (**) (* /5 width=14/ is too slow *)
+(* case 3: zeta *)
+| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1
+ elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
+ lapply (tw_lift … HUU10) -HUU10 #HUU10
+ elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2
+ @ex2_1_intro
+ [2: @tpr_flat
+ |1: skip
+ |3: @tpr_zeta [2: @lift_flat |1: skip |3: @tpr_flat ]
+ ] /2 width=5/ (**) (* /5 width=5/ is too slow *)
+]
+qed.
+
+fact tpr_conf_flat_cast:
+ ∀X2,V0,V1,T0,T1. (
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 →
+ ∃∃X. 𝕔{Cast} V1. T1 ⇒ X & X2 ⇒ X.
+#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
+elim (IH … HT01 … HT02) -HT01 HT02 IH /3/
+qed.
+
+fact tpr_conf_beta_beta:
+ ∀W0:term. ∀V0,V1,T0,T1,V2,T2. (
+ ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
+ ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X.
+#W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
+elim (IH … HV01 … HV02) -HV01 HV02 //
+elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
+qed.
+
+(* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
+fact tpr_conf_delta_delta:
+ ∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
+ ⋆. 𝕓{I1} V1 ⊢ T1 [O, 1] ≫ TT1 →
+ ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ≫ TT2 →
+ ∃∃X. 𝕓{I1} V1. TT1 ⇒ X & 𝕓{I1} V2. TT2 ⇒ X.
+#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
+elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
+elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
+elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
+@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
+qed.
+
+fact tpr_conf_delta_zeta:
+ ∀X2,V0,V1,T0,T1,TT1,T2. (
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → T0 ⇒ T1 → ⋆. 𝕓{Abbr} V1 ⊢ T1 [O,1] ≫ TT1 →
+ T2 ⇒ X2 → ↑[O, 1] T2 ≡ T0 →
+ ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X.
+#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
+elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
+lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct -T1;
+lapply (tw_lift … HTT20) -HTT20 #HTT20
+elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/
+qed.
+
+(* Basic_1: was: pr0_upsilon_upsilon *)
+fact tpr_conf_theta_theta:
+ ∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. (
+ ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ V0 ⇒ V1 → V0 ⇒ V2 → W0 ⇒ W1 → W0 ⇒ W2 → T0 ⇒ T1 → T0 ⇒ T2 →
+ ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 →
+ ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X.
+#VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HW01 … HW02) -HW01 HW02 // #W #HW1 #HW2
+elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
+elim (lift_total V 0 1) #VV #HVV
+lapply (tpr_lift … HV1 … HVV1 … HVV) -HV1 HVV1 #HVV1
+lapply (tpr_lift … HV2 … HVV2 … HVV) -HV2 HVV2 HVV #HVV2
+@ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
+qed.
+
+fact tpr_conf_zeta_zeta:
+ ∀V0:term. ∀X2,TT0,T0,T1,T2. (
+ ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ T0 ⇒ T1 → T2 ⇒ X2 →
+ ↑[O, 1] T0 ≡ TT0 → ↑[O, 1] T2 ≡ TT0 →
+ ∃∃X. T1 ⇒ X & X2 ⇒ X.
+#V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20
+lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct -T0;
+lapply (tw_lift … HTT20) -HTT20 #HTT20
+elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/
+qed.
+
+fact tpr_conf_tau_tau:
+ ∀V0,T0:term. ∀X2,T1. (
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ T0 ⇒ T1 → T0 ⇒ X2 →
+ ∃∃X. T1 ⇒ X & X2 ⇒ X.
+#V0 #T0 #X2 #T1 #IH #HT01 #HT02
+elim (IH … HT01 … HT02) -HT01 HT02 IH /2/
+qed.
+
+(* Confluence ***************************************************************)
+
+fact tpr_conf_aux:
+ ∀Y0:term. (
+ ∀X0:term. #[X0] < #[Y0] →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X
+ ) →
+ ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 →
+ ∃∃X. X1 ⇒ X & X2 ⇒ X.
+#Y0 #IH #X0 #X1 #X2 * -X0 X1
+[ #I1 #H1 #H2 destruct -Y0;
+ lapply (tpr_inv_atom1 … H1) -H1
+(* case 1: atom, atom *)
+ #H1 destruct -X2 //
+| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+ elim (tpr_inv_flat1 … H1) -H1 *
+(* case 2: flat, flat *)
+ [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+ /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *)
+(* case 3: flat, beta *)
+ | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
+ /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *)
+(* case 4: flat, theta *)
+ | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I
+ /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *)
+(* case 5: flat, tau *)
+ | #HT02 #H destruct -I
+ /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *)
+ ]
+| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+ elim (tpr_inv_appl1 … H1) -H1 *
+(* case 6: beta, flat (repeated) *)
+ [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+ @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/
+(* case 7: beta, beta *)
+ | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2
+ /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *)
+(* case 8, beta, theta (excluded) *)
+ | #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct
+ ]
+| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0;
+ elim (tpr_inv_bind1 … H1) -H1 *
+(* case 9: delta, delta *)
+ [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
+ /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
+(* case 10: delta, zata *)
+ | #T2 #HT20 #HTX2 #H destruct -I1;
+ /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
+ ]
+| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0;
+ elim (tpr_inv_appl1 … H1) -H1 *
+(* case 11: theta, flat (repeated) *)
+ [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+ @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/
+(* case 12: theta, beta (repeated) *)
+ | #V2 #WW0 #TT0 #T2 #_ #_ #H destruct
+(* case 13: theta, theta *)
+ | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2
+ /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *)
+ ]
+| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0;
+ elim (tpr_inv_abbr1 … H1) -H1 *
+(* case 14: zeta, delta (repeated) *)
+ [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
+ @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
+(* case 15: zeta, zeta *)
+ | #T2 #HTT20 #HTX2
+ /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)
+ ]
+| #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0;
+ elim (tpr_inv_cast1 … H1) -H1
+(* case 16: tau, flat (repeated) *)
+ [ * #V2 #T2 #HV02 #HT02 #H destruct -X2
+ @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/
+(* case 17: tau, tau *)
+ | #HT02
+ /3 width=5 by tpr_conf_tau_tau/
+ ]
+]
+qed.
+
+(* Basic_1: was: pr0_confluence *)
+theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ⇒ T1 → T0 ⇒ T2 →
+ ∃∃T. T1 ⇒ T & T2 ⇒ T.
+#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/
+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/unfold/ltpss_ltpss.ma".
+include "Basic_2/reducibility/ltpr_ldrop.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Unfold properties ********************************************************)
+
+(* Basic_1: was: pr0_subst1 *)
+lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 →
+ ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
+ ∀L2. L1 ⇒ L2 →
+ ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
+#T1 #T2 #H elim H -H T1 T2
+[ #I #L1 #d #e #X #H
+ elim (tps_inv_atom1 … H) -H
+ [ #H destruct -X /2/
+ | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I;
+ elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H
+ elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X;
+ elim (lift_total V2 0 (i+1)) #U2 #HVU2
+ lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12
+ @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *)
+ ]
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X;
+ elim (IHV12 … HVW1 … HL12) -IHV12 HVW1;
+ elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/
+| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
+ elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y;
+ elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
+ elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
+| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
+ elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
+ elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
+ lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2
+ elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2
+ lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
+ lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
+ lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2
+ lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
+ elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y;
+ elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
+ elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2
+ elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
+ elim (lift_total VV2 0 1) #VV #H2VV
+ lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV
+ @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
+| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X;
+ elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2
+ elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 <minus_plus_m_m /3/
+| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
+ elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
+ elim (IHT12 … HTT1 … HL12) -IHT12 HTT1 HL12 /3/
+]
+qed.
+
+lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ⇒ V2 → T1 ⇒ T2 →
+ ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 →
+ ∃∃U2. U1 ⇒ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ U2.
+#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -HT12 HTU1 /3/
+qed.
+
+lemma tpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
+ ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
+ ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
+#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
+[ /2/
+| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
+ elim (tpr_tps_ltpr … HUT … HU1 … HL12) -HUT HU1 HL12 #U2 #HU12 #HTU2
+ lapply (tpss_trans_eq … HT2 … HTU2) -T /2/
+]
+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/term_simple.ma".
+
+(* CONTEXT-FREE REDUCIBLE AND IRREDUCIBLE TERMS *****************************)
+
+(* reducible terms *)
+inductive trf: term → Prop ≝
+| trf_abst_sn: ∀V,T. trf V → trf (𝕔{Abst} V. T)
+| trf_abst_dx: ∀V,T. trf T → trf (𝕔{Abst} V. T)
+| trf_appl_sn: ∀V,T. trf V → trf (𝕔{Appl} V. T)
+| trf_appl_dx: ∀V,T. trf T → trf (𝕔{Appl} V. T)
+| trf_abbr : ∀V,T. trf (𝕔{Abbr} V. T)
+| trf_cast : ∀V,T. trf (𝕔{Cast} V. T)
+| trf_beta : ∀V,W,T. trf (𝕔{Appl} V. 𝕔{Abst} W. T)
+.
+
+interpretation
+ "context-free reducibility (term)"
+ 'Reducible T = (trf T).
+
+(* irreducible terms *)
+definition tif: term → Prop ≝
+ λT. ℝ[T] → False.
+
+interpretation
+ "context-free irreducibility (term)"
+ 'NotReducible T = (tif T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T = 𝕒{I} → False.
+#I #T * -T
+[ #V #T #_ #H destruct
+| #V #T #_ #H destruct
+| #V #T #_ #H destruct
+| #V #T #_ #H destruct
+| #V #T #H destruct
+| #V #T #H destruct
+| #V #W #T #H destruct
+]
+qed.
+
+lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
+/2/ qed.
+
+fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
+#W #U #T * -T
+[ #V #T #HV #H destruct -V T /2/
+| #V #T #HT #H destruct -V T /2/
+| #V #T #_ #H destruct
+| #V #T #_ #H destruct
+| #V #T #H destruct
+| #V #T #H destruct
+| #V #W0 #T #H destruct
+]
+qed.
+
+lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
+/2/ qed.
+
+fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Appl} W. U →
+ ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
+#W #U #T * -T
+[ #V #T #_ #H destruct
+| #V #T #_ #H destruct
+| #V #T #HV #H destruct -V T /2/
+| #V #T #HT #H destruct -V T /2/
+| #V #T #H destruct
+| #V #T #H destruct
+| #V #W0 #T #H destruct -V U
+ @or3_intro2 #H elim (simple_inv_bind … H)
+]
+qed.
+
+lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
+/2/ qed.
+
+lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
+/2/ qed.
+
+lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
+/4/ qed.
+
+lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
+#V #T #HVT @and3_intro /3/
+generalize in match HVT -HVT; elim T -T //
+* // * #U #T #_ #_ #H elim (H ?) -H /2/
+qed.
+
+lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
+/2/ qed.
+
+(* Basic properties *********************************************************)
+
+lemma tif_atom: ∀I. 𝕀[𝕒{I}].
+/2/ qed.
+
+lemma tif_abst: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕀[𝕔 {Abst}V.T].
+#V #T #HV #HT #H
+elim (trf_inv_abst … H) -H /2/
+qed.
+
+lemma tif_appl: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕊[T] → 𝕀[𝕔{Appl}V.T].
+#V #T #HV #HT #S #H
+elim (trf_inv_appl … H) -H /2/
+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/cl_shift.ma".
-include "Basic_2/unfold/tpss.ma".
-include "Basic_2/reduction/tpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
-
-(* Basic_1: includes: pr2_delta1 *)
-definition cpr: lenv → relation term ≝
- λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫* T2.
-
-interpretation
- "context-sensitive parallel reduction (term)"
- 'PRed L T1 T2 = (cpr L T1 T2).
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was by definition: pr2_free *)
-lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
-/2/ qed.
-
-lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 ⇒ T2.
-/3 width=5/ qed.
-
-lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
-/2/ qed.
-
-(* Note: new property *)
-(* Basic_1: was only: pr2_thin_dx *)
-lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
- L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
-qed.
-
-lemma cpr_cast: ∀L,V,T1,T2.
- L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2.
-#L #V #T1 #T2 * /3/
-qed.
-
-(* Note: it does not hold replacing |L1| with |L2| *)
-(* Basic_1: was only: pr2_change *)
-lemma cpr_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 →
- ∀L2. L1 [0, |L1|] ≼ L2 → L2 ⊢ T1 ⇒ T2.
-#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
-lapply (tpss_lsubs_conf … HT2 … HL12) -HT2 HL12 /3/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-(* Basic_1: was: pr2_gen_csort *)
-lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
-#T1 #T2 * #T #HT normalize #HT2
-<(tpss_inv_refl_O2 … HT2) -HT2 //
-qed.
-
-(* Basic_1: was: pr2_gen_sort *)
-lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k.
-#L #T2 #k * #X #H
->(tpr_inv_atom1 … H) -H #H
->(tpss_inv_sort1 … H) -H //
-qed.
-
-(* Basic_1: was: pr2_gen_cast *)
-lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → (
- ∃∃V2,T2. L ⊢ V1 ⇒ V2 & L ⊢ T1 ⇒ T2 &
- U2 = 𝕔{Cast} V2. T2
- ) ∨ L ⊢ T1 ⇒ U2.
-#L #V1 #T1 #U2 * #X #H #HU2
-elim (tpr_inv_cast1 … H) -H /3/
-* #V #T #HV1 #HT1 #H destruct -X;
-elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/
-qed.
-
-(* Basic_1: removed theorems 5:
- pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
- Basic_1: removed local theorems 3:
- pr2_free_free pr2_free_delta pr2_delta_delta
-*)
-
-(*
-pr2/fwd pr2_gen_appl
-pr2/fwd pr2_gen_abbr
-*)
+++ /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/reduction/tpr_tpr.ma".
-include "Basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 →
- L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12
-@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *)
-qed.
-
-(* Basic_1: was only: pr2_gen_cbind *)
-lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 →
- L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
-elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
-lapply (tpss_tps … HT0) -HT0 #HT0
-@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2/ ] (**) (* /3 width=5/ is too slow *)
-qed.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2.
-#L elim L -L
-[ /2/
-| normalize /3/
-].
-qed.
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was: pr2_confluence *)
-theorem cpr_conf: ∀L,U0,T1,T2. L ⊢ U0 ⇒ T1 → L ⊢ U0 ⇒ T2 →
- ∃∃T. L ⊢ T1 ⇒ T & L ⊢ T2 ⇒ T.
-#L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2
-elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2
-elim (tpr_tpss_ltpr ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1
-elim (tpr_tpss_ltpr ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2
-elim (tpss_conf_eq … HU1 … HU2) -U /3 width=5/
-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/unfold/tpss_lift.ma".
-include "Basic_2/reduction/tpr_lift.ma".
-include "Basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma cpr_cdelta: ∀L,K,V1,W1,W2,i.
- ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫* W1 →
- ↑[0, i + 1] W1 ≡ W2 → L ⊢ #i ⇒ W2.
-#L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12
-@ex2_1_intro [2: // | skip | @tpss_subst /2 width=6/ ] (**) (* /4 width=6/ is too slow *)
-qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_1: was: pr2_gen_lref *)
-lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
- T2 = #i ∨
- ∃∃K,V1,T1. ↓[0, i] L ≡ K. 𝕓{Abbr} V1 &
- K ⊢ V1 [0, |L| - i - 1] ≫* T1 &
- ↑[0, i + 1] T1 ≡ T2 &
- i < |L|.
-#L #T2 #i * #X #H
->(tpr_inv_atom1 … H) -H #H
-elim (tpss_inv_lref1 … H) -H /2/
-* /3 width=6/
-qed.
-
-(* Basic_1: was: pr2_gen_abst *)
-lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
- ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-/2/ qed.
-
-(* Relocation properties ****************************************************)
-
-(* Basic_1: was: pr2_lift *)
-lemma cpr_lift: ∀L,K,d,e. ↓[d, e] L ≡ K →
- ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀T2,U2. ↑[d, e] T2 ≡ U2 →
- K ⊢ T1 ⇒ T2 → L ⊢ U1 ⇒ U2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 * #T #HT1 #HT2
-elim (lift_total T d e) #U #HTU
-lapply (tpr_lift … HT1 … HTU1 … HTU) -T1 #HU1
-elim (lt_or_ge (|K|) d) #HKd
-[ lapply (tpss_lift_le … HT2 … HLK HTU … HTU2) -T2 T HLK [ /2/ | /3/ ]
-| lapply (tpss_lift_be … HT2 … HLK HTU … HTU2) -T2 T HLK // /3/
-]
-qed.
-
-(* Basic_1: was: pr2_gen_lift *)
-lemma cpr_inv_lift: ∀L,K,d,e. ↓[d, e] L ≡ K →
- ∀T1,U1. ↑[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ⇒ U2 →
- ∃∃T2. ↑[d, e] T2 ≡ U2 & K ⊢ T1 ⇒ T2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
-elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
-elim (lt_or_ge (|L|) d) #HLd
-[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U HLK [ /5/ | /2/ ]
-| elim (lt_or_ge (|L|) (d + e)) #HLde
- [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U HLK // [ /5/ | /2/ ]
- | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U HLK // /5/
- ]
-]
-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/reduction/tpr_tpss.ma".
-include "Basic_2/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
-
-(* Unfold properties ********************************************************)
-
-(* Note: we could invoke tpss_weak_all instead of ltpr_fwd_length *)
-
-(* Basic_1: was only: pr2_subst1 *)
-lemma cpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L2 ⊢ T1 ⇒ T2 →
- ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
- ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
-#L1 #L2 #HL12 #T1 #T2 * #T #HT1 #HT2 #d #e #U1 #HTU1
-elim (tpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U #HU1 #HTU
-elim (tpss_conf_eq … HT2 … HTU) -T /3/
-qed.
-
-lemma cpr_ltpr_conf_eq: ∀L1,T1,T2. L1 ⊢ T1 ⇒ T2 → ∀L2. L1 ⇒ L2 →
- ∃∃T. L2 ⊢ T1 ⇒ T & T2 ⇒ T.
-#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12
->(ltpr_fwd_length … HL12) in HT2 #HT2
-elim (tpr_tpss_ltpr … HL12 … HT2) -L1 HT2 /3/
-qed.
-
-lemma cpr_ltpr_conf_tpss: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. L1 ⊢ T1 ⇒ T2 →
- ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
- ∃∃U2. L2 ⊢ U1 ⇒ U2 & L2 ⊢ T2 ⇒ U2.
-#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1
-elim (cpr_ltpr_conf_eq … HT12 … HL12) -HT12 #T #HT1 #HT2
-elim (cpr_tpss_ltpr … HL12 … HT1 … HTU1) -L1 HT1 #U2 #HU12 #HTU2
-lapply (tpss_weak_all … HTU2) -HTU2 #HTU2 /3 width=5/ (**) (* /4 width=5/ is 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/reduction/cpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
-
-inductive lcpr: relation lenv ≝
-| lcpr_sort: lcpr (⋆) (⋆)
-| lcpr_item: ∀K1,K2,I,V1,V2.
- lcpr K1 K2 → K2 ⊢ V1 ⇒ V2 → lcpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
-.
-
-interpretation
- "context-sensitive parallel reduction (environment)"
- 'CPRed L1 L2 = (lcpr L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lcpr_inv_item1_aux: ∀L1,L2. L1 ⊢ ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
- ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-#L1 #L2 * -L1 L2
-[ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
-]
-qed.
-
-lemma lcpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⊢ ⇒ L2 →
- ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-/2/ 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/reduction/tpr.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
-
-inductive ltpr: relation lenv ≝
-| ltpr_sort: ltpr (⋆) (⋆)
-| ltpr_item: ∀K1,K2,I,V1,V2.
- ltpr K1 K2 → V1 ⇒ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
-.
-
-interpretation
- "context-free parallel reduction (environment)"
- 'PRed L1 L2 = (ltpr L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma ltpr_refl: ∀L:lenv. L ⇒ L.
-#L elim L -L /2/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact ltpr_inv_atom1_aux: ∀L1,L2. L1 ⇒ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 L2
-[ //
-| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
-]
-qed.
-
-(* Basic_1: was: wcpr0_gen_sort *)
-lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆.
-/2/ qed.
-
-fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
- ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-#L1 #L2 * -L1 L2
-[ #K1 #I #V1 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
-]
-qed.
-
-(* Basic_1: was: wcpr0_gen_head *)
-lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 →
- ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
-/2/ qed.
-
-fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆.
-#L1 #L2 * -L1 L2
-[ //
-| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct
-]
-qed.
-
-lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆.
-/2/ qed.
-
-fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ⇒ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
- ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
-#L1 #L2 * -L1 L2
-[ #K2 #I #V2 #H destruct
-| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct -K2 I V2 /2 width=5/
-]
-qed.
-
-lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 →
- ∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
-/2/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|.
-#L1 #L2 #H elim H -H L1 L2; normalize //
-qed.
-
-(* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
+++ /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/reduction/tpr_lift.ma".
-include "Basic_2/reduction/ltpr.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
-
-(* Basic_1: was: wcpr0_ldrop *)
-lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 →
- ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2.
-#L1 #K1 #d #e #H elim H -H L1 K1 d e
-[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
-| #K1 #I #V1 #X #H
- elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
- elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
- elim (IHLK1 … HL12) -IHLK1 HL12 /3/
-| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
- elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct -X;
- elim (tpr_inv_lift … HV12 … HWV1) -HV12 HWV1;
- elim (IHLK1 … HL12) -IHLK1 HL12 /3 width=5/
-]
-qed.
-
-(* Basic_1: was: wcpr0_ldrop_back *)
-lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 →
- ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2.
-#L1 #K1 #d #e #H elim H -H L1 K1 d e
-[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
-| #K1 #I #V1 #X #H
- elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
- elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
-| #L1 #K1 #I #V1 #W1 #d #e #_ #HWV1 #IHLK1 #X #H
- elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct -X;
- elim (lift_total W2 d e) #V2 #HWV2
- lapply (tpr_lift … HW12 … HWV1 … HWV2) -HW12 HWV1;
- elim (IHLK1 … HK12) -IHLK1 HK12 /3 width=5/
-]
-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/substitution/tps.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-(* Basic_1: includes: pr0_delta1 *)
-inductive tpr: relation term ≝
-| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
-| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
- tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
-| tpr_beta : ∀V1,V2,W,T1,T2.
- tpr V1 V2 → tpr T1 T2 →
- tpr (𝕔{Appl} V1. 𝕔{Abst} W. T1) (𝕔{Abbr} V2. T2)
-| tpr_delta: ∀I,V1,V2,T1,T2,T.
- tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T →
- tpr (𝕓{I} V1. T1) (𝕓{I} V2. T)
-| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
- tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
- tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2)
-| tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 →
- tpr (𝕔{Abbr} V. T) T2
-| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2
-.
-
-interpretation
- "context-free parallel reduction (term)"
- 'PRed T1 T2 = (tpr T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
- 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
-/2/ qed.
-
-(* Basic_1: was by definition: pr0_refl *)
-lemma tpr_refl: ∀T. T ⇒ T.
-#T elim T -T //
-#I elim I -I /2/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}.
-#U1 #U2 * -U1 U2
-[ //
-| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
-| #V #T #T1 #T2 #_ #_ #k #H destruct
-| #V #T1 #T2 #_ #k #H destruct
-]
-qed.
-
-(* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
-lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
-/2/ qed.
-
-fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
- (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
- ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕓{I} V2. T
- ) ∨
- ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-#U1 #U2 * -U1 U2
-[ #J #I #V #T #H destruct
-| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
-| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
-| #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
-]
-qed.
-
-lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
- (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
- ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕓{I} V2. T
- ) ∨
- ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-/2/ qed.
-
-(* Basic_1: was pr0_gen_abbr *)
-lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
- (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
- ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕓{Abbr} V2. T
- ) ∨
- ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
-#V1 #T1 #U2 #H
-elim (tpr_inv_bind1 … H) -H * /3 width=7/
-qed.
-
-fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 →
- ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
- U2 = 𝕗{I} V2. T2
- | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2 & I = Appl
- | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
- ↑[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
- I = Appl
- | (U0 ⇒ U2 ∧ I = Cast).
-#U1 #U2 * -U1 U2
-[ #I #J #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H
- destruct -J V1 T0 /3 width=12/
-| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
-| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
-]
-qed.
-
-lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
- ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
- U2 = 𝕗{I} V2. T2
- | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2 & I = Appl
- | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
- ↑[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
- I = Appl
- | (U0 ⇒ U2 ∧ I = Cast).
-/2/ qed.
-
-(* Basic_1: was pr0_gen_appl *)
-lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
- ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
- U2 = 𝕔{Appl} V2. T2
- | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2
- | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
- ↑[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
-#V1 #U0 #U2 #H
-elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
-qed.
-
-(* Basic_1: was: pr0_gen_cast *)
-lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 →
- (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2)
- ∨ T1 ⇒ U2.
-#V1 #T1 #U2 #H
-elim (tpr_inv_flat1 … H) -H * /3 width=5/
-[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
-| #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
-]
-qed.
-
-fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
- ∨∨ T1 = #i
- | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
- T1 = 𝕔{Abbr} V. T
- | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
-#T1 #T2 * -T1 T2
-[ #I #i #H destruct /2/
-| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
-| #V #T1 #T2 #HT12 #i #H destruct /3/
-]
-qed.
-
-lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
- ∨∨ T1 = #i
- | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
- T1 = 𝕔{Abbr} V. T
- | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
-/2/ qed.
-
-(* Basic_1: removed theorems 3:
- pr0_subst0_back pr0_subst0_fwd pr0_subst0
- Basic_1: removed local theorems: 1: pr0_delta_tau
-*)
+++ /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/tps_lift.ma".
-include "Basic_2/reduction/tpr.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-(* Relocation properties ****************************************************)
-
-(* Basic_1: was: pr0_lift *)
-lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
- ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2.
-#T1 #T2 #H elim H -H T1 T2
-[ * #i #d #e #U1 #HU1 #U2 #HU2
- lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1
- [ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
- | lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
- | lapply (lift_inv_gref1 … HU2) -HU2 #H destruct -U2 //
- ]
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
- elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
- elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/
-| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
- elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
- elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
- elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/
-| #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
- elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
- elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2;
- elim (lift_total T2 (d + 1) e) #U2 #HTU2
- @tpr_delta
- [4: @(tps_lift_le … HT2 … HTU2 HTU0 ?) /2/ |1: skip |2: /2/ |3: /2/ ] (**) (*/3. is too slow *)
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
- elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
- elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
- elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2;
- elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X;
- elim (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // /3/
-| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX #T0 #HT20
- elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
- elim (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // /3 width=6/
-| #V #T1 #T2 #_ #IHT12 #d #e #X #HX #T #HT2
- elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X /3/
-]
-qed.
-
-(* Basic_1: was: pr0_gen_lift *)
-lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
- ∀d,e,U1. ↑[d, e] U1 ≡ T1 →
- ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2.
-#T1 #T2 #H elim H -H T1 T2
-[ * #i #d #e #U1 #HU1
- [ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/
- | lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/
- | lapply (lift_inv_gref2 … HU1) -HU1 #H destruct -U1 /2/
- ]
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
- elim (IHV12 … HV01) -IHV12 HV01;
- elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
-| #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
- elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
- elim (IHV12 … HV01) -IHV12 HV01;
- elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
- elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X;
- elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12
- elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12
- elim (tps_inv_lift1_le … HT20 … HUT2 ?) -HT20 HUT2 // [3: /2 width=5/ |2: skip ] #U0 #HU20 #HUT0
- @ex2_1_intro [2: /2/ |1: skip |3: /2/ ] (**) (* /3 width=5/ is slow *)
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X;
- elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
- elim (IHV12 … HV01) -IHV12 HV01 #V3 #HV32 #HV03
- elim (IHW12 … HW01) -IHW12 HW01 #W3 #HW32 #HW03
- elim (IHT12 … HT01) -IHT12 HT01 #T3 #HT32 #HT03
- elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2
- @ex2_1_intro [2: /3/ |1: skip |3: /2/ ] (**) (* /4 width=5/ is slow *)
-| #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #X #HX
- elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X;
- elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1
- elim (IHT12 … HT1) -IHT12 HT1 /3 width=5/
-| #V #T1 #T2 #_ #IHT12 #d #e #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X;
- elim (IHT12 … HT01) -IHT12 HT01 /3/
-]
-qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 →
- ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-#U1 #U2 * -U1 U2
-[ #I #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1;
- <(tps_inv_refl_SO2 … HT2 ? ? ?) -HT2 T /2 width=5/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
-]
-qed.
-
-(* Basic_1: was pr0_gen_abst *)
-lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
- ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
-/2/ 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/reduction/tpr_tpss.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-(* Confluence lemmas ********************************************************)
-
-fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ⇒ X & 𝕒{I} ⇒ X.
-/2/ qed.
-
-fact tpr_conf_flat_flat:
- ∀I,V0,V1,T0,T1,V2,T2. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
- ∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0.
-#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/
-qed.
-
-fact tpr_conf_flat_beta:
- ∀V0,V1,T1,V2,W0,U0,T2. (
- ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- V0 ⇒ V1 → V0 ⇒ V2 →
- U0 ⇒ T2 → 𝕔{Abst} W0. U0 ⇒ T1 →
- ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} V2. T2 ⇒ X.
-#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
-elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1;
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/
-qed.
-
-(* basic-1: was:
- pr0_cong_upsilon_refl pr0_cong_upsilon_zeta
- pr0_cong_upsilon_cong pr0_cong_upsilon_delta
-*)
-fact tpr_conf_flat_theta:
- ∀V0,V1,T1,V2,V,W0,W2,U0,U2. (
- ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V →
- W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 →
- ∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X.
-#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
-elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2
-elim (lift_total VV 0 1) #VVV #HVV
-lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
-elim (tpr_inv_abbr1 … H) -H *
-(* case 1: delta *)
-[ -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1;
- elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2
- elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2
- elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1
- @ex2_1_intro
- [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ]
- |1:skip
- |3: @tpr_delta [3: @tpr_flat |1: skip ] /2 width=5/
- ] (**) (* /5 width=14/ is too slow *)
-(* case 3: zeta *)
-| -HW02 HVV HVVV #UU1 #HUU10 #HUUT1
- elim (tpr_inv_lift … HU02 … HUU10) -HU02 #UU #HUU2 #HUU1
- lapply (tw_lift … HUU10) -HUU10 #HUU10
- elim (IH … HUUT1 … HUU1) -HUUT1 HUU1 IH // -HUU10 #U #HU2 #HUUU2
- @ex2_1_intro
- [2: @tpr_flat
- |1: skip
- |3: @tpr_zeta [2: @lift_flat |1: skip |3: @tpr_flat ]
- ] /2 width=5/ (**) (* /5 width=5/ is too slow *)
-]
-qed.
-
-fact tpr_conf_flat_cast:
- ∀X2,V0,V1,T0,T1. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- V0 ⇒ V1 → T0 ⇒ T1 → T0 ⇒ X2 →
- ∃∃X. 𝕔{Cast} V1. T1 ⇒ X & X2 ⇒ X.
-#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
-elim (IH … HT01 … HT02) -HT01 HT02 IH /3/
-qed.
-
-fact tpr_conf_beta_beta:
- ∀W0:term. ∀V0,V1,T0,T1,V2,T2. (
- ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
- ∃∃X. 𝕔{Abbr} V1. T1 ⇒X & 𝕔{Abbr} V2. T2 ⇒ X.
-#W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 HV02 //
-elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
-qed.
-
-(* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
-fact tpr_conf_delta_delta:
- ∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
- ⋆. 𝕓{I1} V1 ⊢ T1 [O, 1] ≫ TT1 →
- ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ≫ TT2 →
- ∃∃X. 𝕓{I1} V1. TT1 ⇒ X & 𝕓{I1} V2. TT2 ⇒ X.
-#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
-elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
-elim (tpr_tps_bind … HV2 HT2 … HTT2) -HT2 HTT2 #U2 #TTU2 #HTU2
-elim (tps_conf_eq … HTU1 … HTU2) -HTU1 HTU2 #U #HU1 #HU2
-@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
-qed.
-
-fact tpr_conf_delta_zeta:
- ∀X2,V0,V1,T0,T1,TT1,T2. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- V0 ⇒ V1 → T0 ⇒ T1 → ⋆. 𝕓{Abbr} V1 ⊢ T1 [O,1] ≫ TT1 →
- T2 ⇒ X2 → ↑[O, 1] T2 ≡ T0 →
- ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X.
-#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
-elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
-lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct -T1;
-lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/
-qed.
-
-(* Basic_1: was: pr0_upsilon_upsilon *)
-fact tpr_conf_theta_theta:
- ∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. (
- ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- V0 ⇒ V1 → V0 ⇒ V2 → W0 ⇒ W1 → W0 ⇒ W2 → T0 ⇒ T1 → T0 ⇒ T2 →
- ↑[O, 1] V1 ≡ VV1 → ↑[O, 1] V2 ≡ VV2 →
- ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X.
-#VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HW01 … HW02) -HW01 HW02 // #W #HW1 #HW2
-elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
-elim (lift_total V 0 1) #VV #HVV
-lapply (tpr_lift … HV1 … HVV1 … HVV) -HV1 HVV1 #HVV1
-lapply (tpr_lift … HV2 … HVV2 … HVV) -HV2 HVV2 HVV #HVV2
-@ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
-qed.
-
-fact tpr_conf_zeta_zeta:
- ∀V0:term. ∀X2,TT0,T0,T1,T2. (
- ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- T0 ⇒ T1 → T2 ⇒ X2 →
- ↑[O, 1] T0 ≡ TT0 → ↑[O, 1] T2 ≡ TT0 →
- ∃∃X. T1 ⇒ X & X2 ⇒ X.
-#V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20
-lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct -T0;
-lapply (tw_lift … HTT20) -HTT20 #HTT20
-elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/
-qed.
-
-fact tpr_conf_tau_tau:
- ∀V0,T0:term. ∀X2,T1. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- T0 ⇒ T1 → T0 ⇒ X2 →
- ∃∃X. T1 ⇒ X & X2 ⇒ X.
-#V0 #T0 #X2 #T1 #IH #HT01 #HT02
-elim (IH … HT01 … HT02) -HT01 HT02 IH /2/
-qed.
-
-(* Confluence ***************************************************************)
-
-fact tpr_conf_aux:
- ∀Y0:term. (
- ∀X0:term. #[X0] < #[Y0] →
- ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X
- ) →
- ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 →
- ∃∃X. X1 ⇒ X & X2 ⇒ X.
-#Y0 #IH #X0 #X1 #X2 * -X0 X1
-[ #I1 #H1 #H2 destruct -Y0;
- lapply (tpr_inv_atom1 … H1) -H1
-(* case 1: atom, atom *)
- #H1 destruct -X2 //
-| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
- elim (tpr_inv_flat1 … H1) -H1 *
-(* case 2: flat, flat *)
- [ #V2 #T2 #HV02 #HT02 #H destruct -X2
- /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *)
-(* case 3: flat, beta *)
- | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
- /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *)
-(* case 4: flat, theta *)
- | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I
- /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *)
-(* case 5: flat, tau *)
- | #HT02 #H destruct -I
- /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *)
- ]
-| #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
- elim (tpr_inv_appl1 … H1) -H1 *
-(* case 6: beta, flat (repeated) *)
- [ #V2 #T2 #HV02 #HT02 #H destruct -X2
- @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/
-(* case 7: beta, beta *)
- | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2
- /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *)
-(* case 8, beta, theta (excluded) *)
- | #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct
- ]
-| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0;
- elim (tpr_inv_bind1 … H1) -H1 *
-(* case 9: delta, delta *)
- [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
- /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
-(* case 10: delta, zata *)
- | #T2 #HT20 #HTX2 #H destruct -I1;
- /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
- ]
-| #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0;
- elim (tpr_inv_appl1 … H1) -H1 *
-(* case 11: theta, flat (repeated) *)
- [ #V2 #T2 #HV02 #HT02 #H destruct -X2
- @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/
-(* case 12: theta, beta (repeated) *)
- | #V2 #WW0 #TT0 #T2 #_ #_ #H destruct
-(* case 13: theta, theta *)
- | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2
- /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *)
- ]
-| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0;
- elim (tpr_inv_abbr1 … H1) -H1 *
-(* case 14: zeta, delta (repeated) *)
- [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
- @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
-(* case 15: zeta, zeta *)
- | #T2 #HTT20 #HTX2
- /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)
- ]
-| #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0;
- elim (tpr_inv_cast1 … H1) -H1
-(* case 16: tau, flat (repeated) *)
- [ * #V2 #T2 #HV02 #HT02 #H destruct -X2
- @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/
-(* case 17: tau, tau *)
- | #HT02
- /3 width=5 by tpr_conf_tau_tau/
- ]
-]
-qed.
-
-(* Basic_1: was: pr0_confluence *)
-theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ⇒ T1 → T0 ⇒ T2 →
- ∃∃T. T1 ⇒ T & T2 ⇒ T.
-#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/
-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/unfold/ltpss_ltpss.ma".
-include "Basic_2/reduction/ltpr_ldrop.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-
-(* Unfold properties ********************************************************)
-
-(* Basic_1: was: pr0_subst1 *)
-lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 →
- ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
- ∀L2. L1 ⇒ L2 →
- ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
-#T1 #T2 #H elim H -H T1 T2
-[ #I #L1 #d #e #X #H
- elim (tps_inv_atom1 … H) -H
- [ #H destruct -X /2/
- | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I;
- elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 HL12 #X #HLK2 #H
- elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X;
- elim (lift_total V2 0 (i+1)) #U2 #HVU2
- lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12
- @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *)
- ]
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X;
- elim (IHV12 … HVW1 … HL12) -IHV12 HVW1;
- elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
- elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y;
- elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
- elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
- lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
- elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
- elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
- elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
- lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2
- elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2
- lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
- lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
- lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2
- lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
- elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y;
- elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
- elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2
- elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
- elim (lift_total VV2 0 1) #VV #H2VV
- lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV
- @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X;
- elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2
- elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 <minus_plus_m_m /3/
-| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
- elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
- elim (IHT12 … HTT1 … HL12) -IHT12 HTT1 HL12 /3/
-]
-qed.
-
-lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ⇒ V2 → T1 ⇒ T2 →
- ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 →
- ∃∃U2. U1 ⇒ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ U2.
-#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -HT12 HTU1 /3/
-qed.
-
-lemma tpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
- ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
- ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
-#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
-[ /2/
-| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
- elim (tpr_tps_ltpr … HUT … HU1 … HL12) -HUT HU1 HL12 #U2 #HU12 #HTU2
- lapply (tpss_trans_eq … HT2 … HTU2) -T /2/
-]
-qed.
]
qed.
-theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
+theorem lift_mono: ∀d,e,T,U1. ↑[d,e] T ≡ U1 → ∀U2. ↑[d,e] T ≡ U2 → U1 = U2.
#d #e #T #U1 #H elim H -H d e T U1
[ #k #d #e #X #HX
lapply (lift_inv_sort1 … HX) -HX //
| #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hded
elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
elim (IHV12 … HV20 ?) -IHV12 HV20 //
- elim (IHT12 … HT20 ?) -IHT12 HT20 // /3 width=5/ (**) (* just /3 width=5/ crashes *)
+ elim (IHT12 … HT20 ?) -IHT12 HT20 // /3 width=5/
]
qed.
#L #L2 #_ #HL2 #IHL destruct -L
>(ltps_inv_atom1 … HL2) -HL2 //
qed.
-(*
-fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
- L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆.
-#d #e #L1 #L2 * -d e L1 L2
-[ //
-| #L #I #V #H destruct
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
-]
+
+fact ltpss_inv_atom2_aux: ∀d,e,L1,L2.
+ L1 [d, e] ≫* L2 → L2 = ⋆ → L1 = ⋆.
+#d #e #L1 #L2 #H @(ltpss_ind … H) -L2 //
+#L2 #L #_ #HL2 #IHL2 #H destruct -L;
+lapply (ltps_inv_atom2 … HL2) -HL2 /2/
qed.
-lemma ldrop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆.
+lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ≫* ⋆ → L1 = ⋆.
/2 width=5/ qed.
-
+(*
fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →
∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
∃∃K1,V1. K1 [0, e - 1] ≫ K2 &
K2 ⊢ V1 [d - 1, e] ≫ V2 &
L1 = K1. 𝕓{I} V1.
/2/ qed.
-
*)
(* Advanced forward lemmas **************************************************)
-lemma ltpss_fwd_tpsa21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2 →
+lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2 →
∃∃K2,V2. K1 [0, e - 1] ≫* K2 & K1 ⊢ V1 [0, e - 1] ≫* V2 &
L2 = K2. 𝕓{I} V2.
#e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2
∀a2. TC … R a1 a2 → P a2.
#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
qed.
+
+definition NF: ∀A. relation A → relation A → A → Prop ≝
+ λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
+
+inductive SN (A) (R,S:relation A): A → Prop ≝
+| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1
+.
+
+lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
+#A #R #S #a1 #Ha1
+@SN_intro #a2 #HRa12 #HSa12
+elim (HSa12 ?) -HSa12 /2/
+qed.
-->
</section>
<section name="xoa">
- <key name="output_dir">contribs/lambda_delta/Ground-2/</key>
+ <key name="output_dir">contribs/lambda_delta/Ground_2/</key>
<key name="objects">xoa</key>
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
<key name="ex">7 6</key>
<key name="or">3</key>
<key name="or">4</key>
-<!--
<key name="and">3</key>
--->
</section>
</helm_registry>
interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
+(* multiple conjunction connective (3) *)
+
+inductive and3 (P0,P1,P2:Prop) : Prop ≝
+ | and3_intro: P0 → P1 → P2 → and3 ? ? ?
+.
+
+interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2).
+
non associative with precedence 30
for @{ 'Or $P0 $P1 $P2 $P3 }.
+(* multiple conjunction connective (3) *)
+
+notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)"
+ non associative with precedence 35
+ for @{ 'And $P0 $P1 $P2 }.
+
projects / helm.git / commitdiff