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