1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "multiplicity.ma".
17 (* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
19 (* Note: the application "(A B)" is represented by "@B.A"
20 as for labelled sequential reduction
22 inductive pred: relation term ≝
23 | pred_vref: ∀i. pred (#i) (#i)
24 | pred_abst: ∀A,C. pred A C → pred (𝛌.A) (𝛌.C)
25 | pred_appl: ∀B,D,A,C. pred B D → pred A C → pred (@B.A) (@D.C)
26 | pred_beta: ∀B,D,A,C. pred B D → pred A C → pred (@B.𝛌.A) ([⬐D]C)
29 interpretation "parallel reduction"
30 'ParRed M N = (pred M N).
32 notation "hvbox( M break ⥤ break term 46 N )"
33 non associative with precedence 45
34 for @{ 'ParRed $M $N }.
36 lemma pred_refl: reflexive … pred.
37 #M elim M -M // /2 width=1/
40 lemma pred_inv_vref: ∀M,N. M ⥤ N → ∀i. #i = M → #i = N.
42 [ #A #C #_ #i #H destruct
43 | #B #D #A #C #_ #_ #i #H destruct
44 | #B #D #A #C #_ #_ #i #H destruct
48 lemma pred_inv_abst: ∀M,N. M ⥤ N → ∀A. 𝛌.A = M →
52 | #A #C #HAC #A0 #H destruct /2 width=3/
53 | #B #D #A #C #_ #_ #A0 #H destruct
54 | #B #D #A #C #_ #_ #A0 #H destruct
58 lemma pred_lift: liftable pred.
59 #h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/
60 #D #D #A #C #_ #_ #IHBD #IHAC #d <dsubst_lift_le // /2 width=1/
63 lemma pred_inv_lift: deliftable pred.
64 #h #N1 #N2 #H elim H -N1 -N2 /2 width=3/
65 [ #C1 #C2 #_ #IHC12 #d #M1 #H
66 elim (lift_inv_abst … H) -H #A1 #HAC1 #H
67 elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
68 @(ex2_1_intro … (𝛌.A2)) // /2 width=1/
69 | #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
70 elim (lift_inv_appl … H) -H #B1 #A1 #HBD1 #HAC1 #H
71 elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
72 elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
73 @(ex2_1_intro … (@B2.A2)) // /2 width=1/
74 | #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
75 elim (lift_inv_appl … H) -H #B1 #M #HBD1 #HM #H1
76 elim (lift_inv_abst … HM) -HM #A1 #HAC1 #H
77 elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
78 elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
79 @(ex2_1_intro … ([⬐B2]A2)) /2 width=1/