pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
pc3/wcpr0 pc3_wcpr0_t
pc3/wcpr0 pc3_wcpr0
+pr0/fwd pr0_gen_void
pr0/dec nf0_dec
+pr0/subst1 pr0_subst1_back
+pr0/subst1 pr0_subst1_fwd
pr1/pr1 pr1_strip
pr1/pr1 pr1_confluence
pr1/props pr1_pr0
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+(* Basic-1: includes: pr0_delta1 *)
inductive tpr: term → term → Prop ≝
| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr 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-1: was: pr0_gen_sort pr0_gen_lref *)
lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
/2/ qed.
∃∃T. ↑[0,1] T ≡ T1 & tpr 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 &
| (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
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.
T1 = 𝕔{Abbr} V. T
| ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
/2/ qed.
-(*
-pr0/fwd pr0_gen_sort
-pr0/fwd pr0_gen_lref
-pr0/fwd pr0_gen_abst
-pr0/fwd pr0_gen_appl
-pr0/fwd pr0_gen_cast
-pr0/fwd pr0_gen_abbr
-pr0/fwd pr0_gen_void
-pr0/fwd pr0_gen_lift
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta
-pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta
-pr0/pr0 pr0_confluence__pr0_cong_delta
-pr0/pr0 pr0_confluence__pr0_upsilon_upsilon
-pr0/pr0 pr0_confluence__pr0_delta_delta
-pr0/pr0 pr0_confluence__pr0_delta_tau
-pr0/pr0 pr0_confluence
-pr0/props pr0_lift
-pr0/props pr0_subst0_back
-pr0/props pr0_subst0_fwd
-pr0/props pr0_subst0
-pr0/subst1 pr0_delta1
-pr0/subst1 pr0_subst1_back
-pr0/subst1 pr0_subst1_fwd
-pr0/subst1 pr0_subst1
-*)
\ No newline at end of file
+
+(* Basic-1: removed theorems 3:
+ pr0_subst0_back pr0_subst0_fwd pr0_subst0
+ Basic-1: removed local theorems: 1: pr0_delta_tau
+*)
(* 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
]
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.
]
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.
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 →
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 →
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 →
]
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/
(**************************************************************************)
include "Basic-2/substitution/tps_tps.ma".
+include "Basic-2/substitution/ltps_tps.ma".
include "Basic-2/reduction/ltpr_drop.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
-axiom tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 →
- ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
+(* 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 →
∀L2. L1 ⇒ L2 →
- ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫ U2.
-(*
+ ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, 1] ≫ U2.
#T1 #T2 #H elim H -H T1 T2
-[ #I #L1 #d #e #X #H
+[ #I #L1 #d #X #H
elim (tps_inv_atom1 … H) -H
[ #H destruct -X /2/
| * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I;
lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12
@ex2_1_intro [2: @HU12 | skip | /2/ ] (**) (* /3 width=6/ is too slow *)
]
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #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
+| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #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} W) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
- lapply (tps_leq_repl … HTT2 (L2. 𝕓{Abbr} V2) ?) -HTT2 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+ 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
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} V2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
-(*lapply (tps_leq_repl … HTT2 (L2. 𝕓{I} VV2) ?) -HTT2 /2/ #HTT2 *)
- elim (tps_conf_neq … HTU2 … HTT2 ?) -HTU2 HTT2 T2 /2/ #T2 #HUT2 #HTT2
- @ex2_1_intro
- [2: @tpr_delta [4: @HVV12 |5: @HTT12 |1,2: skip |6: ] (*|6: ]1,2: skip ]*)
- |1: skip
- |3: @tps_bind [@HVV2 | @HUT2 ]
- ]
-*)
+ 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
+ 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 (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
+ 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
+ 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 →
]
qed.
-lemma ltps_trans_conf_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
+lemma ltps_drop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
elim (IHTU2 … HL01) -IHTU2 HL01 /3 width=5/
]
qed.
-(*
-lemma ltps_tps_trans: (t1,t2,u2:?; j:?) (subst0 j u2 t1 t2) ->
- (u1,u:?; i:?) (subst0 i u u1 u2) ->
- (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)).
-*)
\ No newline at end of file
+lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
+ ∀L1,d1,e1. L1 [d1, e1] ≫ L0 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 [d2, e2] ≫ U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2
+[ //
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
+ lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
+ lapply (ltps_drop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /2/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
+ @tps_bind [ /2/ | @IHTU2 [3: /2/ |1,2: skip | /2/ ] ] (**) (* /3/ is too slow *)
+| /3/
+]
+qed.
+
+lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
+ ∀L1,d1,e1. L1 [d1, e1] ≫ L0 →
+ ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
+ L0 ⊢ T [d1, e1] ≫ U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2
+[ /2/
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
+ elim (lt_or_ge i2 d1) #Hi2d1
+ [ elim (ltps_drop_trans_le … HL10 … HLK0 ?) -HL10 /2/ #X #H #HLK1
+ elim (ltps_inv_tps12 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
+ lapply (drop_fwd_drop2 … HLK0) -HLK0 #H
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // >arith_a2 /3/
+ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
+ [ elim (ltps_drop_trans_be … HL10 … HLK0 ? ?) -HL10 [2,3: /2/ ] #X #H #HLK1
+ elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
+ lapply (drop_fwd_drop2 … HLK0) -HLK0 #H
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // normalize #HW01
+ lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 //
+ | lapply (ltps_drop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /3/
+ ]
+ ]
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
+ elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
+ elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 [2: /2/ ] -HL10 /3 width=5/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
+ elim (IHVW2 … HL10) -IHVW2;
+ elim (IHTU2 … HL10) -IHTU2 HL10 /3 width=5/
+]
+qed.
(* Basic-1: removed theorems 23:
subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
- subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
+ subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt
- subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
+ subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
subst0_confluence_lift subst0_tlt
subst1_head subst1_gen_head
*)
]
qed.
+(* Note: the constant 1 comes from tps_subst *)
+theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ≫ T0 →
+ ∀T2. L ⊢ T0 [d, 1] ≫ T2 → 1 ≤ e →
+ L ⊢ T1 [d, e] ≫ T2.
+#L #T1 #T0 #d #e #H elim H -L T1 T0 d e
+[ #L #I #d #e #T2 #H #He
+ elim (tps_inv_atom1 … H) -H
+ [ #H destruct -T2 //
+ | * #K #V #i #Hd2i #Hide2 #HLK #HVT2 #H destruct -I;
+ lapply (lt_to_le_to_lt … (d + e) Hide2 ?) /2/
+ ]
+| #L #K #V #V2 #i #d #e #Hdi #Hide #HLK #HVW #T2 #HVT2 #He
+ lapply (tps_weak … HVT2 0 (i +1) ? ?) -HVT2 /2/ #HVT2
+ <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2/
+| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
+ elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X;
+ lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02
+ lapply (IHT10 … HT02 He) -IHT10 HT02 #HT12
+ lapply (tps_leq_repl_dx … HT12 (L. 𝕓{I} V2) ?) -HT12 /3/
+| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
+ elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X /3/
+]
+qed.
+
theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫ T0 →
∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → d2 + e2 ≤ d1 →
∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T [d1, e1] ≫ T2.
@printf '\e[0m\n'
@printf '\e[1;40;31m'
@printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l`
- @printf ' %-8s %5i' Comments `grep "(\*[^*]*$$" $(MAS) | wc -l`
+ @printf ' %-8s %5i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l`
@printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
@printf ' %-10s' ''
@printf '\e[0m\n'
projects / helm.git / commitdiff