From 74223db3fc45caccb3cfac80971b29cb0613da28 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 24 Jun 2022 23:48:36 +0200 Subject: [PATCH] update in delayed_updating + ifr_lift proved + ifr corrected + minor corrections --- .../delayed_updating/reduction/dfr_ifr.ma | 6 ++-- .../delayed_updating/reduction/dfr_lift.ma | 1 - .../delayed_updating/reduction/ifr.ma | 5 ++-- .../delayed_updating/reduction/ifr_lift.ma | 17 +++++------ .../delayed_updating/reduction/ifr_unwind.ma | 17 ++++++----- .../unwind/unwind2_path_inner.ma | 28 ------------------- .../unwind/unwind2_path_structure.ma | 10 +++++++ .../unwind/unwind2_prototerm_inner.ma | 2 +- 8 files changed, 35 insertions(+), 51 deletions(-) delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma 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 fd5f76b54..92bd90699 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma @@ -18,9 +18,11 @@ include "delayed_updating/reduction/ifr.ma". 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/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". @@ -51,9 +53,9 @@ theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 → @(subset_eq_trans … (unwind2_term_fsubst …)) [ @fsubst_eq_repl [ // | // ] @(subset_eq_trans … (unwind2_term_iref …)) - @(subset_eq_canc_sn … (unwind2_term_eq_repl_dx …)) + @(subset_eq_canc_sn … (lift_term_eq_repl_dx …)) [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1 - @(subset_eq_trans … (unwind2_term_after …)) + @(subset_eq_trans … (lift_unwind2_term_after …)) @unwind2_term_eq_repl_sn (* Note: crux of the proof begins *) @nstream_eq_inv_ext #m diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma index f71d6974e..7273cd780 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma @@ -17,7 +17,6 @@ include "delayed_updating/reduction/dfr.ma". include "delayed_updating/substitution/fsubst_lift.ma". include "delayed_updating/substitution/fsubst_eq.ma". include "delayed_updating/substitution/lift_constructors.ma". -include "delayed_updating/substitution/lift_prototerm_eq.ma". include "delayed_updating/substitution/lift_path_head.ma". include "delayed_updating/substitution/lift_rmap_head.ma". diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma index fcc12edbf..8be4493b7 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma @@ -12,10 +12,11 @@ (* *) (**************************************************************************) -include "delayed_updating/unwind/unwind2_prototerm.ma". 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_reverse.ma". include "delayed_updating/notation/relations/black_rightarrow_if_4.ma". (* IMMEDIATE FOCUSED REDUCTION ************************************************) @@ -24,7 +25,7 @@ definition ifr (p) (q): relation2 prototerm prototerm ≝ λt1,t2. ∃n:pnat. let r ≝ p●𝗔◗𝗟◗q in ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 & - t1[⋔r←▼[𝐮❨n❩](t1⋔(p◖𝗦))] ⇔ t2 + t1[⋔r←↑[𝐮❨n❩](t1⋔(p◖𝗦))] ⇔ t2 . interpretation diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma index 6d5cb47f0..6eb354905 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma @@ -14,14 +14,14 @@ include "delayed_updating/reduction/ifr.ma". -include "delayed_updating/unwind/unwind2_path_lift.ma". - include "delayed_updating/substitution/fsubst_lift.ma". include "delayed_updating/substitution/fsubst_eq.ma". -include "delayed_updating/substitution/lift_prototerm_eq.ma". include "delayed_updating/substitution/lift_path_head.ma". include "delayed_updating/substitution/lift_rmap_head.ma". +include "ground/relocation/tr_uni_compose.ma". +include "ground/relocation/tr_compose_eq.ma". + (* IMMEDIATE FOCUSED REDUCTION **********************************************) (* Constructions with lift **************************************************) @@ -41,15 +41,16 @@ theorem ifr_lift_bi (f) (p) (q) (t1) (t2): @(subset_eq_trans … Ht2) -t2 @(subset_eq_trans … (lift_term_fsubst …)) @fsubst_eq_repl [ // | list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx /2 width=1 by tls_lift_rmap_append_closed/ (* Note: crux of the proof ends *) ] qed. -*) \ No newline at end of file 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 f05d86db3..13f6f3fa0 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma @@ -14,15 +14,15 @@ include "delayed_updating/reduction/ifr.ma". -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_inner.ma". +include "delayed_updating/unwind/unwind2_prototerm_lift.ma". include "delayed_updating/unwind/unwind2_rmap_head.ma". include "delayed_updating/substitution/fsubst_eq.ma". +include "delayed_updating/substitution/lift_prototerm_proper.ma". +include "delayed_updating/substitution/lift_prototerm_eq.ma". -include "delayed_updating/syntax/prototerm_proper_inner.ma". include "delayed_updating/syntax/path_head_structure.ma". include "delayed_updating/syntax/path_structure_depth.ma". include "delayed_updating/syntax/path_structure_reverse.ma". @@ -33,7 +33,7 @@ include "delayed_updating/syntax/path_depth_reverse.ma". (* Constructions with unwind ************************************************) lemma ifr_unwind_bi (f) (p) (q) (t1) (t2): - t1 ϵ 𝐓 → t1⋔(p◖𝗦) ⧸≬ 𝐈 → + t1 ϵ 𝐓 → t1⋔(p◖𝗦) ϵ 𝐏 → t1 ➡𝐢𝐟[p,q] t2 → ▼[f]t1 ➡𝐢𝐟[⊗p,⊗q] ▼[f]t2. #f #p #q #t1 #t2 #H1t1 #H2t1 * #n * #H1n #Ht1 #Ht2 @@ -51,10 +51,10 @@ lemma ifr_unwind_bi (f) (p) (q) (t1) (t2): @(subset_eq_trans … Ht2) -t2 @(subset_eq_trans … (unwind2_term_fsubst …)) [ @fsubst_eq_repl [ // | // ] - @(subset_eq_canc_dx … (unwind2_term_after …)) - @(subset_eq_canc_sn … (unwind2_term_eq_repl_dx …)) + @(subset_eq_canc_sn … (lift_term_eq_repl_dx …)) [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1 - @(subset_eq_trans … (unwind2_term_after …)) + @(subset_eq_trans … (lift_unwind2_term_after …)) + @(subset_eq_canc_dx … (unwind2_term_after_lift …)) @unwind2_term_eq_repl_sn (* Note: crux of the proof begins *) @nstream_eq_inv_ext #m @@ -68,8 +68,7 @@ lemma ifr_unwind_bi (f) (p) (q) (t1) (t2): (* Note: crux of the proof ends *) | // | /2 width=2 by ex_intro/ - | @term_proper_outer #H0 (**) (* full auto does not work *) - /3 width=2 by unwind2_term_des_inner/ + | /2 width=6 by lift_term_proper/ ] ] qed. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma deleted file mode 100644 index 2ec01a2f6..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_inner.ma +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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_path_structure.ma". -include "delayed_updating/syntax/path_inner.ma". - -(* UNWIND FOR PATH **********************************************************) - -(* Destructions with inner condition for path *******************************) - -lemma unwind2_path_des_inner (f) (p): - ▼[f]p ϵ 𝐈 → p ϵ 𝐈. -#f #p @(list_ind_rcons … p) -p // -#p * [ #n ] #_ // -