oxilean_std/ord/
functions.rs

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

oxilean_std/ord/
functions.rs
