From b531c938515b0ea6cb92df2e8732c587e0bc026b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 24 Aug 2006 18:42:12 +0000 Subject: [PATCH] - new legature == for \equiv used in the notation for NPlus FIXME: notation precedence not correct w.r.t. \to \land ... - added notation for NLE - added a comment to dependenciesParser.ml :p --- .../content_pres/cicNotationLexer.ml | 1 + .../grafite_parser/dependenciesParser.ml | 11 ++++++ .../matita/contribs/RELATIONAL/NLE/defs.ma | 14 +++++++- .../matita/contribs/RELATIONAL/NPlus/defs.ma | 8 +++++ .../matita/contribs/RELATIONAL/NPlus/fwd.ma | 34 ++++++++++--------- .../matita/contribs/RELATIONAL/NPlus/props.ma | 27 ++++++++------- 6 files changed, 65 insertions(+), 30 deletions(-) diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index fb459a94e..749731bda 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -123,6 +123,7 @@ let _ = [ ("->", <:unicode>); ("=>", <:unicode>); ("<=", <:unicode>); (">=", <:unicode>); ("<>", <:unicode>); (":=", <:unicode>); + ("==", <:unicode>); ] let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+ diff --git a/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml index 5e80d8b4c..b7b4151fa 100644 --- a/helm/software/components/grafite_parser/dependenciesParser.ml +++ b/helm/software/components/grafite_parser/dependenciesParser.ml @@ -25,6 +25,17 @@ (* $Id$ *) +(* FG + * From Cambridge dictionary + * Dependency: + * a country which is supported and governed by another country + * Dependence: + * when you need something or someone all the time, especially in order to + * continue existing or operating + * + * Fate vobis ... + *) + exception UnableToInclude of string (* statements meaningful for matitadep *) diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma index 19e45c3bc..59c02653e 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma @@ -14,8 +14,20 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/defs". +include "logic/equality.ma". + include "Nat/defs.ma". inductive NLE: Nat \to Nat \to Prop \def | NLE_zero: \forall q. NLE zero q - | NLE_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q). + | NLE_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q) +. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "natural 'less or equal to'" 'leq x y = + (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y). + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "natural 'less than'" 'lt x y = + (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) + (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y). diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma index 92561bc5c..2bc2e8fe0 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma @@ -21,3 +21,11 @@ include "Nat/defs.ma". inductive NPlus (p:Nat): Nat \to Nat \to Prop \def | nplus_zero_2: NPlus p zero p | nplus_succ_2: \forall q, r. NPlus p q r \to NPlus p (succ q) (succ r). + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "natural plus (relational)" 'rel_plus x y z = + (cic:/matita/RELATIONAL/NPlus/defs/NPlus.ind#xpointer(1/1) x y z). + +notation "hvbox(a break + b break == c)" + non associative with precedence 95 +for @{ 'rel_plus $a $b $c}. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma index bae48d405..9b23cb2fb 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma @@ -19,15 +19,15 @@ include "NPlus/defs.ma". (* primitive generation lemmas proved by elimination and inversion *) -theorem nplus_gen_zero_1: \forall q,r. NPlus zero q r \to q = r. +theorem nplus_gen_zero_1: \forall q,r. (zero + q == r) \to q = r. intros. elim H; clear H q r; intros; [ reflexivity | clear H1. auto ]. qed. -theorem nplus_gen_succ_1: \forall p,q,r. NPlus (succ p) q r \to - \exists s. r = (succ s) \land NPlus p q s. +theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to + \exists s. r = (succ s) \land (p + q == s). intros. elim H; clear H q r; intros; [ | clear H1. @@ -36,7 +36,7 @@ theorem nplus_gen_succ_1: \forall p,q,r. NPlus (succ p) q r \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem nplus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r. +theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r. intros. inversion H; clear H; intros; [ auto | clear H H1. @@ -44,8 +44,8 @@ theorem nplus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r. ]. qed. -theorem nplus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to - \exists s. r = (succ s) \land NPlus p q s. +theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to + \exists s. r = (succ s) \land (p + q == s). intros. inversion H; clear H; intros; [ lapply eq_gen_succ_zero to H as H0. apply H0 | clear H1 H3 r. @@ -55,7 +55,8 @@ theorem nplus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to ]. qed. -theorem nplus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zero. +theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to + p = zero \land q = zero. intros. inversion H; clear H; intros; [ rewrite < H1. clear H1 p. auto @@ -64,9 +65,9 @@ theorem nplus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zer ]. qed. -theorem nplus_gen_succ_3: \forall p,q,r. NPlus p q (succ r) \to - \exists s. p = succ s \land NPlus s q r \lor - q = succ s \land NPlus p s r. +theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to + \exists s. p = succ s \land (s + q == r) \lor + q = succ s \land (p + s == r). intros. inversion H; clear H; intros; [ rewrite < H1. clear H1 p | clear H1. @@ -77,7 +78,8 @@ qed. (* (* alternative proofs invoking nplus_gen_2 *) -variant nplus_gen_zero_3_alt: \forall p,q. NPlus p q zero \to p = zero \land q = zero. +variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to + p = zero \land q = zero. intros 2. elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p. @@ -89,9 +91,9 @@ variant nplus_gen_zero_3_alt: \forall p,q. NPlus p q zero \to p = zero \land q = ]. qed. -variant nplus_gen_succ_3_alt: \forall p,q,r. NPlus p q (succ r) \to - \exists s. p = succ s \land NPlus s q r \lor - q = succ s \land NPlus p s r. +variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to + \exists s. p = succ s \land (s + q == r) \lor + q = succ s \land (p + s == r). intros 2. elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p @@ -105,7 +107,7 @@ qed. *) (* other simplification lemmas *) -theorem nplus_gen_eq_2_3: \forall p,q. NPlus p q q \to p = zero. +theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero. intros 2. elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p @@ -116,7 +118,7 @@ theorem nplus_gen_eq_2_3: \forall p,q. NPlus p q q \to p = zero. ]; auto. qed. -theorem nplus_gen_eq_1_3: \forall p,q. NPlus p q p \to q = zero. +theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero. intros 1. elim p; clear p; intros; [ lapply linear nplus_gen_zero_1 to H as H0. rewrite > H0. clear H0 q diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma index 56146a3bf..a80e13fa5 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma @@ -16,11 +16,12 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/props". include "NPlus/fwd.ma". -theorem nplus_zero_1: \forall q. NPlus zero q q. +theorem nplus_zero_1: \forall q. zero + q == q. intros. elim q; clear q; auto. qed. -theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to NPlus (succ p) q (succ r). +theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to + (succ p) + q == (succ r). intros 2. elim q; clear q; [ lapply linear nplus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p @@ -30,7 +31,7 @@ theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to NPlus (succ p) q (succ r). ]; auto. qed. -theorem nplus_sym: \forall p,q,r. NPlus p q r \to NPlus q p r. +theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r. intros 2. elim q; clear q; [ lapply linear nplus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p @@ -41,7 +42,7 @@ theorem nplus_sym: \forall p,q,r. NPlus p q r \to NPlus q p r. qed. theorem nplus_shift_succ_sx: \forall p,q,r. - NPlus p (succ q) r \to NPlus (succ p) q r. + (p + (succ q) == r) \to (succ p) + q == r. intros. lapply linear nplus_gen_succ_2 to H as H0. decompose. @@ -50,7 +51,7 @@ theorem nplus_shift_succ_sx: \forall p,q,r. qed. theorem nplus_shift_succ_dx: \forall p,q,r. - NPlus (succ p) q r \to NPlus p (succ q) r. + ((succ p) + q == r) \to p + (succ q) == r. intros. lapply linear nplus_gen_succ_1 to H as H0. decompose. @@ -58,9 +59,9 @@ theorem nplus_shift_succ_dx: \forall p,q,r. auto. qed. -theorem nplus_trans_1: \forall p,q1,r1. NPlus p q1 r1 \to - \forall q2,r2. NPlus r1 q2 r2 \to - \exists q. NPlus q1 q2 q \land NPlus p q r2. +theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to + \forall q2,r2. (r1 + q2 == r2) \to + \exists q. (q1 + q2 == q) \land p + q == r2. intros 2; elim q1; clear q1; intros; [ lapply linear nplus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p @@ -75,9 +76,9 @@ theorem nplus_trans_1: \forall p,q1,r1. NPlus p q1 r1 \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem nplus_trans_2: \forall p1,q,r1. NPlus p1 q r1 \to - \forall p2,r2. NPlus p2 r1 r2 \to - \exists p. NPlus p1 p2 p \land NPlus p q r2. +theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to + \forall p2,r2. (p2 + r1 == r2) \to + \exists p. (p1 + p2 == p) \land p + q == r2. intros 2; elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p1 @@ -92,8 +93,8 @@ theorem nplus_trans_2: \forall p1,q,r1. NPlus p1 q r1 \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem nplus_conf: \forall p,q,r1. NPlus p q r1 \to - \forall r2. NPlus p q r2 \to r1 = r2. +theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to + \forall r2. (p + q == r2) \to r1 = r2. intros 2. elim q; clear q; intros; [ lapply linear nplus_gen_zero_2 to H as H0. rewrite > H0 in H1. clear H0 p -- 2.39.2