From: Ferruccio Guidi Date: Wed, 23 Aug 2006 08:04:36 +0000 (+0000) Subject: new naming X-Git-Tag: make_still_working~6982 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e8c961814b55b806652b8b8243d6f56108bda9c;p=helm.git new naming --- diff --git a/helm/software/matita/contribs/RELATIONAL/BEq/BEq.ma b/helm/software/matita/contribs/RELATIONAL/BEq/BEq.ma deleted file mode 100644 index 3d40598f0..000000000 --- a/helm/software/matita/contribs/RELATIONAL/BEq/BEq.ma +++ /dev/null @@ -1,24 +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/BEq/defs". - -include "logic/equality.ma". - -include "BNot/BNot.ma". - -inductive BEq (b1:Bool): Bool \to Bool \to Prop \def - | beq_false: \forall b2. BNot b1 b2 \to BEq b1 false b2 - | beq_true : BEq b1 true b1 -. diff --git a/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma new file mode 100644 index 000000000..0b52af116 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/BEq/defs.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/BEq/defs". + +include "logic/equality.ma". + +include "BNot/defs.ma". + +inductive BEq (b1:Bool): Bool \to Bool \to Prop \def + | beq_false: \forall b2. BNot b1 b2 \to BEq b1 false b2 + | beq_true : BEq b1 true b1 +. diff --git a/helm/software/matita/contribs/RELATIONAL/BNot/BNot.ma b/helm/software/matita/contribs/RELATIONAL/BNot/BNot.ma deleted file mode 100644 index f83a3c8ca..000000000 --- a/helm/software/matita/contribs/RELATIONAL/BNot/BNot.ma +++ /dev/null @@ -1,22 +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/BNot/defs". - -include "Bool/Bool.ma". - -inductive BNot: Bool \to Bool \to Prop \def - | bnot_false: BNot false true - | bnot_true : BNot true false -. diff --git a/helm/software/matita/contribs/RELATIONAL/BNot/defs.ma b/helm/software/matita/contribs/RELATIONAL/BNot/defs.ma new file mode 100644 index 000000000..d62264513 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/BNot/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/BNot/defs". + +include "Bool/defs.ma". + +inductive BNot: Bool \to Bool \to Prop \def + | bnot_false: BNot false true + | bnot_true : BNot true false +. diff --git a/helm/software/matita/contribs/RELATIONAL/Bool/Bool.ma b/helm/software/matita/contribs/RELATIONAL/Bool/Bool.ma deleted file mode 100644 index 18f0c2c71..000000000 --- a/helm/software/matita/contribs/RELATIONAL/Bool/Bool.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/helm/software/matita/contribs/RELATIONAL/Bool/defs.ma b/helm/software/matita/contribs/RELATIONAL/Bool/defs.ma new file mode 100644 index 000000000..18f0c2c71 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/Bool/defs.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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/helm/software/matita/contribs/RELATIONAL/NLE/NLE.ma b/helm/software/matita/contribs/RELATIONAL/NLE/NLE.ma deleted file mode 100644 index 29d15e2ab..000000000 --- a/helm/software/matita/contribs/RELATIONAL/NLE/NLE.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/NLE/defs". - -include "Nat/Nat.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). diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma b/helm/software/matita/contribs/RELATIONAL/NLE/defs.ma new file mode 100644 index 000000000..19e45c3bc --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/NLE/defs.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/NLE/defs". + +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). diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus.ma deleted file mode 100644 index 271bce10b..000000000 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus.ma +++ /dev/null @@ -1,23 +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/defs". - -include "logic/equality.ma". - -include "Nat/Nat.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). diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma deleted file mode 100644 index d6de420e2..000000000 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/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/Nat_fwd.ma". -include "NPlus/NPlus.ma". - -(* primitive generation lemmas proved by elimination and inversion *) - -theorem nplus_gen_zero_1: \forall q,r. NPlus 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. - intros. elim H; clear H q r; intros; - [ - | clear H1. - decompose. - rewrite > H1. clear H1 n2 - ]; apply ex_intro; [| auto || auto ]. (**) -qed. - -theorem nplus_gen_zero_2: \forall p,r. NPlus 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 nplus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to - \exists s. r = (succ s) \land NPlus 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 nplus_gen_zero_3: \forall p,q. NPlus 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 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. - 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 nplus_gen_2 *) - -variant nplus_gen_zero_3_alt: \forall p,q. NPlus 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. - auto - | 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. 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. - intros 2. elim q; clear q; intros; - [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | clear H. - lapply linear nplus_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 nplus_gen_eq_2_3: \forall p,q. NPlus 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 - | lapply linear nplus_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 nplus_gen_eq_1_3: \forall p,q. NPlus 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 - | lapply linear nplus_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/NPlus/NPlus_props.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_props.ma deleted file mode 100644 index eb580c983..000000000 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/NPlus_props.ma +++ /dev/null @@ -1,107 +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/props". - -include "NPlus/NPlus_fwd.ma". - -theorem nplus_zero_1: \forall q. NPlus 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). - intros 2. elim q; clear q; - [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H2. clear H2 r - ]; auto. -qed. - -theorem nplus_sym: \forall p,q,r. NPlus p q r \to NPlus q p r. - intros 2. elim q; clear q; - [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H2. clear H2 r - ]; auto. -qed. - -theorem nplus_shift_succ_sx: \forall p,q,r. - NPlus p (succ q) r \to NPlus (succ p) q r. - intros. - lapply linear nplus_gen_succ_2 to H as H0. - decompose. - rewrite > H1. clear H1 r. - auto. -qed. - -theorem nplus_shift_succ_dx: \forall p,q,r. - NPlus (succ p) q r \to NPlus p (succ q) r. - intros. - lapply linear nplus_gen_succ_1 to H as H0. - decompose. - rewrite > H1. clear H1 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. - intros 2; elim q1; clear q1; intros; - [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply linear nplus_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 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. - intros 2; elim q; clear q; intros; - [ lapply linear nplus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p1 - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply linear nplus_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 nplus_conf: \forall p,q,r1. NPlus p q r1 \to - \forall r2. NPlus 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 - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. clear H3 r1. - lapply linear nplus_gen_succ_2 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. - ]; auto. -qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma new file mode 100644 index 000000000..92561bc5c --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/defs". + +include "logic/equality.ma". + +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). diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma new file mode 100644 index 000000000..bae48d405 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/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/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. NPlus 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. + intros. elim H; clear H q r; intros; + [ + | clear H1. + decompose. + rewrite > H1. clear H1 n2 + ]; apply ex_intro; [| auto || auto ]. (**) +qed. + +theorem nplus_gen_zero_2: \forall p,r. NPlus 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 nplus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to + \exists s. r = (succ s) \land NPlus 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 nplus_gen_zero_3: \forall p,q. NPlus 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 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. + 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 nplus_gen_2 *) + +variant nplus_gen_zero_3_alt: \forall p,q. NPlus 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. + auto + | 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. 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. + intros 2. elim q; clear q; intros; + [ lapply linear nplus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | clear H. + lapply linear nplus_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 nplus_gen_eq_2_3: \forall p,q. NPlus 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 + | lapply linear nplus_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 nplus_gen_eq_1_3: \forall p,q. NPlus 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 + | lapply linear nplus_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/NPlus/props.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma new file mode 100644 index 000000000..56146a3bf --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/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/NPlus/props". + +include "NPlus/fwd.ma". + +theorem nplus_zero_1: \forall q. NPlus 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). + intros 2. elim q; clear q; + [ lapply linear nplus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear nplus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H2. clear H2 r + ]; auto. +qed. + +theorem nplus_sym: \forall p,q,r. NPlus p q r \to NPlus q p r. + intros 2. elim q; clear q; + [ lapply linear nplus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear nplus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H2. clear H2 r + ]; auto. +qed. + +theorem nplus_shift_succ_sx: \forall p,q,r. + NPlus p (succ q) r \to NPlus (succ p) q r. + intros. + lapply linear nplus_gen_succ_2 to H as H0. + decompose. + rewrite > H1. clear H1 r. + auto. +qed. + +theorem nplus_shift_succ_dx: \forall p,q,r. + NPlus (succ p) q r \to NPlus p (succ q) r. + intros. + lapply linear nplus_gen_succ_1 to H as H0. + decompose. + rewrite > H1. clear H1 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. + intros 2; elim q1; clear q1; intros; + [ lapply linear nplus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear nplus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. rewrite > H3 in H2. clear H3 r1. + lapply linear nplus_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 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. + intros 2; elim q; clear q; intros; + [ lapply linear nplus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p1 + | lapply linear nplus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. rewrite > H3 in H2. clear H3 r1. + lapply linear nplus_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 nplus_conf: \forall p,q,r1. NPlus p q r1 \to + \forall r2. NPlus 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 + | lapply linear nplus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. clear H3 r1. + lapply linear nplus_gen_succ_2 to H2 as H0. + decompose. + rewrite > H2. clear H2 r2. + ]; auto. +qed. diff --git a/helm/software/matita/contribs/RELATIONAL/Nat/Nat.ma b/helm/software/matita/contribs/RELATIONAL/Nat/Nat.ma deleted file mode 100644 index 983731938..000000000 --- a/helm/software/matita/contribs/RELATIONAL/Nat/Nat.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/helm/software/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma b/helm/software/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma deleted file mode 100644 index 28c8733cb..000000000 --- a/helm/software/matita/contribs/RELATIONAL/Nat/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/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/Nat/defs.ma b/helm/software/matita/contribs/RELATIONAL/Nat/defs.ma new file mode 100644 index 000000000..983731938 --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/Nat/defs.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma b/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma new file mode 100644 index 000000000..09847de2e --- /dev/null +++ b/helm/software/matita/contribs/RELATIONAL/Nat/fwd.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 (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.