From: Ferruccio Guidi Date: Sun, 20 Aug 2006 12:19:55 +0000 (+0000) Subject: new naming X-Git-Tag: make_still_working~6993 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=526841e632a8ffd31f854c904c852da6c9811f64;hp=50229be94c70a788071ba13d4e5e4aa5479e9897;p=helm.git new naming --- diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma new file mode 100644 index 000000000..bc0624140 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +include "logic/equality.ma". + +inductive Nat: Set \def + | zero: Nat + | succ: Nat \to Nat. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma new file mode 100644 index 000000000..ede85286a --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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_fwd". + +include "Nat.ma". + +theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P. + intros. discriminate H. +qed. + +theorem eq_gen_succ_zero: \forall (P:Prop). \forall m1. succ m1 = zero \to P. + intros. discriminate H. +qed. + +theorem eq_gen_succ_succ: \forall m1,m2. succ m1 = succ m2 \to m1 = m2. + intros. injection H. assumption. +qed. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma new file mode 100644 index 000000000..5d8f4f3ec --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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/Plus". + +include "Nat.ma". + +inductive Plus (p:Nat): Nat \to Nat \to Prop \def + | Plus_zero_2: Plus p zero p + | Plus_succ_2: \forall q, r. Plus p q r \to Plus p (succ q) (succ r). diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma new file mode 100644 index 000000000..8f3e20a3c --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma @@ -0,0 +1,128 @@ +(**************************************************************************) +(* ___ *) +(* ||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/Plus_fwd". + +include "Nat_fwd.ma". +include "Plus.ma". + +(* primitive generation lemmas proved by elimination and inversion *) + +theorem Plus_gen_zero_1: \forall q,r. Plus zero q r \to q = r. + intros. elim H; clear H q r; intros; + [ reflexivity + | clear H1. auto + ]. +qed. + +theorem Plus_gen_succ_1: \forall p,q,r. Plus (succ p) q r \to + \exists s. r = (succ s) \land Plus p q s. + intros. elim H; clear H q r; intros; + [ + | clear H1. + decompose. + rewrite > H1. clear H1 n2 + ]; apply ex_intro; [| auto || auto ]. (**) +qed. + +theorem Plus_gen_zero_2: \forall p,r. Plus p zero r \to p = r. + intros. inversion H; clear H; intros; + [ auto + | clear H H1. + lapply eq_gen_zero_succ to H2 as H0. apply H0 + ]. +qed. + +theorem Plus_gen_succ_2: \forall p,q,r. Plus p (succ q) r \to + \exists s. r = (succ s) \land Plus p q s. + intros. inversion H; clear H; intros; + [ lapply eq_gen_succ_zero to H as H0. apply H0 + | clear H1 H3 r. + lapply linear eq_gen_succ_succ to H2 as H0. + rewrite > H0. clear H0 q. + apply ex_intro; [| auto ] (**) + ]. +qed. + +theorem Plus_gen_zero_3: \forall p,q. Plus p q zero \to p = zero \land q = zero. + intros. inversion H; clear H; intros; + [ rewrite < H1. clear H1 p. + auto + | clear H H1. + lapply eq_gen_zero_succ to H3 as H0. apply H0 + ]. +qed. + +theorem Plus_gen_succ_3: \forall p,q,r. Plus p q (succ r) \to + \exists s. p = succ s \land Plus s q r \lor + q = succ s \land Plus p s r. + intros. inversion H; clear H; intros; + [ rewrite < H1. clear H1 p + | clear H1. + lapply linear eq_gen_succ_succ to H3 as H0. + rewrite > H0. clear H0 r. + ]; apply ex_intro; [| auto || auto ] (**) +qed. +(* +(* alternative proofs invoking Plus_gen_2 *) + +variant Plus_gen_zero_3_alt: \forall p,q. Plus p q zero \to p = zero \land q = zero. + intros 2. elim q; clear q; intros; + [ lapply linear Plus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p. + auto + | clear H. + lapply linear Plus_gen_succ_2 to H1 as H0. + decompose. + lapply linear eq_gen_zero_succ to H1 as H0. apply H0 + ]. +qed. + +variant Plus_gen_succ_3_alt: \forall p,q,r. Plus p q (succ r) \to + \exists s. p = succ s \land Plus s q r \lor + q = succ s \land Plus p s r. + intros 2. elim q; clear q; intros; + [ lapply linear Plus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | clear H. + lapply linear Plus_gen_succ_2 to H1 as H0. + decompose. + lapply linear eq_gen_succ_succ to H1 as H0. + rewrite > H0. clear H0 r. + ]; apply ex_intro; [| auto || auto ]. (**) +qed. +*) +(* other simplification lemmas *) + +theorem Plus_gen_eq_2_3: \forall p,q. Plus p q q \to p = zero. + intros 2. elim q; clear q; intros; + [ lapply linear Plus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear Plus_gen_succ_2 to H1 as H0. + decompose. + lapply linear eq_gen_succ_succ to H2 as H0. + rewrite < H0 in H3. clear H0 a + ]; auto. +qed. + +theorem Plus_gen_eq_1_3: \forall p,q. Plus p q p \to q = zero. + intros 1. elim p; clear p; intros; + [ lapply linear Plus_gen_zero_1 to H as H0. + rewrite > H0. clear H0 q + | lapply linear Plus_gen_succ_1 to H1 as H0. + decompose. + lapply linear eq_gen_succ_succ to H2 as H0. + rewrite < H0 in H3. clear H0 a + ]; auto. +qed. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma new file mode 100644 index 000000000..b2608397c --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||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-ARITHMETICsucc/Plus_props". + +include "Plus_fwd.ma". + +theorem Plus_zero_1: \forall q. Plus zero q q. + intros. elim q; clear q; auto. +qed. + +theorem Plus_succ_1: \forall p,q,r. Plus p q r \to Plus (succ p) q (succ r). + intros 2. elim q; clear q; + [ lapply linear Plus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear Plus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H2. clear H2 r + ]; auto. +qed. + +theorem Plus_sym: \forall p,q,r. Plus p q r \to Plus q p r. + intros 2. elim q; clear q; + [ lapply linear Plus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear Plus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H2. clear H2 r + ]; auto. +qed. + +theorem Plus_shift_succ_sx: \forall p,q,r. + Plus p (succ q) r \to Plus (succ p) q r. + intros. + lapply linear Plus_gen_succ_2 to H as H0. + decompose. + rewrite > H1. clear H1 r. + auto. +qed. + +theorem Plus_shift_succ_dx: \forall p,q,r. + Plus (succ p) q r \to Plus p (succ q) r. + intros. + lapply linear Plus_gen_succ_1 to H as H0. + decompose. + rewrite > H1. clear H1 r. + auto. +qed. + +theorem Plus_trans_1: \forall p,q1,r1. Plus p q1 r1 \to + \forall q2,r2. Plus r1 q2 r2 \to + \exists q. Plus q1 q2 q \land Plus p q r2. + intros 2; elim q1; clear q1; intros; + [ lapply linear Plus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear Plus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. rewrite > H3 in H2. clear H3 r1. + lapply linear Plus_gen_succ_1 to H2 as H0. + decompose. + rewrite > H2. clear H2 r2. + lapply linear H to H4, H3 as H0. + decompose. + ]; apply ex_intro; [| auto || auto ]. (**) +qed. + +theorem Plus_trans_2: \forall p1,q,r1. Plus p1 q r1 \to + \forall p2,r2. Plus p2 r1 r2 \to + \exists p. Plus p1 p2 p \land Plus p q r2. + intros 2; elim q; clear q; intros; + [ lapply linear Plus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p1 + | lapply linear Plus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. rewrite > H3 in H2. clear H3 r1. + lapply linear Plus_gen_succ_2 to H2 as H0. + decompose. + rewrite > H2. clear H2 r2. + lapply linear H to H4, H3 as H0. + decompose. + ]; apply ex_intro; [| auto || auto ]. (**) +qed. + +theorem Plus_conf: \forall p,q,r1. Plus p q r1 \to + \forall r2. Plus p q r2 \to r1 = r2. + intros 2. elim q; clear q; intros; + [ lapply linear Plus_gen_zero_2 to H as H0. + rewrite > H0 in H1. clear H0 p + | lapply linear Plus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. clear H3 r1. + lapply linear Plus_gen_succ_2 to H2 as H0. + decompose. + rewrite > H2. clear H2 r2. + ]; auto. +qed. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma deleted file mode 100644 index 77d6921a9..000000000 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma +++ /dev/null @@ -1,21 +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-ARITHMETICS/add_defs". - -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_fwd.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma deleted file mode 100644 index c630d3dfe..000000000 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_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-ARITHMETICS/add_fwd". - -include "nat_fwd.ma". -include "add_defs.ma". - -(* primitive generation lemmas proved by elimination and inversion *) - -theorem add_gen_O_1: \forall q,r. add O q r \to q = r. - intros. elim H; clear H q r; intros; - [ reflexivity - | clear H1. auto - ]. -qed. - -theorem add_gen_S_1: \forall p,q,r. add (S p) q r \to - \exists s. r = (S s) \land add p q s. - intros. elim H; clear H q r; intros; - [ - | clear H1. - decompose. - rewrite > H1. clear H1 n2 - ]; apply ex_intro; [| auto || auto ]. (**) -qed. - -theorem add_gen_O_2: \forall p,r. add p O r \to p = r. - intros. inversion H; clear H; intros; - [ auto - | clear H H1. - 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 - | clear H1 H3 r. - lapply linear eq_gen_S_S to H2 as H0. - rewrite > H0. clear H0 q. - apply ex_intro; [| auto ] (**) - ]. -qed. - -theorem add_gen_O_3: \forall p,q. add p q O \to p = O \land q = O. - intros. inversion H; clear H; intros; - [ rewrite < H1. clear H1 p. - auto - | clear H H1. - lapply eq_gen_O_S to H3 as H0. apply H0 - ]. -qed. - -theorem add_gen_S_3: \forall p,q,r. add p q (S r) \to - \exists s. p = S s \land add s q r \lor - q = S s \land add p s r. - intros. inversion H; clear H; intros; - [ rewrite < H1. clear H1 p - | clear H1. - lapply linear eq_gen_S_S to H3 as H0. - rewrite > H0. clear H0 r. - ]; apply ex_intro; [| auto || auto ] (**) -qed. -(* -(* alternative proofs invoking add_gen_2 *) - -variant add_gen_O_3_alt: \forall p,q. add p q O \to p = O \land q = O. - intros 2. elim q; clear q; intros; - [ lapply linear add_gen_O_2 to H as H0. - rewrite > H0. clear H0 p. - auto - | clear H. - lapply linear add_gen_S_2 to H1 as H0. - decompose. - lapply linear eq_gen_O_S to H1 as H0. apply H0 - ]. -qed. - -variant add_gen_S_3_alt: \forall p,q,r. add p q (S r) \to - \exists s. p = S s \land add s q r \lor - q = S s \land add p s r. - intros 2. elim q; clear q; intros; - [ lapply linear add_gen_O_2 to H as H0. - rewrite > H0. clear H0 p - | clear H. - lapply linear add_gen_S_2 to H1 as H0. - decompose. - lapply linear eq_gen_S_S to H1 as H0. - rewrite > H0. clear H0 r. - ]; apply ex_intro; [| auto || auto ]. (**) -qed. -*) -(* other simplification lemmas *) - -theorem add_gen_eq_2_3: \forall p,q. add p q q \to p = O. - intros 2. elim q; clear q; intros; - [ lapply linear add_gen_O_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. - decompose. - lapply linear eq_gen_S_S to H2 as H0. - rewrite < H0 in H3. clear H0 a - ]; auto. -qed. - -theorem add_gen_eq_1_3: \forall p,q. add p q p \to q = O. - intros 1. elim p; clear p; intros; - [ lapply linear add_gen_O_1 to H as H0. - rewrite > H0. clear H0 q - | lapply linear add_gen_S_1 to H1 as H0. - decompose. - lapply linear eq_gen_S_S to H2 as H0. - rewrite < H0 in H3. clear H0 a - ]; auto. -qed. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma deleted file mode 100644 index dd360676b..000000000 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma +++ /dev/null @@ -1,105 +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-ARITHMETICS/add_props". - -include "add_fwd.ma". - -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 linear add_gen_O_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. - decompose. - rewrite > H2. clear H2 r - ]; auto. -qed. - -theorem add_sym: \forall p,q,r. add p q r \to add q p r. - intros 2. elim q; clear q; - [ lapply linear add_gen_O_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. - decompose. - rewrite > H2. clear H2 r - ]; auto. -qed. - -theorem add_shift_S_sx: \forall p,q,r. add p (S q) r \to add (S p) q r. - intros. - lapply linear add_gen_S_2 to H as H0. - decompose. - rewrite > H1. clear H1 r. - auto. -qed. - -theorem add_shift_S_dx: \forall p,q,r. add (S p) q r \to add p (S q) r. - intros. - lapply linear add_gen_S_1 to H as H0. - decompose. - rewrite > H1. clear H1 r. - auto. -qed. - -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 linear add_gen_O_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. - decompose. - rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply linear add_gen_S_1 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. - lapply linear H to H4, H3 as H0. - decompose. - ]; 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 linear add_gen_O_2 to H as H0. - rewrite > H0. clear H0 p1 - | lapply linear add_gen_S_2 to H1 as H0. - decompose. - rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply linear add_gen_S_2 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. - lapply linear H to H4, H3 as H0. - decompose. - ]; 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 linear add_gen_O_2 to H as H0. - rewrite > H0 in H1. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. - decompose. - rewrite > H3. clear H3 r1. - lapply linear add_gen_S_2 to H2 as H0. - decompose. - rewrite > H2. clear H2 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 deleted file mode 100644 index 30d6cfb5c..000000000 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma +++ /dev/null @@ -1,21 +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-ARITHMETICS/nat_defs". - -include "logic/equality.ma". - -inductive nat: Set \def - | O: nat - | S: nat \to nat. diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma deleted file mode 100644 index 952a8cbf0..000000000 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.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-ARITHMETICS/nat_fwd". - -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.