- 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 (file)
index 0000000..c5bf4ba
--- /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 fa36983af635ee6689a23bfcc09591c61db272d8..3d5efb8f2acf300c1107057d1e5b50d7a5ca0073 100644 (file)
--- 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 dbc8efe481e76951ed06e1d713d87eb864c58acc..f6e05c93fa740e664bad3e766e73cde027eb232d 100644 (file)
--- 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 edb99b8c0c9dac85517e253e9282d7f34597bd89..56935028f65015812b79fdc15fb8762b012d14cf 100644 (file)
--- 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 0dbc5b75e5a7fc1032e802871d07008fa2cadaec..2972d58e978c67ae99a1130cc1e4525b3c042a2a 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1508,8 +1508,8 @@ let predefined_classes = [
  ["#"; "⌘"; ];
  ["-"; "÷"; "⊢"; "⊩"; ];
  ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ];  
- ["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
- ["â\87\92"; "â\9e¾"; "â\87¨"; "â\9e¡"; "â\9e¸"; "â\87\89"; "⥤"; "⥰"; ] ;
+ ["â\86\92"; "â\87\80"; "â\87\9d"; "â\87¾"; "â¤\8d"; "â¤\8f"; "⤳"; ] ;
+ ["â\87\92"; "⥤"; "â\9e¾"; "â\87¨"; "â\9e¡"; "â\9e¸"; "â\87\89"; "⥰"; ] ;
  ["^"; "↑"; ] ;
  ["⇑"; "⇧"; "⬆"; ] ; 
  ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;