matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.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.ma".
  16 include "delayed_updating/substitution/fsubst_constructors.ma".
  17 include "delayed_updating/substitution/fsubst_eq.ma".
  18 include "delayed_updating/syntax/prototerm_constructors_eq.ma".
  19
  20 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
  21
  22 (* Constructions with constructors for prototerm ****************************)
  23
  24 lemma dbfr_abst_hd (t1) (t2) (r):
  25       t1 ➡𝐝𝐛𝐟[r] t2 → 𝛌.t1 ➡𝐝𝐛𝐟[𝗟◗r] 𝛌.t2.
  26 #t1 #t2 #r *
  27 #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
  28 @(ex6_5_intro … (𝗟◗p) … Hb Hm Hn) -Hb -Hm -Hn
  29 [ -Ht2 //
  30 | -Ht2 /2 width=1 by in_comp_abst_hd/
  31 | @(subset_eq_trans … (abst_eq_repl … Ht2)) -Ht1 -Ht2
  32   @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
  33   @fsubst_eq_repl // @iref_eq_repl
  34   >list_cons_shift @(subset_eq_canc_sn … (grafted_abst_hd … )) //
  35 ]
  36 qed.
  37
  38 lemma dbfr_appl_hd (v) (t1) (t2) (r):
  39       t1 ➡𝐝𝐛𝐟[r] t2 → ＠v.t1 ➡𝐝𝐛𝐟[𝗔◗r] ＠v.t2.
  40 #v #t1 #t2 #r *
  41 #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
  42 @(ex6_5_intro … (𝗔◗p) … Hb Hm Hn) -Hb -Hm -Hn
  43 [ -Ht2 //
  44 | -Ht2 /2 width=1 by in_comp_appl_hd/
  45 | @(subset_eq_trans … (appl_eq_repl … Ht2)) -Ht1 -Ht2 [|*: // ]
  46   @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
  47   @fsubst_eq_repl // @iref_eq_repl
  48   >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_hd … )) //
  49 ]
  50 qed.
  51
  52 lemma dbfr_appl_sd (v1) (v2) (t) (r):
  53       v1 ➡𝐝𝐛𝐟[r] v2 → ＠v1.t ➡𝐝𝐛𝐟[𝗦◗r] ＠v2.t.
  54 #v1 #v2 #t #r *
  55 #p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
  56 @(ex6_5_intro … (𝗦◗p) … Hb Hm Hn) -Hb -Hm -Hn
  57 [ -Hv2 //
  58 | -Hv2 /2 width=1 by in_comp_appl_sd/
  59 | @(subset_eq_trans ????? (appl_eq_repl …)) [3: @Hv2 |2,4: // |5: skip ]
  60   @(subset_eq_canc_sn … (fsubst_appl_sd …)) @appl_eq_repl [| // ]
  61   @fsubst_eq_repl // @iref_eq_repl
  62   >list_cons_shift @(subset_eq_canc_sn … (grafted_appl_sd … )) //
  63 ]
  64 qed.
  65
  66 lemma dbfr_beta_0 (v) (t) (q) (n):
  67       q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
  68       ＠v.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗟◗q] ＠v.𝛌.(t[⋔q←𝛕↑n.v]).
  69 #v #t #q #n #Hn #Ht
  70 @(ex6_5_intro … (𝐞) (𝐞) q (𝟎) … Hn) -Hn
  71 [ //
  72 | //
  73 | //
  74 | /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
  75 | @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
  76   @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
  77   @fsubst_eq_repl // <nplus_zero_sn @iref_eq_repl
  78   >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
  79   @(subset_eq_canc_sn … (grafted_empty_dx … )) //
  80 ]
  81 qed.
  82 (*
  83 lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
  84       q ϵ 𝐂❨Ⓕ,n❩ → q◖𝗱↑n ϵ t →
  85       ＠v.＠v1.𝛌.𝛌.t ➡𝐝𝐛𝐟[𝗔◗𝗔◗𝗟◗𝗟◗q] ＠v.＠v1.𝛌.𝛌.(t[⋔q←🠡[𝐮❨↑↑n❩]v]).
  86 #v #v1 #t #q #n #Hn #Ht
  87 @(ex6_5_intro … (𝐞) (𝗔◗𝗟◗𝐞) q (𝟏) … Hn) -Hn
  88 [ //
  89 | /2 width=1 by pbc_empty, pbc_redex/
  90 | /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
  91 | /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
  92 | @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
  93   @(subset_eq_canc_sn … (fsubst_appl_hd …)) @appl_eq_repl [ // ]
  94   @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
  95   @(subset_eq_canc_sn … (fsubst_abst_hd …)) @abst_eq_repl
  96   @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
  97   >list_cons_comm @(subset_eq_canc_sn … (grafted_appl_sd … ))
  98   @(subset_eq_canc_sn … (grafted_empty_dx … )) //
  99 ]
 100 qed.
 101 *)