From b404a3a94c83d766923b7cbb8f8c4fb9b8002b63 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 23 Aug 2006 07:46:11 +0000 Subject: [PATCH] removing old contrib dir --- .../RELATIONAL-ARITHMETICS/BEq/BEq.ma | 24 ---- .../RELATIONAL-ARITHMETICS/BNot/BNot.ma | 22 --- .../RELATIONAL-ARITHMETICS/Bool/Bool.ma | 20 --- .../RELATIONAL-ARITHMETICS/NLE/NLE.ma | 21 --- .../RELATIONAL-ARITHMETICS/NPlus/NPlus.ma | 23 ---- .../RELATIONAL-ARITHMETICS/NPlus/NPlus_fwd.ma | 128 ------------------ .../NPlus/NPlus_props.ma | 107 --------------- .../RELATIONAL-ARITHMETICS/Nat/Nat.ma | 20 --- .../RELATIONAL-ARITHMETICS/Nat/Nat_fwd.ma | 31 ----- .../contribs/RELATIONAL-ARITHMETICS/makefile | 33 ----- 10 files changed, 429 deletions(-) delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/BEq/BEq.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/BNot/BNot.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/Bool/Bool.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/NLE/NLE.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_fwd.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_props.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat_fwd.ma delete mode 100644 matita/contribs/RELATIONAL-ARITHMETICS/makefile diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/BEq/BEq.ma b/matita/contribs/RELATIONAL-ARITHMETICS/BEq/BEq.ma deleted file mode 100644 index 3d40598f0..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/BNot/BNot.ma b/matita/contribs/RELATIONAL-ARITHMETICS/BNot/BNot.ma deleted file mode 100644 index f83a3c8ca..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/Bool/Bool.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Bool/Bool.ma deleted file mode 100644 index 18f0c2c71..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/NLE/NLE.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NLE/NLE.ma deleted file mode 100644 index 29d15e2ab..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus.ma deleted file mode 100644 index 271bce10b..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_fwd.ma deleted file mode 100644 index d6de420e2..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_props.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_props.ma deleted file mode 100644 index eb580c983..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat.ma deleted file mode 100644 index 983731938..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat_fwd.ma deleted file mode 100644 index 28c8733cb..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/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/matita/contribs/RELATIONAL-ARITHMETICS/makefile b/matita/contribs/RELATIONAL-ARITHMETICS/makefile deleted file mode 100644 index a9ac2184e..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/makefile +++ /dev/null @@ -1,33 +0,0 @@ -H=@ - -RT_BASEDIR=/home/fguidi/svn/software/matita/ -OPTIONS=-bench -MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) -CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) -CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) - -devel:=$(shell basename `pwd`) - -all: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all - -%.mo: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ -%.mo.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@ - -preall: - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -- 2.39.2