From 9def1b8a298aac85a7abdc75c4a33657fe7e6df7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 29 Nov 2012 15:26:59 +0000 Subject: [PATCH] - labelled sequential reduction started ... - bug fix in precedence relation on redex pointers --- .../lambda/labelled_sequential_reduction.ma | 51 +++++++++++++++++++ matita/matita/contribs/lambda/preamble.ma | 5 ++ .../matita/contribs/lambda/redex_pointer.ma | 7 +-- matita/matita/lib/arithmetics/nat.ma | 4 ++ matita/matita/predefined_virtuals.ml | 4 +- 5 files changed, 66 insertions(+), 5 deletions(-) create mode 100644 matita/matita/contribs/lambda/labelled_sequential_reduction.ma 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 = [ ["#"; "⌘"; ]; ["-"; "÷"; "⊢"; "⊩"; ]; ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; - ["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; - ["⇒"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥤"; "⥰"; ] ; + ["→"; "⇀"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["⇒"; "⥤"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; -- 2.39.2