matita/matita/contribs/lambda/parallel_reduction.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "multiplicity.ma".
  16
  17 (* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
  18
  19 (* Note: the application "(A B)" is represented by "@B.A"
  20          as for labelled sequential reduction
  21 *)
  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)
  27 .
  28
  29 interpretation "parallel reduction"
  30     'ParRed M N = (pred M N).
  31
  32 notation "hvbox( M break ⥤ break term 46 N )"
  33    non associative with precedence 45
  34    for @{ 'ParRed $M $N }.
  35
  36 lemma pred_refl: reflexive … pred.
  37 #M elim M -M // /2 width=1/
  38 qed.
  39
  40 lemma pred_inv_vref: ∀M,N. M ⥤ N → ∀i. #i = M → #i = N.
  41 #M #N * -M -N //
  42 [ #A #C #_ #i #H destruct
  43 | #B #D #A #C #_ #_ #i #H destruct
  44 | #B #D #A #C #_ #_ #i #H destruct
  45 ]
  46 qed-.
  47
  48 lemma pred_inv_abst: ∀M,N. M ⥤ N → ∀A. 𝛌.A = M →
  49                      ∃∃C. A ⥤ C & 𝛌.C = N.
  50 #M #N * -M -N
  51 [ #i #A0 #H destruct
  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
  55 ]
  56 qed-.
  57
  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/
  61 qed.
  62
  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/
  80 ]
  81 qed-.