From 9ca53c3604f5816916216e7bae2de6c30d3255f7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 23 Aug 2006 07:24:43 +0000 Subject: [PATCH] new naming --- .../RELATIONAL-ARITHMETICS/{ => BEq}/BEq.ma | 9 ++-- .../RELATIONAL-ARITHMETICS/{ => BNot}/BNot.ma | 9 ++-- .../RELATIONAL-ARITHMETICS/{ => Bool}/Bool.ma | 5 +- .../RELATIONAL-ARITHMETICS/{ => NLE}/NLE.ma | 4 +- .../{ => NPlus}/NPlus.ma | 8 +-- .../{ => NPlus}/NPlus_fwd.ma | 44 ++++++++-------- .../{ => NPlus}/NPlus_props.ma | 50 +++++++++---------- .../RELATIONAL-ARITHMETICS/{ => Nat}/Nat.ma | 5 +- .../{ => Nat}/Nat_fwd.ma | 4 +- .../contribs/RELATIONAL-ARITHMETICS/makefile | 2 +- 10 files changed, 72 insertions(+), 68 deletions(-) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => BEq}/BEq.ma (86%) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => BNot}/BNot.ma (87%) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => Bool}/Bool.ma (93%) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => NLE}/NLE.ma (93%) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => NPlus}/NPlus.ma (86%) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => NPlus}/NPlus_fwd.ma (73%) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => NPlus}/NPlus_props.ma (67%) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => Nat}/Nat.ma (92%) rename matita/contribs/RELATIONAL-ARITHMETICS/{ => Nat}/Nat_fwd.ma (94%) diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma b/matita/contribs/RELATIONAL-ARITHMETICS/BEq/BEq.ma similarity index 86% rename from matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/BEq/BEq.ma index cf837aee7..3d40598f0 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/BEq/BEq.ma @@ -12,12 +12,13 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/BEq". +set "baseuri" "cic:/matita/RELATIONAL/BEq/defs". include "logic/equality.ma". -include "BNot.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. + | 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.ma b/matita/contribs/RELATIONAL-ARITHMETICS/BNot/BNot.ma similarity index 87% rename from matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/BNot/BNot.ma index 8d6405407..f83a3c8ca 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/BNot/BNot.ma @@ -12,10 +12,11 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/BNot". +set "baseuri" "cic:/matita/RELATIONAL/BNot/defs". -include "Bool.ma". +include "Bool/Bool.ma". inductive BNot: Bool \to Bool \to Prop \def - | BNot_false: BNot false true - | BNot_true : BNot true false. + | bnot_false: BNot false true + | bnot_true : BNot true false +. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Bool/Bool.ma similarity index 93% rename from matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/Bool/Bool.ma index 1d7b343fc..18f0c2c71 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/Bool/Bool.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Bool". +set "baseuri" "cic:/matita/RELATIONAL/Bool/defs". inductive Bool: Set \def | false: Bool - | true: Bool. + | true: Bool +. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NLE/NLE.ma similarity index 93% rename from matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/NLE/NLE.ma index 8e9c492c8..29d15e2ab 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/NLE/NLE.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NLE". +set "baseuri" "cic:/matita/RELATIONAL/NLE/defs". -include "Nat.ma". +include "Nat/Nat.ma". inductive NLE: Nat \to Nat \to Prop \def | NLE_zero: \forall q. NLE zero q diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus.ma similarity index 86% rename from matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus.ma index 8531c766b..271bce10b 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus". +set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs". include "logic/equality.ma". -include "Nat.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). + | 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_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_fwd.ma similarity index 73% rename from matita/contribs/RELATIONAL-ARITHMETICS/NPlus_fwd.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_fwd.ma index bb73113e3..d6de420e2 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_fwd.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_fwd.ma @@ -12,21 +12,21 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus_fwd". +set "baseuri" "cic:/matita/RELATIONAL/NPlus/fwd". -include "Nat_fwd.ma". -include "NPlus.ma". +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. +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 +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; [ @@ -36,7 +36,7 @@ theorem NPlus_gen_succ_1: \forall p,q,r. NPlus (succ p) q r \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem NPlus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r. +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. @@ -44,7 +44,7 @@ theorem NPlus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r. ]. qed. -theorem NPlus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to +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 @@ -55,7 +55,7 @@ theorem NPlus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to ]. qed. -theorem NPlus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zero. +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 @@ -64,7 +64,7 @@ theorem NPlus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zer ]. qed. -theorem NPlus_gen_succ_3: \forall p,q,r. NPlus p q (succ r) \to +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; @@ -75,28 +75,28 @@ theorem NPlus_gen_succ_3: \forall p,q,r. NPlus p q (succ r) \to ]; apply ex_intro; [| auto || auto ] (**) qed. (* -(* alternative proofs invoking NPlus_gen_2 *) +(* 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. +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. + [ 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. + 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 +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. + [ 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. + 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. @@ -105,22 +105,22 @@ qed. *) (* other simplification lemmas *) -theorem NPlus_gen_eq_2_3: \forall p,q. NPlus p q q \to p = zero. +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. + [ 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. + | 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. +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. + [ 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. + | 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 diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_props.ma similarity index 67% rename from matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_props.ma index de0de1b8a..eb580c983 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus/NPlus_props.ma @@ -12,62 +12,62 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus_props". +set "baseuri" "cic:/matita/RELATIONAL/NPlus/props". -include "NPlus_fwd.ma". +include "NPlus/NPlus_fwd.ma". -theorem NPlus_zero_1: \forall q. NPlus zero q q. +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). +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. + [ 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. + | 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. +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. + [ 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. + | 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. +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. + 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. +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. + 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 +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. + [ 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. + | 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. + lapply linear nplus_gen_succ_1 to H2 as H0. decompose. rewrite > H2. clear H2 r2. lapply linear H to H4, H3 as H0. @@ -75,16 +75,16 @@ theorem NPlus_trans_1: \forall p,q1,r1. NPlus p q1 r1 \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem NPlus_trans_2: \forall p1,q,r1. NPlus p1 q r1 \to +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. + [ 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. + | 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. + lapply linear nplus_gen_succ_2 to H2 as H0. decompose. rewrite > H2. clear H2 r2. lapply linear H to H4, H3 as H0. @@ -92,15 +92,15 @@ theorem NPlus_trans_2: \forall p1,q,r1. NPlus p1 q r1 \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem NPlus_conf: \forall p,q,r1. NPlus p q r1 \to +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. + [ 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. + | 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. + lapply linear nplus_gen_succ_2 to H2 as H0. decompose. rewrite > H2. clear H2 r2. ]; auto. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat.ma similarity index 92% rename from matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat.ma index e3721fcd4..983731938 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Nat". +set "baseuri" "cic:/matita/RELATIONAL/Nat/defs". inductive Nat: Set \def | zero: Nat - | succ: Nat \to Nat. + | succ: Nat \to Nat +. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat_fwd.ma similarity index 94% rename from matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat_fwd.ma index adfdcace4..28c8733cb 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/Nat/Nat_fwd.ma @@ -12,11 +12,11 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Nat_fwd". +set "baseuri" "cic:/matita/RELATIONAL/Nat/fwd". include "logic/equality.ma". -include "Nat.ma". +include "Nat/Nat.ma". theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P. intros. discriminate H. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/makefile b/matita/contribs/RELATIONAL-ARITHMETICS/makefile index dc30e2595..a9ac2184e 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/makefile +++ b/matita/contribs/RELATIONAL-ARITHMETICS/makefile @@ -1,6 +1,6 @@ H=@ -RT_BASEDIR=/home/fguidi/svn/trunk/helm/software/matita/ +RT_BASEDIR=/home/fguidi/svn/software/matita/ OPTIONS=-bench MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -- 2.39.2