definition dsubstable_dx: predicate (relation term) ≝ λR.
∀D,M1,M2. R M1 M2 → ∀d. R ([d ↙ D] M1) ([d ↙ D] M2).
-(*
-definition dsubstable_sn: predicate (relation term) ≝ λR.
- ∀D1,D2. R D1 D2 → ∀M,d. R ([d ↙ D1] M) ([d ↙ D2] M).
-*)
+
definition dsubstable: predicate (relation term) ≝ λR.
∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ D1] M1) ([d ↙ D2] M2).
lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
#R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/
qed.
-(*
-lemma star_dsubstable_sn: ∀R. dsubstable_sn R → dsubstable_sn (star … R).
-#R #HR #D1 #D2 #H elim H -D2 // /3 width=3/
-qed.
-*)
+
lemma lstar_dsubstable_dx: ∀T,R. (∀t. dsubstable_dx (R t)) →
∀l. dsubstable_dx (lstar T … R l).
#T #R #HR #l #D #M1 #M2 #H
@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
qed.
+
+lemma star_dsubstable: ∀R. reflexive ? R →
+ dsubstable R → dsubstable (star … R).
+#R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/
+qed.
(**************************************************************************)
include "pointer_sequence.ma".
-include "labelled_sequential_reduction.ma".
+include "parallel_computation.ma".
(* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************)
non associative with precedence 45
for @{ 'SeqRedStar $M $s $N }.
+lemma lsreds_refl: reflexive … (lsreds (◊)).
+//
+qed.
+
+lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2.
+/2 width=3/
+qed-.
+
+lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2.
+/2 width=3/
+qed-.
+
lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2.
/2 width=1/
qed.
/3 width=1/
qed.
-lemma lsred_compatible_sn: ho_compatible_sn lsreds.
+lemma lsreds_compatible_sn: ho_compatible_sn lsreds.
/3 width=1/
qed.
-lemma lsred_compatible_dx: ho_compatible_dx lsreds.
+lemma lsreds_compatible_dx: ho_compatible_dx lsreds.
/3 width=1/
qed.
/2 width=3 by lstar_ltransitive/
qed-.
+lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
+ @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2.
+#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
+@(lsreds_trans … (@B2.A1)) /2 width=1/
+qed.
+
+lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 →
+ @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::sn:::s)@◊::◊] [↙B2] A2.
+#r #B1 #B2 #HB12 #s #A1 #A2 #HA12
+@(lsreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1
+@(lsreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/
+qed.
+
(* Note: "|s|" should be unparetesized *)
lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ↦*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
@(transitive_le … IHM2) -M2
/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
qed-.
+
+theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#a #s #M1 #M #HM1 #_ #IHM2
+@(preds_step_sn … IHM2) -M2 /2 width=2/
+qed.
+
+lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2.
+#M1 #M2 #H elim H -M1 -M2 /2 width=2/
+[ #A1 #A2 #_ * /3 width=2/
+| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
+| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/
+qed-.
+
+theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2.
+#M1 #M2 #H elim H -M2 /2 width=2/
+#M #M2 #_ #HM2 * #r #HM1
+elim (pred_lsreds … HM2) -HM2 #s #HM2
+lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/
+qed-.
+
+theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 →
+ ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M.
+#s1 #M0 #M1 #HM01 #s2 #M2 #HM02
+lapply (lsreds_preds … HM01) -s1 #HM01
+lapply (lsreds_preds … HM02) -s2 #HM02
+elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2
+elim (preds_lsreds … HM1) -HM1
+elim (preds_lsreds … HM2) -HM2 /2 width=5/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "parallel_reduction.ma".
+
+(* PARALLEL COMPUTATION (MULTISTEP) *****************************************)
+
+definition preds: relation term ≝ star … pred.
+
+interpretation "parallel computation"
+ 'ParRedStar M N = (preds M N).
+
+notation "hvbox( M ⤇* break term 46 N )"
+ non associative with precedence 45
+ for @{ 'ParRedStar $M $N }.
+
+lemma preds_refl: reflexive … preds.
+//
+qed.
+
+lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2.
+/2 width=3/
+qed-.
+
+lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2.
+/2 width=3/
+qed-.
+
+lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2.
+/2 width=1/
+qed.
+
+lemma preds_compatible_abst: compatible_abst preds.
+/3 width=1/
+qed.
+
+lemma preds_compatible_sn: compatible_sn preds.
+/3 width=1/
+qed.
+
+lemma preds_compatible_dx: compatible_dx preds.
+/3 width=1/
+qed.
+
+lemma preds_compatible_appl: compatible_appl preds.
+/3 width=1/
+qed.
+
+lemma preds_lift: liftable preds.
+/2 width=1/
+qed.
+
+lemma preds_inv_lift: deliftable_sn preds.
+/3 width=3 by star_deliftable_sn, pred_inv_lift/
+qed-.
+
+lemma preds_dsubst_dx: dsubstable_dx preds.
+/2 width=1/
+qed.
+
+lemma preds_dsubst: dsubstable preds.
+/2 width=1/
+qed.
+
+theorem preds_trans: transitive … preds.
+/2 width=3 by trans_star/
+qed-.
+
+lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 →
+ ∃∃M. M1 ⤇ M & M2 ⤇* M.
+/3 width=3 by star_strip, pred_conf/
+qed-.
+
+theorem preds_conf: confluent … preds.
+/3 width=3 by star_confluent, pred_conf/
+qed-.
notation "hvbox( @ term 46 C . break term 46 A )"
non associative with precedence 46
for @{ 'Application $C $A }.
-(*
-definition appl_compatible_dx: predicate (relation term) ≝ λR.
- ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2).
-lemma star_appl_compatible_dx: ∀R. appl_compatible_dx R →
- appl_compatible_dx (star … R).
+definition compatible_abst: predicate (relation term) ≝ λR.
+ ∀A1,A2. R A1 A2 → R (𝛌.A1) (𝛌.A2).
+
+definition compatible_sn: predicate (relation term) ≝ λR.
+ ∀A,B1,B2. R B1 B2 → R (@B1.A) (@B2.A).
+
+definition compatible_dx: predicate (relation term) ≝ λR.
+ ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2).
+
+definition compatible_appl: predicate (relation term) ≝ λR.
+ ∀B1,B2. R B1 B2 → ∀A1,A2. R A1 A2 →
+ R (@B1.A1) (@B2.A2).
+
+lemma star_compatible_abst: ∀R. compatible_abst R → compatible_abst (star … R).
+#R #HR #A1 #A2 #H elim H -A2 // /3 width=3/
+qed.
+
+lemma star_compatible_sn: ∀R. compatible_sn R → compatible_sn (star … R).
+#R #HR #A #B1 #B2 #H elim H -B2 // /3 width=3/
+qed.
+
+lemma star_compatible_dx: ∀R. compatible_dx R → compatible_dx (star … R).
#R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/
qed.
-*)
+
+lemma star_compatible_appl: ∀R. reflexive ? R →
+ compatible_appl R → compatible_appl (star … R).
+#R #H1R #H2R #B1 #B2 #H elim H -B2 /3 width=1/ /3 width=5/
+qed.
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
<key name="ex">2 2</key>
+ <key name="ex">2 3</key>
<key name="ex">3 2</key>
<key name="ex">3 3</key>
<key name="ex">4 3</key>
interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
+(* multiple existental quantifier (2, 3) *)
+
+inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝
+ | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1).
+
(* multiple existental quantifier (3, 2) *)
inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }.
+(* multiple existental quantifier (2, 3) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }.
+
(* multiple existental quantifier (3, 2) *)
notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
| #H12 @(bi_TC_ind_dx ?????????? H12) -a1 -b1 /2 width=5/ -H /3 width=5/
]
qed-.
+
+(* ************ confluence of star *****************)
+
+lemma star_strip: ∀A,R. confluent A R →
+ ∀a0,a1. star … R a0 a1 → ∀a2. R a0 a2 →
+ ∃∃a. R a1 a & star … R a2 a.
+#A #R #HR #a0 #a1 #H elim H -a1 /2 width=3/
+#a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
+elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
+elim (HR … Ha1 … Ha0) -a /3 width=5/
+qed-.
+
+lemma star_confluent: ∀A,R. confluent A R → confluent A (star … R).
+#A #R #HR #a0 #a1 #H elim H -a1 /2 width=3/
+#a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
+elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
+elim (star_strip … HR … Ha0 … Ha1) -a /3 width=5/
+qed-.
projects / helm.git / commitdiff