+++ /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 "lambda-delta/substitution/lift_fun.ma".
-include "lambda-delta/substitution/lift_main.ma".
-include "lambda-delta/substitution/drop_main.ma".
-include "lambda-delta/reduction/pr_defs.ma".
-
-lemma pr_lift: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → ∀d,e,K. ↑[d,e] L ≡ K →
- ∀U1. ↑[d,e] T1 ≡ U1 → ∀U2. ↑[d,e] T2 ≡ U2 → K ⊢ U1 ⇒ U2.
-#L #T1 #T2 #H elim H -H L T1 T2
-[ #L #k #d #e #K #_ #U1 #HU1 #U2 #HU2
- lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
- lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
-| #L #i #d #e #K #_ #U1 #HU1 #U2 #HU2
- lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
- lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
- elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
- elim (lift_inv_bind1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2
- /5 width=5/
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #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 width=5/
-| #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #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
- /5 width=5/
-| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HKL #X #HX #V3 #HV03
- lapply (lift_inv_lref1 … HX) -HX * * #Hid #H destruct -X;
- [ -HV12;
- elim (lift_trans_ge … HV20 … HV03 ?) -HV20 HV03 V0 // #V0 #HV20 #HV03
- elim (drop_trans_le … HKL … HLK0 ?) -HKL HLK0 L /2/ #L #HKL #HLK0
- elim (drop_inv_skip2 … HLK0 ?) -HLK0 /2/ #K1 #V #HK10 #HV #H destruct -L;
- @pr_delta [4,6: // |1,2,3: skip |5: /2 width=5/] (**) (* /2 width=5/ *)
- | -IHV12;
- lapply (lift_trans_be … HV20 … HV03 ? ?) -HV20 HV03 V0 /2/ #HV23
- lapply (drop_trans_ge … HKL … HLK0 ?) -HKL HLK0 L // -Hid #HKK0
- @pr_delta /width=6/
- ]
-| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HKL #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;
- lapply (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // * #V #HV2 #HV3
- @pr_theta /3 width=5/
-| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HKL #X #HX #T0 #HT20
- elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
- lapply (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // * #T #HT1 #HT3
- @pr_zeta [2: // |1:skip | /2 width=5/] (**) (* /2 width=5/ *)
-| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HKL #X #HX #T #HT2
- elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X;
- @pr_tau /2 width=5/
-]
-qed.
-
-lemma pr_inv_lift: ∀L,T1,T2. L ⊢ T1 ⇒ T2 →
- ∀d,e,K. ↑[d,e] K ≡ L → ∀U1. ↑[d,e] U1 ≡ T1 →
- ∃∃U2. ↑[d,e] U2 ≡ T2 & K ⊢ U1 ⇒ U2.
-#L #T1 #T2 #H elim H -H L T1 T2
-[ #L #k #d #e #K #_ #U1 #HU1
- lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/
-| #L #i #d #e #K #_ #U1 #HU1
- lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX
- elim (lift_inv_bind2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
- elim (IHV12 … HLK … HV01) -IHV12 #V3 #HV32 #HV03
- elim (IHT12 … HT01) -IHT12 HT01 [2,3: -HV32 HV03 /3/] -HLK HV01 /3 width=5/
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
- elim (IHV12 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03
- elim (IHT12 … HLK … HT01) -IHT12 HT01 HLK /3 width=5/
-| #L #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #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 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03
- elim (IHT12 … HT01) -IHT12 HT01
- [3: -HV32 HV03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3 width=5/ is too slow *)
- -HLK HW01
- /3 width=5/
-| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HLK #X #HX
- lapply (lift_inv_lref2 … HX) -HX * * #Hid #HX destruct -X;
- [ -HV12;
- elim (drop_conf_lt … HLK … HLK0 Hid) -HLK HLK0 L #L #V3 #HKL #HK0L #HV31
- elim (IHV12 … HK0L … HV31) -IHV12 HK0L HV31 #V4 #HV42 #HV34
- elim (lift_trans_le … HV42 … HV20 ?) -HV42 HV20 V2 // #V2 #HV42
- >arith5 // -Hid #HV20
- @(ex2_1_intro … V2) /2 width=6/ (**) (* /3 width=8/ is slow *)
- | -IHV12;
- lapply (drop_conf_ge … HLK … HLK0 Hid) -HLK HLK0 L #HK
- elim (lift_free … HV20 d (i - e + 1) ? ? ?) -HV20 /2/
- >arith3 /2/ -Hid /3 width=8/ (**) (* just /3 width=8/ is a bit slow *)
- ]
-| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HLK #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 ? ? ? HLK ? HV01) -IHV12 HV01 #V3 #HV32 #HV03
- elim (IHW12 ? ? ? HLK ? HW01) -IHW12 #W3 #HW32 #HW03
- elim (IHT12 … HT01) -IHT12 HT01
- [3: -HV2 HV32 HV03 HW32 HW03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3/ is too slow *)
- -HLK HW01 #T3 #HT32 #HT03
- elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2
- @(ex2_1_intro … (𝕓{Abbr}W3.𝕗{Appl}V2.T3)) /3/ (**) (* /4/ loops *)
-| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HLK #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 … HLK … HT1) -IHT12 HLK HT1 /3 width=5/
-| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HLK #X #HX
- elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X;
- elim (IHT12 … HLK … HT01) -IHT12 HLK HT01 /3/
-]
-qed.
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
-
-include "lambda-delta/syntax/weight.ma".
-include "lambda-delta/reduction/pr_lift.ma".
-
-(* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************)
-
-(* Confluence lemmas ********************************************************)
-
-lemma pr_conf_sort_sort: ∀L,k1. ∃∃T0. L ⊢ (⋆k1) ⇒ T0 & L ⊢ (⋆k1) ⇒ T0.
-/2/ qed.
-
-lemma pr_conf_lref_lref: ∀L,i1. ∃∃T0. L ⊢ (#i1) ⇒ T0 & L ⊢ (#i1) ⇒ T0.
-/2/ qed.
-
-lemma pr_conf_bind_bind:
- ∀L,I1,V11,V12,T11,T12,V22,T22. (
- ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) →
- ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
- ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
- ) →
- L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 →
- L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 →
- ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0.
-#L #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
-elim (IH … HV1 … HV2) [2: /2/ ] #V #HV1 #HV2
-elim (IH … HT1 … HT2) [2: normalize // ] -HT1 HT2 T11 IH #T #HT1 #HT2
-@ex2_1_intro [2: @pr_bind [3: @HV1 |1: skip |4:
-
-(* Confluence ***************************************************************)
-
-lemma pr_conf_aux:
- ∀L,T. (
- ∀L1,T1. #[L1, T1] < #[L, T] →
- ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
- ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
- ) →
- ∀K1,U1,T1,K2,U2,T2. K1 ⊢ U1 ⇒ T1 → K2 ⊢ U2 ⇒ T2 →
- K1 = L → U1 = T → K2 = L → U2 = T →
- ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0.
-#L #T #IH #K1 #U1 #T1 #K2 #U2 #T2
-* -K1 U1 T1
-[ #K1 #k1 * -K2 U2 T2
-(* case 1: sort, sort *)
- [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 //
-(* case 2: sort, lref (excluded) *)
- | #K2 #i2 #H1 #H2 #H3 #H4 destruct
-(* case 3: sort, bind (excluded) *)
- | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 4: sort, flat (excluded) *)
- | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 5: sort, beta (excluded) *)
- | #K2 #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 6: sort, delta (excluded) *)
- | #K2 #K22 #V21 #V22 #V2 #i2 #_ #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 7: sort, theta (excluded) *)
- | #K2 #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 8: sort, zeta (excluded) *)
- | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 9: sort, tau (excluded) *)
- | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
- ]
-| #K1 #i1 * -K2 U2 T2
-(* case 10: lref, sort (excluded) broken *)
- [ #K2 #k2 #H1 #H2 #H3 #H4 destruct
-(* case 11: lref, sort (excluded) *)
- | #K2 #i2 #H1 #H2 #H3 #H4 destruct -K1 K2 T i2 //
-(* case 12: lref, bind (excluded) *)
- | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 13: lref, flat (excluded) *)
- | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 14: lref, beta (excluded) *)
- | #K2 #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 15: lref, delta (excluded) *)
- | #K2 #K22 #V21 #V22 #V2 #i2 #_ #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 16: lref, theta (excluded) *)
- | #K2 #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 17: lref, zeta (excluded) *)
- | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct
-(* case 18: lref, tau (excluded) *)
- | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
- ]
-| #K1 #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -K2 U2 T2
-(* case 19: bind, sort (excluded) broken *)
- [ #K2 #k2 #H1 #H2 #H3 #H4 destruct
-(* case 20: bind, lref (excluded) *)
- | #K2 #i2 #H1 #H2 #H3 #H4 destruct
-(* case 21: bind, bind *)
- | #K2 #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2 #H3 #H4
- destruct -T K1 K2 I2 V21 T21;
-
-
-theorem pr_conf: ∀L,T,T1,T2. L ⊢ T ⇒ T1 → L ⊢ T ⇒ T2 →
- ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0.
-#L #T @(cw_wf_ind … L T) -L T /3 width=12/
-qed.
-
-lemma pr_conf_bind_bind:
- ∀L,I1,V11,V12,T11,T12,V22,T22. (
- ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) →
- ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 →
- ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0
- ) →
- L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 →
- L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 →
- ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0.
\ /
V_______________________________________________________________ *)
-include "lambda-delta/substitution/subst_defs.ma".
+include "lambda-delta/substitution/ps_defs.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
| tpr_beta : ∀V1,V2,W,T1,T2.
tpr V1 V2 → tpr T1 T2 →
tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
-| tpr_delta: ∀V1,V2,T1,T2,T0,T.
- tpr V1 V2 → tpr T1 T2 →
- ⋆. 𝕓{Abbr} V2 ⊢ ↓[0, 1] T2 ≡ T0 → ↑[0, 1] T0 ≡ T →
+| tpr_delta: ∀V1,V2,T1,T2,T.
+ tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T →
tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} V2. T)
| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
interpretation
"context-free parallel reduction (term)"
- 'PR T1 T2 = (tpr T1 T2).
+ 'PRed T1 T2 = (tpr T1 T2).
(* Basic properties *********************************************************)
| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
| #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #V1 #V2 #T1 #T2 #T0 #T #_ #_ #_ #_ #_ #_ #i #H destruct
+| #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/
--- /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 "lambda-delta/substitution/lift_fun.ma".
+include "lambda-delta/substitution/lift_main.ma".
+include "lambda-delta/substitution/drop_main.ma".
+*)
+include "lambda-delta/reduction/tpr_defs.ma".
+
+axiom tpr_lift: ∀T1,T2. T1 ⇒ T2 →
+ ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2.
+(*
+#L #T1 #T2 #H elim H -H L T1 T2
+[ #L #k #d #e #K #_ #U1 #HU1 #U2 #HU2
+ lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
+ lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
+| #L #i #d #e #K #_ #U1 #HU1 #U2 #HU2
+ lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
+ lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2
+ elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
+ elim (lift_inv_bind1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2
+ /5 width=5/
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #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 width=5/
+| #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #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
+ /5 width=5/
+| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HKL #X #HX #V3 #HV03
+ lapply (lift_inv_lref1 … HX) -HX * * #Hid #H destruct -X;
+ [ -HV12;
+ elim (lift_trans_ge … HV20 … HV03 ?) -HV20 HV03 V0 // #V0 #HV20 #HV03
+ elim (drop_trans_le … HKL … HLK0 ?) -HKL HLK0 L /2/ #L #HKL #HLK0
+ elim (drop_inv_skip2 … HLK0 ?) -HLK0 /2/ #K1 #V #HK10 #HV #H destruct -L;
+ @pr_delta [4,6: // |1,2,3: skip |5: /2 width=5/] (**) (* /2 width=5/ *)
+ | -IHV12;
+ lapply (lift_trans_be … HV20 … HV03 ? ?) -HV20 HV03 V0 /2/ #HV23
+ lapply (drop_trans_ge … HKL … HLK0 ?) -HKL HLK0 L // -Hid #HKK0
+ @pr_delta /width=6/
+ ]
+| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HKL #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;
+ lapply (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // * #V #HV2 #HV3
+ @pr_theta /3 width=5/
+| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HKL #X #HX #T0 #HT20
+ elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X;
+ lapply (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // * #T #HT1 #HT3
+ @pr_zeta [2: // |1:skip | /2 width=5/] (**) (* /2 width=5/ *)
+| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HKL #X #HX #T #HT2
+ elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X;
+ @pr_tau /2 width=5/
+]
+qed.
+*)
+axiom tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
+ ∀d,e,U1. ↑[d, e] U1 ≡ T1 →
+ ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2.
+(*
+#L #T1 #T2 #H elim H -H L T1 T2
+[ #L #k #d #e #K #_ #U1 #HU1
+ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/
+| #L #i #d #e #K #_ #U1 #HU1
+ lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX
+ elim (lift_inv_bind2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
+ elim (IHV12 … HLK … HV01) -IHV12 #V3 #HV32 #HV03
+ elim (IHT12 … HT01) -IHT12 HT01 [2,3: -HV32 HV03 /3/] -HLK HV01 /3 width=5/
+| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX
+ elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
+ elim (IHV12 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03
+ elim (IHT12 … HLK … HT01) -IHT12 HT01 HLK /3 width=5/
+| #L #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #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 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03
+ elim (IHT12 … HT01) -IHT12 HT01
+ [3: -HV32 HV03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3 width=5/ is too slow *)
+ -HLK HW01
+ /3 width=5/
+| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HLK #X #HX
+ lapply (lift_inv_lref2 … HX) -HX * * #Hid #HX destruct -X;
+ [ -HV12;
+ elim (drop_conf_lt … HLK … HLK0 Hid) -HLK HLK0 L #L #V3 #HKL #HK0L #HV31
+ elim (IHV12 … HK0L … HV31) -IHV12 HK0L HV31 #V4 #HV42 #HV34
+ elim (lift_trans_le … HV42 … HV20 ?) -HV42 HV20 V2 // #V2 #HV42
+ >arith5 // -Hid #HV20
+ @(ex2_1_intro … V2) /2 width=6/ (**) (* /3 width=8/ is slow *)
+ | -IHV12;
+ lapply (drop_conf_ge … HLK … HLK0 Hid) -HLK HLK0 L #HK
+ elim (lift_free … HV20 d (i - e + 1) ? ? ?) -HV20 /2/
+ >arith3 /2/ -Hid /3 width=8/ (**) (* just /3 width=8/ is a bit slow *)
+ ]
+| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HLK #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 ? ? ? HLK ? HV01) -IHV12 HV01 #V3 #HV32 #HV03
+ elim (IHW12 ? ? ? HLK ? HW01) -IHW12 #W3 #HW32 #HW03
+ elim (IHT12 … HT01) -IHT12 HT01
+ [3: -HV2 HV32 HV03 HW32 HW03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3/ is too slow *)
+ -HLK HW01 #T3 #HT32 #HT03
+ elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2
+ @(ex2_1_intro … (𝕓{Abbr}W3.𝕗{Appl}V2.T3)) /3/ (**) (* /4/ loops *)
+| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HLK #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 … HLK … HT1) -IHT12 HLK HT1 /3 width=5/
+| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HLK #X #HX
+ elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X;
+ elim (IHT12 … HLK … HT01) -IHT12 HLK HT01 /3/
+]
+qed.
+*)
\ No newline at end of file
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/lift_weight.ma".
+include "lambda-delta/reduction/tpr_main.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Confluence lemmas ********************************************************)
+
+lemma tpr_conf_sort_sort: ∀k1. ∃∃T0. ⋆k1 ⇒ T0 & ⋆k1 ⇒ T0.
+/2/ qed.
+
+lemma tpr_conf_lref_lref: ∀i1. ∃∃T0. #i1 ⇒ T0 & #i1 ⇒ T0.
+/2/ qed.
+
+lemma tpr_conf_bind_bind:
+ ∀I1,V11,V12,T11,T12,V22,T22. (
+ ∀T1. #T1 < #V11 + #T11 + 1 →
+ ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+ ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+ ) →
+ V11 ⇒ V12 → T11 ⇒ T12 →
+ V11 ⇒ V22 → T11 ⇒ T22 →
+ ∃∃T0. 𝕓{I1} V12. T12 ⇒ T0 & 𝕓{I1} V22. T22 ⇒ T0.
+#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
+elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
+elim (IH … HT1 … HT2) -HT1 HT2 // #T #HT1 #HT2
+/3 width=5/
+qed.
+
+lemma tpr_conf_bind_zeta:
+ ∀V11,V12,T11,T12,T22,T20. (
+ ∀T1. #T1 < #V11 + #T11 +1 →
+ ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+ ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+ ) →
+ V11 ⇒ V12 → T22 ⇒ T20 → T11 ⇒ T12 → ↑[O, 1] T22 ≡ T11 →
+ ∃∃T0. 𝕓{Abbr} V12. T12 ⇒ T0 & T20 ⇒ T0.
+#V11 #V12 #T11 #T12 #T22 #T20 #IH #HV112 #HT202 #HT112 #HT
+elim (tpr_inv_lift … HT112 … HT) -HT112 #T #HT12 #HT22
+lapply (tw_lift … HT) -HT #HT
+elim (IH … HT202 … HT22) -HT202 HT22 IH /3/
+qed.
+
+lemma tpr_conf_flat_flat:
+ ∀I1,V11,V12,T11,T12,V22,T22. (
+ ∀T1. #T1 < #V11 + #T11 + 1 →
+ ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+ ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+ ) →
+ V11 ⇒ V12 → T11 ⇒ T12 →
+ V11 ⇒ V22 → T11 ⇒ T22 →
+ ∃∃T0. 𝕗{I1} V12. T12 ⇒ T0 & 𝕗{I1} V22. T22 ⇒ T0.
+#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
+elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
+elim (IH … HT1 … HT2) -HT1 HT2 // #T #HT1 #HT2
+/3 width=5/
+qed.
+
+(* Confluence ***************************************************************)
+
+lemma tpr_conf_aux:
+ ∀T. (
+ ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
+ ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+ ) →
+ ∀U1,T1,U2,T2. U1 ⇒ T1 → U2 ⇒ T2 →
+ U1 = T → U2 = T →
+ ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
+#T #IH #U1 #T1 #U2 #T2
+* -U1 T1
+[ #k1 * -U2 T2
+(* case 1: sort, sort *)
+ [ #k2 #H1 #H2 destruct -T k2 //
+(* case 2: sort, lref (excluded) *)
+ | #i2 #H1 #H2 destruct
+(* case 3: sort, bind (excluded) *)
+ | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 4: sort, flat (excluded) *)
+ | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 5: sort, beta (excluded) *)
+ | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 6: sort, delta (excluded) *)
+ | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
+(* case 7: sort, theta (excluded) *)
+ | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
+(* case 8: sort, zeta (excluded) *)
+ | #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 destruct
+(* case 9: sort, tau (excluded) *)
+ | #V2 #T21 #T22 #_ #H1 #H2 destruct
+ ]
+| #i1 * -U2 T2
+(* case 10: lref, sort (excluded) broken *)
+ [ #k2 #H1 #H2 destruct
+(* case 11: lref, sort (excluded) *)
+ | #i2 #H1 #H2 destruct -T i2 //
+(* case 12: lref, bind (excluded) *)
+ | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 13: lref, flat (excluded) *)
+ | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 14: lref, beta (excluded) *)
+ | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 15: lref, delta (excluded) *)
+ | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
+(* case 16: lref, theta (excluded) *)
+ | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
+(* case 17: lref, zeta (excluded) *)
+ | #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 destruct
+(* case 18: lref, tau (excluded) *)
+ | #V2 #T21 #T22 #_ #H1 #H2 destruct
+ ]
+| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2
+(* case 19: bind, sort (excluded) *)
+ [ #k2 #H1 #H2 destruct
+(* case 20: bind, lref (excluded) *)
+ | #i2 #H1 #H2 destruct
+(* case 21: bind, bind *)
+ | #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2
+ destruct -T I2 V21 T21 /3 width=7/
+(* case 22: bind, flat (excluded) *)
+ | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 23: bind, beta (excluded) *)
+ | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 24: bind, delta (excluded) *)
+ | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
+(* case 25: bind, theta (excluded) *)
+ | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
+(* case 26: bind, zeta *)
+ | #V2 #T21 #T22 #T20 #HT212 #HT220 #H1 #H2
+ destruct -I1 V2 T21 T /3 width=8/
+(* case 27: bind, tau (excluded) *)
+ | #V2 #T21 #T22 #_ #H1 #H2 destruct
+ ]
+| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2
+(* case 28: flat, sort (excluded) *)
+ [ #k2 #H1 #H2 destruct
+(* case 29: flat, lref (excluded) *)
+ | #i2 #H1 #H2 destruct
+(* case 30: flat, bind (excluded) *)
+ | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
+(* case 31: flat, flat *)
+ | #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2
+ destruct -T I2 V21 T21 /3 width=7/
+(* case 32: flat, beta *)
+ | #V21 #V22 #W2 #T21 #T22 #HV212 #HT212 #H1 #H2
+ destruct -I1 V21 T11 T;
+
+theorem pr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 →
+ ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
+#T @(tw_wf_ind … T) -T /3 width=8/
+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 "lambda-delta/syntax/weight.ma".
+include "lambda-delta/substitution/lift_defs.ma".
+
+(* RELOCATION ***************************************************************)
+
+lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #T1 = #T2.
+#d #e #T1 #T2 #H elim H -d e T1 T2 normalize //
+qed.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "lambda-delta/substitution/drop_defs.ma".
+
+(* PARALLEL SUBSTITUTION ****************************************************)
+
+inductive ps: lenv → term → nat → nat → term → Prop ≝
+| ps_sort : ∀L,k,d,e. ps L (⋆k) d e (⋆k)
+| ps_lref : ∀L,i,d,e. ps L (#i) d e (#i)
+| ps_subst: ∀L,K,V,U1,U2,i,d,e.
+ d ≤ i → i < d + e →
+ ↓[0, i] L ≡ K. 𝕓{Abbr} V → ps K V 0 (d + e - i - 1) U1 →
+ ↑[0, i + 1] U1 ≡ U2 → ps L (#i) d e U2
+| ps_bind : ∀L,I,V1,V2,T1,T2,d,e.
+ ps L V1 d e V2 → ps (L. 𝕓{I} V1) T1 (d + 1) e T2 →
+ ps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
+| ps_flat : ∀L,I,V1,V2,T1,T2,d,e.
+ ps L V1 d e V2 → ps L T1 d e T2 →
+ ps L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
+.
+
+interpretation "parallel substritution" 'PSubst L T1 d e T2 = (ps L T1 d e T2).
+
+(* Basic properties *********************************************************)
+
+lemma subst_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T.
+#T elim T -T //
+#I elim I -I /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
+ ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &
+ L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
+ U2 = 𝕓{I} V2. T2.
+#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
+[ #L #k #d #e #I #V1 #T1 #H destruct
+| #L #i #d #e #I #V1 #T1 #H destruct
+| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
+| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
+]
+qed.
+
+lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &
+ L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
+ U2 = 𝕓{I} V2. T2.
+/2/ qed.
+
+lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
+ ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
+ U2 = 𝕗{I} V2. T2.
+#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
+[ #L #k #d #e #I #V1 #T1 #H destruct
+| #L #i #d #e #I #V1 #T1 #H destruct
+| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
+| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
+]
+qed.
+
+lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫ U2 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
+ U2 = 𝕗{I} V2. T2.
+/2/ qed.
+++ /dev/null
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
-
-include "lambda-delta/substitution/drop_defs.ma".
-
-(* PARALLEL SUBSTITUTION ****************************************************)
-
-inductive ps: lenv → term → nat → nat → term → Prop ≝
-| ps_sort : ∀L,k,d,e. ps L (⋆k) d e (⋆k)
-| ps_lref : ∀L,i,d,e. ps L (#i) d e (#i)
-| ps_subst: ∀L,K,V,U1,U2,i,d,e.
- d ≤ i → i < d + e →
- ↓[0, i] L ≡ K. 𝕓{Abbr} V → ps K V 0 (d + e - i - 1) U1 →
- ↑[0, i + 1] U1 ≡ U2 → ps L (#i) d e U2
-| ps_bind : ∀L,I,V1,V2,T1,T2,d,e.
- ps L V1 d e V2 → ps (L. 𝕓{I} V1) T1 (d + 1) e T2 →
- ps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
-| ps_flat : ∀L,I,V1,V2,T1,T2,d,e.
- ps L V1 d e V2 → ps L T1 d e T2 →
- ps L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
-.
-
-interpretation "parallel substritution" 'PSubst L T1 d e T2 = (ps L T1 d e T2).
-
-(* Basic properties *********************************************************)
-
-lemma subst_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T.
-#T elim T -T //
-#I elim I -I /2/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma ps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
- ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &
- L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
- U2 = 𝕓{I} V2. T2.
-#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
-[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #i #d #e #I #V1 #T1 #H destruct
-| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
-| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
-]
-qed.
-
-lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &
- L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
- U2 = 𝕓{I} V2. T2.
-/2/ qed.
-
-lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
- ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
- U2 = 𝕗{I} V2. T2.
-#d #e #L #U1 #U2 #H elim H -H d e L U1 U2
-[ #L #k #d #e #I #V1 #T1 #H destruct
-| #L #i #d #e #I #V1 #T1 #H destruct
-| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct
-| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/
-]
-qed.
-
-lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫ U2 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
- U2 = 𝕗{I} V2. T2.
-/2/ qed.
interpretation "weight (closure)" 'Weight L T = (cw L T).
+axiom tw_wf_ind: ∀P:term→Prop.
+ (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) →
+ ∀T. P T.
+
axiom cw_wf_ind: ∀P:lenv→term→Prop.
(∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
∀L,T. P L T.
projects / helm.git / commitdiff