]> matita.cs.unibo.it Git - helm.git/blob - weblib/basics/relations.ma
- support for atomic arities and candidates of reducibility started
[helm.git] / weblib / basics / relations.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "basics/logic.ma".
13
14 (********** relations **********)
15 definition relation : Type[0] → Type[0]
16 ≝ λA.A→A→Prop. 
17
18 definition reflexive: ∀A.∀R :\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
19 ≝ λA.λR.∀x:A.R x x.
20
21 definition symmetric: ∀A.∀R: \ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
22 ≝ λA.λR.∀x,y:A.R x y → R y x.
23
24 definition transitive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
25 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
26
27 definition irreflexive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
28 ≝ λA.λR.∀x:A.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(R x x).
29
30 definition cotransitive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
31 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 R z y.
32
33 definition tight_apart: ∀A.∀eq,ap:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
34 ≝ λA.λeq,ap.∀x,y:A. (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y) → eq x y) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6
35 (eq x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y)).
36
37 definition antisymmetric: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
38 ≝ λA.λR.∀x,y:A. R x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(R y x).
39
40 (********** functions **********)
41
42 definition compose ≝
43   λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
44
45 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
46
47 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
48 ≝ λA,B.λf.∀x,y:A.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y → x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y.
49
50 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
51 ≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6x:A.z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
52
53 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop 
54 ≝ λA.λf.∀x,y.f x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y x.
55
56 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
57 ≝ λA,B.λf.∀x,y.f x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y x.
58
59 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
60 ≝ λA.λf.∀x,y,z.f (f x y) z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x (f y z).
61
62 (* functions and relations *)
63 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
64 ∀f:A→A.Prop ≝
65 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
66
67 (* functions and functions *)
68 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
69 ≝ λA.λf,g.∀x,y,z:A. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g (f x y) (f x z).
70
71 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
72 ≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g (f x y) (f x z).
73
74 lemma injective_compose : ∀A,B,C,f,g.
75 \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A B f → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 B C g → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A C (λx.g (f x)).
76 /3/; qed.
77
78 (* extensional equality *)
79
80 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
81 λA.λP,Q.∀a.\ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (P a) (Q a).
82
83 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
84 λA,B.λR,S.∀a.∀b.\ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (R a b) (S a b).
85
86 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
87 λA,B.λf,g.∀a.f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g a.
88
89 notation " x \eqP y " non associative with precedence 45 
90 for @{'eqP A $x $y}.
91
92 interpretation "functional extentional equality" 
93 'eqP A x y = (exteqP A x y).
94
95 notation "x \eqR y" non associative with precedence 45 
96 for @{'eqR ? ? x y}.
97
98 interpretation "functional extentional equality" 
99 'eqR A B R S = (exteqR A B R S).
100
101 notation " f \eqF g " non associative with precedence 45
102 for @{'eqF ? ? f g}.
103
104 interpretation "functional extentional equality" 
105 'eqF A B f g = (exteqF A B f g).