From 3bd88fb8b932e2f76762e8068b19745167cb1ce1 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 Jan 2010 08:18:20 +0000 Subject: [PATCH] rebuilding the library --- helm/software/matita/nlibrary/basics/eq.ma | 42 +++++++++++++ .../matita/nlibrary/basics/functions.ma | 60 +++++++++++++++++++ .../matita/nlibrary/basics/relations.ma | 42 +++++++++++++ 3 files changed, 144 insertions(+) create mode 100644 helm/software/matita/nlibrary/basics/eq.ma create mode 100644 helm/software/matita/nlibrary/basics/functions.ma create mode 100644 helm/software/matita/nlibrary/basics/relations.ma diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma new file mode 100644 index 000000000..6ccfa6259 --- /dev/null +++ b/helm/software/matita/nlibrary/basics/eq.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "basics/relations.ma". + +interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). + +ntheorem reflexive_eq : ∀A:Type. reflexive A (eq A). +//; nqed. + +ntheorem symmetric_eq: ∀A:Type. symmetric A (eq A). +//; nqed. + +ntheorem transitive_eq : ∀A:Type. transitive A (eq A). +//; nqed. + +ntheorem symmetric_not_eq: ∀A:Type. symmetric A (λx,y.x ≠ y). +/2/; nqed. + +ntheorem eq_f: ∀A,B:Type.∀f:A→B.∀x,y:A. x=y → f x = f y. +//; nqed. + +(* +theorem eq_f': \forall A,B:Type.\forall f:A\to B. +\forall x,y:A. x=y \to f y = f x. +intros.elim H.apply refl_eq. +qed. *) + +ntheorem eq_f2: ∀A,B,C:Type.∀f:A→B→C. +∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2. +//; nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/basics/functions.ma b/helm/software/matita/nlibrary/basics/functions.ma new file mode 100644 index 000000000..a4a8f240d --- /dev/null +++ b/helm/software/matita/nlibrary/basics/functions.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "Plogic/equality.ma". +include "Plogic/connectives.ma". + +ndefinition compose ≝ + λA,B,C:Type.λf:B→C.λg:A→B.λx:A. + f (g x). + +interpretation "function composition" 'compose f g = (compose ? ? ? f g). + +ndefinition injective: ∀A,B:Type[0].∀ f:A→B.Prop +≝ λA,B.λf.∀x,y:A.f x = f y → x=y. + +ndefinition surjective: ∀A,B:Type[0].∀f:A→B.Prop +≝λA,B.λf.∀z:B.∃x:A.z = f x. + +ndefinition symmetric: ∀A:Type[0].∀f:A→A→A.Prop +≝ λA.λf.∀x,y.f x y = f y x. + +ndefinition symmetric2: ∀A,B:Type[0].∀f:A→A→B.Prop +≝ λA,B.λf.∀x,y.f x y = f y x. + +ndefinition associative: ∀A:Type[0].∀f:A→A→A.Prop +≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z). + +ntheorem eq_f_g_h: + ∀A,B,C,D:Type[0].∀f:C→D.∀g:B→C.∀h:A→B. + f∘(g∘h) = (f∘g)∘h. + //. +nqed. + +(* functions and relations *) +ndefinition monotonic : ∀A:Type.∀R:A→A→Prop. +∀f:A→A.Prop ≝ +λA.λR.λf.∀x,y:A.R x y → R (f x) (f y). + +(* functions and functions *) +ndefinition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop +≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z). + +ndefinition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop +≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z). + +nlemma injective_compose : ∀A,B,C,f,g. +injective A B f → injective B C g → injective A C (λx.g (f x)). +/3/. +nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/basics/relations.ma b/helm/software/matita/nlibrary/basics/relations.ma new file mode 100644 index 000000000..e70a5877a --- /dev/null +++ b/helm/software/matita/nlibrary/basics/relations.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "Plogic/connectives.ma". + +ndefinition relation : Type \to Type +≝ λA:Type.A→A→Prop. + +ndefinition reflexive: ∀A:Type.∀R :relation A.Prop +≝ λA.λR.∀x:A.R x x. + +ndefinition symmetric: ∀A:Type.∀R: relation A.Prop +≝ λA.λR.∀x,y:A.R x y → R y x. + +ndefinition transitive: ∀A:Type.∀R:relation A.Prop +≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z. + +ndefinition irreflexive: ∀A:Type.∀R:relation A.Prop +≝ λA.λR.∀x:A.¬(R x x). + +ndefinition cotransitive: ∀A:Type.∀R:relation A.Prop +≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y. + +ndefinition tight_apart: ∀A:Type.∀eq,ap:relation A.Prop +≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧ +(eq x y → ¬(ap x y)). + +ndefinition antisymmetric: ∀A:Type.∀R:relation A.Prop +≝ λA.λR.∀x,y:A. R x y → ¬(R y x). + + -- 2.39.2