From d9824956d9132109ed5f23380a0a1f9c5181d18a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 26 Feb 2021 20:42:23 +0100 Subject: [PATCH] removing old contribs + RELATIONAL + ONAG --- matita/matita/contribs/ONAG/game.ma | 46 ------- matita/matita/contribs/ONAG/notation.ma | 19 --- matita/matita/contribs/ONAG/root | 1 - matita/matita/contribs/ONAG/test.ma | 39 ------ matita/matita/contribs/RELATIONAL/Makefile | 16 --- matita/matita/contribs/RELATIONAL/NLE/defs.ma | 40 ------ matita/matita/contribs/RELATIONAL/NLE/inv.ma | 40 ------ .../matita/contribs/RELATIONAL/NLE/nplus.ma | 27 ---- .../matita/contribs/RELATIONAL/NLE/order.ma | 52 -------- .../matita/contribs/RELATIONAL/NLE/props.ma | 31 ----- .../matita/contribs/RELATIONAL/NPlus/defs.ma | 27 ---- .../matita/contribs/RELATIONAL/NPlus/fun.ma | 40 ------ .../matita/contribs/RELATIONAL/NPlus/inv.ma | 81 ------------ .../contribs/RELATIONAL/NPlus/monoid.ma | 121 ------------------ .../contribs/RELATIONAL/NPlusList/defs.ma | 38 ------ .../contribs/RELATIONAL/NPlusList/props.ma | 34 ----- matita/matita/contribs/RELATIONAL/ZEq/defs.ma | 26 ---- .../matita/contribs/RELATIONAL/ZEq/setoid.ma | 37 ------ .../contribs/RELATIONAL/datatypes/Bool.ma | 22 ---- .../contribs/RELATIONAL/datatypes/List.ma | 39 ------ .../contribs/RELATIONAL/datatypes/Nat.ma | 22 ---- .../contribs/RELATIONAL/datatypes/Zah.ma | 19 --- matita/matita/contribs/RELATIONAL/depends | 21 --- matita/matita/contribs/RELATIONAL/preamble.ma | 19 --- matita/matita/contribs/RELATIONAL/root | 1 - 25 files changed, 858 deletions(-) delete mode 100644 matita/matita/contribs/ONAG/game.ma delete mode 100644 matita/matita/contribs/ONAG/notation.ma delete mode 100644 matita/matita/contribs/ONAG/root delete mode 100644 matita/matita/contribs/ONAG/test.ma delete mode 100644 matita/matita/contribs/RELATIONAL/Makefile delete mode 100644 matita/matita/contribs/RELATIONAL/NLE/defs.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NLE/inv.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NLE/nplus.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NLE/order.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NLE/props.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NPlus/defs.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NPlus/fun.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NPlus/inv.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NPlus/monoid.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NPlusList/defs.ma delete mode 100644 matita/matita/contribs/RELATIONAL/NPlusList/props.ma delete mode 100644 matita/matita/contribs/RELATIONAL/ZEq/defs.ma delete mode 100644 matita/matita/contribs/RELATIONAL/ZEq/setoid.ma delete mode 100644 matita/matita/contribs/RELATIONAL/datatypes/Bool.ma delete mode 100644 matita/matita/contribs/RELATIONAL/datatypes/List.ma delete mode 100644 matita/matita/contribs/RELATIONAL/datatypes/Nat.ma delete mode 100644 matita/matita/contribs/RELATIONAL/datatypes/Zah.ma delete mode 100644 matita/matita/contribs/RELATIONAL/depends delete mode 100644 matita/matita/contribs/RELATIONAL/preamble.ma delete mode 100644 matita/matita/contribs/RELATIONAL/root diff --git a/matita/matita/contribs/ONAG/game.ma b/matita/matita/contribs/ONAG/game.ma deleted file mode 100644 index 32da35bb1..000000000 --- a/matita/matita/contribs/ONAG/game.ma +++ /dev/null @@ -1,46 +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 *) -(* *) -(**************************************************************************) - -(* ON NUMBERS AND GAMES: MATITA SOURCE FILES - * Invocation: - * - Patience on me to gain peace and perfection! - - * 2012 May 25: - * specification starts. - *) - -include "basics/pts.ma". -include "notation.ma". - -(* GAMES ********************************************************************) - -inductive Game: Type[1] ≝ -| game: ∀L,R:Type[0]. (L → Game) → (R → Game) → Game -. - -interpretation "game" 'Game = Game. -(* -notation > - "'Let' term 46 g ≡ { L , l | R , r } 'in' term 46 t" - non associative with precedence 46 - for @{ 'Destructor (match $g with [ game ${ident L} ${ident R} ${ident l} ${ident r} ⇒ $t]) }. -*) -interpretation "game destructor" 'Destructor x = x. - -definition pippo ≝ λx. -match x with [ game L R F G ⇒ x ]. - -(* -notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46 - for @{ match $e return $T with [ true ⇒ $t | false ⇒ $f] }. -*) \ No newline at end of file diff --git a/matita/matita/contribs/ONAG/notation.ma b/matita/matita/contribs/ONAG/notation.ma deleted file mode 100644 index 1dacc850e..000000000 --- a/matita/matita/contribs/ONAG/notation.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR ONAG ********************************************************) - -notation "𝔾" - non associative with precedence 90 - for @{ 'Game }. diff --git a/matita/matita/contribs/ONAG/root b/matita/matita/contribs/ONAG/root deleted file mode 100644 index 7fc7f48ce..000000000 --- a/matita/matita/contribs/ONAG/root +++ /dev/null @@ -1 +0,0 @@ -baseuri=cic:/matita/ONAG/ diff --git a/matita/matita/contribs/ONAG/test.ma b/matita/matita/contribs/ONAG/test.ma deleted file mode 100644 index 1f4fac570..000000000 --- a/matita/matita/contribs/ONAG/test.ma +++ /dev/null @@ -1,39 +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 *) -(* *) -(**************************************************************************) - -universe constraint Type[0] < Type[1]. - -notation "hvbox(a break \to b)" - right associative with precedence 20 -for @{ \forall $_:$a.$b }. - -notation "hvbox( * )" - non associative with precedence 90 - for @{ 'B }. - -inductive l: Type[0] ≝ L: l. - -inductive g: Type[0] ≝ G: g. - -axiom f: l → Prop. - -interpretation "b" 'B = L. - -interpretation "b" 'B = G. - -(* FG: two interpretations of the same notation and with the same description - override eachother, so the description is not just informative -*) - -axiom s: f *. diff --git a/matita/matita/contribs/RELATIONAL/Makefile b/matita/matita/contribs/RELATIONAL/Makefile deleted file mode 100644 index a3e891435..000000000 --- a/matita/matita/contribs/RELATIONAL/Makefile +++ /dev/null @@ -1,16 +0,0 @@ -include ../Makefile.defs - -DIR=$(shell basename $$PWD) - -$(DIR) all: - $(BIN)matitac -$(DIR).opt opt all.opt: - $(BIN)matitac.opt -clean: - $(BIN)matitaclean -clean.opt: - $(BIN)matitaclean.opt -depend: - $(BIN)matitadep -depend.opt: - $(BIN)matitadep.opt diff --git a/matita/matita/contribs/RELATIONAL/NLE/defs.ma b/matita/matita/contribs/RELATIONAL/NLE/defs.ma deleted file mode 100644 index 535b717aa..000000000 --- a/matita/matita/contribs/RELATIONAL/NLE/defs.ma +++ /dev/null @@ -1,40 +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 *) -(* *) -(**************************************************************************) - - - -include "NPlus/defs.ma". - -inductive NLE: Nat \to Nat \to Prop \def - | nle_zero_1: \forall q. NLE zero q - | nle_succ_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q) -. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "natural 'greater or equal to'" 'geq y x= - (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y). - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "natural 'greater than'" 'gt y x = - (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) - (cic:/matita/RELATIONAL/datatypes/Nat/Nat.ind#xpointer(1/1/2) x) y). - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "natural 'less or equal to'" 'leq x y = - (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y). - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "natural 'less than'" 'lt x y = - (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) - (cic:/matita/RELATIONAL/datatypes/Nat/Nat.ind#xpointer(1/1/2) x) y). diff --git a/matita/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/matita/contribs/RELATIONAL/NLE/inv.ma deleted file mode 100644 index 649a5b8a4..000000000 --- a/matita/matita/contribs/RELATIONAL/NLE/inv.ma +++ /dev/null @@ -1,40 +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 *) -(* *) -(**************************************************************************) - - - -include "NLE/defs.ma". - -theorem nle_inv_succ_1: ∀x,y. x < y → - ∃z. y = succ z ∧ x ≤ z. - intros; inversion H; clear H; intros; destruct. autobatch. -qed. - -theorem nle_inv_succ_succ: ∀x,y. x < succ y → x ≤ y. - intros; inversion H; clear H; intros; destruct. autobatch. -qed. - -theorem nle_inv_succ_zero: ∀x. x < zero → False. - intros. inversion H; clear H; intros; destruct. -qed. - -theorem nle_inv_zero_2: ∀x. x ≤ zero → x = zero. - intros; inversion H; clear H; intros; destruct. autobatch. -qed. - -theorem nle_inv_succ_2: ∀y,x. x ≤ succ y → - x = zero ∨ ∃z. x = succ z ∧ z ≤ y. - intros; inversion H; clear H; intros; destruct; - autobatch depth = 4. -qed. diff --git a/matita/matita/contribs/RELATIONAL/NLE/nplus.ma b/matita/matita/contribs/RELATIONAL/NLE/nplus.ma deleted file mode 100644 index 22998c038..000000000 --- a/matita/matita/contribs/RELATIONAL/NLE/nplus.ma +++ /dev/null @@ -1,27 +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 *) -(* *) -(**************************************************************************) - - - -include "NLE/defs.ma". - -theorem nle_nplus: ∀p, q, r. p ⊕ q ≍ r → q ≤ r. - intros; elim H; clear H q r; autobatch. -qed. - -axiom nle_nplus_comp: ∀x1,x2,x3. x1 ⊕ x2 ≍ x3 → ∀y1,y2,y3. y1 ⊕ y2 ≍ y3 → - x1 ≤ y1 → x2 ≤ y2 → x3 ≤ y3. - -axiom nle_nplus_comp_lt_2: ∀x1,x2,x3. x1 ⊕ x2 ≍ x3 → ∀y1,y2,y3. y1 ⊕ y2 ≍ y3 → - x1 ≤ y1 → x2 < y2 → x3 < y3. diff --git a/matita/matita/contribs/RELATIONAL/NLE/order.ma b/matita/matita/contribs/RELATIONAL/NLE/order.ma deleted file mode 100644 index 473ac601d..000000000 --- a/matita/matita/contribs/RELATIONAL/NLE/order.ma +++ /dev/null @@ -1,52 +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 *) -(* *) -(**************************************************************************) - - - -include "NLE/inv.ma". - -theorem nle_refl: ∀x. x ≤ x. - intros; elim x; clear x; autobatch. -qed. - -theorem nle_trans: ∀x,y. x ≤ y → ∀z. y ≤ z → x ≤ z. - intros 3; elim H; clear H x y; - [ autobatch - | lapply linear nle_inv_succ_1 to H3. decompose. destruct. - autobatch - ]. -qed. - -theorem nle_false: ∀x,y. x ≤ y → y < x → False. - intros 3; elim H; clear H x y; autobatch. -qed. - -theorem nle_irrefl: ∀x. x < x → False. - intros. autobatch. -qed. - -theorem nle_irrefl_ei: ∀x, z. z ≤ x → z = succ x → False. - intros 3; elim H; clear H x z; destruct; autobatch. -qed. - -theorem nle_irrefl_smart: ∀x. x < x → False. - intros 1. elim x; clear x; autobatch. -qed. - -theorem nle_lt_or_eq: ∀y, x. x ≤ y → x < y ∨ x = y. - intros; elim H; clear H x y; - [ elim n; clear n - | decompose - ]; autobatch. -qed. diff --git a/matita/matita/contribs/RELATIONAL/NLE/props.ma b/matita/matita/contribs/RELATIONAL/NLE/props.ma deleted file mode 100644 index ba563b7af..000000000 --- a/matita/matita/contribs/RELATIONAL/NLE/props.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 *) -(* *) -(**************************************************************************) - - - -include "NLE/order.ma". - -theorem nle_trans_succ: ∀x,y. x ≤ y → x ≤ succ y. - intros; elim H; clear H x y; autobatch. -qed. - -theorem nle_gt_or_le: ∀x, y. y > x ∨ y ≤ x. - intros 2; elim y; clear y; - [ autobatch - | decompose; - [ lapply linear nle_inv_succ_1 to H1 - | lapply linear nle_lt_or_eq to H1 - ]; decompose; destruct; autobatch depth = 4 - ]. -qed. diff --git a/matita/matita/contribs/RELATIONAL/NPlus/defs.ma b/matita/matita/contribs/RELATIONAL/NPlus/defs.ma deleted file mode 100644 index 15a16b72c..000000000 --- a/matita/matita/contribs/RELATIONAL/NPlus/defs.ma +++ /dev/null @@ -1,27 +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 *) -(* *) -(**************************************************************************) - - - -include "datatypes/Nat.ma". - -inductive NPlus (p:Nat): Nat → Nat → Prop ≝ - | nplus_zero_2: NPlus p zero p - | nplus_succ_2: ∀q, r. NPlus p q r → NPlus p (succ q) (succ r). - -interpretation "natural plus predicate" 'rel_plus x y z = (NPlus x y z). - -notation "hvbox(a break ⊕ b break ≍ c)" - non associative with precedence 45 -for @{'rel_plus $a $b $c}. diff --git a/matita/matita/contribs/RELATIONAL/NPlus/fun.ma b/matita/matita/contribs/RELATIONAL/NPlus/fun.ma deleted file mode 100644 index 4fcdab720..000000000 --- a/matita/matita/contribs/RELATIONAL/NPlus/fun.ma +++ /dev/null @@ -1,40 +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 *) -(* *) -(**************************************************************************) - - - -include "NPlus/inv.ma". - -(* Functional properties ****************************************************) - -theorem nplus_total: ∀p,q. ∃r. p ⊕ q ≍ r. - intros; elim q; clear q; - [ autobatch | decompose; autobatch ]. -qed. - -theorem nplus_mono: ∀p,q,r1. p ⊕ q ≍ r1 → - ∀r2. p ⊕ q ≍ r2 → r1 = r2. - intros 4; elim H; clear H q r1; - [ lapply linear nplus_inv_zero_2 to H1 - | lapply linear nplus_inv_succ_2 to H3. decompose - ]; destruct; autobatch. -qed. - -theorem nplus_inj_1: ∀p1, q, r. p1 ⊕ q ≍ r → - ∀p2. p2 ⊕ q ≍ r → p2 = p1. - intros 4; elim H; clear H q r; - [ lapply linear nplus_inv_zero_2 to H1 - | lapply linear nplus_inv_succ_2_3 to H3 - ]; autobatch. -qed. diff --git a/matita/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/matita/contribs/RELATIONAL/NPlus/inv.ma deleted file mode 100644 index cfba0a843..000000000 --- a/matita/matita/contribs/RELATIONAL/NPlus/inv.ma +++ /dev/null @@ -1,81 +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 *) -(* *) -(**************************************************************************) - - - -include "NPlus/defs.ma". - -(* Inversion lemmas *********************************************************) - -theorem nplus_inv_zero_1: ∀q,r. zero ⊕ q ≍ r → q = r. - intros. elim H; clear H q r; autobatch. -qed. - -theorem nplus_inv_succ_1: ∀p,q,r. succ p ⊕ q ≍ r → - ∃s. r = succ s ∧ p ⊕ q ≍ s. - intros. elim H; clear H q r; intros; - [ autobatch depth = 3 - | clear H1; decompose; destruct; autobatch depth = 4 - ] -qed. - -theorem nplus_inv_zero_2: ∀p,r. p ⊕ zero ≍ r → p = r. - intros; inversion H; clear H; intros; destruct; autobatch. -qed. - -theorem nplus_inv_succ_2: ∀p,q,r. p ⊕ succ q ≍ r → - ∃s. r = succ s ∧ p ⊕ q ≍ s. - intros; inversion H; clear H; intros; destruct. - autobatch depth = 3. -qed. - -theorem nplus_inv_zero_3: ∀p,q. p ⊕ q ≍ zero → - p = zero ∧ q = zero. - intros; inversion H; clear H; intros; destruct; autobatch. -qed. - -theorem nplus_inv_succ_3: ∀p,q,r. p ⊕ q ≍ succ r → - ∃s. p = succ s ∧ s ⊕ q ≍ r ∨ - q = succ s ∧ p ⊕ s ≍ r. - intros; inversion H; clear H; intros; destruct; - autobatch depth = 4. -qed. - -(* Corollaries to inversion lemmas ******************************************) - -theorem nplus_inv_succ_2_3: ∀p,q,r. - p ⊕ succ q ≍ succ r → p ⊕ q ≍ r. - intros; - lapply linear nplus_inv_succ_2 to H; decompose; destruct; autobatch. -qed. - -theorem nplus_inv_succ_1_3: ∀p,q,r. - succ p ⊕ q ≍ succ r → p ⊕ q ≍ r. - intros; - lapply linear nplus_inv_succ_1 to H; decompose; destruct; autobatch. -qed. - -theorem nplus_inv_eq_2_3: ∀p,q. p ⊕ q ≍ q → p = zero. - intros 2; elim q; clear q; - [ lapply linear nplus_inv_zero_2 to H - | lapply linear nplus_inv_succ_2_3 to H1 - ]; autobatch. -qed. - -theorem nplus_inv_eq_1_3: ∀p,q. p ⊕ q ≍ p → q = zero. - intros 1; elim p; clear p; - [ lapply linear nplus_inv_zero_1 to H - | lapply linear nplus_inv_succ_1_3 to H1 - ]; autobatch. -qed. diff --git a/matita/matita/contribs/RELATIONAL/NPlus/monoid.ma b/matita/matita/contribs/RELATIONAL/NPlus/monoid.ma deleted file mode 100644 index 7a9bb8da0..000000000 --- a/matita/matita/contribs/RELATIONAL/NPlus/monoid.ma +++ /dev/null @@ -1,121 +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 *) -(* *) -(**************************************************************************) - - - -include "NPlus/fun.ma". - -(* Monoidal properties ******************************************************) - -theorem nplus_zero_1: ∀q. zero ⊕ q ≍ q. - intros; elim q; clear q; autobatch. -qed. - -theorem nplus_succ_1: ∀p,q,r. p ⊕ q ≍ r → succ p ⊕ q ≍ succ r. - intros; elim H; clear H q r; autobatch. -qed. - -theorem nplus_comm: ∀p, q, x. p ⊕ q ≍ x → ∀y. q ⊕ p ≍ y → x = y. - intros 4; elim H; clear H q x; - [ lapply linear nplus_inv_zero_1 to H1 - | lapply linear nplus_inv_succ_1 to H3. decompose - ]; destruct; autobatch. -qed. - -theorem nplus_comm_rew: ∀p,q,r. p ⊕ q ≍ r → q ⊕ p ≍ r. - intros; elim H; clear H q r; autobatch. -qed. - -theorem nplus_ass: ∀p1, p2, r1. p1 ⊕ p2 ≍ r1 → ∀p3, s1. r1 ⊕ p3 ≍ s1 → - ∀r3. p2 ⊕ p3 ≍ r3 → ∀s3. p1 ⊕ r3 ≍ s3 → s1 = s3. - intros 4; elim H; clear H p2 r1; - [ lapply linear nplus_inv_zero_1 to H2. destruct. - lapply nplus_mono to H1, H3. destruct. autobatch - | lapply linear nplus_inv_succ_1 to H3. decompose. destruct. - lapply linear nplus_inv_succ_1 to H4. decompose. destruct. - lapply linear nplus_inv_succ_2 to H5. decompose. destruct. autobatch - ]. -qed. - -(* Corollaries of functional properties **************************************) - -theorem nplus_inj_2: ∀p, q1, r. p ⊕ q1 ≍ r → ∀q2. p ⊕ q2 ≍ r → q1 = q2. - intros. autobatch. -qed. - -(* Corollaries of nonoidal properties ***************************************) - -theorem nplus_comm_1: ∀p1, q, r1. p1 ⊕ q ≍ r1 → ∀p2, r2. p2 ⊕ q ≍ r2 → - ∀x. p2 ⊕ r1 ≍ x → ∀y. p1 ⊕ r2 ≍ y → x = y. - intros 4; elim H; clear H q r1; - [ lapply linear nplus_inv_zero_2 to H1 - | lapply linear nplus_inv_succ_2 to H3. - lapply linear nplus_inv_succ_2 to H4. decompose. destruct. - lapply linear nplus_inv_succ_2 to H5. decompose - ]; destruct; autobatch. -qed. - -theorem nplus_comm_1_rew: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ q ≍ r2 → - ∀s. p1 ⊕ r2 ≍ s → p2 ⊕ r1 ≍ s. - intros 4; elim H; clear H q r1; - [ lapply linear nplus_inv_zero_2 to H1. destruct - | lapply linear nplus_inv_succ_2 to H3. decompose. destruct. - lapply linear nplus_inv_succ_2 to H4. decompose. destruct - ]; autobatch. -qed. - -(* -theorem nplus_shift_succ_sx: \forall p,q,r. - (p \oplus (succ q) \asymp r) \to (succ p) \oplus q \asymp r. - intros. - lapply linear nplus_inv_succ_2 to H as H0. - decompose. destruct. auto new timeout=100. -qed. - -theorem nplus_shift_succ_dx: \forall p,q,r. - ((succ p) \oplus q \asymp r) \to p \oplus (succ q) \asymp r. - intros. - lapply linear nplus_inv_succ_1 to H as H0. - decompose. destruct. auto new timeout=100. -qed. - -theorem nplus_trans_1: \forall p,q1,r1. (p \oplus q1 \asymp r1) \to - \forall q2,r2. (r1 \oplus q2 \asymp r2) \to - \exists q. (q1 \oplus q2 \asymp q) \land p \oplus q \asymp r2. - intros 2; elim q1; clear q1; intros; - [ lapply linear nplus_inv_zero_2 to H as H0. - destruct. - | lapply linear nplus_inv_succ_2 to H1 as H0. - decompose. destruct. - lapply linear nplus_inv_succ_1 to H2 as H0. - decompose. destruct. - lapply linear H to H4, H3 as H0. - decompose. - ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) -qed. - -theorem nplus_trans_2: ∀p1,q,r1. p1 ⊕ q ≍ r1 → ∀p2,r2. p2 ⊕ r1 ≍ r2 → - ∃p. p1 ⊕ p2 ≍ p ∧ p ⊕ q ≍ r2. - intros 2; elim q; clear q; intros; - [ lapply linear nplus_inv_zero_2 to H as H0. - destruct - | lapply linear nplus_inv_succ_2 to H1 as H0. - decompose. destruct. - lapply linear nplus_inv_succ_2 to H2 as H0. - decompose. destruct. - lapply linear H to H4, H3 as H0. - decompose. - ]; autobatch. apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) -qed. -*) diff --git a/matita/matita/contribs/RELATIONAL/NPlusList/defs.ma b/matita/matita/contribs/RELATIONAL/NPlusList/defs.ma deleted file mode 100644 index cac07f91a..000000000 --- a/matita/matita/contribs/RELATIONAL/NPlusList/defs.ma +++ /dev/null @@ -1,38 +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 *) -(* *) -(**************************************************************************) - - - -include "datatypes/List.ma". -include "NPlus/defs.ma". - - -inductive NPlusList: (List Nat) \to Nat \to Prop \def - | nplus_nil: NPlusList (nil ?) zero - | nplus_cons: \forall l,p,q,r. - NPlusList l p \to NPlus p q r \to NPlusList (cons ? l q) r -. - -definition NPlusListEq: (List Nat) \to (List Nat) \to Prop \def - \lambda ns1,ns2. \exists n. NPlusList ns1 n \land NPlusList ns2 n. - -(* -(*CSC: the URI must disappear: there is a bug now *) -interpretation "ternary natural plus predicate" 'rel_plus3 x y z = - (cic:/matita/RELATIONAL/NPlus/defs/NPlus3.con w x y z). - -notation "hvbox(a break + b break + c == d)" - non associative with precedence 95 -for @{ 'rel_plus3 $a $b $c $d}. -*) diff --git a/matita/matita/contribs/RELATIONAL/NPlusList/props.ma b/matita/matita/contribs/RELATIONAL/NPlusList/props.ma deleted file mode 100644 index 4b70088a2..000000000 --- a/matita/matita/contribs/RELATIONAL/NPlusList/props.ma +++ /dev/null @@ -1,34 +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 *) -(* *) -(**************************************************************************) - - - -include "NPlusList/defs.ma". -(* -axiom npluslist_gen_cons: \forall l,q,r. - NPlusList (cons ? l q) r \to - \exists p. NPlusList l p \land NPlus p q r. -(* - intros. inversion H; clear H; intros; - [ id - | destruct. -*) - -theorem npluslist_inj_2: \forall ns1,ns2,n. - NPlusListEq (cons ? ns1 n) (cons ? ns2 n) \to - NPlusListEq ns1 ns2. - unfold NPlusListEq. intros. decompose. - lapply linear npluslist_gen_cons to H. decompose. - lapply linear npluslist_gen_cons to H2. decompose. -*) \ No newline at end of file diff --git a/matita/matita/contribs/RELATIONAL/ZEq/defs.ma b/matita/matita/contribs/RELATIONAL/ZEq/defs.ma deleted file mode 100644 index 0fa85f7f0..000000000 --- a/matita/matita/contribs/RELATIONAL/ZEq/defs.ma +++ /dev/null @@ -1,26 +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 *) -(* *) -(**************************************************************************) - - - -include "datatypes/Zah.ma". -include "NPlus/defs.ma". - -inductive ZEq: Zah → Zah → Prop := - | zeq: ∀m1,m2,m3,m4,n. m1 ⊕ m4 ≍ n → m3 ⊕ m2 ≍ n → - ZEq 〈m1,m2〉 〈m3, m4〉 -. - -interpretation "integer equality" 'napart x y = (ZEq x y). - diff --git a/matita/matita/contribs/RELATIONAL/ZEq/setoid.ma b/matita/matita/contribs/RELATIONAL/ZEq/setoid.ma deleted file mode 100644 index 03075bb75..000000000 --- a/matita/matita/contribs/RELATIONAL/ZEq/setoid.ma +++ /dev/null @@ -1,37 +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 *) -(* *) -(**************************************************************************) - - - -include "NPlus/fun.ma". -include "ZEq/defs.ma". - -theorem zeq_refl: ∀z. z ≈ z. - intros; elim z. clear z. - lapply (nplus_total a b); decompose; - autobatch. -qed. - -theorem zeq_sym: ∀z1,z2. z1 ≈ z2 → z2 ≈ z1. - intros; elim H; clear H z1 z2; autobatch. -qed. -(* -theorem zeq_trans: \forall z1,z2. z1 = z2 \to - \forall z3. z2 = z3 \to z1 = z3. - intros 3. elim H. clear H z1 z2. - inversion H3. clear H3. intros. destruct. - lapply (nplus_total n5 n6). decompose. - lapply (nplus_total n4 n9). decompose. - apply zeq. -*) diff --git a/matita/matita/contribs/RELATIONAL/datatypes/Bool.ma b/matita/matita/contribs/RELATIONAL/datatypes/Bool.ma deleted file mode 100644 index 970d6694c..000000000 --- a/matita/matita/contribs/RELATIONAL/datatypes/Bool.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 *) -(* *) -(**************************************************************************) - - - -include "preamble.ma". - -inductive Bool: Type \def - | false: Bool - | true : Bool -. diff --git a/matita/matita/contribs/RELATIONAL/datatypes/List.ma b/matita/matita/contribs/RELATIONAL/datatypes/List.ma deleted file mode 100644 index fc989d376..000000000 --- a/matita/matita/contribs/RELATIONAL/datatypes/List.ma +++ /dev/null @@ -1,39 +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 *) -(* *) -(**************************************************************************) - - - -include "preamble.ma". - -inductive List (A: Type): Type \def - | nil: List A - | cons: List A \to A \to List A -. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "nil" 'nil = - (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/1) ?). - -notation "hvbox([])" - non associative with precedence 95 -for @{ 'nil }. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "right cons" 'rcons x y = - (cic:/matita/RELATIONAL/datatypes/List/List.ind#xpointer(1/2) ? x y). - -notation "hvbox([a break @ b])" - non associative with precedence 95 -for @{ 'rcons $a $b}. - diff --git a/matita/matita/contribs/RELATIONAL/datatypes/Nat.ma b/matita/matita/contribs/RELATIONAL/datatypes/Nat.ma deleted file mode 100644 index ed45a35fe..000000000 --- a/matita/matita/contribs/RELATIONAL/datatypes/Nat.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 *) -(* *) -(**************************************************************************) - - - -include "preamble.ma". - -inductive Nat: Type \def - | zero: Nat - | succ: Nat \to Nat -. diff --git a/matita/matita/contribs/RELATIONAL/datatypes/Zah.ma b/matita/matita/contribs/RELATIONAL/datatypes/Zah.ma deleted file mode 100644 index 45ce72c56..000000000 --- a/matita/matita/contribs/RELATIONAL/datatypes/Zah.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - - - -include "datatypes/Nat.ma". - -definition Zah \def Nat \times Nat. diff --git a/matita/matita/contribs/RELATIONAL/depends b/matita/matita/contribs/RELATIONAL/depends deleted file mode 100644 index 9d79219ac..000000000 --- a/matita/matita/contribs/RELATIONAL/depends +++ /dev/null @@ -1,21 +0,0 @@ -preamble.ma datatypes/constructors.ma logic/connectives.ma logic/equality.ma -datatypes/Nat.ma preamble.ma -datatypes/Zah.ma datatypes/Nat.ma -datatypes/List.ma preamble.ma -datatypes/Bool.ma preamble.ma -ZEq/setoid.ma NPlus/fun.ma ZEq/defs.ma -ZEq/defs.ma NPlus/defs.ma datatypes/Zah.ma -NLE/nplus.ma NLE/defs.ma -NLE/props.ma NLE/order.ma -NLE/inv.ma NLE/defs.ma -NLE/defs.ma NPlus/defs.ma datatypes/Nat.ma -NLE/order.ma NLE/inv.ma -NPlusList/props.ma NPlusList/defs.ma -NPlusList/defs.ma NPlus/defs.ma datatypes/List.ma -NPlus/inv.ma NPlus/defs.ma -NPlus/monoid.ma NPlus/fun.ma -NPlus/defs.ma datatypes/Nat.ma -NPlus/fun.ma NPlus/inv.ma -datatypes/constructors.ma -logic/connectives.ma -logic/equality.ma diff --git a/matita/matita/contribs/RELATIONAL/preamble.ma b/matita/matita/contribs/RELATIONAL/preamble.ma deleted file mode 100644 index e030ad1ad..000000000 --- a/matita/matita/contribs/RELATIONAL/preamble.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - - - -include "logic/equality.ma". -include "logic/connectives.ma". -include "datatypes/constructors.ma". diff --git a/matita/matita/contribs/RELATIONAL/root b/matita/matita/contribs/RELATIONAL/root deleted file mode 100644 index eadc56b03..000000000 --- a/matita/matita/contribs/RELATIONAL/root +++ /dev/null @@ -1 +0,0 @@ -baseuri=cic:/matita/RELATIONAL -- 2.39.2