From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 6 Jul 2022 12:18:48 +0000 (+0200)
Subject: partial commit in delayed_updating
X-Git-Tag: make_still_working~52
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c038f0446312091a30179fd80e6ffd3ec39ab446;p=helm.git

partial commit in delayed_updating

+ parchin reverse operator for paths
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/nec_r_1.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/nec_r_1.etc
new file mode 100644
index 000000000..79df117c7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/nec_r_1.etc
@@ -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( p á´¿ )"
+  non associative with precedence 71
+  for @{ 'NEcR $p }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_depth_reverse.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_depth_reverse.etc
new file mode 100644
index 000000000..33f678ade
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_depth_reverse.etc
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_depth.ma".
+include "delayed_updating/syntax/path_reverse.ma".
+
+(* DEPTH FOR PATH ***********************************************************)
+
+(* Constructions with reverse ***********************************************)
+
+lemma depth_reverse (p):
+      ♭p = ♭pᴿ.
+#p elim p -p //
+* [ #n ] #p #IH <reverse_lcons
+[ <depth_d_sn <depth_d_dx //
+| <depth_m_sn <depth_m_dx //
+| <depth_L_sn <depth_L_dx //
+| <depth_A_sn <depth_A_dx //
+| <depth_S_sn <depth_S_dx //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_reverse.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_reverse.etc
new file mode 100644
index 000000000..7fa03a41e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_reverse.etc
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.ma".
+include "delayed_updating/notation/functions/nec_r_1.ma".
+
+(* REVERSE FOR PATH *********************************************************)
+
+rec definition reverse (p) on p: path ≝
+match p with
+[ list_empty     ⇒ 𝐞
+| list_lcons l q ⇒ (reverse q)◖l
+].
+
+interpretation
+  "reverse (path)"
+  'NEcR p = (reverse p).
+
+(* Basic constructions ******************************************************)
+
+lemma reverse_empty: 𝐞 = 𝐞ᴿ.
+// qed.
+
+lemma reverse_lcons (p) (l): pᴿ◖l = (l◗p)ᴿ.
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem reverse_append (p1) (p2):
+        (p2ᴿ)●(p1ᴿ) = (p1●p2)ᴿ.
+#p1 elim p1 -p1 //
+#l1 #p1 #IH #p2
+<list_append_lcons_sn <reverse_lcons <reverse_lcons //
+qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma reverse_rcons (p) (l):
+      l◗(pᴿ) = (p◖l)ᴿ.
+#p #l
+<reverse_append //
+qed.
+
+(* Main constructions *******************************************************)
+
+theorem reverse_reverse (p):
+        p = pá´¿á´¿.
+#p elim p -p //
+#l #p #IH
+<reverse_lcons <reverse_rcons //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_structure_reverse.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_structure_reverse.etc
new file mode 100644
index 000000000..1cc32777b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/reverse/path_structure_reverse.etc
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_reverse.ma".
+
+(* STRUCTURE FOR PATH *******************************************************)
+
+(* Constructions with reverse ***********************************************)
+
+lemma structure_reverse (p):
+      (⊗p)ᴿ = ⊗(pᴿ).
+#p elim p -p //
+* [ #n ] #p #IH <reverse_lcons //
+[ <structure_d_sn <structure_d_dx //
+| <structure_m_sn <structure_m_dx //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/names.txt b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
new file mode 100644
index 000000000..aee943494
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/names.txt
@@ -0,0 +1,9 @@
+METAVARIABLES
+
+  b         : balanced path
+  f, g      : update function
+  h, k      : reference index by depth
+  l         : label
+  m, n      : natural number
+  p, q, r, s: path
+  t, u, v, w: term
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nec_r_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nec_r_1.ma
deleted file mode 100644
index 79df117c7..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/nec_r_1.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( p á´¿ )"
-  non associative with precedence 71
-  for @{ 'NEcR $p }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_reverse.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_reverse.ma
deleted file mode 100644
index 33f678ade..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_reverse.ma
+++ /dev/null
@@ -1,32 +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_depth.ma".
-include "delayed_updating/syntax/path_reverse.ma".
-
-(* DEPTH FOR PATH ***********************************************************)
-
-(* Constructions with reverse ***********************************************)
-
-lemma depth_reverse (p):
-      ♭p = ♭pᴿ.
-#p elim p -p //
-* [ #n ] #p #IH <reverse_lcons
-[ <depth_d_sn <depth_d_dx //
-| <depth_m_sn <depth_m_dx //
-| <depth_L_sn <depth_L_dx //
-| <depth_A_sn <depth_A_dx //
-| <depth_S_sn <depth_S_dx //
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_reverse.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_reverse.ma
deleted file mode 100644
index 7fa03a41e..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_reverse.ma
+++ /dev/null
@@ -1,62 +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.ma".
-include "delayed_updating/notation/functions/nec_r_1.ma".
-
-(* REVERSE FOR PATH *********************************************************)
-
-rec definition reverse (p) on p: path ≝
-match p with
-[ list_empty     ⇒ 𝐞
-| list_lcons l q ⇒ (reverse q)◖l
-].
-
-interpretation
-  "reverse (path)"
-  'NEcR p = (reverse p).
-
-(* Basic constructions ******************************************************)
-
-lemma reverse_empty: 𝐞 = 𝐞ᴿ.
-// qed.
-
-lemma reverse_lcons (p) (l): pᴿ◖l = (l◗p)ᴿ.
-// qed.
-
-(* Main constructions *******************************************************)
-
-theorem reverse_append (p1) (p2):
-        (p2ᴿ)●(p1ᴿ) = (p1●p2)ᴿ.
-#p1 elim p1 -p1 //
-#l1 #p1 #IH #p2
-<list_append_lcons_sn <reverse_lcons <reverse_lcons //
-qed.
-
-(* Constructions with list_rcons ********************************************)
-
-lemma reverse_rcons (p) (l):
-      l◗(pᴿ) = (p◖l)ᴿ.
-#p #l
-<reverse_append //
-qed.
-
-(* Main constructions *******************************************************)
-
-theorem reverse_reverse (p):
-        p = pá´¿á´¿.
-#p elim p -p //
-#l #p #IH
-<reverse_lcons <reverse_rcons //
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_reverse.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_reverse.ma
deleted file mode 100644
index 1cc32777b..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_reverse.ma
+++ /dev/null
@@ -1,29 +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_structure.ma".
-include "delayed_updating/syntax/path_reverse.ma".
-
-(* STRUCTURE FOR PATH *******************************************************)
-
-(* Constructions with reverse ***********************************************)
-
-lemma structure_reverse (p):
-      (⊗p)ᴿ = ⊗(pᴿ).
-#p elim p -p //
-* [ #n ] #p #IH <reverse_lcons //
-[ <structure_d_sn <structure_d_dx //
-| <structure_m_sn <structure_m_dx //
-]
-qed.