From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 29 Nov 2012 15:26:59 +0000 (+0000)
Subject: - labelled sequential reduction started ...
X-Git-Tag: make_still_working~1429
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9def1b8a298aac85a7abdc75c4a33657fe7e6df7;p=helm.git

- labelled sequential reduction started ...
- bug fix in precedence relation on redex pointers
---

diff --git a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma
new file mode 100644
index 000000000..c5bf4ba99
--- /dev/null
+++ b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "redex_pointer.ma".
+include "multiplicity.ma".
+
+(* LABELLED SEQUENTIAL REDUCTION (ONE STEP) *********************************)
+
+(* Note: the application "(A B)" is represented by "@B.A" following:
+         F. Kamareddine and R.P. Nederpelt: "A useful λ-notation".
+         Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109.
+*)
+inductive lsred: rpointer → relation term ≝
+| lsred_beta   : ∀A,D. lsred (◊) (@D.𝛌.A) ([⬐D]A)
+| lsred_abst   : ∀p,A,C. lsred p A C → lsred p (𝛌.A) (𝛌.C) 
+| lsred_appl_sn: ∀p,B,D,A. lsred p B D → lsred (true::p) (@B.A) (@D.A)
+| lsred_appl_dx: ∀p,B,A,C. lsred p A C → lsred (false::p) (@B.A) (@B.C)
+.
+
+interpretation "labelled sequential reduction"
+    'LablSeqRed M p N = (lsred p M N).
+
+(* Note: we do not use → since it is reserved by CIC *)
+notation "hvbox( M break ⇀ [ term 46 p ] break term 46 N )"
+   non associative with precedence 45
+   for @{ 'LablSeqRed $M $p $N }.
+
+theorem lsred_fwd_mult: ∀p,M,N. M ⇀[p] N → #{N} < #{M} * #{M}.
+#p #M #N #H elim H -p -M -N
+[ #A #D @(le_to_lt_to_lt … (#{A}*#{D})) //
+  normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *) 
+| //
+| #p #B #D #A #_ #IHBD
+  @(lt_to_le_to_lt … (#{B}*#{B}+#{A})) [ /2 width=1/ ] -D -p
+| #p #B #A #C #_ #IHAC
+  @(lt_to_le_to_lt … (#{B}+#{A}*#{A})) [ /2 width=1/ ] -C -p
+]
+@(transitive_le … (#{B}*#{B}+#{A}*#{A})) [ /2 width=1/ ]
+>distributive_times_plus normalize /2 width=1/
+qed-.
diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma
index fa36983af..3d5efb8f2 100644
--- a/matita/matita/contribs/lambda/preamble.ma
+++ b/matita/matita/contribs/lambda/preamble.ma
@@ -19,6 +19,11 @@ include "arithmetics/nat.ma".
 include "xoa_notation.ma".
 include "xoa.ma".
 
+(* Note: notation for nil not involving brackets *)
+notation > "◊"
+  non associative with precedence 90
+  for @{'nil}.
+
 (* Note: For some reason this cannot be in the standard library *) 
 interpretation "logical false" 'false = False.
 
diff --git a/matita/matita/contribs/lambda/redex_pointer.ma b/matita/matita/contribs/lambda/redex_pointer.ma
index dbc8efe48..f6e05c93f 100644
--- a/matita/matita/contribs/lambda/redex_pointer.ma
+++ b/matita/matita/contribs/lambda/redex_pointer.ma
@@ -21,17 +21,18 @@ include "term.ma".
 *)
 (* Note: this is a path in the tree representation of a term
          in which abstraction nodes are omitted;
-         on application nodes, "false" means "proceed left"
-         and "true" means "proceed right"
+         on application nodes, "false" means "proceed right"
+         and "true" means "proceed left"
 *)
 definition rpointer: Type[0] ≝ list bool.
 
 (* Note: precedence relation on redex pointers: p ≺ q
          to serve as base for the order relations: p < q and p ≤ q *)
 inductive rpprec: relation rpointer ≝
-| rpprec_nil : ∀b,q.   rpprec ([]) (b::q)
+| rpprec_nil : ∀b,q.   rpprec (◊) (b::q)
 | rppprc_cons: ∀p,q.   rpprec (false::p) (true::q)
 | rpprec_comp: ∀b,p,q. rpprec p q → rpprec (b::p) (b::q)
+| rpprec_skip: ∀p,q.   rpprec (false::p) q → rpprec p q
 .
 
 interpretation "'precedes' on redex pointers"
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index edb99b8c0..56935028f 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -305,6 +305,10 @@ lemma lt_to_le: ∀x,y. x < y → x ≤ y.
 lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
 // qed-.
 
+lemma le_x_times_x: ∀x. x ≤ x * x.
+#x elim x -x //
+qed.
+
 (* lt *)
 
 theorem transitive_lt: transitive nat lt.
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 0dbc5b75e..2972d58e9 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1508,8 +1508,8 @@ let predefined_classes = [
  ["#"; "⌘"; ];
  ["-"; "÷"; "⊢"; "⊩"; ];
  ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ];  
- ["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
- ["⇒"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥤"; "⥰"; ] ;
+ ["→"; "⇀"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
+ ["⇒"; "⥤"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥰"; ] ;
  ["^"; "↑"; ] ;
  ["⇑"; "⇧"; "⬆"; ] ; 
  ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;