matita/matita/lib/lambda/paths/labeled_st_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/subterms/booleanized.ma".
  16 include "lambda/paths/labeled_sequential_reduction.ma".
  17 include "lambda/paths/standard_order.ma".
  18
  19 include "lambda/notation/relations/std_3.ma".
  20
  21 include "lambda/xoa/ex_4_1.ma".
  22 include "lambda/xoa/ex_3_4.ma".
  23
  24 (* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************)
  25
  26 (* Note: this is standard reduction on marked redexes,
  27          left residuals are unmarked in the reductum
  28 *)
  29 inductive pl_st: path → relation subterms ≝
  30 | pl_st_beta   : ∀V,T. pl_st (◊) ({⊤}@V.{⊤}𝛌.T) ([↙V]T)
  31 | pl_st_abst   : ∀b,p,T1,T2. pl_st p T1 T2 → pl_st (rc::p) ({b}𝛌.T1) ({⊥}𝛌.T2)
  32 | pl_st_appl_sn: ∀b,p,V1,V2,T. pl_st p V1 V2 → pl_st (sn::p) ({b}@V1.T) ({⊥}@V2.{⊥}⇕T)
  33 | pl_st_appl_dx: ∀b,p,V,T1,T2. pl_st p T1 T2 → pl_st (dx::p) ({b}@V.T1) ({b}@V.T2)
  34 .
  35
  36 interpretation "path-labeled standard reduction"
  37     'Std F p G = (pl_st p F G).
  38
  39 lemma pl_st_fwd_pl_sred: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → ⇓F1 ↦[p] ⇓F2.
  40 #p #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/
  41 qed-.
  42
  43 lemma pl_st_inv_vref: ∀p,F,G. F Ⓡ↦[p] G → ∀b,i. {b}#i = F → ⊥.
  44 #p #F #G #HFG #b #i #H
  45 lapply (pl_st_fwd_pl_sred … HFG) -HFG #HFG
  46 lapply (eq_f … carrier … H) -H normalize #H
  47 /2 width=6 by pl_sred_inv_vref/
  48 qed-.
  49
  50 lemma pl_st_inv_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀c,U1. {c}𝛌.U1 = F →
  51                       ∃∃q,U2. U1 Ⓡ↦[q] U2 & rc::q = p & {⊥}𝛌.U2 = G.
  52 #p #F #G * -p -F -G
  53 [ #V #T #c #U1 #H destruct
  54 | #b #p #T1 #T2 #HT12 #c #U1 #H destruct /2 width=5/
  55 | #b #p #V1 #V2 #T #_ #c #U1 #H destruct
  56 | #b #p #V #T1 #T2 #_ #c #U1 #H destruct
  57 ]
  58 qed-.
  59
  60 lemma pl_st_inv_appl: ∀p,F,G. F Ⓡ↦[p] G → ∀c,W,U. {c}@W.U = F →
  61                       ∨∨ (∃∃U0. ⊤ = c & ◊ = p & {⊤}𝛌.U0 = U & [↙W] U0 = G)
  62                        | (∃∃q,W0. sn::q = p & W Ⓡ↦[q] W0 & {⊥}@W0.{⊥}⇕U = G)
  63                        | (∃∃q,U0. dx::q = p & U Ⓡ↦[q] U0 & {c}@W.U0 = G).
  64 #p #F #G * -p -F -G
  65 [ #V #T #c #W #U #H destruct /3 width=3/
  66 | #b #p #T1 #T2 #_ #c #W #U #H destruct
  67 | #b #p #V1 #V2 #T #HV12 #c #W #U #H destruct /3 width=5/
  68 | #b #p #V #T1 #T2 #HT12 #c #W #U #H destruct /3 width=5/
  69 ]
  70 qed-.
  71
  72 lemma pl_st_fwd_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀c,U2. {c}𝛌.U2 = G →
  73                       ◊ = p ∨ ∃q. rc::q = p.
  74 #p #F #G * -p -F -G
  75 [ /2 width=1/
  76 | /3 width=2/
  77 | #b #p #V1 #V2 #T #_ #c #U2 #H destruct
  78 | #b #p #V #T1 #T2 #_ #c #U2 #H destruct
  79 ]
  80 qed-.
  81
  82 lemma pl_st_inv_nil: ∀p,F,G. F Ⓡ↦[p] G → ◊ = p →
  83                      ∃∃V,T. {⊤}@V.{⊤} 𝛌.T = F & [↙V] T = G.
  84 #p #F #G * -p -F -G
  85 [ #V #T #_ destruct /2 width=4/
  86 | #b #p #T1 #T2 #_ #H destruct
  87 | #b #p #V1 #V2 #T #_ #H destruct
  88 | #b #p #V #T1 #T2 #_ #H destruct
  89 ]
  90 qed-.
  91
  92 lemma pl_st_inv_rc: ∀p,F,G. F Ⓡ↦[p] G → ∀q. rc::q = p →
  93                     ∃∃b,T1,T2. T1 Ⓡ↦[q] T2 & {b}𝛌.T1 = F & {⊥}𝛌.T2 = G.
  94 #p #F #G * -p -F -G
  95 [ #V #T #q #H destruct
  96 | #b #p #T1 #T2 #HT12 #q #H destruct /2 width=6/
  97 | #b #p #V1 #V2 #T #_ #q #H destruct
  98 | #b #p #V #T1 #T2 #_ #q #H destruct
  99 ]
 100 qed-.
 101
 102 lemma pl_st_inv_sn: ∀p,F,G. F Ⓡ↦[p] G → ∀q. sn::q = p →
 103                     ∃∃b,V1,V2,T. V1 Ⓡ↦[q] V2 & {b}@V1.T = F & {⊥}@V2.{⊥}⇕T = G.
 104 #p #F #G * -p -F -G
 105 [ #V #T #q #H destruct
 106 | #b #p #T1 #T2 #_ #q #H destruct
 107 | #b #p #V1 #V2 #T #HV12 #q #H destruct /2 width=7/
 108 | #b #p #V #T1 #T2 #_ #q #H destruct
 109 ]
 110 qed-.
 111
 112 lemma pl_st_inv_dx: ∀p,F,G. F Ⓡ↦[p] G → ∀q. dx::q = p →
 113                     ∃∃b,V,T1,T2. T1 Ⓡ↦[q] T2 & {b}@V.T1 = F & {b}@V.T2 = G.
 114 #p #F #G * -p -F -G
 115 [ #V #T #q #H destruct
 116 | #b #p #T1 #T2 #_ #q #H destruct
 117 | #b #p #V1 #V2 #T #_ #q #H destruct
 118 | #b #p #V #T1 #T2 #HT12 #q #H destruct /2 width=7/
 119 ]
 120 qed-.
 121
 122 lemma pl_st_inv_pl_sred: ∀p. in_whd p → ∀M1,F2. {⊤}⇑M1 Ⓡ↦[p] F2 →
 123                          ∃∃M2. M1 ↦[p] M2 & {⊤}⇑M2 = F2.
 124 #p @(in_whd_ind … p) -p
 125 [ #M1 #F2 #H
 126   elim (pl_st_inv_nil … H …) -H // #V #T #HM1 #H
 127   elim (boolean_inv_appl … (sym_eq … HM1)) -HM1 #B #N #_ #HB #HN #HM1
 128   elim (boolean_inv_abst … HN) -HN #A #_ #HA #HN destruct /2 width=3/
 129 | #p #_ #IHp #M1 #F2 #H
 130   elim (pl_st_inv_dx … H …) -H [3: // |2:skip ] #b #V #T1 #T2 #HT12 #HM1 #H (**) (* simplify line *)
 131   elim (boolean_inv_appl … (sym_eq … HM1)) -HM1 #B #A #Hb #HB #HA #HM1 destruct
 132   elim (IHp … HT12) -IHp -HT12 #C #HAC #H destruct
 133   @(ex2_intro … (@B.C)) // /2 width=1/ (**) (* auto needs some help here *)
 134 ]
 135 qed-.
 136
 137 lemma pl_st_lift: ∀p. sliftable (pl_st p).
 138 #p #h #F1 #F2 #H elim H -p -F1 -F2 /2 width=1/
 139 [ #V #T #d normalize <sdsubst_slift_le //
 140 | #b #p #V1 #V2 #T #_ #IHV12 #d
 141   whd in ⊢ (??%%); <booleanized_lift /2 width=1/ (**) (* auto needs some help here *)
 142 ]
 143 qed.
 144
 145 lemma pl_st_inv_lift: ∀p. sdeliftable_sn (pl_st p).
 146 #p #h #G1 #G2 #H elim H -p -G1 -G2
 147 [ #W #U #d #F1 #H
 148   elim (slift_inv_appl … H) -H #V #F #H0 #HF #H destruct
 149   elim (slift_inv_abst … HF) -HF #T #H0 #H destruct /3 width=3/
 150 | #b #p #U1 #U2 #_ #IHU12 #d #F1 #H
 151   elim (slift_inv_abst … H) -H #T1 #HTU1 #H
 152   elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
 153   @(ex2_intro … ({⊥}𝛌.T2)) // /2 width=1/
 154 | #b #p #W1 #W2 #U1 #_ #IHW12 #d #F1 #H
 155   elim (slift_inv_appl … H) -H #V1 #T #HVW1 #H1 #H2
 156   elim (IHW12 … HVW1) -W1 #V2 #HV12 #HVW2 destruct
 157   @(ex2_intro … ({⊥}@V2.{⊥}⇕T)) [ /2 width=1/ ]
 158   whd in ⊢ (??%%); // (**) (* auto needs some help here *)
 159 | #b #p #W1 #U1 #U2 #_ #IHU12 #d #F1 #H
 160   elim (slift_inv_appl … H) -H #V #T1 #H1 #HTU1 #H2
 161   elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
 162   @(ex2_intro … ({b}@V.T2)) // /2 width=1/
 163 ]
 164 qed-.
 165
 166 lemma pl_st_dsubst: ∀p. sdsubstable_f_dx … (booleanized ⊥) (pl_st p).
 167 #p #W1 #F1 #F2 #H elim H -p -F1 -F2 /2 width=1/
 168 [ #W2 #T #d normalize >sdsubst_sdsubst_ge //
 169 | #b #p #V1 #V2 #T #_ #IHV12 #d
 170   whd in ⊢ (??%%); <(booleanized_booleanized ⊥) in ⊢ (???(???%)); <booleanized_dsubst /2 width=1/ (**) (* auto needs some help here *)
 171 ]
 172 qed.
 173
 174 lemma pl_st_inv_empty: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → ∀M1. {⊥}⇑M1 = F1 → ⊥.
 175 #p #F1 #F2 #H elim H -p -F1 -F2
 176 [ #V #T #M1 #H
 177   elim (boolean_inv_appl … H) -H #B #A #H destruct
 178 | #b #p #T1 #T2 #_ #IHT12 #M1 #H
 179   elim (boolean_inv_abst … H) -H /2 width=2/
 180 | #b #p #V1 #V2 #T #_ #IHV12 #M1 #H
 181   elim (boolean_inv_appl … H) -H /2 width=2/
 182 | #b #p #V #T1 #T2 #_ #IHT12 #M1 #H
 183   elim (boolean_inv_appl … H) -H /2 width=2/
 184 ]
 185 qed-.
 186
 187 theorem pl_st_mono: ∀p. singlevalued … (pl_st p).
 188 #p #F #G1 #H elim H -p -F -G1
 189 [ #V #T #G2 #H elim (pl_st_inv_nil … H …) -H //
 190   #W #U #H #HG2 destruct //
 191 | #b #p #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_rc … H …) -H [3: // |2: skip ] (**) (* simplify line *)
 192   #c #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
 193 | #b #p #V1 #V2 #T #_ #IHV12 #G2 #H elim (pl_st_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *)
 194   #c #W1 #W2 #U #HW12 #H #HG2 destruct /3 width=1/
 195 | #b #p #V #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *)
 196   #c #W #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
 197 ]
 198 qed-.
 199
 200 theorem pl_st_fwd_sle: ∀p1,F1,F. F1 Ⓡ↦[p1] F →
 201                        ∀p2,F2. F Ⓡ↦[p2] F2 → p1 ≤ p2.
 202 #p1 #F1 #F #H elim H -p1 -F1 -F //
 203 [ #b #p #T1 #T #_ #IHT1 #p2 #F2 #H elim (pl_st_inv_abst … H …) -H [3: // |2,4: skip ] (**) (* simplify line *)
 204   #q #T2 #HT2 #H1 #H2 destruct /3 width=2/
 205 | #b #p #V1 #V #T #_ #IHV1 #p2 #F2 #H elim (pl_st_inv_appl … H …) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
 206   [ #U #H destruct
 207   | #q #V2 #H1 #HV2 #H2 destruct /3 width=2/
 208   | #q #U #_ #H elim (pl_st_inv_empty … H …) [ // | skip ] (**) (* simplify line *)
 209   ]
 210 | #b #p #V #T1 #T #HT1 #IHT1 #p2 #F2 #H elim (pl_st_inv_appl … H …) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
 211   [ #U #_ #H1 #H2 #_ -b -V -F2 -IHT1
 212     elim (pl_st_fwd_abst … HT1 … H2) // -H1 * #q #H
 213     elim (pl_st_inv_rc … HT1 … H) -HT1 -H #b #U1 #U2 #_ #_ #H -b -q -T1 -U1 destruct
 214   | #q #V2 #H1 #_ #_ -b -F2 -T1 -T -V -V2 destruct //
 215   | #q #T2 #H1 #HT2 #H2 -b -F2 -T1 -V /3 width=2/
 216   ]
 217 ]
 218 qed-.