From 3e6c235fa9b462ce0824ab4ac7c3a38ed8bad68c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 23 Aug 2006 07:44:24 +0000 Subject: [PATCH 1/1] changing the contribution name --- matita/contribs/RELATIONAL/BEq/BEq.ma | 24 ++++ matita/contribs/RELATIONAL/BNot/BNot.ma | 22 +++ matita/contribs/RELATIONAL/Bool/Bool.ma | 20 +++ matita/contribs/RELATIONAL/NLE/NLE.ma | 21 +++ matita/contribs/RELATIONAL/NPlus/NPlus.ma | 23 ++++ matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma | 128 ++++++++++++++++++ .../contribs/RELATIONAL/NPlus/NPlus_props.ma | 107 +++++++++++++++ matita/contribs/RELATIONAL/Nat/Nat.ma | 20 +++ matita/contribs/RELATIONAL/Nat/Nat_fwd.ma | 31 +++++ matita/contribs/RELATIONAL/makefile | 33 +++++ 10 files changed, 429 insertions(+) create mode 100644 matita/contribs/RELATIONAL/BEq/BEq.ma create mode 100644 matita/contribs/RELATIONAL/BNot/BNot.ma create mode 100644 matita/contribs/RELATIONAL/Bool/Bool.ma create mode 100644 matita/contribs/RELATIONAL/NLE/NLE.ma create mode 100644 matita/contribs/RELATIONAL/NPlus/NPlus.ma create mode 100644 matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma create mode 100644 matita/contribs/RELATIONAL/NPlus/NPlus_props.ma create mode 100644 matita/contribs/RELATIONAL/Nat/Nat.ma create mode 100644 matita/contribs/RELATIONAL/Nat/Nat_fwd.ma create mode 100644 matita/contribs/RELATIONAL/makefile diff --git a/matita/contribs/RELATIONAL/BEq/BEq.ma b/matita/contribs/RELATIONAL/BEq/BEq.ma new file mode 100644 index 000000000..3d40598f0 --- /dev/null +++ b/matita/contribs/RELATIONAL/BEq/BEq.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/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/BNot/BNot.ma b/matita/contribs/RELATIONAL/BNot/BNot.ma new file mode 100644 index 000000000..f83a3c8ca --- /dev/null +++ b/matita/contribs/RELATIONAL/BNot/BNot.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/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/Bool/Bool.ma b/matita/contribs/RELATIONAL/Bool/Bool.ma new file mode 100644 index 000000000..18f0c2c71 --- /dev/null +++ b/matita/contribs/RELATIONAL/Bool/Bool.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/matita/contribs/RELATIONAL/NLE/NLE.ma b/matita/contribs/RELATIONAL/NLE/NLE.ma new file mode 100644 index 000000000..29d15e2ab --- /dev/null +++ b/matita/contribs/RELATIONAL/NLE/NLE.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/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/NPlus/NPlus.ma b/matita/contribs/RELATIONAL/NPlus/NPlus.ma new file mode 100644 index 000000000..271bce10b --- /dev/null +++ b/matita/contribs/RELATIONAL/NPlus/NPlus.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/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/NPlus/NPlus_fwd.ma b/matita/contribs/RELATIONAL/NPlus/NPlus_fwd.ma new file mode 100644 index 000000000..d6de420e2 --- /dev/null +++ b/matita/contribs/RELATIONAL/NPlus/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/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/NPlus/NPlus_props.ma b/matita/contribs/RELATIONAL/NPlus/NPlus_props.ma new file mode 100644 index 000000000..eb580c983 --- /dev/null +++ b/matita/contribs/RELATIONAL/NPlus/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/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/Nat/Nat.ma b/matita/contribs/RELATIONAL/Nat/Nat.ma new file mode 100644 index 000000000..983731938 --- /dev/null +++ b/matita/contribs/RELATIONAL/Nat/Nat.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/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma b/matita/contribs/RELATIONAL/Nat/Nat_fwd.ma new file mode 100644 index 000000000..28c8733cb --- /dev/null +++ b/matita/contribs/RELATIONAL/Nat/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/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/makefile b/matita/contribs/RELATIONAL/makefile new file mode 100644 index 000000000..a9ac2184e --- /dev/null +++ b/matita/contribs/RELATIONAL/makefile @@ -0,0 +1,33 @@ +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