oxilean_std/ord/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::Node;
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
7
8use super::types::{OrdResult, Permutation, SortedMap, SortedSet};
9
10/// Build Ord type class in the environment.
11pub fn build_ord_env(env: &mut Environment) -> Result<(), String> {
12    let type1 = Expr::Sort(Level::succ(Level::zero()));
13    let type2 = Expr::Sort(Level::succ(Level::succ(Level::zero())));
14    let ordering_ty = type1.clone();
15    env.add(Declaration::Axiom {
16        name: Name::str("Ordering"),
17        univ_params: vec![],
18        ty: ordering_ty,
19    })
20    .map_err(|e| e.to_string())?;
21    for variant in &["Ordering.lt", "Ordering.eq", "Ordering.gt"] {
22        env.add(Declaration::Axiom {
23            name: Name::str(*variant),
24            univ_params: vec![],
25            ty: Expr::Const(Name::str("Ordering"), vec![]),
26        })
27        .map_err(|e| e.to_string())?;
28    }
29    let ord_ty = Expr::Pi(
30        BinderInfo::Default,
31        Name::str("α"),
32        Node::new(type1.clone()),
33        Node::new(type2.clone()),
34    );
35    env.add(Declaration::Axiom {
36        name: Name::str("Ord"),
37        univ_params: vec![],
38        ty: ord_ty,
39    })
40    .map_err(|e| e.to_string())?;
41    let compare_ty = Expr::Pi(
42        BinderInfo::Implicit,
43        Name::str("α"),
44        Node::new(type1.clone()),
45        Node::new(Expr::Pi(
46            BinderInfo::InstImplicit,
47            Name::str("_"),
48            Node::new(Expr::App(
49                Node::new(Expr::Const(Name::str("Ord"), vec![])),
50                Node::new(Expr::BVar(0)),
51            )),
52            Node::new(Expr::Pi(
53                BinderInfo::Default,
54                Name::str("a"),
55                Node::new(Expr::BVar(1)),
56                Node::new(Expr::Pi(
57                    BinderInfo::Default,
58                    Name::str("b"),
59                    Node::new(Expr::BVar(2)),
60                    Node::new(Expr::Const(Name::str("Ordering"), vec![])),
61                )),
62            )),
63        )),
64    );
65    env.add(Declaration::Axiom {
66        name: Name::str("Ord.compare"),
67        univ_params: vec![],
68        ty: compare_ty,
69    })
70    .map_err(|e| e.to_string())?;
71    add_ordering_predicate(env, "Ordering.isLT")?;
72    add_ordering_predicate(env, "Ordering.isEQ")?;
73    add_ordering_predicate(env, "Ordering.isGT")?;
74    add_ordering_predicate(env, "Ordering.isLE")?;
75    add_ordering_predicate(env, "Ordering.isGE")?;
76    let swap_ty = Expr::Pi(
77        BinderInfo::Default,
78        Name::str("o"),
79        Node::new(Expr::Const(Name::str("Ordering"), vec![])),
80        Node::new(Expr::Const(Name::str("Ordering"), vec![])),
81    );
82    env.add(Declaration::Axiom {
83        name: Name::str("Ordering.swap"),
84        univ_params: vec![],
85        ty: swap_ty,
86    })
87    .map_err(|e| e.to_string())?;
88    let then_ty = Expr::Pi(
89        BinderInfo::Default,
90        Name::str("o1"),
91        Node::new(Expr::Const(Name::str("Ordering"), vec![])),
92        Node::new(Expr::Pi(
93            BinderInfo::Default,
94            Name::str("o2"),
95            Node::new(Expr::Const(Name::str("Ordering"), vec![])),
96            Node::new(Expr::Const(Name::str("Ordering"), vec![])),
97        )),
98    );
99    env.add(Declaration::Axiom {
100        name: Name::str("Ordering.then"),
101        univ_params: vec![],
102        ty: then_ty,
103    })
104    .map_err(|e| e.to_string())?;
105    Ok(())
106}
107/// Helper: add a predicate `name : Ordering → Bool` to the environment.
108pub fn add_ordering_predicate(env: &mut Environment, name: &str) -> Result<(), String> {
109    let ty = Expr::Pi(
110        BinderInfo::Default,
111        Name::str("o"),
112        Node::new(Expr::Const(Name::str("Ordering"), vec![])),
113        Node::new(Expr::Const(Name::str("Bool"), vec![])),
114    );
115    env.add(Declaration::Axiom {
116        name: Name::str(name),
117        univ_params: vec![],
118        ty,
119    })
120    .map_err(|e| e.to_string())
121}
122/// Compare two values that implement `Ord` and return an `OrdResult`.
123pub fn compare<T: Ord>(a: &T, b: &T) -> OrdResult {
124    OrdResult::from_std(a.cmp(b))
125}
126/// Compare by a key function.
127pub fn compare_by_key<T, K: Ord, F: Fn(&T) -> K>(a: &T, b: &T, key: F) -> OrdResult {
128    OrdResult::from_std(key(a).cmp(&key(b)))
129}
130/// Lexicographic comparison of two slices.
131pub fn compare_slices<T: Ord>(a: &[T], b: &[T]) -> OrdResult {
132    OrdResult::from_std(a.cmp(b))
133}
134/// Return the minimum of two values.
135pub fn ord_min<T: Ord>(a: T, b: T) -> T {
136    if a <= b {
137        a
138    } else {
139        b
140    }
141}
142/// Return the maximum of two values.
143pub fn ord_max<T: Ord>(a: T, b: T) -> T {
144    if a >= b {
145        a
146    } else {
147        b
148    }
149}
150/// Clamp a value within `[lo, hi]`.
151pub fn ord_clamp<T: Ord>(val: T, lo: T, hi: T) -> T {
152    if val < lo {
153        lo
154    } else if val > hi {
155        hi
156    } else {
157        val
158    }
159}
160/// Stable sort a `Vec` using a comparison closure returning `OrdResult`.
161pub fn sort_by<T, F>(v: &mut [T], mut cmp: F)
162where
163    F: FnMut(&T, &T) -> OrdResult,
164{
165    v.sort_by(|a, b| cmp(a, b).to_std());
166}
167/// Return `true` if a slice is sorted in non-decreasing order.
168pub fn is_sorted<T: Ord>(s: &[T]) -> bool {
169    s.windows(2).all(|w| w[0] <= w[1])
170}
171/// Return `true` if a slice is sorted in non-increasing order.
172pub fn is_sorted_desc<T: Ord>(s: &[T]) -> bool {
173    s.windows(2).all(|w| w[0] >= w[1])
174}
175/// Binary search returning an `OrdResult`-based position description.
176///
177/// Returns `Ok(index)` if found, `Err(index)` for the insertion point.
178pub fn ord_binary_search<T: Ord>(s: &[T], target: &T) -> Result<usize, usize> {
179    s.binary_search(target)
180}
181/// Chain multiple comparisons together with `then`.
182///
183/// Evaluates comparisons left-to-right, stopping as soon as one is not `Equal`.
184pub fn compare_chain(comparisons: &[OrdResult]) -> OrdResult {
185    comparisons
186        .iter()
187        .copied()
188        .fold(OrdResult::Equal, OrdResult::then)
189}
190/// Reverse a comparison function (swap its output).
191pub fn reverse_cmp<T, F>(a: &T, b: &T, cmp: F) -> OrdResult
192where
193    F: Fn(&T, &T) -> OrdResult,
194{
195    cmp(a, b).swap()
196}
197/// `true` if `a < b`.
198pub fn lt<T: Ord>(a: &T, b: &T) -> bool {
199    a < b
200}
201/// `true` if `a <= b`.
202pub fn le<T: Ord>(a: &T, b: &T) -> bool {
203    a <= b
204}
205/// `true` if `a > b`.
206pub fn gt<T: Ord>(a: &T, b: &T) -> bool {
207    a > b
208}
209/// `true` if `a >= b`.
210pub fn ge<T: Ord>(a: &T, b: &T) -> bool {
211    a >= b
212}
213/// `true` if `a == b`.
214pub fn eq<T: Ord>(a: &T, b: &T) -> bool {
215    a == b
216}
217/// `true` if `a != b`.
218pub fn ne<T: Ord>(a: &T, b: &T) -> bool {
219    a != b
220}
221#[cfg(test)]
222mod tests {
223    use super::*;
224    #[test]
225    fn test_build_ord_env() {
226        let mut env = Environment::new();
227        assert!(build_ord_env(&mut env).is_ok());
228        assert!(env.get(&Name::str("Ordering")).is_some());
229        assert!(env.get(&Name::str("Ord")).is_some());
230        assert!(env.get(&Name::str("Ord.compare")).is_some());
231    }
232    #[test]
233    fn test_ord_result_swap() {
234        assert_eq!(OrdResult::Less.swap(), OrdResult::Greater);
235        assert_eq!(OrdResult::Greater.swap(), OrdResult::Less);
236        assert_eq!(OrdResult::Equal.swap(), OrdResult::Equal);
237    }
238    #[test]
239    fn test_ord_result_then() {
240        assert_eq!(OrdResult::Equal.then(OrdResult::Less), OrdResult::Less);
241        assert_eq!(OrdResult::Less.then(OrdResult::Greater), OrdResult::Less);
242    }
243    #[test]
244    fn test_ord_result_predicates() {
245        let lt = OrdResult::Less;
246        let eq = OrdResult::Equal;
247        let gt = OrdResult::Greater;
248        assert!(lt.is_lt() && lt.is_le() && !lt.is_eq() && !lt.is_gt() && !lt.is_ge());
249        assert!(eq.is_eq() && eq.is_le() && eq.is_ge() && !eq.is_lt() && !eq.is_gt());
250        assert!(gt.is_gt() && gt.is_ge() && !gt.is_lt() && !gt.is_eq() && !gt.is_le());
251    }
252    #[test]
253    fn test_compare() {
254        assert_eq!(compare(&1, &2), OrdResult::Less);
255        assert_eq!(compare(&2, &2), OrdResult::Equal);
256        assert_eq!(compare(&3, &2), OrdResult::Greater);
257    }
258    #[test]
259    fn test_compare_chain() {
260        let chain = compare_chain(&[OrdResult::Equal, OrdResult::Equal, OrdResult::Less]);
261        assert_eq!(chain, OrdResult::Less);
262        let all_eq = compare_chain(&[OrdResult::Equal, OrdResult::Equal]);
263        assert_eq!(all_eq, OrdResult::Equal);
264    }
265    #[test]
266    fn test_sort_by() {
267        let mut v = vec![3, 1, 4, 1, 5, 9, 2, 6];
268        sort_by(&mut v, |a, b| compare(a, b));
269        assert!(is_sorted(&v));
270    }
271    #[test]
272    fn test_is_sorted() {
273        assert!(is_sorted(&[1, 2, 3, 4]));
274        assert!(!is_sorted(&[1, 3, 2]));
275        assert!(is_sorted_desc(&[4, 3, 2, 1]));
276        assert!(!is_sorted_desc(&[1, 2, 3]));
277    }
278    #[test]
279    fn test_ord_min_max_clamp() {
280        assert_eq!(ord_min(3, 5), 3);
281        assert_eq!(ord_max(3, 5), 5);
282        assert_eq!(ord_clamp(10, 0, 5), 5);
283        assert_eq!(ord_clamp(-1, 0, 5), 0);
284        assert_eq!(ord_clamp(3, 0, 5), 3);
285    }
286    #[test]
287    fn test_compare_by_key() {
288        let a = ("b", 1);
289        let b = ("a", 2);
290        let res = compare_by_key(&a, &b, |x| x.0);
291        assert_eq!(res, OrdResult::Greater);
292    }
293    #[test]
294    fn test_compare_slices() {
295        let a = &[1, 2, 3][..];
296        let b = &[1, 2, 4][..];
297        assert_eq!(compare_slices(a, b), OrdResult::Less);
298    }
299    #[test]
300    fn test_signum() {
301        assert_eq!(OrdResult::Less.to_signum(), -1);
302        assert_eq!(OrdResult::Equal.to_signum(), 0);
303        assert_eq!(OrdResult::Greater.to_signum(), 1);
304    }
305    #[test]
306    fn test_display() {
307        assert_eq!(OrdResult::Less.to_string(), "lt");
308        assert_eq!(OrdResult::Equal.to_string(), "eq");
309        assert_eq!(OrdResult::Greater.to_string(), "gt");
310    }
311    #[test]
312    fn test_named_predicates() {
313        assert!(lt(&1, &2));
314        assert!(le(&2, &2));
315        assert!(gt(&3, &2));
316        assert!(ge(&2, &2));
317        assert!(eq(&5, &5));
318        assert!(ne(&5, &6));
319    }
320    #[test]
321    fn test_reverse_cmp() {
322        let res = reverse_cmp(&1i32, &2i32, |a, b| compare(a, b));
323        assert_eq!(res, OrdResult::Greater);
324    }
325    #[test]
326    fn test_binary_search() {
327        let v = vec![1, 3, 5, 7, 9];
328        assert!(ord_binary_search(&v, &5).is_ok());
329        assert!(ord_binary_search(&v, &4).is_err());
330    }
331    #[test]
332    fn test_to_from_std() {
333        let o = OrdResult::Less;
334        assert_eq!(OrdResult::from_std(o.to_std()), o);
335    }
336}
337/// Compare by multiple keys in priority order.
338///
339/// Takes a list of `(a_key, b_key)` pairs and returns the first non-equal
340/// comparison, or `Equal` if all keys are equal.
341pub fn multi_key_compare<K: Ord>(key_pairs: &[(K, K)]) -> OrdResult {
342    for (a, b) in key_pairs {
343        let r = compare(a, b);
344        if r != OrdResult::Equal {
345            return r;
346        }
347    }
348    OrdResult::Equal
349}
350/// Return the median element of a slice (or `None` if empty).
351///
352/// Uses the "lower median" for even-length slices.
353pub fn median<T: Ord + Clone>(v: &[T]) -> Option<T> {
354    if v.is_empty() {
355        return None;
356    }
357    let mut sorted = v.to_vec();
358    sorted.sort();
359    Some(sorted[(sorted.len() - 1) / 2].clone())
360}
361/// Return `true` if `v` is a non-strict subset of `u` (all elements of `v` are in `u`).
362pub fn is_subset<T: Ord>(v: &[T], u: &[T]) -> bool {
363    v.iter().all(|item| u.binary_search(item).is_ok())
364}
365#[cfg(test)]
366mod ord_extra_tests {
367    use super::*;
368    #[test]
369    fn test_sorted_map_insert_get() {
370        let mut m: SortedMap<u32, &str> = SortedMap::new();
371        m.insert(3, "three");
372        m.insert(1, "one");
373        m.insert(2, "two");
374        assert_eq!(m.get(&1), Some(&"one"));
375        assert_eq!(m.get(&3), Some(&"three"));
376        assert!(m.get(&5).is_none());
377    }
378    #[test]
379    fn test_sorted_map_keys_ordered() {
380        let mut m: SortedMap<u32, u32> = SortedMap::new();
381        m.insert(5, 50);
382        m.insert(1, 10);
383        m.insert(3, 30);
384        let keys: Vec<_> = m.keys().copied().collect();
385        assert_eq!(keys, vec![1, 3, 5]);
386    }
387    #[test]
388    fn test_sorted_map_remove() {
389        let mut m: SortedMap<u32, u32> = SortedMap::new();
390        m.insert(1, 100);
391        assert_eq!(m.remove(&1), Some(100));
392        assert!(m.get(&1).is_none());
393    }
394    #[test]
395    fn test_sorted_set_insert_contains() {
396        let mut s: SortedSet<u32> = SortedSet::new();
397        s.insert(5);
398        s.insert(3);
399        s.insert(7);
400        assert!(s.contains(&3));
401        assert!(s.contains(&5));
402        assert!(!s.contains(&4));
403    }
404    #[test]
405    fn test_sorted_set_union_intersection() {
406        let mut a: SortedSet<u32> = SortedSet::new();
407        a.insert(1);
408        a.insert(2);
409        a.insert(3);
410        let mut b: SortedSet<u32> = SortedSet::new();
411        b.insert(2);
412        b.insert(3);
413        b.insert(4);
414        let u = a.union(&b);
415        assert_eq!(u.len(), 4);
416        let i = a.intersection(&b);
417        assert_eq!(i.len(), 2);
418        assert!(i.contains(&2));
419        assert!(i.contains(&3));
420    }
421    #[test]
422    fn test_sorted_set_difference() {
423        let mut a: SortedSet<u32> = SortedSet::new();
424        a.insert(1);
425        a.insert(2);
426        a.insert(3);
427        let mut b: SortedSet<u32> = SortedSet::new();
428        b.insert(2);
429        let diff = a.difference(&b);
430        assert_eq!(diff.len(), 2);
431        assert!(diff.contains(&1));
432        assert!(diff.contains(&3));
433    }
434    #[test]
435    fn test_multi_key_compare() {
436        let result = multi_key_compare(&[(1u32, 1u32), (2u32, 3u32)]);
437        assert_eq!(result, OrdResult::Less);
438        let all_eq = multi_key_compare(&[(1u32, 1u32), (2u32, 2u32)]);
439        assert_eq!(all_eq, OrdResult::Equal);
440    }
441    #[test]
442    fn test_median() {
443        assert_eq!(median(&[3u32, 1, 4, 1, 5]), Some(3));
444        assert_eq!(median::<u32>(&[]), None);
445        assert_eq!(median(&[2u32, 4]), Some(2));
446    }
447    #[test]
448    fn test_is_subset() {
449        let u = vec![1u32, 2, 3, 4, 5];
450        let v = vec![2u32, 4];
451        assert!(is_subset(&v, &u));
452        let w = vec![2u32, 6];
453        assert!(!is_subset(&w, &u));
454    }
455}
456/// Compare two `Option<T>` values: `None < Some(x)` for all `x`.
457#[allow(dead_code)]
458pub fn compare_option<T: Ord>(a: &Option<T>, b: &Option<T>) -> OrdResult {
459    match (a, b) {
460        (None, None) => OrdResult::Equal,
461        (None, Some(_)) => OrdResult::Less,
462        (Some(_), None) => OrdResult::Greater,
463        (Some(x), Some(y)) => compare(x, y),
464    }
465}
466/// Compare two `bool` values (`false < true`).
467#[allow(dead_code)]
468pub fn compare_bool(a: bool, b: bool) -> OrdResult {
469    OrdResult::from_std(a.cmp(&b))
470}
471#[cfg(test)]
472mod ord_final_tests {
473    use super::*;
474    #[test]
475    fn test_compare_option() {
476        assert_eq!(compare_option::<u32>(&None, &None), OrdResult::Equal);
477        assert_eq!(compare_option::<u32>(&None, &Some(1)), OrdResult::Less);
478        assert_eq!(compare_option::<u32>(&Some(1), &None), OrdResult::Greater);
479    }
480    #[test]
481    fn test_compare_bool() {
482        assert_eq!(compare_bool(false, true), OrdResult::Less);
483        assert_eq!(compare_bool(true, true), OrdResult::Equal);
484    }
485}
486/// Simple topological sort for dependency graphs.
487///
488/// Nodes are identified by `usize` indices. Returns a sorted list of node
489/// indices, or an error if the graph has a cycle.
490pub fn topological_sort(n: usize, edges: &[(usize, usize)]) -> Result<Vec<usize>, String> {
491    let mut in_degree = vec![0usize; n];
492    let mut adj: Vec<Vec<usize>> = vec![Vec::new(); n];
493    for &(from, to) in edges {
494        adj[from].push(to);
495        in_degree[to] += 1;
496    }
497    let mut queue: std::collections::VecDeque<usize> =
498        (0..n).filter(|&i| in_degree[i] == 0).collect();
499    let mut result = Vec::new();
500    while let Some(node) = queue.pop_front() {
501        result.push(node);
502        for &next in &adj[node] {
503            in_degree[next] -= 1;
504            if in_degree[next] == 0 {
505                queue.push_back(next);
506            }
507        }
508    }
509    if result.len() == n {
510        Ok(result)
511    } else {
512        Err("cycle detected in dependency graph".to_string())
513    }
514}
515/// Assign dense ranks to a slice of comparable values.
516///
517/// Returns a `Vec<usize>` where the `i`-th entry is the rank of `v\[i\]`
518/// (0 = smallest). Equal values receive the same rank.
519pub fn dense_rank<T: Ord>(v: &[T]) -> Vec<usize> {
520    let mut indexed: Vec<(usize, &T)> = v.iter().enumerate().collect();
521    indexed.sort_by_key(|(_, val)| *val);
522    let mut rank = vec![0usize; v.len()];
523    let mut current_rank = 0usize;
524    for i in 0..indexed.len() {
525        if i > 0 && indexed[i].1 != indexed[i - 1].1 {
526            current_rank += 1;
527        }
528        rank[indexed[i].0] = current_rank;
529    }
530    rank
531}
532/// Assign competition ranks (1224 ranking: equal items get same rank,
533/// next rank skips).
534pub fn competition_rank<T: Ord>(v: &[T]) -> Vec<usize> {
535    let n = v.len();
536    if n == 0 {
537        return Vec::new();
538    }
539    let mut ranks = vec![1usize; n];
540    for i in 0..n {
541        for j in 0..n {
542            if i != j && v[j] < v[i] {
543                ranks[i] += 1;
544            }
545        }
546    }
547    ranks
548}
549/// Extension trait for ordered types providing utility methods.
550pub trait OrdExt: Ord + Sized {
551    /// Return the value clamped to `[lo, hi]`.
552    fn clamped(self, lo: Self, hi: Self) -> Self {
553        ord_clamp(self, lo, hi)
554    }
555    /// Return the `OrdResult` of comparing `self` with `other`.
556    fn ord_cmp(&self, other: &Self) -> OrdResult {
557        compare(self, other)
558    }
559    /// Return `true` if `self` is strictly between `lo` and `hi`.
560    fn strictly_between(&self, lo: &Self, hi: &Self) -> bool {
561        self > lo && self < hi
562    }
563    /// Return `true` if `self` is in the closed interval `[lo, hi]`.
564    fn in_range(&self, lo: &Self, hi: &Self) -> bool {
565        self >= lo && self <= hi
566    }
567}
568impl<T: Ord> OrdExt for T {}
569/// Build `Ord.min : {α : Type} → \[Ord α\] → α → α → α`.
570pub fn build_ord_min(env: &mut Environment) -> Result<(), String> {
571    use oxilean_kernel::{BinderInfo, Declaration, Expr, Level, Name};
572    let type1 = Expr::Sort(Level::succ(Level::zero()));
573    let ty = Expr::Pi(
574        BinderInfo::Implicit,
575        Name::str("α"),
576        Node::new(type1.clone()),
577        Node::new(Expr::Pi(
578            BinderInfo::InstImplicit,
579            Name::str("_"),
580            Node::new(Expr::App(
581                Node::new(Expr::Const(Name::str("Ord"), vec![])),
582                Node::new(Expr::BVar(0)),
583            )),
584            Node::new(Expr::Pi(
585                BinderInfo::Default,
586                Name::str("a"),
587                Node::new(Expr::BVar(1)),
588                Node::new(Expr::Pi(
589                    BinderInfo::Default,
590                    Name::str("b"),
591                    Node::new(Expr::BVar(2)),
592                    Node::new(Expr::BVar(3)),
593                )),
594            )),
595        )),
596    );
597    env.add(Declaration::Axiom {
598        name: Name::str("Ord.min"),
599        univ_params: vec![],
600        ty,
601    })
602    .map_err(|e| e.to_string())
603}
604/// Build `Ord.max : {α : Type} → \[Ord α\] → α → α → α`.
605pub fn build_ord_max(env: &mut Environment) -> Result<(), String> {
606    use oxilean_kernel::{BinderInfo, Declaration, Expr, Level, Name};
607    let type1 = Expr::Sort(Level::succ(Level::zero()));
608    let ty = Expr::Pi(
609        BinderInfo::Implicit,
610        Name::str("α"),
611        Node::new(type1.clone()),
612        Node::new(Expr::Pi(
613            BinderInfo::InstImplicit,
614            Name::str("_"),
615            Node::new(Expr::App(
616                Node::new(Expr::Const(Name::str("Ord"), vec![])),
617                Node::new(Expr::BVar(0)),
618            )),
619            Node::new(Expr::Pi(
620                BinderInfo::Default,
621                Name::str("a"),
622                Node::new(Expr::BVar(1)),
623                Node::new(Expr::Pi(
624                    BinderInfo::Default,
625                    Name::str("b"),
626                    Node::new(Expr::BVar(2)),
627                    Node::new(Expr::BVar(3)),
628                )),
629            )),
630        )),
631    );
632    env.add(Declaration::Axiom {
633        name: Name::str("Ord.max"),
634        univ_params: vec![],
635        ty,
636    })
637    .map_err(|e| e.to_string())
638}
639#[cfg(test)]
640mod ord_advanced_tests {
641    use super::*;
642    #[test]
643    fn test_topological_sort_dag() {
644        let result = topological_sort(3, &[(0, 1), (1, 2)]).expect("operation should succeed");
645        assert!(result.iter().position(|&x| x == 0) < result.iter().position(|&x| x == 1));
646        assert!(result.iter().position(|&x| x == 1) < result.iter().position(|&x| x == 2));
647    }
648    #[test]
649    fn test_topological_sort_cycle() {
650        assert!(topological_sort(2, &[(0, 1), (1, 0)]).is_err());
651    }
652    #[test]
653    fn test_topological_sort_empty() {
654        let result = topological_sort(0, &[]).expect("operation should succeed");
655        assert!(result.is_empty());
656    }
657    #[test]
658    fn test_dense_rank_basic() {
659        let v = vec![3u32, 1, 4, 1, 5, 9, 2, 6];
660        let ranks = dense_rank(&v);
661        assert_eq!(ranks[1], 0);
662        assert_eq!(ranks[3], 0);
663    }
664    #[test]
665    fn test_dense_rank_all_equal() {
666        let v = vec![5u32, 5, 5];
667        let ranks = dense_rank(&v);
668        assert!(ranks.iter().all(|&r| r == 0));
669    }
670    #[test]
671    fn test_competition_rank() {
672        let v = vec![1u32, 2, 2, 3];
673        let ranks = competition_rank(&v);
674        assert_eq!(ranks[0], 1);
675        assert_eq!(ranks[1], 2);
676        assert_eq!(ranks[2], 2);
677        assert_eq!(ranks[3], 4);
678    }
679    #[test]
680    fn test_ord_ext_clamped() {
681        assert_eq!(5u32.clamped(1, 10), 5);
682        assert_eq!(0u32.clamped(1, 10), 1);
683        assert_eq!(15u32.clamped(1, 10), 10);
684    }
685    #[test]
686    fn test_ord_ext_strictly_between() {
687        assert!(5u32.strictly_between(&1, &10));
688        assert!(!1u32.strictly_between(&1, &10));
689        assert!(!10u32.strictly_between(&1, &10));
690    }
691    #[test]
692    fn test_ord_ext_in_range() {
693        assert!(5u32.in_range(&1, &10));
694        assert!(1u32.in_range(&1, &10));
695        assert!(10u32.in_range(&1, &10));
696        assert!(!0u32.in_range(&1, &10));
697    }
698    #[test]
699    fn test_permutation_identity() {
700        let p = Permutation::identity(3);
701        assert!(p.is_identity());
702    }
703    #[test]
704    fn test_permutation_from_sort_order() {
705        let v = vec![3u32, 1, 2];
706        let p = Permutation::from_sort_order(&v);
707        let sorted = p.apply(&v);
708        assert_eq!(sorted, vec![1, 2, 3]);
709    }
710    #[test]
711    fn test_permutation_inverse() {
712        let v = vec![3u32, 1, 2];
713        let p = Permutation::from_sort_order(&v);
714        let inv = p.inverse();
715        let composed = p.compose(&inv);
716        assert!(composed.is_identity());
717    }
718    #[test]
719    fn test_permutation_compose() {
720        let p = Permutation {
721            perm: vec![1, 0, 2],
722        };
723        let q = Permutation {
724            perm: vec![0, 1, 2],
725        };
726        let pq = p.compose(&q);
727        assert_eq!(pq.perm, vec![1, 0, 2]);
728    }
729    #[test]
730    fn test_build_ord_min_max() {
731        let mut env = Environment::new();
732        build_ord_env(&mut env).expect("build_ord_env should succeed");
733        assert!(build_ord_min(&mut env).is_ok());
734        assert!(build_ord_max(&mut env).is_ok());
735    }
736    #[test]
737    fn test_sorted_map_overwrite() {
738        let mut m: SortedMap<u32, u32> = SortedMap::new();
739        m.insert(1, 100);
740        m.insert(1, 200);
741        assert_eq!(m.get(&1), Some(&200));
742        assert_eq!(m.len(), 1);
743    }
744    #[test]
745    fn test_sorted_set_remove() {
746        let mut s: SortedSet<u32> = SortedSet::new();
747        s.insert(3);
748        s.insert(5);
749        assert!(s.remove(&3));
750        assert!(!s.contains(&3));
751        assert!(!s.remove(&3));
752    }
753}
754pub fn ord_e_type1() -> Expr {
755    Expr::Sort(Level::succ(Level::zero()))
756}
757pub fn ord_e_type2() -> Expr {
758    Expr::Sort(Level::succ(Level::succ(Level::zero())))
759}
760pub fn ord_e_prop() -> Expr {
761    Expr::Sort(Level::zero())
762}
763pub fn ord_e_arrow(dom: Expr, cod: Expr) -> Expr {
764    Expr::Pi(
765        BinderInfo::Default,
766        Name::str("_"),
767        Node::new(dom),
768        Node::new(cod),
769    )
770}
771pub fn ord_e_pi(name: &str, dom: Expr, body: Expr) -> Expr {
772    Expr::Pi(
773        BinderInfo::Default,
774        Name::str(name),
775        Node::new(dom),
776        Node::new(body),
777    )
778}
779pub fn ord_e_ipi(name: &str, dom: Expr, body: Expr) -> Expr {
780    Expr::Pi(
781        BinderInfo::Implicit,
782        Name::str(name),
783        Node::new(dom),
784        Node::new(body),
785    )
786}
787pub fn ord_e_app(f: Expr, a: Expr) -> Expr {
788    Expr::App(Node::new(f), Node::new(a))
789}
790pub fn ord_e_app2(f: Expr, a: Expr, b: Expr) -> Expr {
791    ord_e_app(ord_e_app(f, a), b)
792}
793pub fn ord_e_app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
794    ord_e_app(ord_e_app2(f, a, b), c)
795}
796pub fn ord_e_nat() -> Expr {
797    Expr::Const(Name::str("Nat"), vec![])
798}
799pub fn ord_e_bool() -> Expr {
800    Expr::Const(Name::str("Bool"), vec![])
801}
802pub fn ord_e_prop_app2(name: &str, a: Expr, b: Expr) -> Expr {
803    ord_e_app2(Expr::Const(Name::str(name), vec![]), a, b)
804}
805pub fn ord_e_eq(ty: Expr, a: Expr, b: Expr) -> Expr {
806    ord_e_app3(Expr::Const(Name::str("Eq"), vec![]), ty, a, b)
807}
808pub fn ord_e_and(a: Expr, b: Expr) -> Expr {
809    ord_e_prop_app2("And", a, b)
810}
811pub fn ord_e_iff(a: Expr, b: Expr) -> Expr {
812    ord_e_prop_app2("Iff", a, b)
813}
814pub fn ord_e_ordering() -> Expr {
815    Expr::Const(Name::str("Ordering"), vec![])
816}
817pub fn ord_e_ord_inst(alpha: Expr) -> Expr {
818    ord_e_app(Expr::Const(Name::str("Ord"), vec![]), alpha)
819}
820pub fn ord_e_add_axiom(env: &mut Environment, name: &str, ty: Expr) -> Result<(), String> {
821    env.add(Declaration::Axiom {
822        name: Name::str(name),
823        univ_params: vec![],
824        ty,
825    })
826    .map_err(|e| e.to_string())
827}
828/// `OrdCat : Type 2` — the category of preordered sets.
829pub fn axiom_ord_cat_ty() -> Expr {
830    ord_e_type2()
831}
832/// `OrdCat.obj : OrdCat → Type` — extract the underlying type.
833pub fn axiom_ord_cat_obj_ty() -> Expr {
834    ord_e_arrow(Expr::Const(Name::str("OrdCat"), vec![]), ord_e_type1())
835}
836/// `MonotoneMap : {α β : Type} → \[Ord α\] → \[Ord β\] → Type` — monotone maps.
837pub fn axiom_monotone_map_ty() -> Expr {
838    ord_e_ipi(
839        "α",
840        ord_e_type1(),
841        ord_e_ipi(
842            "β",
843            ord_e_type1(),
844            Expr::Pi(
845                BinderInfo::InstImplicit,
846                Name::str("_"),
847                Node::new(ord_e_ord_inst(Expr::BVar(1))),
848                Node::new(Expr::Pi(
849                    BinderInfo::InstImplicit,
850                    Name::str("_"),
851                    Node::new(ord_e_ord_inst(Expr::BVar(1))),
852                    Node::new(ord_e_type1()),
853                )),
854            ),
855        ),
856    )
857}
858/// `MonotoneMap.mk : (f : α → β) → (∀ a b, a ≤ b → f a ≤ f b) → MonotoneMap`
859pub fn axiom_monotone_map_mk_ty() -> Expr {
860    ord_e_ipi(
861        "α",
862        ord_e_type1(),
863        ord_e_ipi(
864            "β",
865            ord_e_type1(),
866            ord_e_pi(
867                "f",
868                ord_e_arrow(Expr::BVar(1), Expr::BVar(0)),
869                ord_e_pi(
870                    "mono",
871                    Expr::Const(Name::str("MonotoneMap.mono_proof_ty"), vec![]),
872                    Expr::Const(Name::str("MonotoneMap"), vec![]),
873                ),
874            ),
875        ),
876    )
877}
878/// `MonotoneMapsFormCat : Prop` — order-preserving maps form a category.
879pub fn axiom_monotone_maps_form_cat_ty() -> Expr {
880    ord_e_prop()
881}
882/// `GaloisConnection : {α β : Type} → \[Ord α\] → \[Ord β\] → (α → β) → (β → α) → Prop`
883pub fn axiom_galois_connection_ty() -> Expr {
884    ord_e_ipi(
885        "α",
886        ord_e_type1(),
887        ord_e_ipi(
888            "β",
889            ord_e_type1(),
890            Expr::Pi(
891                BinderInfo::InstImplicit,
892                Name::str("_"),
893                Node::new(ord_e_ord_inst(Expr::BVar(1))),
894                Node::new(Expr::Pi(
895                    BinderInfo::InstImplicit,
896                    Name::str("_"),
897                    Node::new(ord_e_ord_inst(Expr::BVar(1))),
898                    Node::new(ord_e_pi(
899                        "l",
900                        ord_e_arrow(Expr::BVar(3), Expr::BVar(2)),
901                        ord_e_pi("r", ord_e_arrow(Expr::BVar(3), Expr::BVar(4)), ord_e_prop()),
902                    )),
903                )),
904            ),
905        ),
906    )
907}
908/// `GaloisConnection.adjoint_iff : Prop` — adjoint functors as Galois connections.
909pub fn axiom_galois_adjoint_iff_ty() -> Expr {
910    ord_e_prop()
911}
912/// `OrdEnrichedCat : Type 2` — Ord-enriched categories.
913pub fn axiom_ord_enriched_cat_ty() -> Expr {
914    ord_e_type2()
915}
916/// `FixpointExists : {α : Type} → \[Ord α\] → (α → α) → Prop` — Knaster-Tarski fixpoint.
917pub fn axiom_fixpoint_exists_ty() -> Expr {
918    ord_e_ipi(
919        "α",
920        ord_e_type1(),
921        Expr::Pi(
922            BinderInfo::InstImplicit,
923            Name::str("_"),
924            Node::new(ord_e_ord_inst(Expr::BVar(0))),
925            Node::new(ord_e_pi(
926                "f",
927                ord_e_arrow(Expr::BVar(1), Expr::BVar(1)),
928                ord_e_prop(),
929            )),
930        ),
931    )
932}
933/// `KnasterTarski : {α : Type} → \[CompleteLattice α\] → (α → α) → α` — least fixpoint.
934pub fn axiom_knaster_tarski_ty() -> Expr {
935    ord_e_ipi(
936        "α",
937        ord_e_type1(),
938        Expr::Pi(
939            BinderInfo::InstImplicit,
940            Name::str("_"),
941            Node::new(ord_e_app(
942                Expr::Const(Name::str("CompleteLattice"), vec![]),
943                Expr::BVar(0),
944            )),
945            Node::new(ord_e_pi(
946                "f",
947                ord_e_arrow(Expr::BVar(1), Expr::BVar(1)),
948                Expr::BVar(2),
949            )),
950        ),
951    )
952}
953/// `KnasterTarski.least_fixpoint : Prop` — KT produces the least fixpoint.
954pub fn axiom_knaster_tarski_least_ty() -> Expr {
955    ord_e_prop()
956}
957/// `ScottContinuous : {α β : Type} → \[Ord α\] → \[Ord β\] → (α → β) → Prop`.
958pub fn axiom_scott_continuous_ty() -> Expr {
959    ord_e_ipi(
960        "α",
961        ord_e_type1(),
962        ord_e_ipi(
963            "β",
964            ord_e_type1(),
965            Expr::Pi(
966                BinderInfo::InstImplicit,
967                Name::str("_"),
968                Node::new(ord_e_ord_inst(Expr::BVar(1))),
969                Node::new(Expr::Pi(
970                    BinderInfo::InstImplicit,
971                    Name::str("_"),
972                    Node::new(ord_e_ord_inst(Expr::BVar(1))),
973                    Node::new(ord_e_pi(
974                        "f",
975                        ord_e_arrow(Expr::BVar(3), Expr::BVar(2)),
976                        ord_e_prop(),
977                    )),
978                )),
979            ),
980        ),
981    )
982}
983/// `DCPO : Type 2` — directed-complete partial orders.
984pub fn axiom_dcpo_ty() -> Expr {
985    ord_e_type2()
986}
987/// `DCPO.lfp : {D : DCPO} → (D.carrier → D.carrier) → D.carrier` — least fixpoint in DCPO.
988pub fn axiom_dcpo_lfp_ty() -> Expr {
989    ord_e_pi(
990        "D",
991        Expr::Const(Name::str("DCPO"), vec![]),
992        ord_e_pi(
993            "f",
994            ord_e_arrow(
995                ord_e_app(
996                    Expr::Const(Name::str("DCPO.carrier"), vec![]),
997                    Expr::BVar(0),
998                ),
999                ord_e_app(
1000                    Expr::Const(Name::str("DCPO.carrier"), vec![]),
1001                    Expr::BVar(0),
1002                ),
1003            ),
1004            ord_e_app(
1005                Expr::Const(Name::str("DCPO.carrier"), vec![]),
1006                Expr::BVar(1),
1007            ),
1008        ),
1009    )
1010}
1011/// `OmegaCPO : Type 2` — omega-complete partial orders.
1012pub fn axiom_omega_cpo_ty() -> Expr {
1013    ord_e_type2()
1014}
1015/// `OmegaCPO.chain_limit : {D : OmegaCPO} → (Nat → D.carrier) → D.carrier`.
1016pub fn axiom_omega_cpo_chain_limit_ty() -> Expr {
1017    ord_e_pi(
1018        "D",
1019        Expr::Const(Name::str("OmegaCPO"), vec![]),
1020        ord_e_pi(
1021            "chain",
1022            ord_e_arrow(
1023                ord_e_nat(),
1024                ord_e_app(
1025                    Expr::Const(Name::str("OmegaCPO.carrier"), vec![]),
1026                    Expr::BVar(0),
1027                ),
1028            ),
1029            ord_e_app(
1030                Expr::Const(Name::str("OmegaCPO.carrier"), vec![]),
1031                Expr::BVar(1),
1032            ),
1033        ),
1034    )
1035}
1036/// `LazyEvalOrd : {α : Type} → \[Ord α\] → Thunk α → Thunk α → Ordering` — lazy comparison.
1037pub fn axiom_lazy_eval_ord_ty() -> Expr {
1038    ord_e_ipi(
1039        "α",
1040        ord_e_type1(),
1041        Expr::Pi(
1042            BinderInfo::InstImplicit,
1043            Name::str("_"),
1044            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1045            Node::new(ord_e_pi(
1046                "a",
1047                ord_e_app(Expr::Const(Name::str("Thunk"), vec![]), Expr::BVar(1)),
1048                ord_e_pi(
1049                    "b",
1050                    ord_e_app(Expr::Const(Name::str("Thunk"), vec![]), Expr::BVar(2)),
1051                    ord_e_ordering(),
1052                ),
1053            )),
1054        ),
1055    )
1056}
1057/// `SortingNetworkCorrect : (n : Nat) → (net : SortingNetwork n) → Prop`.
1058pub fn axiom_sorting_network_correct_ty() -> Expr {
1059    ord_e_pi(
1060        "n",
1061        ord_e_nat(),
1062        ord_e_pi(
1063            "net",
1064            ord_e_app(
1065                Expr::Const(Name::str("SortingNetwork"), vec![]),
1066                Expr::BVar(0),
1067            ),
1068            ord_e_prop(),
1069        ),
1070    )
1071}
1072/// `ComparisonSortLowerBound : Prop` — Omega(n log n) lower bound for comparison sorts.
1073pub fn axiom_comparison_sort_lower_bound_ty() -> Expr {
1074    ord_e_prop()
1075}
1076/// `BTreeInvariant : {α : Type} → \[Ord α\] → (t : BTree α) → Prop`.
1077pub fn axiom_btree_invariant_ty() -> Expr {
1078    ord_e_ipi(
1079        "α",
1080        ord_e_type1(),
1081        Expr::Pi(
1082            BinderInfo::InstImplicit,
1083            Name::str("_"),
1084            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1085            Node::new(ord_e_pi(
1086                "t",
1087                ord_e_app(Expr::Const(Name::str("BTree"), vec![]), Expr::BVar(1)),
1088                ord_e_prop(),
1089            )),
1090        ),
1091    )
1092}
1093/// `RedBlackBalance : {α : Type} → \[Ord α\] → (t : RBTree α) → Prop`.
1094pub fn axiom_red_black_balance_ty() -> Expr {
1095    ord_e_ipi(
1096        "α",
1097        ord_e_type1(),
1098        Expr::Pi(
1099            BinderInfo::InstImplicit,
1100            Name::str("_"),
1101            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1102            Node::new(ord_e_pi(
1103                "t",
1104                ord_e_app(Expr::Const(Name::str("RBTree"), vec![]), Expr::BVar(1)),
1105                ord_e_prop(),
1106            )),
1107        ),
1108    )
1109}
1110/// `WellFounded.lt : {α : Type} → \[Ord α\] → WellFounded (· < ·)` — well-foundedness.
1111pub fn axiom_well_founded_lt_ty() -> Expr {
1112    ord_e_ipi(
1113        "α",
1114        ord_e_type1(),
1115        Expr::Pi(
1116            BinderInfo::InstImplicit,
1117            Name::str("_"),
1118            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1119            Node::new(ord_e_app(
1120                Expr::Const(Name::str("WellFounded"), vec![]),
1121                Expr::Const(Name::str("LT.lt"), vec![]),
1122            )),
1123        ),
1124    )
1125}
1126/// `Antisymm : {α : Type} → \[Ord α\] → ∀ a b, a ≤ b → b ≤ a → a = b`.
1127pub fn axiom_antisymm_ty() -> Expr {
1128    ord_e_ipi(
1129        "α",
1130        ord_e_type1(),
1131        Expr::Pi(
1132            BinderInfo::InstImplicit,
1133            Name::str("_"),
1134            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1135            Node::new(ord_e_pi(
1136                "a",
1137                Expr::BVar(1),
1138                ord_e_pi(
1139                    "b",
1140                    Expr::BVar(2),
1141                    ord_e_pi(
1142                        "h1",
1143                        ord_e_prop_app2("LE.le", Expr::BVar(1), Expr::BVar(0)),
1144                        ord_e_pi(
1145                            "h2",
1146                            ord_e_prop_app2("LE.le", Expr::BVar(1), Expr::BVar(2)),
1147                            ord_e_eq(Expr::BVar(4), Expr::BVar(3), Expr::BVar(2)),
1148                        ),
1149                    ),
1150                ),
1151            )),
1152        ),
1153    )
1154}
1155/// `Transitivity : {α : Type} → \[Ord α\] → ∀ a b c, a ≤ b → b ≤ c → a ≤ c`.
1156pub fn axiom_transitivity_ty() -> Expr {
1157    ord_e_ipi(
1158        "α",
1159        ord_e_type1(),
1160        Expr::Pi(
1161            BinderInfo::InstImplicit,
1162            Name::str("_"),
1163            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1164            Node::new(ord_e_pi(
1165                "a",
1166                Expr::BVar(1),
1167                ord_e_pi(
1168                    "b",
1169                    Expr::BVar(2),
1170                    ord_e_pi(
1171                        "c",
1172                        Expr::BVar(3),
1173                        ord_e_pi(
1174                            "hab",
1175                            ord_e_prop_app2("LE.le", Expr::BVar(2), Expr::BVar(1)),
1176                            ord_e_pi(
1177                                "hbc",
1178                                ord_e_prop_app2("LE.le", Expr::BVar(2), Expr::BVar(1)),
1179                                ord_e_prop_app2("LE.le", Expr::BVar(4), Expr::BVar(2)),
1180                            ),
1181                        ),
1182                    ),
1183                ),
1184            )),
1185        ),
1186    )
1187}
1188/// `Totality : {α : Type} → \[Ord α\] → ∀ a b, a ≤ b ∨ b ≤ a`.
1189pub fn axiom_totality_ty() -> Expr {
1190    ord_e_ipi(
1191        "α",
1192        ord_e_type1(),
1193        Expr::Pi(
1194            BinderInfo::InstImplicit,
1195            Name::str("_"),
1196            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1197            Node::new(ord_e_pi(
1198                "a",
1199                Expr::BVar(1),
1200                ord_e_pi(
1201                    "b",
1202                    Expr::BVar(2),
1203                    ord_e_app2(
1204                        Expr::Const(Name::str("Or"), vec![]),
1205                        ord_e_prop_app2("LE.le", Expr::BVar(1), Expr::BVar(0)),
1206                        ord_e_prop_app2("LE.le", Expr::BVar(0), Expr::BVar(1)),
1207                    ),
1208                ),
1209            )),
1210        ),
1211    )
1212}
1213/// `Reflexivity : {α : Type} → \[Ord α\] → ∀ a, a ≤ a`.
1214pub fn axiom_reflexivity_ty() -> Expr {
1215    ord_e_ipi(
1216        "α",
1217        ord_e_type1(),
1218        Expr::Pi(
1219            BinderInfo::InstImplicit,
1220            Name::str("_"),
1221            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1222            Node::new(ord_e_pi(
1223                "a",
1224                Expr::BVar(1),
1225                ord_e_prop_app2("LE.le", Expr::BVar(0), Expr::BVar(0)),
1226            )),
1227        ),
1228    )
1229}
1230/// `Monotone : {α β : Type} → \[Ord α\] → \[Ord β\] → (α → β) → Prop`.
1231pub fn axiom_monotone_ty() -> Expr {
1232    ord_e_ipi(
1233        "α",
1234        ord_e_type1(),
1235        ord_e_ipi(
1236            "β",
1237            ord_e_type1(),
1238            Expr::Pi(
1239                BinderInfo::InstImplicit,
1240                Name::str("_"),
1241                Node::new(ord_e_ord_inst(Expr::BVar(1))),
1242                Node::new(Expr::Pi(
1243                    BinderInfo::InstImplicit,
1244                    Name::str("_"),
1245                    Node::new(ord_e_ord_inst(Expr::BVar(1))),
1246                    Node::new(ord_e_pi(
1247                        "f",
1248                        ord_e_arrow(Expr::BVar(3), Expr::BVar(2)),
1249                        ord_e_prop(),
1250                    )),
1251                )),
1252            ),
1253        ),
1254    )
1255}
1256/// `StrictMono : {α β : Type} → \[Ord α\] → \[Ord β\] → (α → β) → Prop`.
1257pub fn axiom_strict_mono_ty() -> Expr {
1258    ord_e_ipi(
1259        "α",
1260        ord_e_type1(),
1261        ord_e_ipi(
1262            "β",
1263            ord_e_type1(),
1264            Expr::Pi(
1265                BinderInfo::InstImplicit,
1266                Name::str("_"),
1267                Node::new(ord_e_ord_inst(Expr::BVar(1))),
1268                Node::new(Expr::Pi(
1269                    BinderInfo::InstImplicit,
1270                    Name::str("_"),
1271                    Node::new(ord_e_ord_inst(Expr::BVar(1))),
1272                    Node::new(ord_e_pi(
1273                        "f",
1274                        ord_e_arrow(Expr::BVar(3), Expr::BVar(2)),
1275                        ord_e_prop(),
1276                    )),
1277                )),
1278            ),
1279        ),
1280    )
1281}
1282/// `CompleteLattice : Type → Type 1`.
1283pub fn axiom_complete_lattice_ty() -> Expr {
1284    ord_e_arrow(ord_e_type1(), ord_e_type2())
1285}
1286/// `CompleteLattice.sSup : {α : Type} → \[CompleteLattice α\] → Set α → α`.
1287pub fn axiom_complete_lattice_ssup_ty() -> Expr {
1288    ord_e_ipi(
1289        "α",
1290        ord_e_type1(),
1291        Expr::Pi(
1292            BinderInfo::InstImplicit,
1293            Name::str("_"),
1294            Node::new(ord_e_app(
1295                Expr::Const(Name::str("CompleteLattice"), vec![]),
1296                Expr::BVar(0),
1297            )),
1298            Node::new(ord_e_pi(
1299                "S",
1300                ord_e_app(Expr::Const(Name::str("Set"), vec![]), Expr::BVar(1)),
1301                Expr::BVar(2),
1302            )),
1303        ),
1304    )
1305}
1306/// `CompleteLattice.sInf : {α : Type} → \[CompleteLattice α\] → Set α → α`.
1307pub fn axiom_complete_lattice_sinf_ty() -> Expr {
1308    ord_e_ipi(
1309        "α",
1310        ord_e_type1(),
1311        Expr::Pi(
1312            BinderInfo::InstImplicit,
1313            Name::str("_"),
1314            Node::new(ord_e_app(
1315                Expr::Const(Name::str("CompleteLattice"), vec![]),
1316                Expr::BVar(0),
1317            )),
1318            Node::new(ord_e_pi(
1319                "S",
1320                ord_e_app(Expr::Const(Name::str("Set"), vec![]), Expr::BVar(1)),
1321                Expr::BVar(2),
1322            )),
1323        ),
1324    )
1325}
1326/// `UpperBound : {α : Type} → \[Ord α\] → Set α → α → Prop`.
1327pub fn axiom_upper_bound_ty() -> Expr {
1328    ord_e_ipi(
1329        "α",
1330        ord_e_type1(),
1331        Expr::Pi(
1332            BinderInfo::InstImplicit,
1333            Name::str("_"),
1334            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1335            Node::new(ord_e_pi(
1336                "S",
1337                ord_e_app(Expr::Const(Name::str("Set"), vec![]), Expr::BVar(1)),
1338                ord_e_pi("x", Expr::BVar(2), ord_e_prop()),
1339            )),
1340        ),
1341    )
1342}
1343/// `LowerBound : {α : Type} → \[Ord α\] → Set α → α → Prop`.
1344pub fn axiom_lower_bound_ty() -> Expr {
1345    ord_e_ipi(
1346        "α",
1347        ord_e_type1(),
1348        Expr::Pi(
1349            BinderInfo::InstImplicit,
1350            Name::str("_"),
1351            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1352            Node::new(ord_e_pi(
1353                "S",
1354                ord_e_app(Expr::Const(Name::str("Set"), vec![]), Expr::BVar(1)),
1355                ord_e_pi("x", Expr::BVar(2), ord_e_prop()),
1356            )),
1357        ),
1358    )
1359}
1360/// `IsLUB : {α : Type} → \[Ord α\] → Set α → α → Prop` — least upper bound predicate.
1361pub fn axiom_is_lub_ty() -> Expr {
1362    ord_e_ipi(
1363        "α",
1364        ord_e_type1(),
1365        Expr::Pi(
1366            BinderInfo::InstImplicit,
1367            Name::str("_"),
1368            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1369            Node::new(ord_e_pi(
1370                "S",
1371                ord_e_app(Expr::Const(Name::str("Set"), vec![]), Expr::BVar(1)),
1372                ord_e_pi("x", Expr::BVar(2), ord_e_prop()),
1373            )),
1374        ),
1375    )
1376}
1377/// `IsGLB : {α : Type} → \[Ord α\] → Set α → α → Prop` — greatest lower bound predicate.
1378pub fn axiom_is_glb_ty() -> Expr {
1379    ord_e_ipi(
1380        "α",
1381        ord_e_type1(),
1382        Expr::Pi(
1383            BinderInfo::InstImplicit,
1384            Name::str("_"),
1385            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1386            Node::new(ord_e_pi(
1387                "S",
1388                ord_e_app(Expr::Const(Name::str("Set"), vec![]), Expr::BVar(1)),
1389                ord_e_pi("x", Expr::BVar(2), ord_e_prop()),
1390            )),
1391        ),
1392    )
1393}
1394/// `OrderIso : {α β : Type} → \[Ord α\] → \[Ord β\] → Type` — order isomorphisms.
1395pub fn axiom_order_iso_ty() -> Expr {
1396    ord_e_ipi(
1397        "α",
1398        ord_e_type1(),
1399        ord_e_ipi(
1400            "β",
1401            ord_e_type1(),
1402            Expr::Pi(
1403                BinderInfo::InstImplicit,
1404                Name::str("_"),
1405                Node::new(ord_e_ord_inst(Expr::BVar(1))),
1406                Node::new(Expr::Pi(
1407                    BinderInfo::InstImplicit,
1408                    Name::str("_"),
1409                    Node::new(ord_e_ord_inst(Expr::BVar(1))),
1410                    Node::new(ord_e_type1()),
1411                )),
1412            ),
1413        ),
1414    )
1415}
1416/// `OrderEmbedding : {α β : Type} → \[Ord α\] → \[Ord β\] → Type` — order embeddings.
1417pub fn axiom_order_embedding_ty() -> Expr {
1418    ord_e_ipi(
1419        "α",
1420        ord_e_type1(),
1421        ord_e_ipi(
1422            "β",
1423            ord_e_type1(),
1424            Expr::Pi(
1425                BinderInfo::InstImplicit,
1426                Name::str("_"),
1427                Node::new(ord_e_ord_inst(Expr::BVar(1))),
1428                Node::new(Expr::Pi(
1429                    BinderInfo::InstImplicit,
1430                    Name::str("_"),
1431                    Node::new(ord_e_ord_inst(Expr::BVar(1))),
1432                    Node::new(ord_e_type1()),
1433                )),
1434            ),
1435        ),
1436    )
1437}
1438/// `Antichain : {α : Type} → \[Ord α\] → Set α → Prop` — an antichain in a partial order.
1439pub fn axiom_antichain_ty() -> Expr {
1440    ord_e_ipi(
1441        "α",
1442        ord_e_type1(),
1443        Expr::Pi(
1444            BinderInfo::InstImplicit,
1445            Name::str("_"),
1446            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1447            Node::new(ord_e_pi(
1448                "S",
1449                ord_e_app(Expr::Const(Name::str("Set"), vec![]), Expr::BVar(1)),
1450                ord_e_prop(),
1451            )),
1452        ),
1453    )
1454}
1455/// `DilworthTheorem : Prop` — Dilworth's theorem relating chains and antichains.
1456pub fn axiom_dilworth_theorem_ty() -> Expr {
1457    ord_e_prop()
1458}
1459/// `MirskysTheorem : Prop` — Mirsky's theorem dual to Dilworth's.
1460pub fn axiom_mirskys_theorem_ty() -> Expr {
1461    ord_e_prop()
1462}
1463/// `OrdCompare.compare_eq_iff : {α : Type} → \[Ord α\] → ∀ a b, compare a b = Ordering.eq ↔ a = b`.
1464pub fn axiom_compare_eq_iff_ty() -> Expr {
1465    ord_e_ipi(
1466        "α",
1467        ord_e_type1(),
1468        Expr::Pi(
1469            BinderInfo::InstImplicit,
1470            Name::str("_"),
1471            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1472            Node::new(ord_e_pi(
1473                "a",
1474                Expr::BVar(1),
1475                ord_e_pi(
1476                    "b",
1477                    Expr::BVar(2),
1478                    ord_e_iff(
1479                        ord_e_eq(
1480                            ord_e_ordering(),
1481                            ord_e_app2(
1482                                Expr::Const(Name::str("Ord.compare"), vec![]),
1483                                Expr::BVar(1),
1484                                Expr::BVar(0),
1485                            ),
1486                            Expr::Const(Name::str("Ordering.eq"), vec![]),
1487                        ),
1488                        ord_e_eq(Expr::BVar(3), Expr::BVar(1), Expr::BVar(0)),
1489                    ),
1490                ),
1491            )),
1492        ),
1493    )
1494}
1495/// `OrdCompare.compare_swap : {α : Type} → \[Ord α\] → ∀ a b, compare a b = (compare b a).swap`.
1496pub fn axiom_compare_swap_ty() -> Expr {
1497    ord_e_ipi(
1498        "α",
1499        ord_e_type1(),
1500        Expr::Pi(
1501            BinderInfo::InstImplicit,
1502            Name::str("_"),
1503            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1504            Node::new(ord_e_pi(
1505                "a",
1506                Expr::BVar(1),
1507                ord_e_pi(
1508                    "b",
1509                    Expr::BVar(2),
1510                    ord_e_eq(
1511                        ord_e_ordering(),
1512                        ord_e_app2(
1513                            Expr::Const(Name::str("Ord.compare"), vec![]),
1514                            Expr::BVar(1),
1515                            Expr::BVar(0),
1516                        ),
1517                        ord_e_app(
1518                            Expr::Const(Name::str("Ordering.swap"), vec![]),
1519                            ord_e_app2(
1520                                Expr::Const(Name::str("Ord.compare"), vec![]),
1521                                Expr::BVar(0),
1522                                Expr::BVar(1),
1523                            ),
1524                        ),
1525                    ),
1526                ),
1527            )),
1528        ),
1529    )
1530}
1531/// `BoolOrd : Ord Bool` — the canonical ordering on `Bool` (false < true).
1532pub fn axiom_bool_ord_ty() -> Expr {
1533    ord_e_ord_inst(ord_e_bool())
1534}
1535/// `NatOrd : Ord Nat` — the canonical ordering on `Nat`.
1536pub fn axiom_nat_ord_ty() -> Expr {
1537    ord_e_ord_inst(ord_e_nat())
1538}
1539/// `ProdOrd : {α β : Type} → \[Ord α\] → \[Ord β\] → Ord (α × β)` — lexicographic product order.
1540pub fn axiom_prod_ord_ty() -> Expr {
1541    ord_e_ipi(
1542        "α",
1543        ord_e_type1(),
1544        ord_e_ipi(
1545            "β",
1546            ord_e_type1(),
1547            Expr::Pi(
1548                BinderInfo::InstImplicit,
1549                Name::str("_"),
1550                Node::new(ord_e_ord_inst(Expr::BVar(1))),
1551                Node::new(Expr::Pi(
1552                    BinderInfo::InstImplicit,
1553                    Name::str("_"),
1554                    Node::new(ord_e_ord_inst(Expr::BVar(1))),
1555                    Node::new(ord_e_ord_inst(ord_e_app2(
1556                        Expr::Const(Name::str("Prod"), vec![]),
1557                        Expr::BVar(3),
1558                        Expr::BVar(2),
1559                    ))),
1560                )),
1561            ),
1562        ),
1563    )
1564}
1565/// `ListOrd : {α : Type} → \[Ord α\] → Ord (List α)` — lexicographic list order.
1566pub fn axiom_list_ord_ty() -> Expr {
1567    ord_e_ipi(
1568        "α",
1569        ord_e_type1(),
1570        Expr::Pi(
1571            BinderInfo::InstImplicit,
1572            Name::str("_"),
1573            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1574            Node::new(ord_e_ord_inst(ord_e_app(
1575                Expr::Const(Name::str("List"), vec![]),
1576                Expr::BVar(1),
1577            ))),
1578        ),
1579    )
1580}
1581/// `OptionOrd : {α : Type} → \[Ord α\] → Ord (Option α)` — option order (None is least).
1582pub fn axiom_option_ord_ty() -> Expr {
1583    ord_e_ipi(
1584        "α",
1585        ord_e_type1(),
1586        Expr::Pi(
1587            BinderInfo::InstImplicit,
1588            Name::str("_"),
1589            Node::new(ord_e_ord_inst(Expr::BVar(0))),
1590            Node::new(ord_e_ord_inst(ord_e_app(
1591                Expr::Const(Name::str("Option"), vec![]),
1592                Expr::BVar(1),
1593            ))),
1594        ),
1595    )
1596}
1597/// `HeytingAlgebra : Type → Type 1` — Heyting algebras (intuitionistic lattices).
1598pub fn axiom_heyting_algebra_ty() -> Expr {
1599    ord_e_arrow(ord_e_type1(), ord_e_type2())
1600}
1601/// `BooleanAlgebra : Type → Type 1` — Boolean algebras.
1602pub fn axiom_boolean_algebra_ty() -> Expr {
1603    ord_e_arrow(ord_e_type1(), ord_e_type2())
1604}
1605/// Register all extended Ord axioms into the environment.
1606pub fn register_ord_extended(env: &mut Environment) -> Result<(), String> {
1607    ord_e_add_axiom(env, "OrdCat", axiom_ord_cat_ty())?;
1608    ord_e_add_axiom(env, "OrdCat.obj", axiom_ord_cat_obj_ty())?;
1609    ord_e_add_axiom(
1610        env,
1611        "MonotoneMapsFormCat",
1612        axiom_monotone_maps_form_cat_ty(),
1613    )?;
1614    ord_e_add_axiom(
1615        env,
1616        "GaloisConnection.adjoint_iff",
1617        axiom_galois_adjoint_iff_ty(),
1618    )?;
1619    ord_e_add_axiom(env, "OrdEnrichedCat", axiom_ord_enriched_cat_ty())?;
1620    ord_e_add_axiom(
1621        env,
1622        "KnasterTarski.least_fixpoint",
1623        axiom_knaster_tarski_least_ty(),
1624    )?;
1625    ord_e_add_axiom(env, "DCPO", axiom_dcpo_ty())?;
1626    ord_e_add_axiom(env, "OmegaCPO", axiom_omega_cpo_ty())?;
1627    ord_e_add_axiom(
1628        env,
1629        "ComparisonSortLowerBound",
1630        axiom_comparison_sort_lower_bound_ty(),
1631    )?;
1632    ord_e_add_axiom(env, "WellFounded.lt", axiom_well_founded_lt_ty())?;
1633    ord_e_add_axiom(env, "Antisymm", axiom_antisymm_ty())?;
1634    ord_e_add_axiom(env, "Transitivity", axiom_transitivity_ty())?;
1635    ord_e_add_axiom(env, "Totality", axiom_totality_ty())?;
1636    ord_e_add_axiom(env, "Reflexivity", axiom_reflexivity_ty())?;
1637    ord_e_add_axiom(env, "Monotone", axiom_monotone_ty())?;
1638    ord_e_add_axiom(env, "StrictMono", axiom_strict_mono_ty())?;
1639    ord_e_add_axiom(env, "CompleteLattice", axiom_complete_lattice_ty())?;
1640    ord_e_add_axiom(env, "UpperBound", axiom_upper_bound_ty())?;
1641    ord_e_add_axiom(env, "LowerBound", axiom_lower_bound_ty())?;
1642    ord_e_add_axiom(env, "IsLUB", axiom_is_lub_ty())?;
1643    ord_e_add_axiom(env, "IsGLB", axiom_is_glb_ty())?;
1644    ord_e_add_axiom(env, "OrderIso", axiom_order_iso_ty())?;
1645    ord_e_add_axiom(env, "OrderEmbedding", axiom_order_embedding_ty())?;
1646    ord_e_add_axiom(env, "Antichain", axiom_antichain_ty())?;
1647    ord_e_add_axiom(env, "DilworthTheorem", axiom_dilworth_theorem_ty())?;
1648    ord_e_add_axiom(env, "MirskysTheorem", axiom_mirskys_theorem_ty())?;
1649    ord_e_add_axiom(env, "OrdCompare.compare_eq_iff", axiom_compare_eq_iff_ty())?;
1650    ord_e_add_axiom(env, "OrdCompare.compare_swap", axiom_compare_swap_ty())?;
1651    ord_e_add_axiom(env, "BoolOrd", axiom_bool_ord_ty())?;
1652    ord_e_add_axiom(env, "NatOrd", axiom_nat_ord_ty())?;
1653    ord_e_add_axiom(env, "ProdOrd", axiom_prod_ord_ty())?;
1654    ord_e_add_axiom(env, "ListOrd", axiom_list_ord_ty())?;
1655    ord_e_add_axiom(env, "OptionOrd", axiom_option_ord_ty())?;
1656    ord_e_add_axiom(env, "HeytingAlgebra", axiom_heyting_algebra_ty())?;
1657    ord_e_add_axiom(env, "BooleanAlgebra", axiom_boolean_algebra_ty())?;
1658    Ok(())
1659}
oxilean_std/ord/functions.rs

oxilean_std/ord/
functions.rs
