From f31020f1ae14e28c246b6cd9cf91b5864f4f536a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 17 Nov 2022 23:08:19 +0100
Subject: [PATCH] update in delayed_updating

+ example of unprotected balanced reduction continued and simplified
---
 .../delayed_updating/reduction/dbfr.ma        |   9 ++
 .../reduction/dbfr_constructors.ma            | 101 ++++++++++++++++++
 .../reduction/dbfr_unprotected.ma             |  67 +++++++-----
 .../unwind/unwind2_prototerm_constructors.ma  |  50 ++++++---
 .../lambdadelta/ground/etc/lib/list_rcons.etc |   3 +
 5 files changed, 191 insertions(+), 39 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/etc/lib/list_rcons.etc

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
index b9b724633..7e4e6dbe3 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
@@ -34,3 +34,12 @@ definition dbfr (r): relation2 prototerm prototerm â
 interpretation
   "balanced focused reduction with delayed updating (prototerm)"
   'BlackRightArrowDBF t1 r t2 = (dbfr r t1 t2).
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma dbfr_eq_trans (t) (t1) (t2) (r):
+      t1 â¡ððð[r] t â t â t2 â t1 â¡ððð[r] t2.
+#t #t1 #t2 #r
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht #Ht2
+/3 width=13 by subset_eq_trans, ex6_5_intro/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
new file mode 100644
index 000000000..4dd861087
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_constructors.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/reduction/dbfr.ma".
+include "delayed_updating/substitution/fsubst_constructors.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors_eq.ma".
+
+(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma dbfr_abst_hd (t1) (t2) (r):
+      t1 â¡ððð[r] t2 â ð.t1 â¡ððð[ðâr] ð.t2.
+#t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro â¦ (ðâp) â¦ Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_abst_hd/
+| @(subset_eq_trans â¦ (abst_eq_repl â¦ Ht2)) -Ht1 -Ht2
+  @(subset_eq_canc_sn â¦ (fsubst_abst_hd â¦)) @abst_eq_repl
+  @fsubst_eq_repl // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn â¦ (grafted_abst_hd â¦ )) //
+]
+qed.
+
+lemma dbfr_appl_hd (v) (t1) (t2) (r):
+      t1 â¡ððð[r] t2 â ï¼ v.t1 â¡ððð[ðâr] ï¼ v.t2.
+#v #t1 #t2 #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro â¦ (ðâp) â¦ Hb Hm Hn) -Hb -Hm -Hn
+[ -Ht2 //
+| -Ht2 /2 width=1 by in_comp_appl_hd/
+| @(subset_eq_trans â¦ (appl_eq_repl â¦ Ht2)) -Ht1 -Ht2 [|*: // ]
+  @(subset_eq_canc_sn â¦ (fsubst_appl_hd â¦)) @appl_eq_repl [ // ]
+  @fsubst_eq_repl // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn â¦ (grafted_appl_hd â¦ )) //
+]
+qed.
+
+lemma dbfr_appl_sd (v1) (v2) (t) (r):
+      v1 â¡ððð[r] v2 â ï¼ v1.t â¡ððð[ð¦âr] ï¼ v2.t.
+#v1 #v2 #t #r *
+#p #b #q #m #n #Hr #Hb #Hm #Hn #Hv1 #Hv2 destruct
+@(ex6_5_intro â¦ (ð¦âp) â¦ Hb Hm Hn) -Hb -Hm -Hn
+[ -Hv2 //
+| -Hv2 /2 width=1 by in_comp_appl_sd/
+| @(subset_eq_trans ????? (appl_eq_repl â¦)) [3: @Hv2 |2,4: // |5: skip ]
+  @(subset_eq_canc_sn â¦ (fsubst_appl_sd â¦)) @appl_eq_repl [| // ]
+  @fsubst_eq_repl // @iref_eq_repl
+  >list_cons_shift @(subset_eq_canc_sn â¦ (grafted_appl_sd â¦ )) //
+]
+qed.
+
+lemma dbfr_beta_0 (v) (t) (q) (n):
+      q Ïµ ðâ¨â»,nâ© â qâð±ân Ïµ t â
+      ï¼ v.ð.t â¡ððð[ðâðâq] ï¼ v.ð.(t[âqâðân.v]).
+#v #t #q #n #Hn #Ht
+@(ex6_5_intro â¦ (ð) (ð) q (ð) â¦ Hn) -Hn
+[ //
+| //
+| //
+| /3 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn â¦ (fsubst_appl_hd â¦)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn â¦ (fsubst_abst_hd â¦)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_zero_sn @iref_eq_repl
+  >list_cons_comm @(subset_eq_canc_sn â¦ (grafted_appl_sd â¦ ))
+  @(subset_eq_canc_sn â¦ (grafted_empty_dx â¦ )) //
+]
+qed.
+(*
+lemma dbfr_beta_1 (v) (v1) (t) (q) (n):
+      q Ïµ ðâ¨â»,nâ© â qâð±ân Ïµ t â
+      ï¼ v.ï¼ v1.ð.ð.t â¡ððð[ðâðâðâðâq] ï¼ v.ï¼ v1.ð.ð.(t[âqâð ¡[ð®â¨âânâ©]v]).
+#v #v1 #t #q #n #Hn #Ht
+@(ex6_5_intro â¦ (ð) (ðâðâð) q (ð) â¦ Hn) -Hn
+[ //
+| /2 width=1 by pbc_empty, pbc_redex/
+| /3 width=1 by pcc_A_sn, pcc_L_sn, pcc_empty/
+| /5 width=1 by in_comp_appl_hd, in_comp_abst_hd/
+| @(subset_eq_canc_sn â¦ (fsubst_appl_hd â¦)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn â¦ (fsubst_appl_hd â¦)) @appl_eq_repl [ // ]
+  @(subset_eq_canc_sn â¦ (fsubst_abst_hd â¦)) @abst_eq_repl
+  @(subset_eq_canc_sn â¦ (fsubst_abst_hd â¦)) @abst_eq_repl
+  @fsubst_eq_repl // <nplus_unit_sn @lift_term_eq_repl_dx
+  >list_cons_comm @(subset_eq_canc_sn â¦ (grafted_appl_sd â¦ ))
+  @(subset_eq_canc_sn â¦ (grafted_empty_dx â¦ )) //
+]
+qed.
+*)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma
index 7c9276021..753d38c68 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected.ma
@@ -12,32 +12,33 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/reduction/dbfr_constructors.ma".
 include "delayed_updating/reduction/ibfr_constructors.ma".
+include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
 include "delayed_updating/substitution/lift_prototerm_constructors.ma".
 include "ground/arith/pnat_two.ma".
 
 (* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
 
-(* Prerequisites ************************************************************)
+(* Example of unprotected balanced Î²-reduction ******************************)
 
-lemma list_rcons_prop_1 (A) (a1) (a2):
-      â â¨­ a1 â¨­{A} a2 = a1 â¨® (â â¨­ a2).
-// qed.
+definition l3_t: prototerm â
+           (ï¼ (â§£ð).ï¼ (ð.â§£ð).ð.â§£ð).
 
-(* Example of unprotected balanced Î²-reduction ******************************)
+definition l3_i1: prototerm â
+           (ï¼ (â§£ð).ï¼ (ð.â§£ð).ð.ð.â§£ð).
 
-definition l3_t0: prototerm â
-           (ð.ï¼ (â§£ð).ï¼ (ð.ï¼ (â§£ð).â§£ð).ð.â§£ð).
+definition l3_i2: prototerm â
+           (ï¼ (â§£ð).ï¼ (ð.â§£ð).ð.ð.â§£âð).
 
-definition l3_t1: prototerm â
-           (ð.ï¼ (â§£ð).ï¼ (ð.ï¼ (â§£ð).â§£ð).ð.(ð.ï¼ (â§£âð).â§£ð)).
+definition l3_d1: prototerm â
+           (ï¼ (â§£ð).ï¼ (ð.â§£ð).ð.ðð.ð.â§£ð).
 
-definition l3_t2: prototerm â
-           (ð.ï¼ (â§£ð).ï¼ (ð.ï¼ (â§£ð).â§£ð).ð.(ð.ï¼ (â§£âð).â§£âð)).
+definition l3_d2: prototerm â
+           (ï¼ (â§£ð).ï¼ (ð.â§£ð).ð.ðð.ð.ðð.â§£ð).
 
-lemma l3_t01:
-      l3_t0 â¡ð¢ðð[ðâðâðâðâð] l3_t1.
-@ibfr_abst_hd
+lemma l3_ti1:
+      l3_t â¡ð¢ðð[ðâðâðâð] l3_i1.
 @ibfr_appl_hd
 @ibfr_eq_trans [| @ibfr_beta_0 // ]
 @appl_eq_repl [ // ]
@@ -45,24 +46,40 @@ lemma l3_t01:
 @(subset_eq_canc_sn â¦ (fsubst_empty_rc â¦))
 @(subset_eq_canc_sn â¦ (lift_term_abst â¦))
 @abst_eq_repl
-@(subset_eq_canc_sn â¦ (lift_term_appl â¦ ))
-@appl_eq_repl
 @(subset_eq_canc_sn â¦ (lift_term_oref_pap â¦ )) //
 qed.
 
-lemma l3_t12:
-      l3_t1 â¡ð¢ðð[ðâðâðâðâðâðâð] l3_t2.
-@ibfr_abst_hd
-@ibfr_eq_trans
-[| @(ibfr_beta_1 â¦ (ð)) [| <list_rcons_prop_1 ]
-   /2 width=3 by pcc_A_sn, in_comp_appl_hd/
-]
+lemma l3_i12:
+      l3_i1 â¡ð¢ðð[ðâðâðâðâð] l3_i2.
+@ibfr_eq_trans [| @ibfr_beta_1 // ]
 @appl_eq_repl [ // ]
 @appl_eq_repl [ // ]
 @abst_eq_repl
 @abst_eq_repl
-@(subset_eq_canc_sn â¦ (fsubst_appl_hd â¦))
-@appl_eq_repl [ // ]
 @(subset_eq_canc_sn â¦ (fsubst_empty_rc â¦))
 @(subset_eq_canc_sn â¦ (lift_term_oref_pap â¦ )) //
 qed.
+
+lemma l3_td1:
+      l3_t â¡ððð[ðâðâðâð] l3_d1.
+@dbfr_appl_hd
+@dbfr_eq_trans [| @dbfr_beta_0 // ]
+@appl_eq_repl [ // ]
+@abst_eq_repl
+@(subset_eq_canc_sn â¦ (fsubst_empty_rc â¦)) //
+qed.
+
+lemma ld_di2:
+      l3_i2 â â¼[ð¢]l3_d2.
+@(subset_eq_canc_sn â¦ (unwind2_term_appl â¦)) @appl_eq_repl
+[ @(subset_eq_canc_sn â¦ (unwind2_term_oref_pap â¦)) // ]
+@(subset_eq_canc_sn â¦ (unwind2_term_appl â¦)) @appl_eq_repl
+[ @(subset_eq_canc_sn â¦ (unwind2_term_abst â¦)) @abst_eq_repl
+  @(subset_eq_canc_sn â¦ (unwind2_term_oref_pap â¦)) //
+]
+@(subset_eq_canc_sn â¦ (unwind2_term_abst â¦)) @abst_eq_repl
+@(subset_eq_canc_sn â¦ (unwind2_term_iref â¦))
+@(subset_eq_canc_sn â¦ (unwind2_term_abst â¦)) @abst_eq_repl
+@(subset_eq_canc_sn â¦ (unwind2_term_iref â¦))
+@(subset_eq_canc_sn â¦ (unwind2_term_oref_pap â¦)) //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
index 96fc1d02e..6e3c96fe7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
@@ -20,21 +20,43 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 
 (* Constructions with constructors for prototerm ****************************)
 
-lemma unwind2_term_iref_sn (f) (t) (k:pnat):
-      â¼[fâð®â¨kâ©]t â â¼[f](ðk.t).
-#f #t #k #p * #q #Hq #H0 destruct
-@(ex2_intro â¦ (ð±kâðºâq))
-/2 width=1 by in_comp_iref_hd/
-qed-.
-
-lemma unwind2_term_iref_dx (f) (t) (k:pnat):
-      â¼[f](ðk.t) â â¼[fâð®â¨kâ©]t.
-#f #t #k #p * #q #Hq #H0 destruct
-elim (in_comp_inv_iref â¦ Hq) -Hq #p #Hp #Ht destruct
-/2 width=1 by in_comp_unwind2_path_term/
-qed-.
+lemma unwind2_term_oref_pap (f) (k):
+      (â§£(fï¼ â§£â¨kâ©)) â â¼[f]â§£k.
+#f #k @conj #p *
+[ /2 width=1 by in_comp_unwind2_path_term/
+| #q * #H0 destruct //
+]
+qed.
 
 lemma unwind2_term_iref (f) (t) (k:pnat):
       â¼[fâð®â¨kâ©]t â â¼[f](ðk.t).
-/3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
+#f #t #k @conj
+#p * #q #Hq #H0 destruct
+[ @(ex2_intro â¦ (ð±kâðºâq))
+  /2 width=1 by in_comp_iref_hd/
+| elim (in_comp_inv_iref â¦ Hq) -Hq #p #Hp #Ht destruct
+  /2 width=1 by in_comp_unwind2_path_term/
+]
+qed.
+
+lemma unwind2_term_abst (f) (t):
+      (ð.â¼[â«¯f]t) â â¼[f]ð.t.
+#f #t @conj #p #Hp
+[ elim (in_comp_inv_abst â¦ Hp) -Hp #q #H1 * #r #Hr #H2 destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+  elim (in_comp_inv_abst â¦ Hq) -Hq #r #H0 #Hr destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
+]
+qed.
+
+lemma unwind2_term_appl (f) (v) (t):
+      ï¼ â¼[f]v.â¼[f]t â â¼[f]ï¼ v.t.
+#f #v #t @conj #p #Hp
+[ elim (in_comp_inv_appl â¦ Hp) -Hp * #q #H1 * #r #Hr #H2 destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+  elim (in_comp_inv_appl â¦ Hq) -Hq * #r #H0 #Hr destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
+]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/etc/lib/list_rcons.etc b/matita/matita/contribs/lambdadelta/ground/etc/lib/list_rcons.etc
new file mode 100644
index 000000000..1583e9a0c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/etc/lib/list_rcons.etc
@@ -0,0 +1,3 @@
+lemma list_rcons_prop_1 (A) (a1) (a2):
+      â â¨­ a1 â¨­{A} a2 = a1 â¨® (â â¨­ a2).
+// qed.
-- 
2.39.2