vstd/
relations.rs

1//! Provides specifications for spec closures as relations.
2#[allow(unused_imports)]
3use super::pervasive::*;
4#[allow(unused_imports)]
5use super::prelude::*;
6#[allow(unused_imports)]
7use super::seq::*;
8#[allow(unused_imports)]
9use super::set::Set;
10
11verus! {
12
13pub open spec fn injective<X, Y>(r: spec_fn(X) -> Y) -> bool {
14    forall|x1: X, x2: X| #[trigger] r(x1) == #[trigger] r(x2) ==> x1 == x2
15}
16
17pub open spec fn injective_on<X, Y>(r: spec_fn(X) -> Y, dom: Set<X>) -> bool {
18    forall|x1: X, x2: X|
19        dom.contains(x1) && dom.contains(x2) && #[trigger] r(x1) == #[trigger] r(x2) ==> x1 == x2
20}
21
22pub open spec fn commutative<T, U>(r: spec_fn(T, T) -> U) -> bool {
23    forall|x: T, y: T| #[trigger] r(x, y) == #[trigger] r(y, x)
24}
25
26pub open spec fn associative<T>(r: spec_fn(T, T) -> T) -> bool {
27    forall|x: T, y: T, z: T| #[trigger] r(x, r(y, z)) == #[trigger] r(r(x, y), z)
28}
29
30pub open spec fn reflexive<T>(r: spec_fn(T, T) -> bool) -> bool {
31    forall|x: T| #[trigger] r(x, x)
32}
33
34pub open spec fn irreflexive<T>(r: spec_fn(T, T) -> bool) -> bool {
35    forall|x: T| #[trigger] r(x, x) == false
36}
37
38pub open spec fn antisymmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
39    forall|x: T, y: T| #[trigger] r(x, y) && #[trigger] r(y, x) ==> x == y
40}
41
42pub open spec fn asymmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
43    forall|x: T, y: T| #[trigger] r(x, y) ==> #[trigger] r(y, x) == false
44}
45
46pub open spec fn symmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
47    forall|x: T, y: T| #[trigger] r(x, y) <==> #[trigger] r(y, x)
48}
49
50pub open spec fn connected<T>(r: spec_fn(T, T) -> bool) -> bool {
51    forall|x: T, y: T| x != y ==> #[trigger] r(x, y) || #[trigger] r(y, x)
52}
53
54pub open spec fn strongly_connected<T>(r: spec_fn(T, T) -> bool) -> bool {
55    forall|x: T, y: T| #[trigger] r(x, y) || #[trigger] r(y, x)
56}
57
58pub open spec fn transitive<T>(r: spec_fn(T, T) -> bool) -> bool {
59    forall|x: T, y: T, z: T| #[trigger] r(x, y) && #[trigger] r(y, z) ==> r(x, z)
60}
61
62pub open spec fn total_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
63    &&& reflexive(r)
64    &&& antisymmetric(r)
65    &&& transitive(r)
66    &&& strongly_connected(r)
67}
68
69pub open spec fn strict_total_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
70    &&& irreflexive(r)
71    &&& antisymmetric(r)
72    &&& transitive(r)
73    &&& connected(r)
74}
75
76pub open spec fn pre_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
77    &&& reflexive(r)
78    &&& transitive(r)
79}
80
81pub open spec fn partial_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
82    &&& reflexive(r)
83    &&& transitive(r)
84    &&& antisymmetric(r)
85}
86
87pub open spec fn equivalence_relation<T>(r: spec_fn(T, T) -> bool) -> bool {
88    &&& reflexive(r)
89    &&& symmetric(r)
90    &&& transitive(r)
91}
92
93/// This function returns true if the input sequence a is sorted, using the input function
94/// less_than to sort the elements
95pub open spec fn sorted_by<T>(a: Seq<T>, less_than: spec_fn(T, T) -> bool) -> bool {
96    forall|i: int, j: int| 0 <= i < j < a.len() ==> #[trigger] less_than(a[i], a[j])
97}
98
99/// An element in an ordered set is called a least element (or a minimum), if it is less than
100/// every other element of the set.
101///
102/// change f to leq bc it is a relation. also these are an ordering relation
103pub open spec fn is_least<T>(leq: spec_fn(T, T) -> bool, min: T, s: Set<T>) -> bool {
104    s.contains(min) && forall|x: T| s.contains(x) ==> #[trigger] leq(min, x)
105}
106
107/// An element in an ordered set is called a minimal element, if no other element is less than it.
108pub open spec fn is_minimal<T>(leq: spec_fn(T, T) -> bool, min: T, s: Set<T>) -> bool {
109    s.contains(min) && forall|x: T|
110        s.contains(x) && #[trigger] leq(x, min) ==> #[trigger] leq(min, x)
111}
112
113/// An element in an ordered set is called a greatest element (or a maximum), if it is greater than
114///every other element of the set.
115pub open spec fn is_greatest<T>(leq: spec_fn(T, T) -> bool, max: T, s: Set<T>) -> bool {
116    s.contains(max) && forall|x: T| s.contains(x) ==> #[trigger] leq(x, max)
117}
118
119/// An element in an ordered set is called a maximal element, if no other element is greater than it.
120pub open spec fn is_maximal<T>(leq: spec_fn(T, T) -> bool, max: T, s: Set<T>) -> bool {
121    s.contains(max) && forall|x: T|
122        s.contains(x) && #[trigger] leq(max, x) ==> #[trigger] leq(x, max)
123}
124
125pub proof fn lemma_new_first_element_still_sorted_by<T>(
126    x: T,
127    s: Seq<T>,
128    less_than: spec_fn(T, T) -> bool,
129)
130    requires
131        sorted_by(s, less_than),
132        s.len() == 0 || less_than(x, s[0]),
133        total_ordering(less_than),
134    ensures
135        sorted_by(seq![x].add(s), less_than),
136{
137    broadcast use group_seq_axioms;
138
139    if s.len() > 1 {
140        assert forall|index: int| 0 < index < s.len() implies #[trigger] less_than(x, s[index]) by {
141            assert(less_than(s[0], s[index]));
142        };
143    }
144}
145
146} // verus!
vstd/relations.rs

vstd/
relations.rs
