vstd/
relations.rs

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

vstd/
relations.rs
