From b0c6bbd5db69489a5ebd1b36de6685fa6de441b3 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 8 Sep 2022 00:13:21 +0200
Subject: [PATCH] update in ground and delayed_updating
+ example of unprotected balanced segment
+ balanced reduction parked for now
+ additions and renaming
---
.../dbfr.ma => etc/balanced/dbfr.etc} | 10 ++---
.../balanced/dbfr_ibfr.etc} | 37 ++++++++--------
.../balanced/dbfr_lift.etc} | 0
.../ibfr.ma => etc/balanced/ibfr.etc} | 10 ++---
.../delayed_updating/reduction/dfr_ifr.ma | 6 +--
.../delayed_updating/reduction/ifr_unwind.ma | 6 +--
.../unwind/unwind2_rmap_closed.ma | 18 ++++++--
.../unwind/unwind2_rmap_unprotected.ma | 43 +++++++++++++++++++
.../ground/relocation/tr_uni_compose.ma | 7 +++
.../lambdadelta/ground/relocation/xap.ma | 5 +++
10 files changed, 102 insertions(+), 40 deletions(-)
rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/dbfr.ma => etc/balanced/dbfr.etc} (83%)
rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/dbfr_ibfr.ma => etc/balanced/dbfr_ibfr.etc} (76%)
rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/dbfr_lift.ma => etc/balanced/dbfr_lift.etc} (100%)
rename matita/matita/contribs/lambdadelta/delayed_updating/{reduction/ibfr.ma => etc/balanced/ibfr.etc} (83%)
create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc
similarity index 83%
rename from matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc
index 349195cb0..f82db8a73 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr.etc
@@ -15,7 +15,7 @@
include "delayed_updating/substitution/fsubst.ma".
include "delayed_updating/syntax/prototerm_constructors.ma".
include "delayed_updating/syntax/prototerm_eq.ma".
-include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_closed.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/notation/relations/black_rightarrow_dbf_3.ma".
@@ -24,13 +24,11 @@ include "ground/xoa/ex_6_5.ma".
(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
-(**) (* explicit ninj because we cannot declare the expectd type of k *)
definition dbfr (r): relation2 prototerm prototerm â
λt1,t2.
- ââp,b,q,h,k. pâðâbâðâq = r &
- âb ϵ ð & b = â³[h]b &
- (ðâq) = â³[ninj k](ðâq) & râð±k ϵ t1 &
- t1[ârâð(k+h).(t1â(pâð¦))] â t2
+ ââp,b,q,m,n. pâðâbâðâq = r &
+ âb ϵ ð & b ϵ ðâ¨mâ© & q ϵ ðâ¨nâ© & râð±ân ϵ t1 &
+ t1[ârâðâ(m+n).(t1â(pâð¦))] â t2
.
interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc
similarity index 76%
rename from matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc
index 043f61085..d7c16ca2b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_ibfr.etc
@@ -19,13 +19,13 @@ include "delayed_updating/unwind/unwind2_constructors.ma".
include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
include "delayed_updating/unwind/unwind2_preterm_eq.ma".
include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_head.ma".
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".
include "delayed_updating/substitution/fsubst_eq.ma".
include "delayed_updating/substitution/lift_prototerm_eq.ma".
include "delayed_updating/syntax/prototerm_proper_constructors.ma".
-include "delayed_updating/syntax/path_head_structure.ma".
+include "delayed_updating/syntax/path_closed_structure.ma".
include "delayed_updating/syntax/path_structure_depth.ma".
(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
@@ -35,22 +35,21 @@ include "delayed_updating/syntax/path_structure_depth.ma".
theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ ð â
t1 â¡ððð[r] t2 â â¼[f]t1 â¡ð¢ðð[âr] â¼[f]t2.
#f #t1 #t2 #r #H0t1
-* #p #b #q #h #k #Hr #Hb #Hh #H1k #Ht1 #Ht2 destruct
-@(ex6_5_intro ⦠(âp) (âb) (âq) (âb) (ââq))
-[ -H0t1 -Hb -Hh -H1k -Ht1 -Ht2 //
-| -H0t1 -Hh -H1k -Ht1 -Ht2 //
-| -H0t1 -Hb -Ht1 -H1k -Ht2
- >Hh in ⢠(??%?); >path_head_structure_depth <Hh -Hh //
-| -H0t1 -Hb -Hh -Ht1 -Ht2
- >structure_L_sn
- >H1k in ⢠(??%?); >path_head_structure_depth <H1k -H1k //
-| lapply (in_comp_unwind2_path_term f ⦠Ht1) -Ht2 -Ht1 -H0t1 -Hb -Hh
- <unwind2_path_d_dx >list_append_rcons_dx >list_append_assoc
- lapply (unwind2_rmap_append_pap_closed f ⦠(pâðâb) ⦠H1k) -H1k
- <depth_L_sn #H2k
- lapply (eq_inv_ninj_bi ⦠H2k) -H2k #H2k <H2k -H2k #Ht1 //
+* #p #b #q #m #n #Hr #Hb #Hm #Hn #Ht1 #Ht2 destruct
+@(ex6_5_intro ⦠(âp) (âb) (âq) (âb) (âq))
+[ -H0t1 -Hb -Hm -Hn -Ht1 -Ht2 //
+| -H0t1 -Hm -Hn -Ht1 -Ht2 //
+| -H0t1 -Hb -Hn -Ht1 -Ht2
+ /2 width=2 by path_closed_structure_depth/
+| -H0t1 -Hb -Hm -Ht1 -Ht2
+ /2 width=2 by path_closed_structure_depth/
+| lapply (in_comp_unwind2_path_term f ⦠Ht1) -H0t1 -Hb -Hm -Ht2 -Ht1
+ <unwind2_path_d_dx <tr_pap_succ_nap >list_append_rcons_dx >list_append_assoc
+ <unwind2_rmap_append_closed_nap //
| lapply (unwind2_term_eq_repl_dx f ⦠Ht2) -Ht2 #Ht2
+(*
lapply (path_head_refl_append_bi ⦠Hh H1k) -Hh -H1k <nrplus_inj_sn #H1k
+*)
@(subset_eq_trans ⦠Ht2) -t2
@(subset_eq_trans ⦠(unwind2_term_fsubst_ppc â¦))
[ @fsubst_eq_repl [ // | // ]
@@ -61,14 +60,16 @@ theorem dbfr_des_ibfr (f) (t1) (t2) (r): t1 ϵ ð â
@unwind2_term_eq_repl_sn
(* Note: crux of the proof begins *)
<list_append_rcons_sn
- @(stream_eq_trans ⦠(tr_compose_uni_dx â¦))
+ @(stream_eq_trans ⦠(tr_compose_uni_dx_pap â¦)) <tr_pap_succ_nap
@tr_compose_eq_repl
- [ <unwind2_rmap_append_pap_closed //
+(* TODO
+ [ <unwind2_rmap_append_closed_nap //
<depth_append <depth_L_sn
<nplus_comm <nrplus_npsucc_sn <nplus_succ_sn //
| >unwind2_rmap_A_dx
/2 width=1 by tls_unwind2_rmap_closed/
]
+*)
(* Note: crux of the proof ends *)
| //
| /2 width=2 by ex_intro/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/dbfr_lift.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc
similarity index 83%
rename from matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc
index b235cb481..dfa14ef98 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/balanced/ibfr.etc
@@ -15,7 +15,7 @@
include "delayed_updating/substitution/fsubst.ma".
include "delayed_updating/substitution/lift_prototerm.ma".
include "delayed_updating/syntax/prototerm_eq.ma".
-include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_closed.ma".
include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/notation/relations/black_rightarrow_ibf_3.ma".
@@ -25,13 +25,11 @@ include "ground/xoa/ex_6_5.ma".
(* IMMEDIATE BALANCED FOCUSED REDUCTION *************************************)
-(**) (* explicit ninj because we cannot declare the expectd type of k *)
definition ibfr (r): relation2 prototerm prototerm â
λt1,t2.
- ââp,b,q,h,k. pâðâbâðâq = r &
- âb ϵ ð & b = â³[h]b &
- (ðâq) = â³[ninj k](ðâq) & râð±k ϵ t1 &
- t1[ârââ[ð®â¨k+hâ©](t1â(pâð¦))] â t2
+ ââp,b,q,m,n. pâðâbâðâq = r &
+ âb ϵ ð & b ϵ ðâ¨mâ© & q ϵ ðâ¨nâ© & râð±ân ϵ t1 &
+ t1[ârââ[ð®â¨â(m+n)â©](t1â(pâð¦))] â t2
.
interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index 5f37abd5f..d64067123 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -42,7 +42,7 @@ theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ϵ ð â
/2 width=2 by path_closed_structure_depth/
| lapply (in_comp_unwind2_path_term f ⦠Ht1) -Ht2 -Ht1 -H0t1
<unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
- <unwind2_rmap_append_closed_nap //
+ <unwind2_rmap_append_closed_Lq_dx_nap_depth //
| lapply (unwind2_term_eq_repl_dx f ⦠Ht2) -Ht2 #Ht2
@(subset_eq_trans ⦠Ht2) -t2
@(subset_eq_trans ⦠(unwind2_term_fsubst_ppc â¦))
@@ -56,8 +56,8 @@ theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ϵ ð â
<list_append_rcons_sn
@(stream_eq_trans ⦠(tr_compose_uni_dx_pap â¦)) <tr_pap_succ_nap
@tr_compose_eq_repl
- [ <unwind2_rmap_append_closed_nap //
- | /2 width=1 by tls_succ_unwind2_rmap_append_L_closed_dx/
+ [ <unwind2_rmap_append_closed_Lq_dx_nap_depth //
+ | /2 width=1 by tls_succ_unwind2_rmap_append_closed_Lq_dx/
]
(* Note: crux of the proof ends *)
| //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
index 077ff798e..d3b567b72 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
@@ -40,7 +40,7 @@ lemma ifr_unwind_bi (f) (t1) (t2) (r):
/2 width=2 by path_closed_structure_depth/
| lapply (in_comp_unwind2_path_term f ⦠Ht1) -Ht2 -Ht1 -H1t1 -H2r
<unwind2_path_d_dx <tr_pap_succ_nap <list_append_rcons_sn
- <unwind2_rmap_append_closed_nap //
+ <unwind2_rmap_append_closed_Lq_dx_nap_depth //
| lapply (unwind2_term_eq_repl_dx f ⦠Ht2) -Ht2 #Ht2
@(subset_eq_trans ⦠Ht2) -t2
@(subset_eq_trans ⦠(unwind2_term_fsubst_pic â¦))
@@ -54,8 +54,8 @@ lemma ifr_unwind_bi (f) (t1) (t2) (r):
<list_append_rcons_sn
@(stream_eq_trans ⦠(tr_compose_uni_dx_pap â¦)) <tr_pap_succ_nap
@tr_compose_eq_repl
- [ <unwind2_rmap_append_closed_nap //
- | /2 width=1 by tls_succ_unwind2_rmap_append_L_closed_dx/
+ [ <unwind2_rmap_append_closed_Lq_dx_nap_depth //
+ | /2 width=1 by tls_succ_unwind2_rmap_append_closed_Lq_dx/
]
(* Note: crux of the proof ends *)
| //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
index 7c551ed85..9879b54fb 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
@@ -48,7 +48,7 @@ lemma unwind2_rmap_append_closed_dx_xap_le (f) (p) (q) (n):
]
qed-.
-lemma unwind2_rmap_append_L_closed_dx_nap (f) (p) (q) (n):
+lemma unwind2_rmap_append_closed_Lq_dx_nap (f) (p) (q) (n):
q ϵ ðâ¨nâ© â
â¶[f](ðâq)ï¼ Â§â¨nâ© = â¶[f](pâðâq)ï¼ Â§â¨nâ©.
#f #p #q #n #Hq
@@ -66,11 +66,11 @@ lemma unwind2_rmap_push_closed_nap (f) (q) (n):
<unwind2_rmap_d_dx <tr_compose_nap //
qed-.
-lemma unwind2_rmap_append_closed_nap (f) (p) (q) (n):
+lemma unwind2_rmap_append_closed_Lq_dx_nap_depth (f) (p) (q) (n):
q ϵ ðâ¨nâ© â
âq = â¶[f](pâðâq)ï¼ Â§â¨nâ©.
#f #p #q #n #Hq
-<unwind2_rmap_append_L_closed_dx_nap //
+<unwind2_rmap_append_closed_Lq_dx_nap //
/2 width=1 by unwind2_rmap_push_closed_nap/
qed-.
@@ -85,8 +85,18 @@ lemma tls_succ_plus_unwind2_rmap_push_closed (f) (q) (n):
]
qed-.
-lemma tls_succ_unwind2_rmap_append_L_closed_dx (f) (p) (q) (n):
+lemma tls_succ_unwind2_rmap_append_closed_Lq_dx (f) (p) (q) (n):
q ϵ ðâ¨nâ© â
â¶[f]p â â*[ân]â¶[f](pâðâq).
/2 width=1 by tls_succ_plus_unwind2_rmap_push_closed/
qed-.
+
+lemma unwind2_rmap_append_closed_Lq_dx_nap_plus (f) (p) (q) (m) (n):
+ q ϵ ðâ¨nâ© â
+ â¶[f]pï¼ â¨mâ©+âq = â¶[f](pâðâq)ï¼ Â§â¨m+nâ©.
+#f #p #q #m #n #Hq
+<tr_nap_plus @eq_f2
+[ <(tr_xap_eq_repl ⦠(tls_succ_unwind2_rmap_append_closed_Lq_dx â¦)) //
+| /2 width=1 by unwind2_rmap_append_closed_Lq_dx_nap_depth/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
new file mode 100644
index 000000000..1f2a9d530
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_unprotected.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* ___ *)
+(* ||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/unwind/unwind2_rmap_closed.ma".
+include "delayed_updating/syntax/path_balanced.ma".
+include "delayed_updating/syntax/path_structure.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Example of unprotected balanced path *************************************)
+
+definition b: path â ðâðâðâð±ð.
+
+lemma b_unfold: ðâðâðâð±ð = b.
+// qed.
+
+lemma b_balanced: âb ϵ ð.
+<b_unfold <structure_d_dx
+/2 width=1 by pbc_empty, pbc_redex/
+qed.
+
+lemma b_closed: b ϵ ðâ¨ðâ©.
+/4 width=1 by pcc_A_sn, pcc_empty, pcc_d_dx, pcc_L_dx/
+qed.
+
+lemma b_unwind2_rmap_unfold (f):
+ (⫯f)âð®â¨ðâ© = â¶[f]b.
+// qed.
+
+lemma b_unwind2_rmap_pap_unit (f):
+ â(fï¼ â§£â¨ðâ©) = â¶[f]bï¼ â§£â¨ðâ©.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
index 2343c74ac..abae78a7e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
@@ -19,6 +19,13 @@ include "ground/lib/stream_hdtl_eq.ma".
(* UNIFORM ELEMENTS FOR TOTAL RELOCATION MAPS *******************************)
+(* Constructions with tr_compose and tr_next ********************************)
+
+lemma tr_compose_uni_unit_sn (f):
+ âf â ð®â¨ðâ©âf.
+#f >nsucc_zero <tr_uni_succ //
+qed.
+
(* Constructions with tr_compose and tr_tl **********************************)
lemma tr_tl_compose_uni_sn (n) (f):
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index aef0c26e1..0f367b218 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -77,3 +77,8 @@ theorem tr_xap_eq_repl (i):
<tr_xap_unfold <tr_xap_unfold
/3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
qed.
+
+lemma tr_nap_plus (f) (m) (n):
+ â*[ân]fï¼ â¨mâ©+fï¼ Â§â¨nâ© = fï¼ Â§â¨m+nâ©.
+/2 width=1 by eq_inv_nsucc_bi/
+qed.
--
2.39.2