rebuilding the library

diff --git a/helm/software/matita/nlibrary/basics/eq.ma b/helm/software/matita/nlibrary/basics/eq.ma
new file mode 100644 (file)
index 0000000..6ccfa62
--- /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 (file)
index 0000000..a4a8f24
--- /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 (file)
index 0000000..e70a587
--- /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).
+
+