1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141

//! Provides specifications for spec closures as relations.
#[allow(unused_imports)]
use super::pervasive::*;
#[allow(unused_imports)]
use super::prelude::*;
#[allow(unused_imports)]
use super::seq::*;
#[allow(unused_imports)]
use super::set::Set;

verus! {

pub open spec fn injective<X, Y>(r: spec_fn(X) -> Y) -> bool {
    forall|x1: X, x2: X| #[trigger] r(x1) == #[trigger] r(x2) ==> x1 == x2
}

pub open spec fn commutative<T, U>(r: spec_fn(T, T) -> U) -> bool {
    forall|x: T, y: T| #[trigger] r(x, y) == #[trigger] r(y, x)
}

pub open spec fn associative<T>(r: spec_fn(T, T) -> T) -> bool {
    forall|x: T, y: T, z: T| #[trigger] r(x, r(y, z)) == #[trigger] r(r(x, y), z)
}

pub open spec fn reflexive<T>(r: spec_fn(T, T) -> bool) -> bool {
    forall|x: T| #[trigger] r(x, x)
}

pub open spec fn irreflexive<T>(r: spec_fn(T, T) -> bool) -> bool {
    forall|x: T| #[trigger] r(x, x) == false
}

pub open spec fn antisymmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
    forall|x: T, y: T| #[trigger] r(x, y) && #[trigger] r(y, x) ==> x == y
}

pub open spec fn asymmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
    forall|x: T, y: T| #[trigger] r(x, y) ==> #[trigger] r(y, x) == false
}

pub open spec fn symmetric<T>(r: spec_fn(T, T) -> bool) -> bool {
    forall|x: T, y: T| #[trigger] r(x, y) <==> #[trigger] r(y, x)
}

pub open spec fn connected<T>(r: spec_fn(T, T) -> bool) -> bool {
    forall|x: T, y: T| x != y ==> #[trigger] r(x, y) || #[trigger] r(y, x)
}

pub open spec fn strongly_connected<T>(r: spec_fn(T, T) -> bool) -> bool {
    forall|x: T, y: T| #[trigger] r(x, y) || #[trigger] r(y, x)
}

pub open spec fn transitive<T>(r: spec_fn(T, T) -> bool) -> bool {
    forall|x: T, y: T, z: T| #[trigger] r(x, y) && #[trigger] r(y, z) ==> r(x, z)
}

pub open spec fn total_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
    &&& reflexive(r)
    &&& antisymmetric(r)
    &&& transitive(r)
    &&& strongly_connected(r)
}

pub open spec fn strict_total_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
    &&& irreflexive(r)
    &&& antisymmetric(r)
    &&& transitive(r)
    &&& connected(r)
}

pub open spec fn pre_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
    &&& reflexive(r)
    &&& transitive(r)
}

pub open spec fn partial_ordering<T>(r: spec_fn(T, T) -> bool) -> bool {
    &&& reflexive(r)
    &&& transitive(r)
    &&& antisymmetric(r)
}

pub open spec fn equivalence_relation<T>(r: spec_fn(T, T) -> bool) -> bool {
    &&& reflexive(r)
    &&& symmetric(r)
    &&& transitive(r)
}

/// This function returns true if the input sequence a is sorted, using the input function
/// less_than to sort the elements
pub open spec fn sorted_by<T>(a: Seq<T>, less_than: spec_fn(T, T) -> bool) -> bool {
    forall|i: int, j: int| 0 <= i < j < a.len() ==> #[trigger] less_than(a[i], a[j])
}

/// An element in an ordered set is called a least element (or a minimum), if it is less than
/// every other element of the set.
///
/// change f to leq bc it is a relation. also these are an ordering relation
pub open spec fn is_least<T>(leq: spec_fn(T, T) -> bool, min: T, s: Set<T>) -> bool {
    s.contains(min) && forall|x: T| s.contains(x) ==> #[trigger] leq(min, x)
}

/// An element in an ordered set is called a minimal element, if no other element is less than it.
pub open spec fn is_minimal<T>(leq: spec_fn(T, T) -> bool, min: T, s: Set<T>) -> bool {
    s.contains(min) && forall|x: T|
        s.contains(x) && #[trigger] leq(x, min) ==> #[trigger] leq(min, x)
}

/// An element in an ordered set is called a greatest element (or a maximum), if it is greater than
///every other element of the set.
pub open spec fn is_greatest<T>(leq: spec_fn(T, T) -> bool, max: T, s: Set<T>) -> bool {
    s.contains(max) && forall|x: T| s.contains(x) ==> #[trigger] leq(x, max)
}

/// An element in an ordered set is called a maximal element, if no other element is greater than it.
pub open spec fn is_maximal<T>(leq: spec_fn(T, T) -> bool, max: T, s: Set<T>) -> bool {
    s.contains(max) && forall|x: T|
        s.contains(x) && #[trigger] leq(max, x) ==> #[trigger] leq(x, max)
}

pub proof fn lemma_new_first_element_still_sorted_by<T>(
    x: T,
    s: Seq<T>,
    less_than: spec_fn(T, T) -> bool,
)
    requires
        sorted_by(s, less_than),
        s.len() == 0 || less_than(x, s[0]),
        total_ordering(less_than),
    ensures
        sorted_by(seq![x].add(s), less_than),
{
    broadcast use group_seq_axioms;

    if s.len() > 1 {
        assert forall|index: int| 0 < index < s.len() implies #[trigger] less_than(x, s[index]) by {
            assert(less_than(s[0], s[index]));
        };
    }
}

} // verus!