1
<html xmlns="http://www.w3.org/1999/xhtml">
3
<meta http-equiv="Content-Type" content="text/html; charset="><link rel="stylesheet" href="style.css" type="text/css"><title>Coq.Relations.Relation_Definitions</title>
8
<h1>Library Coq.Relations.Relation_Definitions</h1>
11
<code class="keyword">Section</code> Relation_Definition.<br/>
14
<code class="keyword">Variable</code> A : Type.<br/>
15
<br/>
16
<code class="keyword">Definition</code> <a name="relation"></a>relation := A -> A -> Prop.<br/>
19
<code class="keyword">Variable</code> R : <a href="Coq.Relations.Relation_Definitions.html#relation">relation</a>.<br/>
20
<br/>
23
<code class="keyword">Section</code> General_Properties_of_Relations.<br/>
26
<code class="keyword">Definition</code> <a name="reflexive"></a>reflexive : Prop := forall x:A, R x x.<br/>
27
<code class="keyword">Definition</code> <a name="transitive"></a>transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.<br/>
28
<code class="keyword">Definition</code> <a name="symmetric"></a>symmetric : Prop := forall x y:A, R x y -> R y x.<br/>
29
<code class="keyword">Definition</code> <a name="antisymmetric"></a>antisymmetric : Prop := forall x y:A, R x y -> R y x -> x = y.<br/>
32
<code class="keyword">Definition</code> <a name="equiv"></a>equiv := <a href="Coq.Relations.Relation_Definitions.html#reflexive">reflexive</a> /\ <a href="Coq.Relations.Relation_Definitions.html#transitive">transitive</a> /\ <a href="Coq.Relations.Relation_Definitions.html#symmetric">symmetric</a>.<br/>
35
<code class="keyword">End</code> General_Properties_of_Relations.<br/>
38
<code class="keyword">Section</code> Sets_of_Relations.<br/>
41
<code class="keyword">Record</code> <a name="preorder"></a>preorder : Prop := <br/>
42
{preord_refl : <a href="Coq.Relations.Relation_Definitions.html#reflexive">reflexive</a>; preord_trans : <a href="Coq.Relations.Relation_Definitions.html#transitive">transitive</a>}.<br/>
45
<code class="keyword">Record</code> <a name="order"></a>order : Prop := <br/>
46
{ord_refl : <a href="Coq.Relations.Relation_Definitions.html#reflexive">reflexive</a>;<br/>
47
ord_trans : <a href="Coq.Relations.Relation_Definitions.html#transitive">transitive</a>;<br/>
48
ord_antisym : <a href="Coq.Relations.Relation_Definitions.html#antisymmetric">antisymmetric</a>}.<br/>
51
<code class="keyword">Record</code> <a name="equivalence"></a>equivalence : Prop := <br/>
52
{equiv_refl : <a href="Coq.Relations.Relation_Definitions.html#reflexive">reflexive</a>;<br/>
53
equiv_trans : <a href="Coq.Relations.Relation_Definitions.html#transitive">transitive</a>;<br/>
54
equiv_sym : <a href="Coq.Relations.Relation_Definitions.html#symmetric">symmetric</a>}.<br/>
55
<br/>
56
<code class="keyword">Record</code> <a name="PER"></a>PER : Prop := {per_sym : <a href="Coq.Relations.Relation_Definitions.html#symmetric">symmetric</a>; per_trans : <a href="Coq.Relations.Relation_Definitions.html#transitive">transitive</a>}.<br/>
59
<code class="keyword">End</code> Sets_of_Relations.<br/>
62
<code class="keyword">Section</code> Relations_of_Relations.<br/>
65
<code class="keyword">Definition</code> <a name="inclusion"></a>inclusion (R1 R2:<a href="Coq.Relations.Relation_Definitions.html#relation">relation</a>) : Prop :=<br/>
66
forall x y:A, R1 x y -> R2 x y.<br/>
69
<code class="keyword">Definition</code> <a name="same_relation"></a>same_relation (R1 R2:<a href="Coq.Relations.Relation_Definitions.html#relation">relation</a>) : Prop :=<br/>
70
<a href="Coq.Relations.Relation_Definitions.html#inclusion">inclusion</a> R1 R2 /\ <a href="Coq.Relations.Relation_Definitions.html#inclusion">inclusion</a> R2 R1.<br/>
71
<br/>
72
<code class="keyword">Definition</code> <a name="commut"></a>commut (R1 R2:<a href="Coq.Relations.Relation_Definitions.html#relation">relation</a>) : Prop :=<br/>
73
forall x y:A,<br/>
74
R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'.<br/>
77
<code class="keyword">End</code> Relations_of_Relations.<br/>
80
<br/>
81
<code class="keyword">End</code> Relation_Definition.<br/>
84
<code class="keyword">Hint</code> Unfold reflexive transitive antisymmetric symmetric: sets v62.<br/>
87
<code class="keyword">Hint</code> Resolve <a href="Coq.Relations.Relation_Definitions.html#Build_preorder">Build_preorder</a> <a href="Coq.Relations.Relation_Definitions.html#Build_order">Build_order</a> <a href="Coq.Relations.Relation_Definitions.html#Build_equivalence">Build_equivalence</a> <a href="Coq.Relations.Relation_Definitions.html#Build_PER">Build_PER</a><br/>
88
<a href="Coq.Relations.Relation_Definitions.html#preord_refl">preord_refl</a> <a href="Coq.Relations.Relation_Definitions.html#preord_trans">preord_trans</a> <a href="Coq.Relations.Relation_Definitions.html#ord_refl">ord_refl</a> <a href="Coq.Relations.Relation_Definitions.html#ord_trans">ord_trans</a> <a href="Coq.Relations.Relation_Definitions.html#ord_antisym">ord_antisym</a> <a href="Coq.Relations.Relation_Definitions.html#equiv_refl">equiv_refl</a><br/>
89
<a href="Coq.Relations.Relation_Definitions.html#equiv_trans">equiv_trans</a> <a href="Coq.Relations.Relation_Definitions.html#equiv_sym">equiv_sym</a> <a href="Coq.Relations.Relation_Definitions.html#per_sym">per_sym</a> <a href="Coq.Relations.Relation_Definitions.html#per_trans">per_trans</a>: sets v62.<br/>
92
<code class="keyword">Hint</code> Unfold inclusion same_relation commut: sets v62.</code>
93
<hr/><a href="index.html">Index</a><hr/><font size="-1">This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a></font>
b'\\ No newline at end of file'
added
removed
library/Coq.Relations.Relation_Definitions.html
