From 092d5c718ea90255ce1009acd5aa0942e4449898 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 15 Feb 2007 15:19:33 +0000 Subject: [PATCH] refactoring --- .../matita/contribs/RELATIONAL/NLE/defs.ma | 12 +++---- .../RELATIONAL/NLE/{fwd.ma => inv.ma} | 10 +++--- .../matita/contribs/RELATIONAL/NLE/nplus.ma | 10 ++++-- .../matita/contribs/RELATIONAL/NLE/props.ma | 14 ++++++++- .../matita/contribs/RELATIONAL/NPlus/defs.ma | 3 +- .../RELATIONAL/NPlus/{fwd.ma => inv.ma} | 17 +++++----- .../matita/contribs/RELATIONAL/NPlus/props.ma | 2 +- .../contribs/RELATIONAL/NPlusList/defs.ma | 2 +- .../matita/contribs/RELATIONAL/Nat/fwd.ma | 31 ------------------- .../{Bool/defs.ma => datatypes/Bool.ma} | 6 ++-- .../{List/defs.ma => datatypes/List.ma} | 8 +++-- .../RELATIONAL/{Nat => datatypes}/defs.ma | 4 ++- .../RELATIONAL/{NLE/dec.ma => preamble.ma} | 17 ++-------- 13 files changed, 56 insertions(+), 80 deletions(-) rename helm/software/matita/contribs/RELATIONAL/NLE/{fwd.ma => inv.ma} (90%) rename helm/software/matita/contribs/RELATIONAL/NPlus/{fwd.ma => inv.ma} (90%) delete mode 100644 helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma rename helm/software/matita/contribs/RELATIONAL/{Bool/defs.ma => datatypes/Bool.ma} (91%) rename helm/software/matita/contribs/RELATIONAL/{List/defs.ma => datatypes/List.ma} (86%) rename helm/software/matita/contribs/RELATIONAL/{Nat => datatypes}/defs.ma (93%) rename helm/software/matita/contribs/RELATIONAL/{NLE/dec.ma => preamble.ma} (74%) diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma index 2cea043d5..146c274b3 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma @@ -20,19 +20,19 @@ inductive NLE (q:Nat) (r:Nat): Prop \def | nle_nplus: \forall p. (p + q == r) \to NLE q r. (*CSC: the URI must disappear: there is a bug now *) -interpretation "natural 'less or equal to'" 'leq x y = +interpretation "natural 'greater or equal to'" 'geq y x= (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 = +interpretation "natural 'greater than'" 'gt y x = (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) - (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y). + (cic:/matita/RELATIONAL/datatypes/Nat/Nat.ind#xpointer(1/1/2) x) y). (*CSC: the URI must disappear: there is a bug now *) -interpretation "natural 'greater or equal to'" 'geq y x= +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 'greater than'" 'gt y x = +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). + (cic:/matita/RELATIONAL/datatypes/Nat/Nat.ind#xpointer(1/1/2) x) y). diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma similarity index 90% rename from helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma rename to helm/software/matita/contribs/RELATIONAL/NLE/inv.ma index 06b7c6fef..e42eecde3 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma @@ -12,11 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/NLE/fwd". +set "baseuri" "cic:/matita/RELATIONAL/NLE/inv". -include "logic/connectives.ma". - -include "NPlus/fwd.ma". +include "NPlus/inv.ma". include "NLE/defs.ma". theorem nle_inv_succ_1: \forall x,y. x < y \to @@ -29,14 +27,14 @@ qed. theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y. intros. lapply linear nle_inv_succ_1 to H. decompose. - lapply linear eq_gen_succ_succ to H1. subst. + destruct H1. clear H1. subst. auto. qed. theorem nle_inv_succ_zero: \forall x. x < zero \to False. intros. lapply linear nle_inv_succ_1 to H. decompose. - lapply linear eq_gen_zero_succ to H1. decompose. + destruct H1. qed. theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma b/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma index 7bcdd6010..f469568d7 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/nplus.ma @@ -16,6 +16,10 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/nplus". include "NLE/defs.ma". -axiom pippo: \forall x1, x2, x3. (x1 + x2 == x3) \to - \forall y1, y2, y3. (y1 + y2 == y3) \to - x1 <= y1 \to x2 < y2 \to x3 < y3. +axiom nle_nplus_comp: \forall x1, x2, x3. (x1 + x2 == x3) \to + \forall y1, y2, y3. (y1 + y2 == y3) \to + x1 <= y1 \to x2 <= y2 \to x3 <= y3. + +axiom nle_nplus_comp_lt_2: \forall x1, x2, x3. (x1 + x2 == x3) \to + \forall y1, y2, y3. (y1 + y2 == y3) \to + x1 <= y1 \to x2 < y2 \to x3 < y3. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma index 34e5d0a24..eccc2f9db 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/props". -include "NLE/fwd.ma". +include "NLE/inv.ma". theorem nle_zero_1: \forall q. zero <= q. intros. auto. @@ -64,3 +64,15 @@ theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y. | decompose; subst; auto ]. qed. + +theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x. + intros 2; elim y; clear y; + [ auto + | decompose; + [ lapply linear nle_inv_succ_1 to H1. decompose. + subst. auto depth=4 + | lapply linear nle_lt_or_eq to H1; decompose; + subst; auto + ] + ]. +qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma index a335b26ed..93c7a2e45 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma @@ -14,8 +14,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs". -include "logic/equality.ma". -include "Nat/defs.ma". +include "datatypes/defs.ma". inductive NPlus (p:Nat): Nat \to Nat \to Prop \def | nplus_zero_2: NPlus p zero p diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma similarity index 90% rename from helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma rename to helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma index 7aea3af9d..c8450346e 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/NPlus/fwd". +set "baseuri" "cic:/matita/RELATIONAL/NPlus/inv". -include "Nat/fwd.ma". include "NPlus/defs.ma". (* primitive generation lemmas proved by elimination and inversion *) @@ -40,16 +39,16 @@ theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r. intros. inversion H; clear H; intros; [ auto new timeout=30 | clear H H1. - lapply eq_gen_zero_succ to H2 as H0. decompose. + destruct H2. ]. qed. 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. decompose. + [ destruct H. | clear H1 H3 r. - lapply linear eq_gen_succ_succ to H2 as H0. + destruct H2; clear H2. subst. apply ex_intro; [| auto new timeout=30 ] (**) ]. @@ -60,7 +59,7 @@ theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to intros. inversion H; clear H; intros; [ subst. auto new timeout=30 | clear H H1. - lapply eq_gen_zero_succ to H3 as H0. decompose. + destruct H3. ]. qed. @@ -70,7 +69,7 @@ theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to intros. inversion H; clear H; intros; [ subst. | clear H1. - lapply linear eq_gen_succ_succ to H3 as H0. + destruct H3. clear H3. subst. ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ] (**) qed. @@ -111,7 +110,7 @@ theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero. subst | lapply linear nplus_gen_succ_2 to H1 as H0. decompose. - lapply linear eq_gen_succ_succ to H2 as H0. + destruct H2. clear H2. subst ]; auto new timeout=30. qed. @@ -122,7 +121,7 @@ theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero. subst | lapply linear nplus_gen_succ_1 to H1 as H0. decompose. - lapply linear eq_gen_succ_succ to H2 as H0. + destruct H2. clear H2. subst ]; auto new timeout=30. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma index 2c908d1d0..d566e8a32 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/props". -include "NPlus/fwd.ma". +include "NPlus/inv.ma". theorem nplus_zero_1: \forall q. zero + q == q. intros. elim q; clear q; auto new timeout=100. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlusList/defs.ma b/helm/software/matita/contribs/RELATIONAL/NPlusList/defs.ma index a07889405..86d023165 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlusList/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlusList/defs.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlusList/defs". -include "List/defs.ma". +include "datatypes/List.ma". include "NPlus/defs.ma". diff --git a/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma b/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma deleted file mode 100644 index b76138fe5..000000000 --- a/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma +++ /dev/null @@ -1,31 +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 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/RELATIONAL/Nat/fwd". - -include "logic/equality.ma". - -include "Nat/defs.ma". - -theorem eq_gen_zero_succ: \forall m2. zero = succ m2 \to False. - intros. destruct H. -qed. - -theorem eq_gen_succ_zero: \forall m1. succ m1 = zero \to False. - intros. destruct H. -qed. - -theorem eq_gen_succ_succ: \forall m1,m2. succ m1 = succ m2 \to m1 = m2. - intros. destruct H. assumption. -qed. diff --git a/helm/software/matita/contribs/RELATIONAL/Bool/defs.ma b/helm/software/matita/contribs/RELATIONAL/datatypes/Bool.ma similarity index 91% rename from helm/software/matita/contribs/RELATIONAL/Bool/defs.ma rename to helm/software/matita/contribs/RELATIONAL/datatypes/Bool.ma index 18f0c2c71..0d0502564 100644 --- a/helm/software/matita/contribs/RELATIONAL/Bool/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/datatypes/Bool.ma @@ -12,9 +12,11 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/Bool/defs". +set "baseuri" "cic:/matita/RELATIONAL/datatypes/Bool". + +include "preamble.ma". inductive Bool: Set \def | false: Bool - | true: Bool + | true : Bool . diff --git a/helm/software/matita/contribs/RELATIONAL/List/defs.ma b/helm/software/matita/contribs/RELATIONAL/datatypes/List.ma similarity index 86% rename from helm/software/matita/contribs/RELATIONAL/List/defs.ma rename to helm/software/matita/contribs/RELATIONAL/datatypes/List.ma index 435d72365..69a53f896 100644 --- a/helm/software/matita/contribs/RELATIONAL/List/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/datatypes/List.ma @@ -12,7 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/List/defs". +set "baseuri" "cic:/matita/RELATIONAL/datatypes/List". + +include "preamble.ma". inductive List (A:Set): Set \def | nil: List A @@ -21,7 +23,7 @@ inductive List (A:Set): Set \def (*CSC: the URI must disappear: there is a bug now *) interpretation "nil" 'nil = - (cic:/matita/RELATIONAL/List/defs/List.ind#xpointer(1/1) _). + (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/1) _). notation "hvbox([])" non associative with precedence 95 @@ -29,7 +31,7 @@ for @{ 'nil }. (*CSC: the URI must disappear: there is a bug now *) interpretation "right cons" 'rcons x y = - (cic:/matita/RELATIONAL/List/defs/List.ind#xpointer(1/2) _ x y). + (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/2) _ x y). notation "hvbox([a break @ b])" non associative with precedence 95 diff --git a/helm/software/matita/contribs/RELATIONAL/Nat/defs.ma b/helm/software/matita/contribs/RELATIONAL/datatypes/defs.ma similarity index 93% rename from helm/software/matita/contribs/RELATIONAL/Nat/defs.ma rename to helm/software/matita/contribs/RELATIONAL/datatypes/defs.ma index 983731938..3a3a4f5ed 100644 --- a/helm/software/matita/contribs/RELATIONAL/Nat/defs.ma +++ b/helm/software/matita/contribs/RELATIONAL/datatypes/defs.ma @@ -12,7 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/Nat/defs". +set "baseuri" "cic:/matita/RELATIONAL/datatypes/Nat". + +include "preamble.ma". inductive Nat: Set \def | zero: Nat diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma b/helm/software/matita/contribs/RELATIONAL/preamble.ma similarity index 74% rename from helm/software/matita/contribs/RELATIONAL/NLE/dec.ma rename to helm/software/matita/contribs/RELATIONAL/preamble.ma index 918acfe53..050d9dece 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma +++ b/helm/software/matita/contribs/RELATIONAL/preamble.ma @@ -12,18 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/NLE/dec". +set "baseuri" "cic:/matita/RELATIONAL/preamble". -include "NLE/props.ma". - -theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x. - intros 2; elim y; clear y; - [ auto - | decompose; - [ lapply linear nle_inv_succ_1 to H1. decompose. - subst. auto depth=4 - | lapply linear nle_lt_or_eq to H1; decompose; - subst; auto - ] - ]. -qed. +include "logic/equality.ma". +include "logic/connectives.ma". -- 2.39.2