matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_zero.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 "delayed_updating/reduction/dbfr_constructors.ma".
  16 include "delayed_updating/reduction/ibfr_constructors.ma".
  17 include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
  18 include "delayed_updating/substitution/lift_prototerm_constructors.ma".
  19 include "ground/arith/pnat_two.ma".
  20
  21 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
  22
  23 (* Example of unprotected balanced β-reduction ******************************)
  24
  25 definition l3_t: prototerm ≝
  26            (𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).⧣𝟏).
  27
  28 definition l3_i1: prototerm ≝
  29            (𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛌.⧣𝟏).
  30
  31 definition l3_i2: prototerm ≝
  32            (𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛌.⧣↑𝟐).
  33
  34 definition l3_i2': prototerm ≝
  35            (𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛌.⧣↑↑𝟐).
  36
  37 definition l3_d1: prototerm ≝
  38            (𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛕𝟏.(𝛌.⧣𝟏)).
  39
  40 definition l3_d2: prototerm ≝
  41            (𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛕𝟏.𝛌.(⧣𝟐)).
  42
  43 definition l3_d2': prototerm ≝
  44            (𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛕𝟏.𝛌.𝛕𝟏.(⧣𝟐)).
  45
  46 lemma l3_ti1:
  47       l3_t ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗟◗𝗔◗𝐞] l3_i1.
  48 @ibfr_abst_hd
  49 @ibfr_eq_trans
  50 [ | @(ibfr_beta_0 … (𝟎))
  51   [ /2 width=1 by pcc_A_sn, pcc_empty/
  52   | >list_append_lcons_sn /2 width=1 by in_comp_appl_hd/
  53   ]
  54 ]
  55 @appl_eq_repl [ // ]
  56 @abst_eq_repl
  57 @(subset_eq_canc_sn … (fsubst_appl_hd …))
  58 @appl_eq_repl [ // ]
  59 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  60 @(subset_eq_canc_sn … (lift_term_abst …))
  61 @abst_eq_repl
  62 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  63 qed.
  64
  65 lemma l3_i12:
  66       l3_i1 ➡𝐢𝐛𝐟[𝗟◗𝗔◗𝗟◗𝗔◗𝗟◗𝐞] l3_i2.
  67 @ibfr_abst_hd
  68 @ibfr_appl_hd
  69 @ibfr_abst_hd
  70 @ibfr_eq_trans [| @ibfr_beta_0 // ]
  71 @appl_eq_repl [ // ]
  72 @abst_eq_repl
  73 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  74 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  75 qed.
  76
  77 lemma l3_td1:
  78       l3_t ➡𝐝𝐛𝐟[𝗟◗𝗔◗𝗟◗𝗔◗𝐞] l3_d1.
  79 @dbfr_abst_hd
  80 @dbfr_eq_trans
  81 [ | @(dbfr_beta_0 … (𝟎))
  82   [ /2 width=1 by pcc_A_sn, pcc_empty/
  83   | >list_append_lcons_sn /2 width=1 by in_comp_appl_hd/
  84   ]
  85 ]
  86 @appl_eq_repl [ // ]
  87 @abst_eq_repl
  88 @(subset_eq_canc_sn … (fsubst_appl_hd …))
  89 @appl_eq_repl [ // ]
  90 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  91 @iref_eq_repl //
  92 qed.
  93
  94 lemma l3_di2:
  95       l3_i2 ⇔ ▼[𝐢]l3_d2.
  96 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
  97 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
  98 [ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
  99   @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 100 ]
 101 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 102 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
 103 [ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 104 ]
 105 @(subset_eq_canc_sn … (unwind2_term_iref …))
 106 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 107 @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 108 qed.
 109
 110 lemma l3_di2':
 111       l3_i2' ⇔ ▼[𝐢]l3_d2'.
 112 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 113 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
 114 [ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 115   @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 116 ]
 117 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 118 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
 119 [ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 120 ]
 121 @(subset_eq_canc_sn … (unwind2_term_iref …))
 122 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 123 @(subset_eq_canc_sn … (unwind2_term_iref …))
 124 @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 125 qed.