matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.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 un_t: prototerm ≝
  26            ＠(𝛌.⧣𝟏).𝛌.𝛌.＠(⧣𝟐).𝛌.＠(⧣𝟐).⧣𝟏.
  27
  28 definition un_i1: prototerm ≝
  29            ＠(𝛌.⧣𝟏).𝛌.𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).⧣𝟏.
  30
  31 lemma un_ti1:
  32       un_t ➡𝐢𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗦◗𝐞] un_i1.
  33 @(ibfr_eq_trans … (ibfr_beta_0 …))
  34 [ >list_append_lcons_sn
  35   /3 width=1 by in_comp_appl_sd, in_comp_abst_hd/
  36 | /3 width=3 by pcc_S_sn, pcc_L_sn/
  37 | skip
  38 ]
  39 @appl_eq_repl [ // ] @abst_eq_repl
  40 @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
  41 @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
  42 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  43 @(subset_eq_canc_sn … (lift_term_abst …)) @abst_eq_repl
  44 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  45 qed.
  46
  47 definition un_i2: prototerm ≝
  48            ＠(𝛌.⧣𝟏).𝛌.𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛌.⧣𝟏.
  49
  50 lemma un_i12:
  51       un_i1 ➡𝐢𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗔◗𝗟◗𝗔◗𝐞] un_i2.
  52 @ibfr_appl_hd
  53 @ibfr_abst_hd
  54 @ibfr_abst_hd
  55 @(ibfr_eq_trans … (ibfr_beta_0 …))
  56 [ >list_append_lcons_sn
  57   /2 width=1 by in_comp_appl_hd/
  58 | /2 width=1 by pcc_A_sn, pcc_empty/
  59 | skip
  60 ]
  61 @appl_eq_repl [ // ] @abst_eq_repl
  62 @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
  63 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  64 @(subset_eq_canc_sn … (lift_term_abst …)) @abst_eq_repl
  65 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  66 qed.
  67
  68 definition un_i3: prototerm ≝
  69            ＠(𝛌.⧣𝟏).𝛌.𝛌.＠(𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛌.⧣↑𝟐.
  70
  71 lemma un_i23:
  72       un_i2 ➡𝐢𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗔◗𝗟◗𝗔◗𝗟◗𝐞] un_i3.
  73 @ibfr_appl_hd
  74 @ibfr_abst_hd
  75 @ibfr_abst_hd
  76 @ibfr_appl_hd
  77 @ibfr_abst_hd
  78 @(ibfr_eq_trans … (ibfr_beta_0 …))
  79 [ // | // | skip ]
  80 @appl_eq_repl [ // ] @abst_eq_repl
  81 @(subset_eq_canc_sn … (fsubst_empty_rc …))
  82 @(subset_eq_canc_sn … (lift_term_oref_pap … )) //
  83 qed.
  84
  85 definition un_d1: prototerm ≝
  86            ＠(𝛌.⧣𝟏).𝛌.𝛌.＠(𝛕𝟐.𝛌.⧣𝟏).𝛌.＠(⧣𝟐).⧣𝟏.
  87
  88 lemma un_td1:
  89       un_t ➡𝐝𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗦◗𝐞] un_d1.
  90 @(dbfr_eq_trans … (dbfr_beta_0 …))
  91 [ >list_append_lcons_sn
  92   /3 width=1 by in_comp_appl_sd, in_comp_abst_hd/
  93 | /3 width=3 by pcc_S_sn, pcc_L_sn/
  94 | skip
  95 ]
  96 @appl_eq_repl [ // ] @abst_eq_repl
  97 @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
  98 @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
  99 @(subset_eq_canc_sn … (fsubst_empty_rc …))
 100 @iref_eq_repl //
 101 qed.
 102
 103 definition un_d2: prototerm ≝
 104            ＠(𝛌.⧣𝟏).𝛌.𝛌.＠(𝛕𝟐.𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛕𝟏.𝛕𝟐.𝛌.⧣𝟏.
 105
 106 lemma un_d12:
 107       un_d1 ➡𝐝𝐛𝐟[𝗔◗𝗟◗𝗟◗𝗔◗𝗟◗𝗔◗𝐞] un_d2.
 108 @dbfr_appl_hd
 109 @dbfr_abst_hd
 110 @dbfr_abst_hd
 111 @(dbfr_eq_trans … (dbfr_beta_0 …))
 112 [ >list_append_lcons_sn /2 width=1 by in_comp_appl_hd/
 113 | /2 width=1 by pcc_A_sn/
 114 | skip
 115 ]
 116 @appl_eq_repl [ // ] @abst_eq_repl
 117 @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
 118 @(subset_eq_canc_sn … (fsubst_empty_rc …))
 119 @iref_eq_repl @iref_eq_repl //
 120 qed.
 121
 122 definition un_d3: prototerm ≝
 123            ＠(𝛌.⧣𝟏).𝛌.𝛌.＠(𝛕𝟐.𝛌.⧣𝟏).𝛌.＠(⧣𝟐).𝛌.𝛕𝟏.⧣𝟐.
 124
 125 lemma un_di3:
 126       un_i3 ⇔ ▼[𝐢] un_d3.
 127 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
 128 [ @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 129   @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 130 ]
 131 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 132 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 133 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
 134 [ @(subset_eq_canc_sn … (unwind2_term_iref …))
 135   @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 136   @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 137 ]
 138 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 139 @(subset_eq_canc_sn … (unwind2_term_appl …)) @appl_eq_repl
 140 [ @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 141 ]
 142 @(subset_eq_canc_sn … (unwind2_term_abst …)) @abst_eq_repl
 143 @(subset_eq_canc_sn … (unwind2_term_iref …))
 144 @(subset_eq_canc_sn … (unwind2_term_oref_pap …)) //
 145 qed.