From: Ferruccio Guidi Date: Thu, 15 Feb 2007 15:19:33 +0000 (+0000) Subject: refactoring X-Git-Tag: 0.4.95@7852~594 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4d945e028b3787f5aa26bdb0ef1639cde3ac30fe;p=helm.git refactoring --- diff --git a/matita/contribs/RELATIONAL/Bool/defs.ma b/matita/contribs/RELATIONAL/Bool/defs.ma deleted file mode 100644 index 18f0c2c71..000000000 --- a/matita/contribs/RELATIONAL/Bool/defs.ma +++ /dev/null @@ -1,20 +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/Bool/defs". - -inductive Bool: Set \def - | false: Bool - | true: Bool -. diff --git a/matita/contribs/RELATIONAL/List/defs.ma b/matita/contribs/RELATIONAL/List/defs.ma deleted file mode 100644 index 435d72365..000000000 --- a/matita/contribs/RELATIONAL/List/defs.ma +++ /dev/null @@ -1,37 +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/List/defs". - -inductive List (A:Set): Set \def - | nil: List A - | cons: List A \to A \to List A -. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "nil" 'nil = - (cic:/matita/RELATIONAL/List/defs/List.ind#xpointer(1/1) _). - -notation "hvbox([])" - non associative with precedence 95 -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). - -notation "hvbox([a break @ b])" - non associative with precedence 95 -for @{ 'rcons $a $b}. - diff --git a/matita/contribs/RELATIONAL/NLE/dec.ma b/matita/contribs/RELATIONAL/NLE/dec.ma deleted file mode 100644 index 918acfe53..000000000 --- a/matita/contribs/RELATIONAL/NLE/dec.ma +++ /dev/null @@ -1,29 +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/NLE/dec". - -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. diff --git a/matita/contribs/RELATIONAL/NLE/defs.ma b/matita/contribs/RELATIONAL/NLE/defs.ma index 2cea043d5..146c274b3 100644 --- a/matita/contribs/RELATIONAL/NLE/defs.ma +++ b/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/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma deleted file mode 100644 index 06b7c6fef..000000000 --- a/matita/contribs/RELATIONAL/NLE/fwd.ma +++ /dev/null @@ -1,56 +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/NLE/fwd". - -include "logic/connectives.ma". - -include "NPlus/fwd.ma". -include "NLE/defs.ma". - -theorem nle_inv_succ_1: \forall x,y. x < y \to - \exists z. y = succ z \land x <= z. - intros. elim H. - lapply linear nplus_gen_succ_2 to H1. - decompose. subst. auto depth = 4. -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. - 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. -qed. - -theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero. - intros 1. elim x; clear x; intros; - [ auto - | lapply linear nle_inv_succ_zero to H1. decompose. - ]. -qed. - -theorem nle_inv_succ_2: \forall y,x. x <= succ y \to - x = zero \lor \exists z. x = succ z \land z <= y. - intros 2; elim x; clear x; intros; - [ auto - | lapply linear nle_inv_succ_succ to H1. - auto depth = 4. - ]. -qed. diff --git a/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/contribs/RELATIONAL/NLE/inv.ma new file mode 100644 index 000000000..e42eecde3 --- /dev/null +++ b/matita/contribs/RELATIONAL/NLE/inv.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/NLE/inv". + +include "NPlus/inv.ma". +include "NLE/defs.ma". + +theorem nle_inv_succ_1: \forall x,y. x < y \to + \exists z. y = succ z \land x <= z. + intros. elim H. + lapply linear nplus_gen_succ_2 to H1. + decompose. subst. auto depth = 4. +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. + 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. + destruct H1. +qed. + +theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero. + intros 1. elim x; clear x; intros; + [ auto + | lapply linear nle_inv_succ_zero to H1. decompose. + ]. +qed. + +theorem nle_inv_succ_2: \forall y,x. x <= succ y \to + x = zero \lor \exists z. x = succ z \land z <= y. + intros 2; elim x; clear x; intros; + [ auto + | lapply linear nle_inv_succ_succ to H1. + auto depth = 4. + ]. +qed. diff --git a/matita/contribs/RELATIONAL/NLE/nplus.ma b/matita/contribs/RELATIONAL/NLE/nplus.ma index 7bcdd6010..f469568d7 100644 --- a/matita/contribs/RELATIONAL/NLE/nplus.ma +++ b/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/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma index 34e5d0a24..eccc2f9db 100644 --- a/matita/contribs/RELATIONAL/NLE/props.ma +++ b/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/matita/contribs/RELATIONAL/NPlus/defs.ma b/matita/contribs/RELATIONAL/NPlus/defs.ma index a335b26ed..93c7a2e45 100644 --- a/matita/contribs/RELATIONAL/NPlus/defs.ma +++ b/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/matita/contribs/RELATIONAL/NPlus/fwd.ma b/matita/contribs/RELATIONAL/NPlus/fwd.ma deleted file mode 100644 index 7aea3af9d..000000000 --- a/matita/contribs/RELATIONAL/NPlus/fwd.ma +++ /dev/null @@ -1,128 +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/NPlus/fwd". - -include "Nat/fwd.ma". -include "NPlus/defs.ma". - -(* primitive generation lemmas proved by elimination and inversion *) - -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 new timeout=30 - ]. -qed. - -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. - decompose. - subst. - ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**) -qed. - -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. - ]. -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. - | clear H1 H3 r. - lapply linear eq_gen_succ_succ to H2 as H0. - subst. - apply ex_intro; [| auto new timeout=30 ] (**) - ]. -qed. - -theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to - p = zero \land q = zero. - intros. inversion H; clear H; intros; - [ subst. auto new timeout=30 - | clear H H1. - lapply eq_gen_zero_succ to H3 as H0. decompose. - ]. -qed. - -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; - [ subst. - | clear H1. - lapply linear eq_gen_succ_succ to H3 as H0. - subst. - ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ] (**) -qed. -(* -(* alternative proofs invoking nplus_gen_2 *) - -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. - subst. auto new timeout=30 - | clear H. - lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - lapply linear eq_gen_zero_succ to H1 as H0. apply H0 - ]. -qed. - -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. - subst - | clear H. - lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - lapply linear eq_gen_succ_succ to H1 as H0. - subst - ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**) -qed. -*) -(* other simplification lemmas *) - -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. - subst - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - lapply linear eq_gen_succ_succ to H2 as H0. - subst - ]; auto new timeout=30. -qed. - -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. - subst - | lapply linear nplus_gen_succ_1 to H1 as H0. - decompose. - lapply linear eq_gen_succ_succ to H2 as H0. - subst - ]; auto new timeout=30. -qed. diff --git a/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/contribs/RELATIONAL/NPlus/inv.ma new file mode 100644 index 000000000..c8450346e --- /dev/null +++ b/matita/contribs/RELATIONAL/NPlus/inv.ma @@ -0,0 +1,127 @@ +(**************************************************************************) +(* ___ *) +(* ||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/NPlus/inv". + +include "NPlus/defs.ma". + +(* primitive generation lemmas proved by elimination and inversion *) + +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 new timeout=30 + ]. +qed. + +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. + decompose. + subst. + ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**) +qed. + +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. + 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; + [ destruct H. + | clear H1 H3 r. + destruct H2; clear H2. + subst. + apply ex_intro; [| auto new timeout=30 ] (**) + ]. +qed. + +theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to + p = zero \land q = zero. + intros. inversion H; clear H; intros; + [ subst. auto new timeout=30 + | clear H H1. + destruct H3. + ]. +qed. + +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; + [ subst. + | clear H1. + destruct H3. clear H3. + subst. + ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ] (**) +qed. +(* +(* alternative proofs invoking nplus_gen_2 *) + +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. + subst. auto new timeout=30 + | clear H. + lapply linear nplus_gen_succ_2 to H1 as H0. + decompose. + lapply linear eq_gen_zero_succ to H1 as H0. apply H0 + ]. +qed. + +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. + subst + | clear H. + lapply linear nplus_gen_succ_2 to H1 as H0. + decompose. + lapply linear eq_gen_succ_succ to H1 as H0. + subst + ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**) +qed. +*) +(* other simplification lemmas *) + +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. + subst + | lapply linear nplus_gen_succ_2 to H1 as H0. + decompose. + destruct H2. clear H2. + subst + ]; auto new timeout=30. +qed. + +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. + subst + | lapply linear nplus_gen_succ_1 to H1 as H0. + decompose. + destruct H2. clear H2. + subst + ]; auto new timeout=30. +qed. diff --git a/matita/contribs/RELATIONAL/NPlus/props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma index 2c908d1d0..d566e8a32 100644 --- a/matita/contribs/RELATIONAL/NPlus/props.ma +++ b/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/matita/contribs/RELATIONAL/NPlusList/defs.ma b/matita/contribs/RELATIONAL/NPlusList/defs.ma index a07889405..86d023165 100644 --- a/matita/contribs/RELATIONAL/NPlusList/defs.ma +++ b/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/matita/contribs/RELATIONAL/Nat/defs.ma b/matita/contribs/RELATIONAL/Nat/defs.ma deleted file mode 100644 index 983731938..000000000 --- a/matita/contribs/RELATIONAL/Nat/defs.ma +++ /dev/null @@ -1,20 +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/defs". - -inductive Nat: Set \def - | zero: Nat - | succ: Nat \to Nat -. diff --git a/matita/contribs/RELATIONAL/Nat/fwd.ma b/matita/contribs/RELATIONAL/Nat/fwd.ma deleted file mode 100644 index b76138fe5..000000000 --- a/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/matita/contribs/RELATIONAL/datatypes/Bool.ma b/matita/contribs/RELATIONAL/datatypes/Bool.ma new file mode 100644 index 000000000..0d0502564 --- /dev/null +++ b/matita/contribs/RELATIONAL/datatypes/Bool.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/datatypes/Bool". + +include "preamble.ma". + +inductive Bool: Set \def + | false: Bool + | true : Bool +. diff --git a/matita/contribs/RELATIONAL/datatypes/List.ma b/matita/contribs/RELATIONAL/datatypes/List.ma new file mode 100644 index 000000000..69a53f896 --- /dev/null +++ b/matita/contribs/RELATIONAL/datatypes/List.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/datatypes/List". + +include "preamble.ma". + +inductive List (A:Set): Set \def + | nil: List A + | cons: List A \to A \to List A +. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "nil" 'nil = + (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/1) _). + +notation "hvbox([])" + non associative with precedence 95 +for @{ 'nil }. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "right cons" 'rcons x y = + (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/2) _ x y). + +notation "hvbox([a break @ b])" + non associative with precedence 95 +for @{ 'rcons $a $b}. + diff --git a/matita/contribs/RELATIONAL/datatypes/defs.ma b/matita/contribs/RELATIONAL/datatypes/defs.ma new file mode 100644 index 000000000..3a3a4f5ed --- /dev/null +++ b/matita/contribs/RELATIONAL/datatypes/defs.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/datatypes/Nat". + +include "preamble.ma". + +inductive Nat: Set \def + | zero: Nat + | succ: Nat \to Nat +. diff --git a/matita/contribs/RELATIONAL/preamble.ma b/matita/contribs/RELATIONAL/preamble.ma new file mode 100644 index 000000000..050d9dece --- /dev/null +++ b/matita/contribs/RELATIONAL/preamble.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||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/preamble". + +include "logic/equality.ma". +include "logic/connectives.ma".