From: Ferruccio Guidi Date: Mon, 19 Jun 2006 16:29:18 +0000 (+0000) Subject: axioms removed X-Git-Tag: make_still_working~7156 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aebd5af5c7d3e422813159d81fde05b6a9778765;p=helm.git axioms removed --- diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma index 4f95ad4e8..77d6921a9 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma @@ -19,4 +19,3 @@ include "nat_defs.ma". inductive add (p:nat): nat \to nat \to Prop \def | add_O_2: add p O p | add_S_2: \forall q, r. add p q r \to add p (S q) (S r). - diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma index 567bb1fed..86aa7c192 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma @@ -14,22 +14,35 @@ set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_props". +include "nat_props.ma". include "add_defs.ma". -axiom add_gen_O_2: \forall p,r. add p O r \to p = r. - -axiom add_gen_S_2: \forall p,q,r. add p (S q) r \to - \exists s. r = (S s) \land add p q s. +theorem add_gen_O_2: \forall p,r. add p O r \to p = r. + intros. inversion H; clear H; intros; + [ reflexivity + | lapply eq_gen_O_S to H2 as H0. apply H0 + ]. +qed. +theorem add_gen_S_2: \forall p,q,r. add p (S q) r \to + \exists s. r = (S s) \land add p q s. + intros. inversion H; clear H; intros; + [ lapply eq_gen_S_O to H as H0. apply H0 + | lapply eq_gen_S_S to H2 as H0. clear H2. + rewrite > H0. clear H0. + apply ex_intro; [| auto ] (**) + ]. +qed. + theorem add_O_1: \forall q. add O q q. intros. elim q; clear q; auto. qed. theorem add_S_1: \forall p,q,r. add p q r \to add (S p) q (S r). intros 2. elim q; clear q; - [ lapply add_gen_O_2 to H using H0. clear H. + [ lapply add_gen_O_2 to H as H0. clear H. rewrite > H0. clear H0. clear p - | lapply add_gen_S_2 to H1 using H0. clear H1. + | lapply add_gen_S_2 to H1 as H0. clear H1. decompose H0. rewrite > H2. clear H2. clear r ]; auto. @@ -37,9 +50,9 @@ qed. theorem add_sym: \forall p,q,r. add p q r \to add q p r. intros 2. elim q; clear q; - [ lapply add_gen_O_2 to H using H0. clear H. + [ lapply add_gen_O_2 to H as H0. clear H. rewrite > H0. clear H0. clear p - | lapply add_gen_S_2 to H1 using H0. clear H1. + | lapply add_gen_S_2 to H1 as H0. clear H1. decompose H0. rewrite > H2. clear H2. clear r ]; auto. @@ -47,7 +60,7 @@ qed. theorem add_shift_S_sx: \forall p,q,r. add p (S q) r \to add (S p) q r. intros. - lapply add_gen_S_2 to H using H0. clear H. + lapply add_gen_S_2 to H as H0. clear H. decompose H0. rewrite > H1. clear H1. clear r. auto. @@ -64,7 +77,7 @@ qed. theorem add_shift_S_dx: \forall p,q,r. add (S p) q r \to add p (S q) r. intros. - lapply add_gen_S_1 to H using H0. clear H. + lapply add_gen_S_1 to H as H0. clear H. decompose H0. rewrite > H1. clear H1. clear r. auto. @@ -74,45 +87,46 @@ theorem add_trans_1: \forall p,q1,r1. add p q1 r1 \to \forall q2,r2. add r1 q2 r2 \to \exists q. add q1 q2 q \land add p q r2. intros 2; elim q1; clear q1; intros; - [ lapply add_gen_O_2 to H using H0. clear H. + [ lapply add_gen_O_2 to H as H0. clear H. rewrite > H0. clear H0. clear p - | lapply add_gen_S_2 to H1 using H0. clear H1. + | lapply add_gen_S_2 to H1 as H0. clear H1. decompose H0. rewrite > H3. rewrite > H3 in H2. clear H3. clear r1. - lapply add_gen_S_1 to H2 using H0. clear H2. + lapply add_gen_S_1 to H2 as H0. clear H2. decompose H0. rewrite > H2. clear H2. clear r2. - lapply H to H4, H3 using H0. clear H. clear H4. clear H3. + lapply H to H4, H3 as H0. clear H. clear H4. clear H3. decompose H0. - ]; apply ex_intro; [| auto || auto ]. + ]; apply ex_intro; [| auto || auto ]. (**) qed. theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to \forall p2,r2. add p2 r1 r2 \to \exists p. add p1 p2 p \land add p q r2. intros 2; elim q; clear q; intros; - [ lapply add_gen_O_2 to H using H0. clear H. + [ lapply add_gen_O_2 to H as H0. clear H. rewrite > H0. clear H0. clear p1 - | lapply add_gen_S_2 to H1 using H0. clear H1. + | lapply add_gen_S_2 to H1 as H0. clear H1. decompose H0. rewrite > H3. rewrite > H3 in H2. clear H3. clear r1. - lapply add_gen_S_2 to H2 using H0. clear H2. + lapply add_gen_S_2 to H2 as H0. clear H2. decompose H0. rewrite > H2. clear H2. clear r2. - lapply H to H4, H3 using H0. clear H. clear H4. clear H3. + lapply H to H4, H3 as H0. clear H. clear H4. clear H3. decompose H0. - ]; apply ex_intro; [| auto || auto ]. + ]; apply ex_intro; [| auto || auto ]. (**) qed. theorem add_conf: \forall p,q,r1. add p q r1 \to \forall r2. add p q r2 \to r1 = r2. intros 2. elim q; clear q; intros; - [ lapply add_gen_O_2 to H using H0. clear H. + [ lapply add_gen_O_2 to H as H0. clear H. rewrite > H0 in H1. clear H0. clear p - | lapply add_gen_S_2 to H1 using H0. clear H1. + | lapply add_gen_S_2 to H1 as H0. clear H1. decompose H0. rewrite > H3. clear H3. clear r1. - lapply add_gen_S_2 to H2 using H0. clear H2. + lapply add_gen_S_2 to H2 as H0. clear H2. decompose H0. rewrite > H2. clear H2. clear r2. ]; auto. +qed. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma index a188208f2..a78886780 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma @@ -19,7 +19,3 @@ include "library/logic/equality.ma". inductive nat: Set \def | O: nat | S: nat \to nat. - -theorem eq_gen_O_S: \forall (P:Prop). \forall m2. O = S m2 \to P. - intros. inversion H. - diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_props.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_props.ma new file mode 100644 index 000000000..3e5dd5220 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_props.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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-ARITHMETICS/nat_props". + +include "library/logic/equality.ma". +include "nat_defs.ma". + +theorem eq_gen_O_S: \forall (P:Prop). \forall m2. O = S m2 \to P. + intros. discriminate H. +qed. + +theorem eq_gen_S_O: \forall (P:Prop). \forall m1. S m1 = O \to P. + intros. discriminate H. +qed. + +theorem eq_gen_S_S: \forall m1,m2. S m1 = S m2 \to m1 = m2. + intros. injection H. assumption. +qed. \ No newline at end of file