oxilean_std/order/
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
7#[allow(dead_code)]
8pub fn app(f: Expr, a: Expr) -> Expr {
9    Expr::App(Box::new(f), Box::new(a))
10}
11#[allow(dead_code)]
12pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
13    app(app(f, a), b)
14}
15#[allow(dead_code)]
16pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
17    app(app2(f, a, b), c)
18}
19pub(super) fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
20    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
21}
22#[allow(dead_code)]
23pub fn lam(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
24    Expr::Lam(bi, Name::str(name), Box::new(dom), Box::new(body))
25}
26pub fn cst(s: &str) -> Expr {
27    Expr::Const(Name::str(s), vec![])
28}
29pub(super) fn prop() -> Expr {
30    Expr::Sort(Level::zero())
31}
32pub(super) fn type0() -> Expr {
33    Expr::Sort(Level::succ(Level::zero()))
34}
35pub fn type1() -> Expr {
36    Expr::Sort(Level::succ(Level::succ(Level::zero())))
37}
38pub(super) fn bvar(n: u32) -> Expr {
39    Expr::BVar(n)
40}
41pub(super) fn add_axiom(
42    env: &mut Environment,
43    name: &str,
44    univ_params: Vec<Name>,
45    ty: Expr,
46) -> Result<(), String> {
47    env.add(Declaration::Axiom {
48        name: Name::str(name),
49        univ_params,
50        ty,
51    })
52    .map_err(|e| e.to_string())
53}
54/// Build `Type → Type 1` (the type of a type class).
55#[allow(dead_code)]
56pub fn mk_class_ty() -> Expr {
57    pi(BinderInfo::Default, "α", type0(), type1())
58}
59/// Build a binary relation method type:
60/// `{α : Type} → [Class α] → α → α → Prop`
61#[allow(dead_code)]
62pub fn mk_relation_method(class: &str) -> Expr {
63    pi(
64        BinderInfo::Implicit,
65        "α",
66        type0(),
67        pi(
68            BinderInfo::InstImplicit,
69            "_inst",
70            app(cst(class), bvar(0)),
71            pi(
72                BinderInfo::Default,
73                "a",
74                bvar(1),
75                pi(BinderInfo::Default, "b", bvar(2), prop()),
76            ),
77        ),
78    )
79}
80/// Build a binary operation method type:
81/// `{α : Type} → [Class α] → α → α → α`
82#[allow(dead_code)]
83pub fn mk_binop_method(class: &str) -> Expr {
84    pi(
85        BinderInfo::Implicit,
86        "α",
87        type0(),
88        pi(
89            BinderInfo::InstImplicit,
90            "_inst",
91            app(cst(class), bvar(0)),
92            pi(
93                BinderInfo::Default,
94                "a",
95                bvar(1),
96                pi(BinderInfo::Default, "b", bvar(2), bvar(3)),
97            ),
98        ),
99    )
100}
101/// Build a nullary method type: `{α : Type} → [Class α] → α`
102#[allow(dead_code)]
103pub fn mk_nullary_method(class: &str) -> Expr {
104    pi(
105        BinderInfo::Implicit,
106        "α",
107        type0(),
108        pi(
109            BinderInfo::InstImplicit,
110            "_inst",
111            app(cst(class), bvar(0)),
112            bvar(1),
113        ),
114    )
115}
116/// Build `Eq @{} α a b`.
117#[allow(dead_code)]
118pub fn mk_eq(ty: Expr, lhs: Expr, rhs: Expr) -> Expr {
119    app3(cst("Eq"), ty, lhs, rhs)
120}
121/// Build a law with ∀ (a : α):
122/// `{α : Type} → [Class α] → ∀ (a : α), <prop>`
123#[allow(dead_code)]
124pub fn mk_law_forall1<F>(class: &str, prop_builder: F) -> Expr
125where
126    F: FnOnce(u32) -> Expr,
127{
128    pi(
129        BinderInfo::Implicit,
130        "α",
131        type0(),
132        pi(
133            BinderInfo::InstImplicit,
134            "_inst",
135            app(cst(class), bvar(0)),
136            pi(BinderInfo::Default, "a", bvar(1), prop_builder(3)),
137        ),
138    )
139}
140/// Build a law with ∀ (a b : α):
141/// `{α : Type} → [Class α] → ∀ (a b : α), <prop>`
142#[allow(dead_code)]
143pub fn mk_law_forall2<F>(class: &str, prop_builder: F) -> Expr
144where
145    F: FnOnce(u32) -> Expr,
146{
147    pi(
148        BinderInfo::Implicit,
149        "α",
150        type0(),
151        pi(
152            BinderInfo::InstImplicit,
153            "_inst",
154            app(cst(class), bvar(0)),
155            pi(
156                BinderInfo::Default,
157                "a",
158                bvar(1),
159                pi(BinderInfo::Default, "b", bvar(2), prop_builder(4)),
160            ),
161        ),
162    )
163}
164/// Build a law with ∀ (a b c : α):
165/// `{α : Type} → [Class α] → ∀ (a b c : α), <prop>`
166#[allow(dead_code)]
167pub fn mk_law_forall3<F>(class: &str, prop_builder: F) -> Expr
168where
169    F: FnOnce(u32) -> Expr,
170{
171    pi(
172        BinderInfo::Implicit,
173        "α",
174        type0(),
175        pi(
176            BinderInfo::InstImplicit,
177            "_inst",
178            app(cst(class), bvar(0)),
179            pi(
180                BinderInfo::Default,
181                "a",
182                bvar(1),
183                pi(
184                    BinderInfo::Default,
185                    "b",
186                    bvar(2),
187                    pi(BinderInfo::Default, "c", bvar(3), prop_builder(5)),
188                ),
189            ),
190        ),
191    )
192}
193/// Build an "extends" projection:
194/// `{α : Type} → [Class α] → ParentClass α`
195#[allow(dead_code)]
196pub fn mk_extends(class: &str, parent: &str) -> Expr {
197    pi(
198        BinderInfo::Implicit,
199        "α",
200        type0(),
201        pi(
202            BinderInfo::InstImplicit,
203            "_inst",
204            app(cst(class), bvar(0)),
205            app(cst(parent), bvar(1)),
206        ),
207    )
208}
209/// Build `LE.le a b`.
210#[allow(dead_code)]
211pub fn mk_le(a: Expr, b: Expr) -> Expr {
212    app2(cst("LE.le"), a, b)
213}
214/// Build `LT.lt a b`.
215#[allow(dead_code)]
216pub fn mk_lt(a: Expr, b: Expr) -> Expr {
217    app2(cst("LT.lt"), a, b)
218}
219/// Build `Sup.sup a b`.
220#[allow(dead_code)]
221pub fn mk_sup(a: Expr, b: Expr) -> Expr {
222    app2(cst("Sup.sup"), a, b)
223}
224/// Build `Inf.inf a b`.
225#[allow(dead_code)]
226pub fn mk_inf(a: Expr, b: Expr) -> Expr {
227    app2(cst("Inf.inf"), a, b)
228}
229/// Build `Min.min a b`.
230#[allow(dead_code)]
231pub fn mk_min(a: Expr, b: Expr) -> Expr {
232    app2(cst("Min.min"), a, b)
233}
234/// Build `Max.max a b`.
235#[allow(dead_code)]
236pub fn mk_max(a: Expr, b: Expr) -> Expr {
237    app2(cst("Max.max"), a, b)
238}
239/// Build `Monotone f` as an expression application.
240#[allow(dead_code)]
241pub fn mk_monotone(f: Expr) -> Expr {
242    app(cst("Monotone"), f)
243}
244/// Build the order environment with all order-theoretic type classes and laws.
245#[allow(clippy::too_many_lines)]
246pub fn build_order_env(env: &mut Environment) -> Result<(), String> {
247    add_axiom(env, "LE", vec![], mk_class_ty())?;
248    add_axiom(env, "LE.le", vec![], mk_relation_method("LE"))?;
249    add_axiom(env, "LT", vec![], mk_class_ty())?;
250    add_axiom(env, "LT.lt", vec![], mk_relation_method("LT"))?;
251    add_axiom(env, "Preorder", vec![], mk_class_ty())?;
252    add_axiom(env, "Preorder.toLE", vec![], mk_extends("Preorder", "LE"))?;
253    add_axiom(env, "Preorder.toLT", vec![], mk_extends("Preorder", "LT"))?;
254    add_axiom(
255        env,
256        "le_refl",
257        vec![],
258        mk_law_forall1("Preorder", |_depth| {
259            let a = bvar(0);
260            app2(cst("LE.le"), a.clone(), a)
261        }),
262    )?;
263    add_axiom(
264        env,
265        "le_trans",
266        vec![],
267        mk_law_forall3("Preorder", |_depth| {
268            let a = bvar(2);
269            let b = bvar(1);
270            let c = bvar(0);
271            pi(
272                BinderInfo::Default,
273                "hab",
274                app2(cst("LE.le"), a.clone(), b.clone()),
275                pi(
276                    BinderInfo::Default,
277                    "hbc",
278                    app2(cst("LE.le"), b, c.clone()),
279                    app2(cst("LE.le"), a, c),
280                ),
281            )
282        }),
283    )?;
284    add_axiom(env, "PartialOrder", vec![], mk_class_ty())?;
285    add_axiom(
286        env,
287        "PartialOrder.toPreorder",
288        vec![],
289        mk_extends("PartialOrder", "Preorder"),
290    )?;
291    add_axiom(
292        env,
293        "le_antisymm",
294        vec![],
295        mk_law_forall2("PartialOrder", |depth| {
296            let alpha = bvar(depth - 1);
297            let a = bvar(1);
298            let b = bvar(0);
299            pi(
300                BinderInfo::Default,
301                "hab",
302                app2(cst("LE.le"), a.clone(), b.clone()),
303                pi(
304                    BinderInfo::Default,
305                    "hba",
306                    app2(cst("LE.le"), b.clone(), a.clone()),
307                    mk_eq(alpha, a, b),
308                ),
309            )
310        }),
311    )?;
312    add_axiom(env, "LinearOrder", vec![], mk_class_ty())?;
313    add_axiom(
314        env,
315        "LinearOrder.toPartialOrder",
316        vec![],
317        mk_extends("LinearOrder", "PartialOrder"),
318    )?;
319    add_axiom(
320        env,
321        "le_total",
322        vec![],
323        mk_law_forall2("LinearOrder", |_depth| {
324            let a = bvar(1);
325            let b = bvar(0);
326            app2(
327                cst("Or"),
328                app2(cst("LE.le"), a.clone(), b.clone()),
329                app2(cst("LE.le"), b, a),
330            )
331        }),
332    )?;
333    add_axiom(env, "DecidableLinearOrder", vec![], mk_class_ty())?;
334    add_axiom(
335        env,
336        "DecidableLinearOrder.toLinearOrder",
337        vec![],
338        mk_extends("DecidableLinearOrder", "LinearOrder"),
339    )?;
340    add_axiom(
341        env,
342        "DecidableLinearOrder.decidableEq",
343        vec![],
344        mk_relation_method("DecidableLinearOrder"),
345    )?;
346    add_axiom(
347        env,
348        "DecidableLinearOrder.decidableLe",
349        vec![],
350        mk_relation_method("DecidableLinearOrder"),
351    )?;
352    add_axiom(
353        env,
354        "DecidableLinearOrder.decidableLt",
355        vec![],
356        mk_relation_method("DecidableLinearOrder"),
357    )?;
358    add_axiom(env, "Sup", vec![], mk_class_ty())?;
359    add_axiom(env, "Sup.sup", vec![], mk_binop_method("Sup"))?;
360    add_axiom(env, "Inf", vec![], mk_class_ty())?;
361    add_axiom(env, "Inf.inf", vec![], mk_binop_method("Inf"))?;
362    add_axiom(env, "SemilatticeSup", vec![], mk_class_ty())?;
363    add_axiom(
364        env,
365        "SemilatticeSup.toPartialOrder",
366        vec![],
367        mk_extends("SemilatticeSup", "PartialOrder"),
368    )?;
369    add_axiom(
370        env,
371        "SemilatticeSup.toSup",
372        vec![],
373        mk_extends("SemilatticeSup", "Sup"),
374    )?;
375    add_axiom(
376        env,
377        "le_sup_left",
378        vec![],
379        mk_law_forall2("SemilatticeSup", |_depth| {
380            let a = bvar(1);
381            let b = bvar(0);
382            app2(cst("LE.le"), a.clone(), app2(cst("Sup.sup"), a, b))
383        }),
384    )?;
385    add_axiom(
386        env,
387        "le_sup_right",
388        vec![],
389        mk_law_forall2("SemilatticeSup", |_depth| {
390            let a = bvar(1);
391            let b = bvar(0);
392            app2(cst("LE.le"), b.clone(), app2(cst("Sup.sup"), a, b))
393        }),
394    )?;
395    add_axiom(
396        env,
397        "sup_le",
398        vec![],
399        mk_law_forall3("SemilatticeSup", |_depth| {
400            let a = bvar(2);
401            let b = bvar(1);
402            let c = bvar(0);
403            pi(
404                BinderInfo::Default,
405                "hac",
406                app2(cst("LE.le"), a.clone(), c.clone()),
407                pi(
408                    BinderInfo::Default,
409                    "hbc",
410                    app2(cst("LE.le"), b.clone(), c.clone()),
411                    app2(cst("LE.le"), app2(cst("Sup.sup"), a, b), c),
412                ),
413            )
414        }),
415    )?;
416    add_axiom(env, "SemilatticeInf", vec![], mk_class_ty())?;
417    add_axiom(
418        env,
419        "SemilatticeInf.toPartialOrder",
420        vec![],
421        mk_extends("SemilatticeInf", "PartialOrder"),
422    )?;
423    add_axiom(
424        env,
425        "SemilatticeInf.toInf",
426        vec![],
427        mk_extends("SemilatticeInf", "Inf"),
428    )?;
429    add_axiom(
430        env,
431        "inf_le_left",
432        vec![],
433        mk_law_forall2("SemilatticeInf", |_depth| {
434            let a = bvar(1);
435            let b = bvar(0);
436            app2(cst("LE.le"), app2(cst("Inf.inf"), a.clone(), b), a)
437        }),
438    )?;
439    add_axiom(
440        env,
441        "inf_le_right",
442        vec![],
443        mk_law_forall2("SemilatticeInf", |_depth| {
444            let a = bvar(1);
445            let b = bvar(0);
446            app2(cst("LE.le"), app2(cst("Inf.inf"), a, b.clone()), b)
447        }),
448    )?;
449    add_axiom(
450        env,
451        "le_inf",
452        vec![],
453        mk_law_forall3("SemilatticeInf", |_depth| {
454            let a = bvar(2);
455            let b = bvar(1);
456            let c = bvar(0);
457            pi(
458                BinderInfo::Default,
459                "hab",
460                app2(cst("LE.le"), a.clone(), b.clone()),
461                pi(
462                    BinderInfo::Default,
463                    "hac",
464                    app2(cst("LE.le"), a.clone(), c.clone()),
465                    app2(cst("LE.le"), a, app2(cst("Inf.inf"), b, c)),
466                ),
467            )
468        }),
469    )?;
470    add_axiom(env, "Lattice", vec![], mk_class_ty())?;
471    add_axiom(
472        env,
473        "Lattice.toSemilatticeSup",
474        vec![],
475        mk_extends("Lattice", "SemilatticeSup"),
476    )?;
477    add_axiom(
478        env,
479        "Lattice.toSemilatticeInf",
480        vec![],
481        mk_extends("Lattice", "SemilatticeInf"),
482    )?;
483    add_axiom(
484        env,
485        "sup_comm",
486        vec![],
487        mk_law_forall2("Lattice", |depth| {
488            let alpha = bvar(depth - 1);
489            let a = bvar(1);
490            let b = bvar(0);
491            mk_eq(
492                alpha,
493                app2(cst("Sup.sup"), a.clone(), b.clone()),
494                app2(cst("Sup.sup"), b, a),
495            )
496        }),
497    )?;
498    add_axiom(
499        env,
500        "inf_comm",
501        vec![],
502        mk_law_forall2("Lattice", |depth| {
503            let alpha = bvar(depth - 1);
504            let a = bvar(1);
505            let b = bvar(0);
506            mk_eq(
507                alpha,
508                app2(cst("Inf.inf"), a.clone(), b.clone()),
509                app2(cst("Inf.inf"), b, a),
510            )
511        }),
512    )?;
513    add_axiom(
514        env,
515        "sup_assoc",
516        vec![],
517        mk_law_forall3("Lattice", |depth| {
518            let alpha = bvar(depth - 1);
519            let a = bvar(2);
520            let b = bvar(1);
521            let c = bvar(0);
522            mk_eq(
523                alpha,
524                app2(
525                    cst("Sup.sup"),
526                    app2(cst("Sup.sup"), a.clone(), b.clone()),
527                    c.clone(),
528                ),
529                app2(cst("Sup.sup"), a, app2(cst("Sup.sup"), b, c)),
530            )
531        }),
532    )?;
533    add_axiom(
534        env,
535        "inf_assoc",
536        vec![],
537        mk_law_forall3("Lattice", |depth| {
538            let alpha = bvar(depth - 1);
539            let a = bvar(2);
540            let b = bvar(1);
541            let c = bvar(0);
542            mk_eq(
543                alpha,
544                app2(
545                    cst("Inf.inf"),
546                    app2(cst("Inf.inf"), a.clone(), b.clone()),
547                    c.clone(),
548                ),
549                app2(cst("Inf.inf"), a, app2(cst("Inf.inf"), b, c)),
550            )
551        }),
552    )?;
553    add_axiom(
554        env,
555        "sup_inf_distrib",
556        vec![],
557        mk_law_forall3("Lattice", |depth| {
558            let alpha = bvar(depth - 1);
559            let a = bvar(2);
560            let b = bvar(1);
561            let c = bvar(0);
562            mk_eq(
563                alpha,
564                app2(
565                    cst("Sup.sup"),
566                    a.clone(),
567                    app2(cst("Inf.inf"), b.clone(), c.clone()),
568                ),
569                app2(
570                    cst("Inf.inf"),
571                    app2(cst("Sup.sup"), a.clone(), b),
572                    app2(cst("Sup.sup"), a, c),
573                ),
574            )
575        }),
576    )?;
577    add_axiom(
578        env,
579        "inf_sup_distrib",
580        vec![],
581        mk_law_forall3("Lattice", |depth| {
582            let alpha = bvar(depth - 1);
583            let a = bvar(2);
584            let b = bvar(1);
585            let c = bvar(0);
586            mk_eq(
587                alpha,
588                app2(
589                    cst("Inf.inf"),
590                    a.clone(),
591                    app2(cst("Sup.sup"), b.clone(), c.clone()),
592                ),
593                app2(
594                    cst("Sup.sup"),
595                    app2(cst("Inf.inf"), a.clone(), b),
596                    app2(cst("Inf.inf"), a, c),
597                ),
598            )
599        }),
600    )?;
601    add_axiom(env, "BoundedOrder", vec![], mk_class_ty())?;
602    add_axiom(
603        env,
604        "BoundedOrder.toPartialOrder",
605        vec![],
606        mk_extends("BoundedOrder", "PartialOrder"),
607    )?;
608    add_axiom(env, "Top", vec![], mk_class_ty())?;
609    add_axiom(env, "Top.top", vec![], mk_nullary_method("Top"))?;
610    add_axiom(env, "Bot", vec![], mk_class_ty())?;
611    add_axiom(env, "Bot.bot", vec![], mk_nullary_method("Bot"))?;
612    add_axiom(
613        env,
614        "BoundedOrder.toTop",
615        vec![],
616        mk_extends("BoundedOrder", "Top"),
617    )?;
618    add_axiom(
619        env,
620        "BoundedOrder.toBot",
621        vec![],
622        mk_extends("BoundedOrder", "Bot"),
623    )?;
624    add_axiom(
625        env,
626        "le_top",
627        vec![],
628        mk_law_forall1("BoundedOrder", |_depth| {
629            let a = bvar(0);
630            app2(cst("LE.le"), a, cst("Top.top"))
631        }),
632    )?;
633    add_axiom(
634        env,
635        "bot_le",
636        vec![],
637        mk_law_forall1("BoundedOrder", |_depth| {
638            let a = bvar(0);
639            app2(cst("LE.le"), cst("Bot.bot"), a)
640        }),
641    )?;
642    add_axiom(env, "CompleteLattice", vec![], mk_class_ty())?;
643    add_axiom(
644        env,
645        "CompleteLattice.toLattice",
646        vec![],
647        mk_extends("CompleteLattice", "Lattice"),
648    )?;
649    add_axiom(
650        env,
651        "CompleteLattice.toBoundedOrder",
652        vec![],
653        mk_extends("CompleteLattice", "BoundedOrder"),
654    )?;
655    add_axiom(
656        env,
657        "CompleteLattice.sSup",
658        vec![],
659        pi(
660            BinderInfo::Implicit,
661            "α",
662            type0(),
663            pi(
664                BinderInfo::InstImplicit,
665                "_inst",
666                app(cst("CompleteLattice"), bvar(0)),
667                pi(
668                    BinderInfo::Default,
669                    "s",
670                    pi(BinderInfo::Default, "_", bvar(1), prop()),
671                    bvar(2),
672                ),
673            ),
674        ),
675    )?;
676    add_axiom(
677        env,
678        "CompleteLattice.sInf",
679        vec![],
680        pi(
681            BinderInfo::Implicit,
682            "α",
683            type0(),
684            pi(
685                BinderInfo::InstImplicit,
686                "_inst",
687                app(cst("CompleteLattice"), bvar(0)),
688                pi(
689                    BinderInfo::Default,
690                    "s",
691                    pi(BinderInfo::Default, "_", bvar(1), prop()),
692                    bvar(2),
693                ),
694            ),
695        ),
696    )?;
697    add_axiom(env, "Min", vec![], mk_class_ty())?;
698    add_axiom(env, "Min.min", vec![], mk_binop_method("Min"))?;
699    add_axiom(env, "Max", vec![], mk_class_ty())?;
700    add_axiom(env, "Max.max", vec![], mk_binop_method("Max"))?;
701    add_axiom(
702        env,
703        "min_le_left",
704        vec![],
705        mk_law_forall2("Min", |_depth| {
706            let a = bvar(1);
707            let b = bvar(0);
708            app2(cst("LE.le"), app2(cst("Min.min"), a.clone(), b), a)
709        }),
710    )?;
711    add_axiom(
712        env,
713        "min_le_right",
714        vec![],
715        mk_law_forall2("Min", |_depth| {
716            let a = bvar(1);
717            let b = bvar(0);
718            app2(cst("LE.le"), app2(cst("Min.min"), a, b.clone()), b)
719        }),
720    )?;
721    add_axiom(
722        env,
723        "le_max_left",
724        vec![],
725        mk_law_forall2("Max", |_depth| {
726            let a = bvar(1);
727            let b = bvar(0);
728            app2(cst("LE.le"), a.clone(), app2(cst("Max.max"), a, b))
729        }),
730    )?;
731    add_axiom(
732        env,
733        "le_max_right",
734        vec![],
735        mk_law_forall2("Max", |_depth| {
736            let a = bvar(1);
737            let b = bvar(0);
738            app2(cst("LE.le"), b.clone(), app2(cst("Max.max"), a, b))
739        }),
740    )?;
741    add_axiom(
742        env,
743        "Monotone",
744        vec![],
745        pi(
746            BinderInfo::Implicit,
747            "α",
748            type0(),
749            pi(
750                BinderInfo::Implicit,
751                "β",
752                type0(),
753                pi(
754                    BinderInfo::InstImplicit,
755                    "_inst1",
756                    app(cst("Preorder"), bvar(1)),
757                    pi(
758                        BinderInfo::InstImplicit,
759                        "_inst2",
760                        app(cst("Preorder"), bvar(1)),
761                        pi(
762                            BinderInfo::Default,
763                            "f",
764                            pi(BinderInfo::Default, "_", bvar(3), bvar(2)),
765                            prop(),
766                        ),
767                    ),
768                ),
769            ),
770        ),
771    )?;
772    add_axiom(
773        env,
774        "Antitone",
775        vec![],
776        pi(
777            BinderInfo::Implicit,
778            "α",
779            type0(),
780            pi(
781                BinderInfo::Implicit,
782                "β",
783                type0(),
784                pi(
785                    BinderInfo::InstImplicit,
786                    "_inst1",
787                    app(cst("Preorder"), bvar(1)),
788                    pi(
789                        BinderInfo::InstImplicit,
790                        "_inst2",
791                        app(cst("Preorder"), bvar(1)),
792                        pi(
793                            BinderInfo::Default,
794                            "f",
795                            pi(BinderInfo::Default, "_", bvar(3), bvar(2)),
796                            prop(),
797                        ),
798                    ),
799                ),
800            ),
801        ),
802    )?;
803    add_axiom(
804        env,
805        "monotone_id",
806        vec![],
807        pi(
808            BinderInfo::Implicit,
809            "α",
810            type0(),
811            pi(
812                BinderInfo::InstImplicit,
813                "_inst",
814                app(cst("Preorder"), bvar(0)),
815                app(
816                    cst("Monotone"),
817                    lam(BinderInfo::Default, "x", bvar(1), bvar(0)),
818                ),
819            ),
820        ),
821    )?;
822    add_axiom(
823        env,
824        "monotone_comp",
825        vec![],
826        pi(
827            BinderInfo::Implicit,
828            "α",
829            type0(),
830            pi(
831                BinderInfo::Implicit,
832                "β",
833                type0(),
834                pi(
835                    BinderInfo::Implicit,
836                    "γ",
837                    type0(),
838                    pi(
839                        BinderInfo::InstImplicit,
840                        "_inst1",
841                        app(cst("Preorder"), bvar(2)),
842                        pi(
843                            BinderInfo::InstImplicit,
844                            "_inst2",
845                            app(cst("Preorder"), bvar(2)),
846                            pi(
847                                BinderInfo::InstImplicit,
848                                "_inst3",
849                                app(cst("Preorder"), bvar(2)),
850                                pi(
851                                    BinderInfo::Implicit,
852                                    "f",
853                                    pi(BinderInfo::Default, "_", bvar(5), bvar(5)),
854                                    pi(
855                                        BinderInfo::Implicit,
856                                        "g",
857                                        pi(BinderInfo::Default, "_", bvar(5), bvar(5)),
858                                        pi(
859                                            BinderInfo::Default,
860                                            "hf",
861                                            app(cst("Monotone"), bvar(1)),
862                                            pi(
863                                                BinderInfo::Default,
864                                                "hg",
865                                                app(cst("Monotone"), bvar(1)),
866                                                app(
867                                                    cst("Monotone"),
868                                                    lam(
869                                                        BinderInfo::Default,
870                                                        "x",
871                                                        bvar(9),
872                                                        app(bvar(3), app(bvar(4), bvar(0))),
873                                                    ),
874                                                ),
875                                            ),
876                                        ),
877                                    ),
878                                ),
879                            ),
880                        ),
881                    ),
882                ),
883            ),
884        ),
885    )?;
886    Ok(())
887}
888#[allow(dead_code)]
889pub(super) fn ord2_ext_app(f: Expr, a: Expr) -> Expr {
890    Expr::App(Box::new(f), Box::new(a))
891}
892#[allow(dead_code)]
893pub(super) fn ord2_ext_app2(f: Expr, a: Expr, b: Expr) -> Expr {
894    ord2_ext_app(ord2_ext_app(f, a), b)
895}
896#[allow(dead_code)]
897pub fn ord2_ext_app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
898    ord2_ext_app(ord2_ext_app2(f, a, b), c)
899}
900#[allow(dead_code)]
901pub(super) fn ord2_ext_cst(s: &str) -> Expr {
902    Expr::Const(Name::str(s), vec![])
903}
904#[allow(dead_code)]
905pub(super) fn ord2_ext_prop() -> Expr {
906    Expr::Sort(Level::zero())
907}
908#[allow(dead_code)]
909pub(super) fn ord2_ext_type0() -> Expr {
910    Expr::Sort(Level::succ(Level::zero()))
911}
912#[allow(dead_code)]
913pub(super) fn ord2_ext_bvar(n: u32) -> Expr {
914    Expr::BVar(n)
915}
916#[allow(dead_code)]
917pub fn ord2_ext_nat_ty() -> Expr {
918    ord2_ext_cst("Nat")
919}
920#[allow(dead_code)]
921pub(super) fn ord2_ext_arrow(dom: Expr, cod: Expr) -> Expr {
922    Expr::Pi(
923        BinderInfo::Default,
924        Name::Anonymous,
925        Box::new(dom),
926        Box::new(cod),
927    )
928}
929#[allow(dead_code)]
930pub(super) fn ord2_ext_pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
931    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
932}
933/// `{α : Type} → [Class α] → α → α → Prop`
934#[allow(dead_code)]
935pub fn ord2_ext_rel_method(class: &str) -> Expr {
936    ord2_ext_pi(
937        BinderInfo::Implicit,
938        "α",
939        ord2_ext_type0(),
940        ord2_ext_pi(
941            BinderInfo::InstImplicit,
942            "_inst",
943            ord2_ext_app(ord2_ext_cst(class), ord2_ext_bvar(0)),
944            ord2_ext_pi(
945                BinderInfo::Default,
946                "a",
947                ord2_ext_bvar(1),
948                ord2_ext_pi(BinderInfo::Default, "b", ord2_ext_bvar(2), ord2_ext_prop()),
949            ),
950        ),
951    )
952}
953/// `{α : Type} → [Class α] → α → α → α`
954#[allow(dead_code)]
955pub(super) fn ord2_ext_binop_method(class: &str) -> Expr {
956    ord2_ext_pi(
957        BinderInfo::Implicit,
958        "α",
959        ord2_ext_type0(),
960        ord2_ext_pi(
961            BinderInfo::InstImplicit,
962            "_inst",
963            ord2_ext_app(ord2_ext_cst(class), ord2_ext_bvar(0)),
964            ord2_ext_pi(
965                BinderInfo::Default,
966                "a",
967                ord2_ext_bvar(1),
968                ord2_ext_pi(BinderInfo::Default, "b", ord2_ext_bvar(2), ord2_ext_bvar(3)),
969            ),
970        ),
971    )
972}
973/// `{α : Type} → [Class α] → α`
974#[allow(dead_code)]
975pub fn ord2_ext_nullary_method(class: &str) -> Expr {
976    ord2_ext_pi(
977        BinderInfo::Implicit,
978        "α",
979        ord2_ext_type0(),
980        ord2_ext_pi(
981            BinderInfo::InstImplicit,
982            "_inst",
983            ord2_ext_app(ord2_ext_cst(class), ord2_ext_bvar(0)),
984            ord2_ext_bvar(1),
985        ),
986    )
987}
988/// `Type → Type 1`
989#[allow(dead_code)]
990pub(super) fn ord2_ext_class_ty() -> Expr {
991    ord2_ext_pi(
992        BinderInfo::Default,
993        "α",
994        ord2_ext_type0(),
995        Expr::Sort(Level::succ(Level::succ(Level::zero()))),
996    )
997}
998/// `{α : Type} → [C α] → ParentClass α`
999#[allow(dead_code)]
1000pub(super) fn ord2_ext_extends(class: &str, parent: &str) -> Expr {
1001    ord2_ext_pi(
1002        BinderInfo::Implicit,
1003        "α",
1004        ord2_ext_type0(),
1005        ord2_ext_pi(
1006            BinderInfo::InstImplicit,
1007            "_inst",
1008            ord2_ext_app(ord2_ext_cst(class), ord2_ext_bvar(0)),
1009            ord2_ext_app(ord2_ext_cst(parent), ord2_ext_bvar(1)),
1010        ),
1011    )
1012}
1013/// Law with ∀ (a : α).
1014#[allow(dead_code)]
1015pub(super) fn ord2_ext_law1<F>(class: &str, f: F) -> Expr
1016where
1017    F: FnOnce(u32) -> Expr,
1018{
1019    ord2_ext_pi(
1020        BinderInfo::Implicit,
1021        "α",
1022        ord2_ext_type0(),
1023        ord2_ext_pi(
1024            BinderInfo::InstImplicit,
1025            "_inst",
1026            ord2_ext_app(ord2_ext_cst(class), ord2_ext_bvar(0)),
1027            ord2_ext_pi(BinderInfo::Default, "a", ord2_ext_bvar(1), f(3)),
1028        ),
1029    )
1030}
1031/// Law with ∀ (a b : α).
1032#[allow(dead_code)]
1033pub(super) fn ord2_ext_law2<F>(class: &str, f: F) -> Expr
1034where
1035    F: FnOnce(u32) -> Expr,
1036{
1037    ord2_ext_pi(
1038        BinderInfo::Implicit,
1039        "α",
1040        ord2_ext_type0(),
1041        ord2_ext_pi(
1042            BinderInfo::InstImplicit,
1043            "_inst",
1044            ord2_ext_app(ord2_ext_cst(class), ord2_ext_bvar(0)),
1045            ord2_ext_pi(
1046                BinderInfo::Default,
1047                "a",
1048                ord2_ext_bvar(1),
1049                ord2_ext_pi(BinderInfo::Default, "b", ord2_ext_bvar(2), f(4)),
1050            ),
1051        ),
1052    )
1053}
1054/// Law with ∀ (a b c : α).
1055#[allow(dead_code)]
1056pub(super) fn ord2_ext_law3<F>(class: &str, f: F) -> Expr
1057where
1058    F: FnOnce(u32) -> Expr,
1059{
1060    ord2_ext_pi(
1061        BinderInfo::Implicit,
1062        "α",
1063        ord2_ext_type0(),
1064        ord2_ext_pi(
1065            BinderInfo::InstImplicit,
1066            "_inst",
1067            ord2_ext_app(ord2_ext_cst(class), ord2_ext_bvar(0)),
1068            ord2_ext_pi(
1069                BinderInfo::Default,
1070                "a",
1071                ord2_ext_bvar(1),
1072                ord2_ext_pi(
1073                    BinderInfo::Default,
1074                    "b",
1075                    ord2_ext_bvar(2),
1076                    ord2_ext_pi(BinderInfo::Default, "c", ord2_ext_bvar(3), f(5)),
1077                ),
1078            ),
1079        ),
1080    )
1081}
1082#[allow(dead_code)]
1083pub(super) fn ord2_ext_eq(ty: Expr, lhs: Expr, rhs: Expr) -> Expr {
1084    ord2_ext_app3(ord2_ext_cst("Eq"), ty, lhs, rhs)
1085}
1086#[allow(dead_code)]
1087pub fn ord2_ext_and(a: Expr, b: Expr) -> Expr {
1088    ord2_ext_app2(ord2_ext_cst("And"), a, b)
1089}
1090#[allow(dead_code)]
1091pub(super) fn ord2_ext_or(a: Expr, b: Expr) -> Expr {
1092    ord2_ext_app2(ord2_ext_cst("Or"), a, b)
1093}
1094#[allow(dead_code)]
1095pub(super) fn ord2_ext_not(p: Expr) -> Expr {
1096    ord2_ext_app(ord2_ext_cst("Not"), p)
1097}
1098#[allow(dead_code)]
1099pub(super) fn ord2_ext_le(a: Expr, b: Expr) -> Expr {
1100    ord2_ext_app2(ord2_ext_cst("LE.le"), a, b)
1101}
1102#[allow(dead_code)]
1103pub(super) fn ord2_ext_sup(a: Expr, b: Expr) -> Expr {
1104    ord2_ext_app2(ord2_ext_cst("Sup.sup"), a, b)
1105}
1106#[allow(dead_code)]
1107pub(super) fn ord2_ext_inf(a: Expr, b: Expr) -> Expr {
1108    ord2_ext_app2(ord2_ext_cst("Inf.inf"), a, b)
1109}
oxilean_std/order/functions.rs

oxilean_std/order/
functions.rs
