From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Tue, 4 Jan 2022 12:09:51 +0000 (+0100)
Subject: update in delayed_updating
X-Git-Tag: make_still_working~116
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=8db3579bec4d9a97af526f95a179587a2fbfe3e3

update in delayed_updating

+ immediate reduction defined
+ some lemmas with lift simplified
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma
deleted file mode 100644
index f27fa0bad..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_4.ma
+++ /dev/null
@@ -1,19 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR DELAYED UPDATING ********************************************)
-
-notation "hvbox( t1 ➡'d''f'[ break term 46 p, break term 46 q ] break term 46 t2 )"
-   non associative with precedence 45
-   for @{ 'BlackRightArrow $t1 $p $q $t2 }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma
new file mode 100644
index 000000000..ca059fc5c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( t1 ➡𝐝𝐟[ break term 46 p, break term 46 q ] break term 46 t2 )"
+   non associative with precedence 45
+   for @{ 'BlackRightArrowDF $t1 $p $q $t2 }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_f_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_f_4.ma
new file mode 100644
index 000000000..c69d6c79b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_f_4.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( t1 ➡𝐟[ break term 46 p, break term 46 q ] break term 46 t2 )"
+   non associative with precedence 45
+   for @{ 'BlackRightArrowF $t1 $p $q $t2 }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index a99d8ca06..8c84de0f2 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -15,9 +15,9 @@
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_balanced.ma".
 include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/notation/relations/black_rightarrow_4.ma".
+include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
 
-(* DELAYED FOCALIZED REDUCTION **********************************************)
+(* DELAYED FOCUSED REDUCTION ************************************************)
 
 inductive dfr (p) (q) (t): predicate preterm ≝
 | dfr_beta (b) (n):
@@ -26,5 +26,5 @@ inductive dfr (p) (q) (t): predicate preterm ≝
 .
 
 interpretation
-  "delayed focalized reduction (preterm)"
-  'BlackRightArrow t1 p q t2 = (dfr p q t1 t2).
+  "focused balanced reduction with delayed updating (preterm)"
+  'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
new file mode 100644
index 000000000..bd62d8e6b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/ifr.ma".
+include "delayed_updating/reduction/dfr.ma".
+
+(* DELAYED FOCUSED REDUCTION ************************************************)
+
+lemma dfr_lift_bi (f) (p) (q) (t1) (t2):
+      t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2.
+#f #p #q #t1 #t2
+* #b #n #Hr #Hb
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
new file mode 100644
index 000000000..53853273b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_balanced.ma".
+include "delayed_updating/substitution/fsubst.ma".
+include "delayed_updating/substitution/lift_preterm.ma".
+include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
+
+(* IMMEDIATE FOCUSED REDUCTION ************************************************)
+
+inductive ifr (p) (q) (t): predicate preterm ≝
+| ifr_beta (b) (n):
+  let r ≝ p●𝗔◗b●𝗟◗q in
+  r◖𝗱❨n❩ ϵ t → ⊓⊗b → ifr p q t (t[⋔r←↑[𝐮❨n❩]t⋔(p◖𝗦)])
+.
+
+interpretation
+  "focused balanced reduction with immediate updating (preterm)"
+  'BlackRightArrowF t1 p q t2 = (ifr p q t1 t2).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index a396beb46..5db8fa945 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -81,3 +81,50 @@ lemma lift_A_sn (A) (k) (p) (f):
 lemma lift_S_sn (A) (k) (p) (f):
       ↑❨(λp. k (𝗦◗p)), p, f❩ = ↑{A}❨k, 𝗦◗p, f❩.
 // qed.
+
+(* Basic constructions with proj_path ***************************************)
+
+lemma lift_path_d_empty_sn (f) (n):
+      𝗱❨f@❨n❩❩◗𝐞 = ↑[f](𝗱❨n❩◗𝐞).
+// qed.
+
+lemma lift_path_d_lcons_sn (f) (p) (l) (n):
+      ↑[f∘𝐮❨ninj n❩](l◗p) = ↑[f](𝗱❨n❩◗l◗p).
+// qed.
+
+(* Basic constructions with proj_rmap ***************************************)
+
+lemma lift_rmap_d_empty_sn (f) (n):
+      f = ↑[𝗱❨n❩◗𝐞]f.
+// qed.
+
+lemma lift_rmap_d_lcons_sn (f) (p) (l) (n):
+      ↑[l◗p](f∘𝐮❨ninj n❩) = ↑[𝗱❨n❩◗l◗p]f.
+// qed.
+
+lemma lift_rmap_L_sn (f) (p):
+      ↑[p](⫯f) = ↑[𝗟◗p]f.
+// qed.
+
+lemma lift_rmap_A_sn (f) (p):
+      ↑[p]f = ↑[𝗔◗p]f.
+// qed.
+
+lemma lift_rmap_S_sn (f) (p):
+      ↑[p]f = ↑[𝗦◗p]f.
+// qed.
+
+(* Advanced eliminations with path ******************************************)
+
+lemma path_ind_lift (Q:predicate …):
+      Q 𝐞 →
+      (∀n. Q 𝐞 → Q (𝗱❨n❩◗𝐞)) →
+      (∀n,l,p. Q (l◗p) → Q (𝗱❨n❩◗l◗p)) →
+      (∀p. Q p → Q (𝗟◗p)) →
+      (∀p. Q p → Q (𝗔◗p)) →
+      (∀p. Q p → Q (𝗦◗p)) →
+      ∀p. Q p.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #p
+elim p -p [| * [ #n * ] ]
+/2 width=1 by/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index c0d7dcbf5..ae3ffbdc6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -28,9 +28,9 @@ interpretation
 
 lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
       k1 ≗{A} k2 → ↑❨k1, p, f❩ = ↑❨k2, p, f❩.
-#A #p elim p -p
+#A #p @(path_ind_lift … p) -p [| #n | #n #l0 #q ]
 [ #k1 #k2 #f #Hk <lift_empty <lift_empty //
-| * [ #n * [| #l0 ]] [|*: #q ] #IH #k1 #k2 #f #Hk /2 width=1 by/
+|*: #IH #k1 #k2 #f #Hk /2 width=1 by/
 ]
 qed-.
 
@@ -49,28 +49,35 @@ lemma lift_append_rcons_sn (A) (k) (f) (p1) (p) (l):
 <list_append_rcons_sn //
 qed.
 
-(* Basic constructions with proj_path ***************************************)
+(* Advanced constructions with proj_path ************************************)
 
-lemma lift_append_sn (p) (f) (q):
+lemma lift_path_append_sn (p) (f) (q):
       q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
-#p elim p -p
-[ //
-| * [ #n * [| #l ]] [|*: #p ] #IH #f #q
-  [ <lift_d_empty_sn <lift_d_empty_sn >lift_lcons_alt >lift_append_rcons_sn
-    <IH <IH -IH <list_append_rcons_sn //
-  | <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
-  | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
-    <IH <IH -IH <list_append_rcons_sn //
-  | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
-    <IH <IH -IH <list_append_rcons_sn //
-  | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
-    <IH <IH -IH <list_append_rcons_sn //
-  ]
+#p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
+[ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
+| <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
+  <IH <IH -IH <list_append_rcons_sn //
+| <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
+  <IH <IH -IH <list_append_rcons_sn //
+| <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
+  <IH <IH -IH <list_append_rcons_sn //
 ]
 qed.
 
-lemma lift_lcons (f) (p) (l):
+lemma lift_path_lcons (f) (p) (l):
       l◗↑[f]p = ↑❨(λp. proj_path (l◗p)), p, f❩.
 #f #p #l
->lift_lcons_alt <lift_append_sn //
+>lift_lcons_alt <lift_path_append_sn //
 qed.
+
+lemma lift_path_L_sn (f) (p):
+      𝗟◗↑[⫯f]p = ↑[f](𝗟◗p).
+// qed.
+
+lemma lift_path_A_sn (f) (p):
+      𝗔◗↑[f]p = ↑[f](𝗔◗p).
+// qed.
+
+lemma lift_path_S_sn (f) (p):
+      𝗦◗↑[f]p = ↑[f](𝗦◗p).
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm.ma
new file mode 100644
index 000000000..f2c78419f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/syntax/preterm.ma".
+include "delayed_updating/substitution/lift.ma".
+
+(* LIFT FOR PRETERM ***********************************************************)
+
+definition lift_preterm (f) (t): preterm ≝
+           λp. ∃∃r. r ϵ t & p = ↑[f]r.
+
+interpretation
+  "lift (preterm)"
+  'UpArrow f t = (lift_preterm f t).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
index 50b35e654..903026e4d 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -21,78 +21,39 @@ include "delayed_updating/substitution/lift_eq.ma".
 
 lemma lift_d_empty_dx (n) (p) (f):
       (⊗p)◖𝗱❨(↑[p◖𝗱❨n❩]f)@❨n❩❩ = ↑[f](p◖𝗱❨n❩).
-#n #p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| <list_cons_shift <list_cons_comm <list_cons_comm //
-| <lift_d_lcons_sn <lift_d_lcons_sn //
-| <lift_L_sn <lift_L_sn <lift_lcons <IH //
-| <lift_A_sn <lift_A_sn <lift_lcons <IH //
-| <lift_S_sn <lift_S_sn <lift_lcons <IH //
+#n #p @(path_ind_lift … p) -p // [ #m #l #p |*: #p ] #IH #f
+[ <lift_rmap_d_lcons_sn <lift_path_d_lcons_sn //
+| <lift_rmap_L_sn <lift_path_L_sn <IH //
+| <lift_rmap_A_sn <lift_path_A_sn <IH //
+| <lift_rmap_S_sn <lift_path_S_sn <IH //
 ]
 qed.
 
 lemma lift_L_dx (p) (f):
       (⊗p)◖𝗟 = ↑[f](p◖𝗟).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift … p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
 qed.
 
 lemma lift_A_dx (p) (f):
       (⊗p)◖𝗔 = ↑[f](p◖𝗔).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift … p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
 qed.
 
 lemma lift_S_dx (p) (f):
       (⊗p)◖𝗦 = ↑[f](p◖𝗦).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift … p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
 qed.
 
 lemma structure_lift (p) (f):
       ⊗p = ⊗↑[f]p.
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift … p) -p // #p #IH #f
+<lift_path_L_sn //
 qed.
 
 lemma lift_structure (p) (f):
       ⊗p = ↑[f]⊗p.
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| //
-| <structure_L_sn <lift_L_sn <lift_lcons //
-| <structure_A_sn <lift_A_sn <lift_lcons //
-| <structure_S_sn <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift … p) -p //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma
deleted file mode 100644
index 60c5a4a41..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/preterm_dephi.ma
+++ /dev/null
@@ -1,21 +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/syntax/path_dephi.ma".
-include "delayed_updating/syntax/preterm_constructors.ma".
-
-(* DEPHI FOR PRETERM ********************************************************)
-
-definition preterm_dephi (f) (t): preterm ≝
-           λp. ∃∃q. q ϵ t & p = path_dephi f q.