matita/matita/lib/lambda/paths/labeled_sequential_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 "lambda/paths/path.ma".
  16 include "lambda/terms/sequential_reduction.ma".
  17
  18 (* PATH-LABELED SEQUENTIAL REDUCTION (SINGLE STEP) **************************)
  19
  20 inductive pl_sred: path → relation term ≝
  21 | pl_sred_beta   : ∀B,A. pl_sred (◊) (@B.𝛌.A) ([↙B]A)
  22 | pl_sred_abst   : ∀p,A1,A2. pl_sred p A1 A2 → pl_sred (rc::p) (𝛌.A1) (𝛌.A2)
  23 | pl_sred_appl_sn: ∀p,B1,B2,A. pl_sred p B1 B2 → pl_sred (sn::p) (@B1.A) (@B2.A)
  24 | pl_sred_appl_dx: ∀p,B,A1,A2. pl_sred p A1 A2 → pl_sred (dx::p) (@B.A1) (@B.A2)
  25 .
  26
  27 interpretation "path-labeled sequential reduction"
  28    'SeqRed M p N = (pl_sred p M N).
  29
  30 lemma sred_pl_sred: ∀M,N. M ↦ N → ∃p. M ↦[p] N.
  31 #M #N #H elim H -M -N
  32 [ /2 width=2/
  33 | #A1 #A2 #_ * /3 width=2/
  34 | #B1 #B2 #A #_ * /3 width=2/
  35 | #B #A1 #A2 #_ * /3 width=2/
  36 ]
  37 qed-.
  38
  39 lemma pl_sred_inv_sred: ∀p,M,N. M ↦[p] N → M ↦ N.
  40 #p #M #N #H elim H -p -M -N // /2 width=1/
  41 qed-.
  42
  43 lemma pl_sred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥.
  44 /3 width=5 by pl_sred_inv_sred, sred_inv_vref/
  45 qed-.
  46
  47 lemma pl_sred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p →
  48                        ∃∃B,A. @B. 𝛌.A = M & [↙B] A = N.
  49 #p #M #N * -p -M -N
  50 [ #B #A #_ destruct /2 width=4/
  51 | #p #A1 #A2 #_ #H destruct
  52 | #p #B1 #B2 #A #_ #H destruct
  53 | #p #B #A1 #A2 #_ #H destruct
  54 ]
  55 qed-.
  56
  57 lemma pl_sred_inv_rc: ∀p,M,N. M ↦[p] N → ∀q. rc::q = p →
  58                       ∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N.
  59 #p #M #N * -p -M -N
  60 [ #B #A #q #H destruct
  61 | #p #A1 #A2 #HA12 #q #H destruct /2 width=5/
  62 | #p #B1 #B2 #A #_ #q #H destruct
  63 | #p #B #A1 #A2 #_ #q #H destruct
  64 ]
  65 qed-.
  66
  67 lemma pl_sred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p →
  68                       ∃∃B1,B2,A. B1 ↦[q] B2 & @B1.A = M & @B2.A = N.
  69 #p #M #N * -p -M -N
  70 [ #B #A #q #H destruct
  71 | #p #A1 #A2 #_ #q #H destruct
  72 | #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/
  73 | #p #B #A1 #A2 #_ #q #H destruct
  74 ]
  75 qed-.
  76
  77 lemma pl_sred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p →
  78                       ∃∃B,A1,A2. A1 ↦[q] A2 & @B.A1 = M & @B.A2 = N.
  79 #p #M #N * -p -M -N
  80 [ #B #A #q #H destruct
  81 | #p #A1 #A2 #_ #q #H destruct
  82 | #p #B1 #B2 #A #_ #q #H destruct
  83 | #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/
  84 ]
  85 qed-.
  86
  87 lemma pl_sred_lift: ∀p. liftable (pl_sred p).
  88 #p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
  89 #B #A #d <dsubst_lift_le //
  90 qed.
  91
  92 lemma pl_sred_inv_lift: ∀p. deliftable_sn (pl_sred p).
  93 #p #h #N1 #N2 #H elim H -p -N1 -N2
  94 [ #D #C #d #M1 #H
  95   elim (lift_inv_appl … H) -H #B #M #H0 #HM #H destruct
  96   elim (lift_inv_abst … HM) -HM #A #H0 #H destruct /3 width=3/
  97 | #p #C1 #C2 #_ #IHC12 #d #M1 #H
  98   elim (lift_inv_abst … H) -H #A1 #HAC1 #H
  99   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
 100   @(ex2_intro … (𝛌.A2)) // /2 width=1/
 101 | #p #D1 #D2 #C1 #_ #IHD12 #d #M1 #H
 102   elim (lift_inv_appl … H) -H #B1 #A #HBD1 #H1 #H2
 103   elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2 destruct
 104   @(ex2_intro … (@B2.A)) // /2 width=1/
 105 | #p #D1 #C1 #C2 #_ #IHC12 #d #M1 #H
 106   elim (lift_inv_appl … H) -H #B #A1 #H1 #HAC1 #H2
 107   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
 108   @(ex2_intro … (@B.A2)) // /2 width=1/
 109 ]
 110 qed-.
 111
 112 lemma pl_sred_dsubst: ∀p. dsubstable_dx (pl_sred p).
 113 #p #D1 #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/
 114 #D2 #A #d >dsubst_dsubst_ge //
 115 qed.
 116
 117 theorem pl_sred_mono: ∀p. singlevalued … (pl_sred p).
 118 #p #M #N1 #H elim H -p -M -N1
 119 [ #B #A #N2 #H elim (pl_sred_inv_nil … H …) -H //
 120   #D #C #H #HN2 destruct //
 121 | #p #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_rc … H …) -H [3: // |2: skip ] (**) (* simplify line *)
 122   #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
 123 | #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (pl_sred_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *)
 124   #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/
 125 | #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (pl_sred_inv_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *)
 126   #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/
 127 ]
 128 qed-.