(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
* Specification started: 2011 April 17
+ * Confluence of context-sensitive parallel reduction closed: 2011 September 21
* Confluence of context-free parallel reduction closed: 2011 September 6
* - Patience on me so that I gain peace and perfection! -
* [ suggested invocation to start formal specifications with ]
(**************************************************************************)
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.
+ λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫* T2.
interpretation
"context-sensitive parallel reduction (term)"
lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
/2/ qed.
-lemma cpr_tps: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 ⇒ T2.
+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.
-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 * /3 width=5/
-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 (tps_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tps_leq_repl_dx … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
-/3 width=5/
-qed.
-
(* Note: new property *)
(* Basic-1: was only: pr2_thin_dx *)
lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
qed.
-lemma cpr_delta: ∀L,K,V,W,i.
- ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → L ⊢ #i ⇒ W.
-/3/
-qed.
-
lemma cpr_cast: ∀L,V,T1,T2.
L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2.
#L #V #T1 #T2 * /3/
(* Basic-1: was: pr2_gen_csort *)
lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
#T1 #T2 * #T #HT normalize #HT2
-<(tps_inv_refl_O2 … HT2) -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
->(tps_inv_sort1 … H) -H //
-qed.
-
-(* Basic-1: was: pr2_gen_lref *)
-lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
- T2 = #i ∨
- ∃∃K,T. ↓[0, i] L ≡ K. 𝕓{Abbr} T & ↑[0, i + 1] T ≡ T2 &
- i < |L|.
-#L #T2 #i * #X #H
->(tpr_inv_atom1 … H) -H #H
-elim (tps_inv_lref1 … H) -H /2/
-* #K #T #_ #Hi #HLK #HTT2 /3/
+>(tpss_inv_sort1 … H) -H //
qed.
(*
(* Basic-1: was: pr2_gen_cast *)
* #V #T #HV1 #HT1 #H whd (* >H in HU2; *) destruct -X;
elim (tps_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
*)
-(* Basic forward lemmas *****************************************************)
-
-lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2.
-#L elim L -L
-[ /2/
-| normalize /3/
-].
-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
-pr2/pr2 pr2_confluence__pr2_free_free
-pr2/pr2 pr2_confluence__pr2_free_delta
-pr2/pr2 pr2_confluence__pr2_delta_delta
-pr2/pr2 pr2_confluence
pr2/props pr2_change
pr2/subst1 pr2_subst1
pr2/subst1 pr2_gen_cabbr
(* 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_leq_repl_dx … 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.
-*)
+
(* *)
(**************************************************************************)
+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 ****************************)
-(* Relocation properties ****************************************************)
-
-(* Basic-1: was: pr2_lift *)
+(* Advanced properties ******************************************************)
-(* Basic-1: was: pr2_gen_lift *)
+lemma cpr_delta: ∀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 *)
+
+(* Basic-1: was: pr2_gen_lift *)
+
⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
U2 = 𝕓{I} V2. T
) ∨
- ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
+ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
/2/ qed.
(* Basic-1: was pr0_gen_abbr *)
⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
U2 = 𝕓{Abbr} V2. T
) ∨
- ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
+ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_bind1 … H) -H * /3 width=7/
qed.
(* *)
(**************************************************************************)
-include "Basic-2/substitution/tps_tps.ma".
-include "Basic-2/substitution/ltps_tps.ma".
+include "Basic-2/unfold/ltpss_ltpss.ma".
include "Basic-2/reduction/ltpr_drop.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-(* Note: the constant 1 comes from tps_subst *)
(* Basic-1: was: pr0_subst1 *)
lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 →
- ∀L1,d,U1. L1 ⊢ T1 [d, 1] ≫ U1 →
+ ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
∀L2. L1 ⇒ L2 →
- ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, 1] ≫ U2.
+ ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
#T1 #T2 #H elim H -H T1 T2
-[ #I #L1 #d #X #H
+[ #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_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 | /2/ ] (**) (* /3 width=6/ is too slow *)
+ @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *)
]
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #X #H #L2 #HL12
+| #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 #X #H #L2 #HL12
+| #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 (tps_leq_repl_dx … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #X #H #L2 #HL12
+ lapply (tpss_leq_repl_dx … 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 (tps_conf_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
+ elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
lapply (tps_leq_repl_dx … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2
- elim (ltps_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) 1 ?) -HTT2 /2/ #W2 #HTTW2 #HTW2
- lapply (tps_leq_repl_dx … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
- lapply (tps_trans_ge … HUT2 … HTW2 ?) -HUT2 HTW2 // #HUW2
- /3 width=5/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #X #H #L2 #HL12
+ elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2
+ lapply (tpss_leq_repl_dx … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
+ lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
+ lapply (tpss_leq_repl_dx … 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 (tps_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 H2VV ?) -HVV2 HV2 /2/ #HVV
- @ex2_1_intro [2: @tpr_theta |1: skip |3: @tps_bind [2: @tps_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #X #H #L2 #HL12
+ 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 #X #H #L2 #HL12
+| #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/
]
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.
-/3 width=7/ qed.
+#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.
\ No newline at end of file
--- /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/ltps.ma".
+include "Basic-2/unfold/tpss.ma".
+
+(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+
+definition ltpss: nat → nat → relation lenv ≝
+ λd,e. TC … (ltps d e).
+
+interpretation "partial unfold (local environment)"
+ 'PSubstStar L1 d e L2 = (ltpss d e L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma ltpss_ind: ∀d,e,L1. ∀R: lenv → Prop. R L1 →
+ (∀L,L2. L1 [d, e] ≫* L → L [d, e] ≫ L2 → R L → R L2) →
+ ∀L2. L1 [d, e] ≫* L2 → R L2.
+#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
+qed.
+
+(* Basic properties *********************************************************)
+
+lemma ltpss_strap: ∀L1,L,L2,d,e.
+ L1 [d, e] ≫ L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2.
+/2/ qed.
+
+lemma ltpss_refl: ∀L,d,e. L [d, e] ≫* L.
+/2/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫* L2 → L1 = L2.
+#d #L1 #L2 #H @(ltpss_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL <(ltps_inv_refl_O2 … HL2) -HL2 //
+qed.
+
+lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫* L2 → L2 = ⋆.
+#d #e #L2 #H @(ltpss_ind … H) -L2 //
+#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
+]
+qed.
+
+lemma drop_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 [0, e - 1] ≫ V2 &
+ L1 = K1. 𝕓{I} V1.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct -L2 I V2 /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
+]
+qed.
+
+lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ≫ K2. 𝕓{I} V2 → 0 < e →
+ ∃∃K1,V1. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 &
+ L1 = K1. 𝕓{I} V1.
+/2 width=5/ qed.
+
+fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d →
+ ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+ ∃∃K1,V1. K1 [d - 1, e] ≫ K2 &
+ K2 ⊢ V1 [d - 1, e] ≫ V2 &
+ L1 = K1. 𝕓{I} V1.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #I #K2 #V2 #H destruct
+| #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct -L2 I V2
+ /2 width=5/
+]
+qed.
+
+lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ≫ K2. 𝕓{I} V2 → 0 < d →
+ ∃∃K1,V1. K1 [d - 1, e] ≫ K2 &
+ K2 ⊢ V1 [d - 1, e] ≫ V2 &
+ L1 = K1. 𝕓{I} V1.
+/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/unfold/ltpss_tpss.ma".
+
+(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+
+(* Main properties **********************************************************)
+
+theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
+ L1 [d, e] ≫* L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2.
+/2/ qed.
+
+lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
+ L1 [0, e] ≫* L2 → L2 ⊢ V1 [0, e] ≫* V2 →
+ L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
+[ /2/
+| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/
+]
+qed.
+
+lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫* V2 →
+ 0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) /2/
+qed.
+
+lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
+ L1 [d, e] ≫* L2 → L2 ⊢ V1 [d, e] ≫* V2 →
+ L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
+[ /2/
+| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/
+]
+qed.
+
+lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫* V2 →
+ 0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) /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/unfold/tpss_ltps.ma".
+include "Basic-2/unfold/ltpss.ma".
+
+(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+
+(* Properties concerning partial unfold on terms ****************************)
+
+lemma ltpss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
+ ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫* U2 →
+ d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2.
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 //
+#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
+lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 HTU2 /2/
+qed.
+
+lemma ltpss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
+ ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
+ d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2.
+#L1 #L0 #d1 #e1 #HL10 #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
+@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2/ (**) (* /3 width=6/ is too slow *)
+qed.
+
+lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 →
+ ∀T2,U2. L1 ⊢ T2 [d, e] ≫* U2 → L0 ⊢ T2 [d, e] ≫* U2.
+#L0 #L1 #d #e #H @(ltpss_ind … H) -L1
+[ /2/
+| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
+ lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 HTU2 /2/
+]
+qed.
+
+lemma ltpss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 →
+ ∀T2,U2. L1 ⊢ T2 [d, e] ≫ U2 → L0 ⊢ T2 [d, e] ≫* U2.
+/3/ qed.
+
+lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
+ L0 ⊢ T2 [d2, e2] ≫* U2 → L0 [d1, e1] ≫* L1 →
+ L1 ⊢ T2 [d2, e2] ≫* U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpss_ind … H) -L1
+[ //
+| -HTU2 #L #L1 #_ #HL1 #IHL
+ lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 IHL //
+]
+qed.
+
+lemma ltpss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
+ L0 ⊢ T2 [d2, e2] ≫ U2 → L0 [d1, e1] ≫* L1 →
+ L1 ⊢ T2 [d2, e2] ≫* U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #HL01
+@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2/ (**) (* /3 width=6/ is too slow *)
+qed.
+
+lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e.
+ L0 ⊢ T2 [d, e] ≫* U2 → L0 [d, e] ≫* L1 →
+ ∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T.
+#L0 #L1 #T2 #U2 #d #e #HTU2 #H @(ltpss_ind … H) -L1
+[ /2/
+| -HTU2 #L #L1 #_ #HL1 * #W2 #HTW2 #HUW2
+ elim (ltps_tpss_conf … HL1 HTW2) -HTW2 #T #HT2 #HW2T
+ elim (ltps_tpss_conf … HL1 HUW2) -HL1 HUW2 #U #HU2 #HW2U
+ elim (tpss_conf_eq … HW2T … HW2U) -HW2T HW2U #V #HTV #HUV
+ lapply (tpss_trans_eq … HT2 … HTV) -T;
+ lapply (tpss_trans_eq … HU2 … HUV) -U /2/
+]
+qed.
+
+lemma ltpss_tps_conf_eq: ∀L0,L1,T2,U2,d,e.
+ L0 ⊢ T2 [d, e] ≫ U2 → L0 [d, e] ≫* L1 →
+ ∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T.
+/3/ qed.
+
+lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
+ ∀L2,ds,es. L1 [ds, es] ≫* L2 →
+ ∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
+#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2
+[ /3/
+| #L #L2 #HL1 #HL2 * #T #HT1 #HT2
+ elim (ltps_tpss_conf … HL2 HT1) -HT1 #T0 #HT10 #HT0
+ lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 HT0 #HT0
+ lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 HT0 #HT0
+ lapply (tpss_trans_eq … HT2 … HT0) -T /2/
+]
+qed.
+
+lemma ltpss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 →
+ ∀L2,ds,es. L1 [ds, es] ≫* L2 →
+ ∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
+/3/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma ltpss_tps2: ∀L1,L2,I,e.
+ L1 [0, e] ≫* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ≫ V2 →
+ L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #e #H @(ltpss_ind … H) -L2
+[ /3/
+| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
+ elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
+ lapply (IHL … HV1) -IHL HV1 #HL1
+ @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+]
+qed.
+
+lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫ V2 →
+ 0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) /2/
+qed.
+
+lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ≫* L2 →
+ ∀V1,V2. L2 ⊢ V1 [d, e] ≫ V2 →
+ L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2
+[ /3/
+| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
+ elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
+ lapply (IHL … HV1) -IHL HV1 #HL1
+ @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+]
+qed.
+
+lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫ V2 →
+ 0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) /2/
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma ltpss_fwd_tpsa21: ∀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
+[ /2 width=5/
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L;
+ elim (ltps_inv_tps21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
+ lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
+ lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
+]
+qed.
+
+lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. 𝕓{I} V1 [d, e] ≫* L2 →
+ ∃∃K2,V2. K1 [d - 1, e] ≫* K2 &
+ K1 ⊢ V1 [d - 1, e] ≫* V2 &
+ L2 = K2. 𝕓{I} V2.
+#d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2
+[ /2 width=5/
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L;
+ elim (ltps_inv_tps11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
+ lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
+ lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
+]
+qed.
(* Advanced properties ******************************************************)
+lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 → L ⊢ T1 [d, 1] ≫ T2.
+#L #T1 #T2 #d #H @(tpss_ind … H) -H T2 //
+#T #T2 #_ #HT2 #IHT1
+lapply (tps_trans_ge … IHT1 … HT2 ?) //
+qed.
+
lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫* T1 →
∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 →
∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T2 [d1, e1] ≫* T.
projects / helm.git / commitdiff