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
9verus! {
10
11pub open spec fn injective<X, Y>(r: spec_fn(X) -> Y) -> bool {
12    forall|x1: X, x2: X| #[trigger] r(x1) == #[trigger] r(x2) ==> x1 == x2
13}
14
15pub open spec fn commutative<T, U>(r: spec_fn(T, T) -> U) -> bool {
16    forall|x: T, y: T| #[trigger] r(x, y) == #[trigger] r(y, x)
17}
18
19pub open spec fn associative<T>(r: spec_fn(T, T) -> T) -> bool {
20    forall|x: T, y: T, z: T| #[trigger] r(x, r(y, z)) == #[trigger] r(r(x, y), z)
21}
22
23pub open spec fn reflexive<T>(r: spec_fn(T, T) -> bool) -> bool {
24    forall|x: T| #[trigger] r(x, x)
25}
26
27pub open spec fn irreflexive<T>(r: spec_fn(T, T) -> bool) -> bool {
28    forall|x: T| #[trigger] r(x, x) == false
29}
30
31pub open spec fn antisymmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
32    forall|x: T, y: T| #[trigger] r(x, y) && #[trigger] r(y, x) ==> x == y
33}
34
35pub open spec fn asymmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
36    forall|x: T, y: T| #[trigger] r(x, y) ==> #[trigger] r(y, x) == false
37}
38
39pub open spec fn symmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
40    forall|x: T, y: T| #[trigger] r(x, y) <==> #[trigger] r(y, x)
41}
42
43pub open spec fn connected<T>(r: spec_fn(T, T) -> bool) -> bool {
44    forall|x: T, y: T| x != y ==> #[trigger] r(x, y) || #[trigger] r(y, x)
45}
46
47pub open spec fn strongly_connected<T>(r: spec_fn(T, T) -> bool) -> bool {
48    forall|x: T, y: T| #[trigger] r(x, y) || #[trigger] r(y, x)
49}
50
51pub open spec fn transitive<T>(r: spec_fn(T, T) -> bool) -> bool {
52    forall|x: T, y: T, z: T| #[trigger] r(x, y) && #[trigger] r(y, z) ==> r(x, z)
53}
54
55pub open spec fn total_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
56    &&& reflexive(r)
57    &&& antisymmetric(r)
58    &&& transitive(r)
59    &&& strongly_connected(r)
60}
61
62pub open spec fn strict_total_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
63    &&& irreflexive(r)
64    &&& antisymmetric(r)
65    &&& transitive(r)
66    &&& connected(r)
67}
68
69pub open spec fn pre_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
70    &&& reflexive(r)
71    &&& transitive(r)
72}
73
74pub open spec fn partial_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
75    &&& reflexive(r)
76    &&& transitive(r)
77    &&& antisymmetric(r)
78}
79
80pub open spec fn equivalence_relation<T>(r: spec_fn(T, T) -> bool) -> bool {
81    &&& reflexive(r)
82    &&& symmetric(r)
83    &&& transitive(r)
84}
85
86/// This function returns true if the input sequence a is sorted, using the input function
87/// less_than to sort the elements
88pub open spec fn sorted_by<T>(a: Seq<T>, less_than: spec_fn(T, T) -> bool) -> bool {
89    forall|i: int, j: int| 0 <= i < j < a.len() ==> #[trigger] less_than(a[i], a[j])
90}
91
92pub proof fn lemma_new_first_element_still_sorted_by<T>(
93    x: T,
94    s: Seq<T>,
95    less_than: spec_fn(T, T) -> bool,
96)
97    requires
98        sorted_by(s, less_than),
99        s.len() == 0 || less_than(x, s[0]),
100        total_ordering(less_than),
101    ensures
102        sorted_by(seq![x].add(s), less_than),
103{
104    broadcast use group_seq_axioms;
105
106    if s.len() > 1 {
107        assert forall|index: int| 0 < index < s.len() implies #[trigger] less_than(x, s[index]) by {
108            assert(less_than(s[0], s[index]));
109        };
110    }
111}
112
113} // verus!
vstd/relations.rs

vstd/
relations.rs
