matita/matita/contribs/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 "subterms/booleanize.ma".
  16 include "paths/standard_order.ma".
  17
  18 (* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************)
  19
  20 (* Note: this is standard reduction on marked redexes,
  21          left residuals are unmarked in the reductum
  22 *)
  23 inductive pl_st: path → relation subterms ≝
  24 | pl_st_beta   : ∀V,T. pl_st (◊) ({⊤}@V.{⊤}𝛌.T) ([↙V]T)
  25 | pl_st_abst   : ∀b,p,T1,T2. pl_st p T1 T2 → pl_st (rc::p) ({b}𝛌.T1) ({⊥}𝛌.T2)
  26 | pl_st_appl_sn: ∀b,p,V1,V2,T. pl_st p V1 V2 → pl_st (sn::p) ({b}@V1.T) ({⊥}@V2.{⊥}⇕T)
  27 | pl_st_appl_dx: ∀b,p,V,T1,T2. pl_st p T1 T2 → pl_st (dx::p) ({b}@V.T1) ({b}@V.T2)
  28 .
  29
  30 interpretation "path-labeled standard reduction"
  31     'Std F p G = (pl_st p F G).
  32
  33 notation "hvbox( F break Ⓡ ↦ [ term 46 p ] break term 46 G )"
  34    non associative with precedence 45
  35    for @{ 'Std $F $p $G }.
  36 (*
  37 lemma pl_st_inv_pl_sred: ∀p,F,G. F Ⓡ↦[p] G → ⇓F ↦[p] ⇓G.
  38 #p #F #G #H elim H -p -F -G // /2 width=1/
  39 qed-.
  40
  41 lemma pl_st_inv_vref: ∀p,F,G. F Ⓡ↦[p] G → ∀b,i. {b}#i = F → ⊥.
  42 /3 width=5 by pl_st_inv_st, st_inv_vref/
  43 qed-.
  44 *)
  45 lemma pl_st_inv_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U1. {b0}𝛌.U1 = F →
  46                       ∃∃q,U2. U1 Ⓡ↦[q] U2 & rc::q = p & {⊥}𝛌.U2 = G.
  47 #p #F #G * -p -F -G
  48 [ #V #T #b0 #U1 #H destruct
  49 | #b #p #T1 #T2 #HT12 #b0 #U1 #H destruct /2 width=5/
  50 | #b #p #V1 #V2 #T #_ #b0 #U1 #H destruct
  51 | #b #p #V #T1 #T2 #_ #b0 #U1 #H destruct
  52 ]
  53 qed-.
  54
  55 lemma pl_st_inv_appl: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,W,U. {b0}@W.U = F →
  56                       ∨∨ (∃∃U0. ⊤ = b0 & ◊ = p & {⊤}𝛌.U0 = U & [↙W] U0 = G)
  57                        | (∃∃q,W0. sn::q = p & W Ⓡ↦[q] W0 & {⊥}@W0.{⊥}⇕U = G)
  58                        | (∃∃q,U0. dx::q = p & U Ⓡ↦[q] U0 & {b0}@W.U0 = G).
  59 #p #F #G * -p -F -G
  60 [ #V #T #b0 #W #U #H destruct /3 width=3/
  61 | #b #p #T1 #T2 #_ #b0 #W #U #H destruct
  62 | #b #p #V1 #V2 #T #HV12 #b0 #W #U #H destruct /3 width=5/
  63 | #b #p #V #T1 #T2 #HT12 #b0 #W #U #H destruct /3 width=5/
  64 ]
  65 qed-.
  66
  67 lemma pl_st_fwd_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U2. {b0}𝛌.U2 = G →
  68                       ◊ = p ∨ ∃q. rc::q = p.
  69 #p #F #G * -p -F -G
  70 [ /2 width=1/
  71 | /3 width=2/
  72 | #b #p #V1 #V2 #T #_ #b0 #U2 #H destruct
  73 | #b #p #V #T1 #T2 #_ #b0 #U2 #H destruct
  74 ]
  75 qed-.
  76
  77 lemma pl_st_inv_nil: ∀p,F,G. F Ⓡ↦[p] G → ◊ = p →
  78                      ∃∃V,T. {⊤}@V.{⊤} 𝛌.T = F & [↙V] T = G.
  79 #p #F #G * -p -F -G
  80 [ #V #T #_ destruct /2 width=4/
  81 | #b #p #T1 #T2 #_ #H destruct
  82 | #b #p #V1 #V2 #T #_ #H destruct
  83 | #b #p #V #T1 #T2 #_ #H destruct
  84 ]
  85 qed-.
  86
  87 lemma pl_st_inv_rc: ∀p,F,G. F Ⓡ↦[p] G → ∀q. rc::q = p →
  88                     ∃∃b,T1,T2. T1 Ⓡ↦[q] T2 & {b}𝛌.T1 = F & {⊥}𝛌.T2 = G.
  89 #p #F #G * -p -F -G
  90 [ #V #T #q #H destruct
  91 | #b #p #T1 #T2 #HT12 #q #H destruct /2 width=6/
  92 | #b #p #V1 #V2 #T #_ #q #H destruct
  93 | #b #p #V #T1 #T2 #_ #q #H destruct
  94 ]
  95 qed-.
  96
  97 lemma pl_st_inv_sn: ∀p,F,G. F Ⓡ↦[p] G → ∀q. sn::q = p →
  98                     ∃∃b,V1,V2,T. V1 Ⓡ↦[q] V2 & {b}@V1.T = F & {⊥}@V2.{⊥}⇕T = G.
  99 #p #F #G * -p -F -G
 100 [ #V #T #q #H destruct
 101 | #b #p #T1 #T2 #_ #q #H destruct
 102 | #b #p #V1 #V2 #T #HV12 #q #H destruct /2 width=7/
 103 | #b #p #V #T1 #T2 #_ #q #H destruct
 104 ]
 105 qed-.
 106
 107 lemma pl_st_inv_dx: ∀p,F,G. F Ⓡ↦[p] G → ∀q. dx::q = p →
 108                     ∃∃b,V,T1,T2. T1 Ⓡ↦[q] T2 & {b}@V.T1 = F & {b}@V.T2 = G.
 109 #p #F #G * -p -F -G
 110 [ #V #T #q #H destruct
 111 | #b #p #T1 #T2 #_ #q #H destruct
 112 | #b #p #V1 #V2 #T #_ #q #H destruct
 113 | #b #p #V #T1 #T2 #HT12 #q #H destruct /2 width=7/
 114 ]
 115 qed-.
 116
 117
 118
 119 (*
 120 lemma pl_st_lift: ∀p. sliftable (pl_st p).
 121 #p #h #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/
 122 [ #V #T #d <sdsubst_slift_le //
 123 | #b #p #V1 #V2 #T #_ #IHV12 #d
 124 qed.
 125
 126 lemma pl_st_inv_lift: ∀p. deliftable_sn (pl_st p).
 127 #p #h #G1 #G2 #H elim H -p -G1 -G2
 128 [ #W #U #d #F1 #H
 129   elim (lift_inv_appl … H) -H #V #F #H0 #HF #H destruct
 130   elim (lift_inv_abst … HF) -HF #T #H0 #H destruct /3 width=3/
 131 | #p #U1 #U2 #_ #IHU12 #d #F1 #H
 132   elim (lift_inv_abst … H) -H #T1 #HTU1 #H
 133   elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
 134   @(ex2_intro … (𝛌.T2)) // /2 width=1/
 135 | #p #W1 #W2 #U1 #_ #IHW12 #d #F1 #H
 136   elim (lift_inv_appl … H) -H #V1 #T #HVW1 #H1 #H2
 137   elim (IHW12 … HVW1) -W1 #V2 #HV12 #HVW2 destruct
 138   @(ex2_intro … (@V2.T)) // /2 width=1/
 139 | #p #W1 #U1 #U2 #_ #IHU12 #d #F1 #H
 140   elim (lift_inv_appl … H) -H #V #T1 #H1 #HTU1 #H2
 141   elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
 142   @(ex2_intro … (@V.T2)) // /2 width=1/
 143 ]
 144 qed-.
 145
 146 lemma pl_st_dsubst: ∀p. sdsubstable_dx (pl_st p).
 147 #p #W1 #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/
 148 #W2 #T #d >dsubst_dsubst_ge //
 149 qed.
 150 *)
 151
 152 lemma pl_st_inv_empty: ∀p,G1,G2. G1 Ⓡ↦[p] G2 → ∀F1. {⊥}⇕F1 = G1 → ⊥.
 153 #p #F1 #F2 #H elim H -p -F1 -F2
 154 [ #V #T #F1 #H
 155   elim (mk_boolean_inv_appl … H) -H #b0 #W #U #H destruct
 156 | #b #p #T1 #T2 #_ #IHT12 #F1 #H
 157   elim (mk_boolean_inv_abst … H) -H /2 width=2/
 158 | #b #p #V1 #V2 #T #_ #IHV12 #F1 #H
 159   elim (mk_boolean_inv_appl … H) -H /2 width=2/
 160 | #b #p #V #T1 #T2 #_ #IHT12 #F1 #H
 161   elim (mk_boolean_inv_appl … H) -H /2 width=2/
 162 ]
 163 qed-.
 164
 165 theorem pl_st_mono: ∀p. singlevalued … (pl_st p).
 166 #p #F #G1 #H elim H -p -F -G1
 167 [ #V #T #G2 #H elim (pl_st_inv_nil … H ?) -H //
 168   #W #U #H #HG2 destruct //
 169 | #b #p #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
 170   #b0 #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
 171 | #b #p #V1 #V2 #T #_ #IHV12 #G2 #H elim (pl_st_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
 172   #b0 #W1 #W2 #U #HW12 #H #HG2 destruct /3 width=1/
 173 | #b #p #V #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
 174   #b0 #W #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
 175 ]
 176 qed-.
 177
 178 theorem pl_st_inv_is_standard: ∀p1,F1,F. F1 Ⓡ↦[p1] F →
 179                                ∀p2,F2. F Ⓡ↦[p2] F2 → p1 ≤ p2.
 180 #p1 #F1 #F #H elim H -p1 -F1 -F //
 181 [ #b #p #T1 #T #_ #IHT1 #p2 #F2 #H elim (pl_st_inv_abst … H ???) -H [3: // |2,4: skip ] (**) (* simplify line *)
 182   #q #T2 #HT2 #H1 #H2 destruct /3 width=2/
 183 | #b #p #V1 #V #T #_ #IHV1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
 184   [ #U #H destruct
 185   | #q #V2 #H1 #HV2 #H2 destruct /3 width=2/
 186   | #q #U #_ #H elim (pl_st_inv_empty … H ??) [ // | skip ] (**) (* simplify line *)
 187   ]
 188 | #b #p #V #T1 #T #HT1 #IHT1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
 189   [ #U #_ #H1 #H2 #_ -b -V -F2 -IHT1
 190     elim (pl_st_fwd_abst … HT1 … H2) // -H1 * #q #H
 191     elim (pl_st_inv_rc … HT1 … H) -HT1 -H #b #U1 #U2 #_ #_ #H -b -q -T1 -U1 destruct
 192   | #q #V2 #H1 #_ #_ -b -F2 -T1 -T -V -V2 destruct //
 193   | #q #T2 #H1 #HT2 #H2 -b -F2 -T1 -V /3 width=2/
 194   ]
 195 ]
 196 qed-.