helm/software/matita/nlibrary/basics/functions.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "Plogic/equality.ma".
  16 include "Plogic/connectives.ma".
  17
  18 ndefinition compose ≝
  19   λA,B,C:Type.λf:B→C.λg:A→B.λx:A.
  20   f (g x).
  21
  22 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
  23
  24 ndefinition injective: ∀A,B:Type[0].∀ f:A→B.Prop
  25 ≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
  26
  27 ndefinition surjective: ∀A,B:Type[0].∀f:A→B.Prop
  28 ≝λA,B.λf.∀z:B.∃x:A.z = f x.
  29
  30 ndefinition symmetric: ∀A:Type[0].∀f:A→A→A.Prop
  31 ≝ λA.λf.∀x,y.f x y = f y x.
  32
  33 ndefinition symmetric2: ∀A,B:Type[0].∀f:A→A→B.Prop
  34 ≝ λA,B.λf.∀x,y.f x y = f y x.
  35
  36 ndefinition associative: ∀A:Type[0].∀f:A→A→A.Prop
  37 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
  38
  39 (*
  40 ntheorem eq_f_g_h:
  41   ∀A,B,C,D:Type[0].∀f:C→D.∀g:B→C.∀h:A→B.
  42   f∘(g∘h) = (f∘g)∘h.
  43   //.
  44 nqed. *)
  45
  46 (* functions and relations *)
  47 ndefinition monotonic : ∀A:Type.∀R:A→A→Prop.
  48 ∀f:A→A.Prop ≝
  49 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
  50
  51 (* functions and functions *)
  52 ndefinition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
  53 ≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
  54
  55 ndefinition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
  56 ≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
  57
  58 nlemma injective_compose : ∀A,B,C,f,g.
  59 injective A B f → injective B C g → injective A C (λx.g (f x)).
  60 /3/.
  61 nqed.