include "basics/list.ma".
include "lambda-delta/xoa_defs.ma".
include "lambda-delta/xoa_notation.ma".
-include "lambda-delta/notation.ma".
(* ARITHMETICAL PROPERTIES **************************************************)
non associative with precedence 90
for @{ 'Star }.
-notation "hvbox( ⋆ k )"
+notation "hvbox( ⋆ term 90 k )"
non associative with precedence 90
for @{ 'Star $k }.
notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )"
non associative with precedence 45
- for @{ 'RSubst $L1 $d $e $L2 }.
+ for @{ 'RDrop $L1 $d $e $L2 }.
-notation "hvbox( L ⊢ break ↓ [ d , break e ] break T1 ≡ break T2 )"
+notation "hvbox( L ⊢ break (term 90 T1) break [ d , break e ] ≫ break T2 )"
non associative with precedence 45
- for @{ 'RSubst $L $T1 $d $e $T2 }.
+ for @{ 'PSubst $L $T1 $d $e $T2 }.
(* reduction ****************************************************************)
notation "hvbox( T1 ⇒ break T2 )"
non associative with precedence 45
- for @{ 'PR $T1 $T2 }.
+ for @{ 'PRed $T1 $T2 }.
notation "hvbox( L ⊢ break (term 90 T1) ⇒ break T2 )"
non associative with precedence 45
- for @{ 'PR $L $T1 $T2 }.
+ for @{ 'PRed $L $T1 $T2 }.
--- /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/reduction/tpr_defs.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+inductive lpr: lenv → lenv → Prop ≝
+| lpr_sort: lpr (⋆) (⋆)
+| lpr_item: ∀K1,K2,I,V1,V2.
+ lpr K1 K2 → V1 ⇒ V2 → lpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
+.
+
+interpretation
+ "context-free parallel reduction (environment)"
+ 'PR L1 L2 = (lpr L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+ ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+#L1 #L2 #H elim H -H 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 lpr_inv_item1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ⇒ L2 →
+ ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+/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".
-
-(* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************)
-
-inductive pr: lenv → term → term → Prop ≝
-| pr_sort : ∀L,k. pr L (⋆k) (⋆k)
-| pr_lref : ∀L,i. pr L (#i) (#i)
-| pr_bind : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr (L. 𝕓{I} V1) T1 T2 →
- pr L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
-| pr_flat : ∀L,I,V1,V2,T1,T2. pr L V1 V2 → pr L T1 T2 →
- pr L (𝕗{I} V1. T1) (𝕗{I} V2. T2)
-| pr_beta : ∀L,V1,V2,W,T1,T2.
- pr L V1 V2 → pr (L. 𝕓{Abst} W) T1 T2 → (*𝕓*)
- pr L (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
-| pr_delta: ∀L,K,V1,V2,V,i.
- ↑[0,i] K. 𝕓{Abbr} V1 ≡ L → pr K V1 V2 → ↑[0,i+1] V2 ≡ V →
- pr L (#i) V
-| pr_theta: ∀L,V,V1,V2,W1,W2,T1,T2.
- pr L V1 V2 → ↑[0,1] V2 ≡ V → pr L W1 W2 → pr (L. 𝕓{Abbr} W1) T1 T2 → (*𝕓*)
- pr L (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2)
-| pr_zeta : ∀L,V,T,T1,T2. ↑[0,1] T1 ≡ T → pr L T1 T2 →
- pr L (𝕚{Abbr} V. T) T2
-| pr_tau : ∀L,V,T1,T2. pr L T1 T2 → pr L (𝕚{Cast} V. T1) T2
-.
-
-interpretation
- "single step parallel reduction (term)"
- 'PR L T1 T2 = (pr L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma pr_refl: ∀T,L. L ⊢ T ⇒ T.
-#T elim T -T //
-#I elim I -I /2/
-qed.
-
-(* The basic inversion lemmas ***********************************************)
-
-lemma pr_inv_lref2_aux: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → ∀i. T2 = #i →
- ∨∨ T1 = #i
- | ∃∃K,V1,j. j < i & K ⊢ V1 ⇒ #(i-j-1) &
- ↑[O,j] K. 𝕓{Abbr} V1 ≡ L & T1 = #j
- | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & L ⊢ T0 ⇒ #i &
- T1 = 𝕓{Abbr} V. T
- | ∃∃V,T. L ⊢ T ⇒ #i & T1 = 𝕗{Cast} V. T.
-#L #T1 #T2 #H elim H -H L T1 T2
-[ #L #k #i #H destruct
-| #L #j #i /2/
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #L #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
-| #L #K #V1 #V2 #V #j #HLK #HV12 #HV2 #_ #i #H destruct -V;
- elim (lift_inv_lref2 … HV2) -HV2 * #H1 #H2
- [ elim (lt_zero_false … H1)
- | destruct -V2 /3 width=7/
- ]
-| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct
-| #L #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/
-| #L #V #T1 #T2 #HT12 #_ #i #H destruct /3/
-]
-qed.
-
-lemma pr_inv_lref2: ∀L,T1,i. L ⊢ T1 ⇒ #i →
- ∨∨ T1 = #i
- | ∃∃K,V1,j. j < i & K ⊢ V1 ⇒ #(i-j-1) &
- ↑[O,j] K. 𝕓{Abbr} V1 ≡ L & T1 = #j
- | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & L ⊢ T0 ⇒ #i &
- T1 = 𝕓{Abbr} V. T
- | ∃∃V,T. L ⊢ T ⇒ #i & T1 = 𝕗{Cast} V. T.
-/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:
* -K1 U1 T1
[ #K1 #k1 * -K2 U2 T2
(* case 1: sort, sort *)
- [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 IH //
+ [ #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 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct
]
| #K1 #i1 * -K2 U2 T2
-(* case 10: lref, sort (excluded) *)
+(* 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 IH //
+ | #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 #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.
--- /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/subst_defs.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+inductive tpr: term → term → Prop ≝
+| tpr_sort : ∀k. tpr (⋆k) (⋆k)
+| tpr_lref : ∀i. tpr (#i) (#i)
+| tpr_bind : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
+ tpr (𝕓{I} V1. T1) (𝕓{I} V2. T2)
+| 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: ∀V1,V2,T1,T2,T0,T.
+ tpr V1 V2 → tpr T1 T2 →
+ ⋆. 𝕓{Abbr} V2 ⊢ ↓[0, 1] T2 ≡ T0 → ↑[0, 1] T0 ≡ 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 →
+ 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)"
+ 'PR T1 T2 = (tpr T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tpr_refl: ∀T. T ⇒ T.
+#T elim T -T //
+#I elim I -I /2/
+qed.
+
+(* The basic inversion lemmas ***********************************************)
+
+lemma 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 #H elim H -H T1 T2
+[ #k #i #H destruct
+| #j #i /2/
+| #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
+| #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.
drop (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2)
.
-interpretation "dropping" 'RLift L2 d e L1 = (drop L1 d e L2).
+interpretation "dropping" 'RDrop L1 d e L2 = (drop L1 d e L2).
(* Basic properties *********************************************************)
lemma drop_drop_lt: ∀L1,L2,I,V,e.
- â\86\91[0, e - 1] L2 â\89¡ L1 â\86\92 0 < e â\86\92 â\86\91[0, e] L2 â\89¡ L1. ð\9d\95\93{I} V.
+ â\86\93[0, e - 1] L1 â\89¡ L2 â\86\92 0 < e â\86\92 â\86\93[0, e] L1. ð\9d\95\93{I} V â\89¡ L2.
#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma drop_inv_refl_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 → e = 0 → L1 = L2.
-#d #e #L2 #L1 #H elim H -H d e L2 L1
+lemma drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2.
+#d #e #L1 #L2 #H elim H -H d e L1 L2
[ //
| #L1 #L2 #I #V #e #_ #_ #_ #H
elim (plus_S_eq_O_false … H)
]
qed.
-lemma drop_inv_refl: ∀L2,L1. ↑[0, 0] L2 ≡ L1 → L1 = L2.
+lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2.
/2 width=5/ qed.
-lemma drop_inv_O1_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 →
+lemma drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 →
∀K,I,V. L1 = K. 𝕓{I} V →
(e = 0 ∧ L2 = K. 𝕓{I} V) ∨
- (0 < e â\88§ â\86\91[d, e - 1] L2 â\89¡ K).
-#d #e #L2 #L1 #H elim H -H d e L2 L1
+ (0 < e â\88§ â\86\93[d, e - 1] K â\89¡ L2).
+#d #e #L1 #L2 #H elim H -H d e L1 L2
[ /3/
| #L1 #L2 #I #V #e #HL12 #_ #_ #K #J #W #H destruct -L1 I V /3/
| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H elim (plus_S_eq_O_false … H)
]
qed.
-lemma drop_inv_O1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V →
+lemma drop_inv_O1: ∀e,K,I,V,L2. ↓[0, e] K. 𝕓{I} V ≡ L2 →
(e = 0 ∧ L2 = K. 𝕓{I} V) ∨
- (0 < e â\88§ â\86\91[0, e - 1] L2 â\89¡ K).
+ (0 < e â\88§ â\86\93[0, e - 1] K â\89¡ L2).
/2/ qed.
-lemma drop_inv_drop1: ∀e,L2,K,I,V.
- â\86\91[0, e] L2 â\89¡ K. ð\9d\95\93{I} V â\86\92 0 < e â\86\92 â\86\91[0, e - 1] L2 â\89¡ K.
-#e #L2 #K #I #V #H #He
+lemma drop_inv_drop1: ∀e,K,I,V,L2.
+ â\86\93[0, e] K. ð\9d\95\93{I} V â\89¡ L2 â\86\92 0 < e â\86\92 â\86\93[0, e - 1] K â\89¡ L2.
+#e #K #I #V #L2 #H #He
elim (drop_inv_O1 … H) -H * // #H destruct -e;
elim (lt_refl_false … He)
qed.
-lemma drop_inv_skip2_aux: â\88\80d,e,L1,L2. â\86\91[d, e] L2 â\89¡ L1 → 0 < d →
+lemma drop_inv_skip2_aux: â\88\80d,e,L1,L2. â\86\93[d, e] L1 â\89¡ L2 → 0 < d →
∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
- â\88\83â\88\83K1,V1. â\86\91[d - 1, e] K2 â\89¡ K1 &
+ â\88\83â\88\83K1,V1. â\86\93[d - 1, e] K1 â\89¡ K2 &
↑[d - 1, e] V2 ≡ V1 &
L1 = K1. 𝕓{I} V1.
#d #e #L1 #L2 #H elim H -H d e L1 L2
]
qed.
-lemma drop_inv_skip2: â\88\80d,e,I,L1,K2,V2. â\86\91[d, e] K2. ð\9d\95\93{I} V2 â\89¡ L1 → 0 < d →
- â\88\83â\88\83K1,V1. â\86\91[d - 1, e] K2 â\89¡ K1 & ↑[d - 1, e] V2 ≡ V1 &
+lemma drop_inv_skip2: â\88\80d,e,I,L1,K2,V2. â\86\93[d, e] L1 â\89¡ K2. ð\9d\95\93{I} V2 → 0 < d →
+ â\88\83â\88\83K1,V1. â\86\93[d - 1, e] K1 â\89¡ K2 & ↑[d - 1, e] V2 ≡ V1 &
L1 = K1. 𝕓{I} V1.
/2/ qed.
(* the main properties ******************************************************)
-lemma drop_conf_ge: â\88\80d1,e1,L,L1. â\86\91[d1, e1] L1 â\89¡ L →
- â\88\80e2,L2. â\86\91[0, e2] L2 â\89¡ L → d1 + e1 ≤ e2 →
- â\86\91[0, e2 - e1] L2 â\89¡ L1.
+lemma drop_conf_ge: â\88\80d1,e1,L,L1. â\86\93[d1, e1] L â\89¡ L1 →
+ â\88\80e2,L2. â\86\93[0, e2] L â\89¡ L2 → d1 + e1 ≤ e2 →
+ â\86\93[0, e2 - e1] L1 â\89¡ L2.
#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
[ //
| #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
]
qed.
-lemma drop_conf_lt: â\88\80d1,e1,L,L1. â\86\91[d1, e1] L1 â\89¡ L →
- â\88\80e2,K2,I,V2. â\86\91[0, e2] K2. ð\9d\95\93{I} V2 â\89¡ L →
+lemma drop_conf_lt: â\88\80d1,e1,L,L1. â\86\93[d1, e1] L â\89¡ L1 →
+ â\88\80e2,K2,I,V2. â\86\93[0, e2] L â\89¡ K2. ð\9d\95\93{I} V2 →
e2 < d1 → let d ≝ d1 - e2 - 1 in
- â\88\83â\88\83K1,V1. â\86\91[0, e2] K1. ð\9d\95\93{I} V1 â\89¡ L1 &
- â\86\91[d, e1] K1 â\89¡ K2 & â\86\91[d,e1] V1 ≡ V2.
+ â\88\83â\88\83K1,V1. â\86\93[0, e2] L1 â\89¡ K1. ð\9d\95\93{I} V1 &
+ â\86\93[d, e1] K2 â\89¡ K1 & â\86\91[d, e1] V1 ≡ V2.
#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
[ #L0 #e2 #K2 #I #V2 #_ #H
elim (lt_zero_false … H)
]
qed.
-lemma drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 →
- â\88\80e2,L2. â\86\91[0, e2] L2 â\89¡ L → e2 ≤ d1 →
- â\88\83â\88\83L0. â\86\91[0, e2] L0 â\89¡ L1 & â\86\91[d1 - e2, e1] L2 â\89¡ L0.
+lemma drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
+ â\88\80e2,L2. â\86\93[0, e2] L â\89¡ L2 → e2 ≤ d1 →
+ â\88\83â\88\83L0. â\86\93[0, e2] L1 â\89¡ L0 & â\86\93[d1 - e2, e1] L0 â\89¡ L2.
#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
[ #L #e2 #L2 #HL2 #H
lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/
]
qed.
-lemma drop_trans_ge: â\88\80d1,e1,L1,L. â\86\91[d1, e1] L â\89¡ L1 →
- â\88\80e2,L2. â\86\91[0, e2] L2 â\89¡ L â\86\92 d1 â\89¤ e2 â\86\92 â\86\91[0, e1 + e2] L2 â\89¡ L1.
+lemma drop_trans_ge: â\88\80d1,e1,L1,L. â\86\93[d1, e1] L1 â\89¡ L →
+ â\88\80e2,L2. â\86\93[0, e2] L â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 â\86\93[0, e1 + e2] L1 â\89¡ L2.
#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
[ //
| /3/
]
qed.
-axiom drop_div: ∀e1,L1. ∀L:lenv. ↑[0, e1] L ≡ L1 → ∀e2,L2. ↑[0, e2] L ≡ L2 →
- â\88\83â\88\83L0. â\86\91[0, e1] L2 â\89¡ L0 & â\86\91[e1, e2] L1 â\89¡ L0.
+axiom drop_div: ∀e1,L1,L. ↓[0, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L2 ≡ L →
+ â\88\83â\88\83L0. â\86\93[0, e1] L0 â\89¡ L2 & â\86\93[e1, e2] L0 â\89¡ L1.
--- /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".
-
-(* TELESCOPIC SUBSTITUTION **************************************************)
-
-inductive subst: lenv → term → nat → nat → term → Prop ≝
-| subst_sort : ∀L,k,d,e. subst L (⋆k) d e (⋆k)
-| subst_lref_lt: ∀L,i,d,e. i < d → subst L (#i) d e (#i)
-| subst_lref_be: ∀L,K,V,U1,U2,i,d,e.
- d ≤ i → i < d + e →
- ↑[0, i] K. 𝕓{Abbr} V ≡ L → subst K V 0 (d + e - i - 1) U1 →
- ↑[0, d] U1 ≡ U2 → subst L (#i) d e U2
-| subst_lref_ge: ∀L,i,d,e. d + e ≤ i → subst L (#i) d e (#(i - e))
-| subst_bind : ∀L,I,V1,V2,T1,T2,d,e.
- subst L V1 d e V2 → subst (L. 𝕓{I} V1) T1 (d + 1) e T2 →
- subst L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2)
-| subst_flat : ∀L,I,V1,V2,T1,T2,d,e.
- subst L V1 d e V2 → subst L T1 d e T2 →
- subst L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2)
-.
-
-interpretation "telescopic substritution" 'RSubst L T1 d e T2 = (subst L T1 d e T2).
-
-(* The basic properties *****************************************************)
-
-lemma subst_lift_inv: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀L. L ⊢ ↓[d,e] T2 ≡ T1.
-#d #e #T1 #T2 #H elim H -H d e T1 T2 /2/
-#i #d #e #Hdi #L >(minus_plus_m_m i e) in ⊢ (? ? ? ? ? %) /3/
-qed.
-(*
-| subst_lref_O : ∀L,V1,V2,e. subst L V1 0 e V2 →
- subst (L. 𝕓{Abbr} V1) #0 0 (e + 1) V2
-| subst_lref_S : ∀L,I,V,i,T1,T2,d,e.
- d ≤ i → i < d + e → subst L #i d e T1 → ↑[d,1] T2 ≡ T1 →
- subst (L. 𝕓{I} V) #(i + 1) (d + 1) e T2
-*)
-(* The basic inversion lemmas ***********************************************)
-
-lemma subst_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ ↓[d, e] U1 ≡ U2 →
- ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
- ∃∃V2,T2. subst L V1 d e V2 &
- subst (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 #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 ⊢ ↓[d, e] 𝕓{I} V1. T1 ≡ U2 →
- ∃∃V2,T2. subst L V1 d e V2 &
- subst (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 ⊢ ↓[d, e] U1 ≡ U2 →
- ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
- ∃∃V2,T2. subst L V1 d e V2 & subst 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 #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 ⊢ ↓[d, e] 𝕗{I} V1. T1 ≡ U2 →
- ∃∃V2,T2. subst L V1 d e V2 & subst L T1 d e T2 &
- U2 = 𝕗{I} V2. T2.
-/2/ qed.
-(*
-lemma subst_inv_lref1_be_aux: ∀d,e,L,T,U. L ⊢ ↓[d, e] T ≡ U →
- ∀i. d ≤ i → i < d + e → T = #i →
- ∃∃K,V. ↑[0, i] K. 𝕓{Abbr} V ≡ L &
- K ⊢ ↓[d, d + e - i - 1] V ≡ U.
-#d #e #L #T #U #H elim H -H d e L T U
-[ #L #k #d #e #i #_ #_ #H destruct
-| #L #j #d #e #Hid #i #Hdi #_ #H destruct -j;
- lapply (le_to_lt_to_lt … Hdi … Hid) -Hdi Hid #Hdd
- elim (lt_false … Hdd)
-| #L #K #V #U #j #d #e #_ #_ #HLK #HVU #_ #i #Hdi #Hide #H destruct -j /2/
-| #L #j #d #e #Hdei #i #_ #Hide #H destruct -j;
- lapply (le_to_lt_to_lt … Hdei … Hide) -Hdei Hide #Hdede
- elim (lt_false … Hdede)
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #_ #_ #H destruct
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #_ #_ #H destruct
-]
-qed.
-
-lemma subst_inv_lref1_be: ∀d,e,i,L,U. L ⊢ ↓[d, e] #i ≡ U →
- d ≤ i → i < d + e →
- ∃∃K,V. ↑[0, i] K. 𝕓{Abbr} V ≡ L &
- K ⊢ ↓[d, d + e - i - 1] V ≡ U.
-/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/subst_defs.ma".
-
-(* THINNING *****************************************************************)
-
-inductive thin: lenv → nat → nat → lenv → Prop ≝
-| thin_refl: ∀L. thin L 0 0 L
-| thin_thin: ∀L1,L2,I,V,e. thin L1 0 e L2 → thin (L1. 𝕓{I} V) 0 (e + 1) L2
-| thin_skip: ∀L1,L2,I,V1,V2,d,e.
- thin L1 d e L2 → L1 ⊢ ↓[d,e] V1 ≡ V2 →
- thin (L1. 𝕓{I} V1) (d + 1) e (L2. 𝕓{I} V2)
-.
-
-interpretation "thinning" 'RSubst L1 d e L2 = (thin L1 d e L2).
-
-(* the basic inversion lemmas ***********************************************)
-
-lemma thin_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
- ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
- ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
- K1 ⊢ ↓[d - 1, e] V1 ≡ V2 &
- L1 = K1. 𝕓{I} V1.
-#d #e #L1 #L2 #H elim H -H d e L1 L2
-[ #L #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #_ #_ #H elim (lt_refl_false … H)
-| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #_ #I #L2 #V2 #H destruct -X Y Z;
- /2 width=5/
-]
-qed.
-
-lemma thin_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
- ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & K1 ⊢ ↓[d - 1, e] V1 ≡ 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 "lambda-delta/substitution/thin_defs.ma".
-
-(* THINNING *****************************************************************)
-
-(* the main properties ******************************************************)
-
-axiom thin_conf_ge: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 →
- ∀e2,L2. ↓[0,e2] L ≡ L2 → d1 + e1 ≤ e2 → ↓[0,e2-e1] L1 ≡ L2.
-
-axiom thin_conf_lt: ∀d1,e1,L,L1. ↓[d1,e1] L ≡ L1 →
- ∀e2,K2,I,V2. ↓[0,e2] L ≡ K2. 𝕓{I} V2 →
- e2 < d1 → let d ≝ d1 - e2 - 1 in
- ∃∃K1,V1. ↓[0,e2] L1 ≡ K1. 𝕓{I} V1 & ↓[d,e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2.
-
-axiom thin_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
- ∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
- ∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.
-
-axiom thin_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
- ∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2.
*)
include "lambda-delta/ground.ma".
+include "lambda-delta/notation.ma".
(* BINARY ITEMS *************************************************************)
interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
-inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝
- | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ?
+inductive or3 (P0,P1,P2:Prop) : Prop ≝
+ | or3_intro0: P0 → or3 ? ? ?
+ | or3_intro1: P1 → or3 ? ? ?
+ | or3_intro2: P2 → or3 ? ? ?
.
-interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3).
-
-inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝
- | or4_intro0: P0 → or4 ? ? ? ?
- | or4_intro1: P1 → or4 ? ? ? ?
- | or4_intro2: P2 → or4 ? ? ? ?
- | or4_intro3: P3 → or4 ? ? ? ?
-.
-
-interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
+interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
non associative with precedence 20
for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) }.
-notation "hvbox(â\88\83â\88\83 ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+notation "hvbox(â\88¨â\88¨ term 19 P0 break | term 19 P1 break | term 19 P2)"
non associative with precedence 20
- for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) (λ${ident x0},${ident x1},${ident x2}.$P3) }.
-
-notation "hvbox(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2 break | term 19 P3)"
- non associative with precedence 20
- for @{ 'Or $P0 $P1 $P2 $P3 }.
+ for @{ 'Or $P0 $P1 $P2 }.
projects / helm.git / commitdiff