oxilean_std/array/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4#![allow(clippy::items_after_test_module)]
5
6use oxilean_kernel::Node;
7use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
8
9/// Prop: `Sort 0`.
10#[allow(dead_code)]
11pub fn prop() -> Expr {
12    Expr::Sort(Level::zero())
13}
14/// Type 1: `Sort 1`.
15#[allow(dead_code)]
16pub fn type1() -> Expr {
17    Expr::Sort(Level::succ(Level::zero()))
18}
19/// Nat type constant.
20#[allow(dead_code)]
21pub fn nat_ty() -> Expr {
22    Expr::Const(Name::str("Nat"), vec![])
23}
24/// Bool type constant.
25#[allow(dead_code)]
26pub fn bool_ty() -> Expr {
27    Expr::Const(Name::str("Bool"), vec![])
28}
29/// `Fin` applied to a size argument.
30#[allow(dead_code)]
31pub fn fin_of(n: Expr) -> Expr {
32    app(Expr::Const(Name::str("Fin"), vec![]), n)
33}
34/// `Array` applied to element type and size.
35#[allow(dead_code)]
36pub fn array_of(elem_ty: Expr, size: Expr) -> Expr {
37    app2(Expr::Const(Name::str("Array"), vec![]), elem_ty, size)
38}
39/// `Option` applied to a type argument.
40#[allow(dead_code)]
41pub fn option_of(ty: Expr) -> Expr {
42    app(Expr::Const(Name::str("Option"), vec![]), ty)
43}
44/// `List` applied to a type argument.
45#[allow(dead_code)]
46pub fn list_of(ty: Expr) -> Expr {
47    app(Expr::Const(Name::str("List"), vec![]), ty)
48}
49/// `Prod` applied to two type arguments.
50#[allow(dead_code)]
51pub fn prod_of(a: Expr, b: Expr) -> Expr {
52    app2(Expr::Const(Name::str("Prod"), vec![]), a, b)
53}
54/// `Nat.succ n` — successor of a Nat expression.
55#[allow(dead_code)]
56pub fn nat_succ(n: Expr) -> Expr {
57    app(Expr::Const(Name::str("Nat.succ"), vec![]), n)
58}
59/// `Nat.add a b`.
60#[allow(dead_code)]
61pub fn nat_add(a: Expr, b: Expr) -> Expr {
62    app2(Expr::Const(Name::str("Nat.add"), vec![]), a, b)
63}
64/// `Nat.sub a b`.
65#[allow(dead_code)]
66pub fn nat_sub(a: Expr, b: Expr) -> Expr {
67    app2(Expr::Const(Name::str("Nat.sub"), vec![]), a, b)
68}
69/// `Nat.min a b`.
70#[allow(dead_code)]
71pub fn nat_min(a: Expr, b: Expr) -> Expr {
72    app2(Expr::Const(Name::str("Nat.min"), vec![]), a, b)
73}
74/// Build a non-dependent arrow `A -> B`.
75#[allow(dead_code)]
76pub fn arrow(a: Expr, b: Expr) -> Expr {
77    Expr::Pi(
78        BinderInfo::Default,
79        Name::str("_"),
80        Node::new(a),
81        Node::new(b),
82    )
83}
84/// Function application `f a`.
85#[allow(dead_code)]
86pub fn app(f: Expr, a: Expr) -> Expr {
87    Expr::App(Node::new(f), Node::new(a))
88}
89/// Function application `f a b`.
90#[allow(dead_code)]
91pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
92    app(app(f, a), b)
93}
94/// Function application `f a b c`.
95#[allow(dead_code)]
96pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
97    app(app2(f, a, b), c)
98}
99/// An implicit Pi binder.
100#[allow(dead_code)]
101pub fn implicit_pi(name: &str, ty: Expr, body: Expr) -> Expr {
102    Expr::Pi(
103        BinderInfo::Implicit,
104        Name::str(name),
105        Node::new(ty),
106        Node::new(body),
107    )
108}
109/// A default (explicit) Pi binder.
110#[allow(dead_code)]
111pub fn default_pi(name: &str, ty: Expr, body: Expr) -> Expr {
112    Expr::Pi(
113        BinderInfo::Default,
114        Name::str(name),
115        Node::new(ty),
116        Node::new(body),
117    )
118}
119/// An instance Pi binder `[inst : ty]`.
120#[allow(dead_code)]
121pub fn inst_pi(name: &str, ty: Expr, body: Expr) -> Expr {
122    Expr::Pi(
123        BinderInfo::InstImplicit,
124        Name::str(name),
125        Node::new(ty),
126        Node::new(body),
127    )
128}
129/// Build `Eq @{} ty a b`.
130#[allow(dead_code)]
131pub fn eq_expr(ty: Expr, a: Expr, b: Expr) -> Expr {
132    app3(Expr::Const(Name::str("Eq"), vec![]), ty, a, b)
133}
134/// Shorthand to add an axiom to env.
135#[allow(dead_code)]
136pub fn add_axiom(
137    env: &mut Environment,
138    name: &str,
139    univ_params: Vec<Name>,
140    ty: Expr,
141) -> Result<(), String> {
142    env.add(Declaration::Axiom {
143        name: Name::str(name),
144        univ_params,
145        ty,
146    })
147    .map_err(|e| e.to_string())
148}
149/// `Ord` type class applied to a type.
150#[allow(dead_code)]
151pub fn ord_of(ty: Expr) -> Expr {
152    app(Expr::Const(Name::str("Ord"), vec![]), ty)
153}
154/// `BEq` type class applied to a type.
155#[allow(dead_code)]
156pub fn beq_of(ty: Expr) -> Expr {
157    app(Expr::Const(Name::str("BEq"), vec![]), ty)
158}
159/// Build the `Array α n` type expression.
160#[allow(dead_code)]
161pub fn mk_array_ty(elem_ty: Expr, size: Expr) -> Expr {
162    array_of(elem_ty, size)
163}
164/// Build `Array.empty` for a given element type (returns `Array α 0`).
165#[allow(dead_code)]
166pub fn mk_array_empty(elem_ty: Expr) -> Expr {
167    app(Expr::Const(Name::str("Array.empty"), vec![]), elem_ty)
168}
169/// Build `Array.push arr elem`.
170#[allow(dead_code)]
171pub fn mk_array_push(arr: Expr, elem: Expr) -> Expr {
172    app2(Expr::Const(Name::str("Array.push"), vec![]), arr, elem)
173}
174/// Build `Array.get arr idx`.
175#[allow(dead_code)]
176pub fn mk_array_get(arr: Expr, idx: Expr) -> Expr {
177    app2(Expr::Const(Name::str("Array.get"), vec![]), arr, idx)
178}
179/// Build `Array.set arr idx val`.
180#[allow(dead_code)]
181pub fn mk_array_set(arr: Expr, idx: Expr, val: Expr) -> Expr {
182    app3(Expr::Const(Name::str("Array.set"), vec![]), arr, idx, val)
183}
184/// Build `Array.map f arr`.
185#[allow(dead_code)]
186pub fn mk_array_map(f: Expr, arr: Expr) -> Expr {
187    app2(Expr::Const(Name::str("Array.map"), vec![]), f, arr)
188}
189/// Build `Array.foldl f init arr`.
190#[allow(dead_code)]
191pub fn mk_array_foldl(f: Expr, init: Expr, arr: Expr) -> Expr {
192    app3(Expr::Const(Name::str("Array.foldl"), vec![]), f, init, arr)
193}
194/// Build `Array.toList arr`.
195#[allow(dead_code)]
196pub fn mk_array_tolist(arr: Expr) -> Expr {
197    app(Expr::Const(Name::str("Array.toList"), vec![]), arr)
198}
199/// Build Array type and all standard declarations, adding them to the
200/// environment.
201///
202/// Assumes that `Nat`, `Fin`, `Bool`, `Option`, `List`, `Prod`, `Eq`,
203/// `Ord`, `BEq`, `Nat.succ`, `Nat.add`, `Nat.sub`, `Nat.min` are
204/// already declared (or referenced by name).
205pub fn build_array_env(env: &mut Environment) -> Result<(), String> {
206    let array_type = Expr::Pi(
207        BinderInfo::Default,
208        Name::str("α"),
209        Node::new(type1()),
210        Node::new(Expr::Pi(
211            BinderInfo::Default,
212            Name::str("n"),
213            Node::new(nat_ty()),
214            Node::new(type1()),
215        )),
216    );
217    add_axiom(env, "Array", vec![], array_type)?;
218    add_axiom(
219        env,
220        "Array.get",
221        vec![],
222        implicit_pi(
223            "α",
224            type1(),
225            implicit_pi(
226                "n",
227                nat_ty(),
228                default_pi(
229                    "arr",
230                    array_of(Expr::BVar(1), Expr::BVar(0)),
231                    default_pi("i", fin_of(Expr::BVar(1)), Expr::BVar(3)),
232                ),
233            ),
234        ),
235    )?;
236    add_axiom(
237        env,
238        "Array.set",
239        vec![],
240        implicit_pi(
241            "α",
242            type1(),
243            implicit_pi(
244                "n",
245                nat_ty(),
246                default_pi(
247                    "arr",
248                    array_of(Expr::BVar(1), Expr::BVar(0)),
249                    default_pi(
250                        "i",
251                        fin_of(Expr::BVar(1)),
252                        default_pi("val", Expr::BVar(3), array_of(Expr::BVar(4), Expr::BVar(3))),
253                    ),
254                ),
255            ),
256        ),
257    )?;
258    add_axiom(
259        env,
260        "Array.empty",
261        vec![],
262        implicit_pi(
263            "α",
264            type1(),
265            array_of(Expr::BVar(0), Expr::Const(Name::str("Nat.zero"), vec![])),
266        ),
267    )?;
268    add_axiom(
269        env,
270        "Array.mk",
271        vec![],
272        implicit_pi(
273            "α",
274            type1(),
275            default_pi(
276                "data",
277                list_of(Expr::BVar(0)),
278                array_of(
279                    Expr::BVar(1),
280                    app(Expr::Const(Name::str("List.length"), vec![]), Expr::BVar(0)),
281                ),
282            ),
283        ),
284    )?;
285    add_axiom(
286        env,
287        "Array.mkEmpty",
288        vec![],
289        implicit_pi(
290            "α",
291            type1(),
292            default_pi(
293                "capacity",
294                nat_ty(),
295                array_of(Expr::BVar(1), Expr::Const(Name::str("Nat.zero"), vec![])),
296            ),
297        ),
298    )?;
299    add_axiom(
300        env,
301        "Array.size",
302        vec![],
303        implicit_pi(
304            "α",
305            type1(),
306            implicit_pi(
307                "n",
308                nat_ty(),
309                default_pi("arr", array_of(Expr::BVar(1), Expr::BVar(0)), nat_ty()),
310            ),
311        ),
312    )?;
313    add_axiom(
314        env,
315        "Array.push",
316        vec![],
317        implicit_pi(
318            "α",
319            type1(),
320            implicit_pi(
321                "n",
322                nat_ty(),
323                default_pi(
324                    "arr",
325                    array_of(Expr::BVar(1), Expr::BVar(0)),
326                    default_pi(
327                        "x",
328                        Expr::BVar(2),
329                        array_of(Expr::BVar(3), nat_succ(Expr::BVar(2))),
330                    ),
331                ),
332            ),
333        ),
334    )?;
335    add_axiom(
336        env,
337        "Array.pop",
338        vec![],
339        implicit_pi(
340            "α",
341            type1(),
342            implicit_pi(
343                "n",
344                nat_ty(),
345                default_pi(
346                    "arr",
347                    array_of(Expr::BVar(1), nat_succ(Expr::BVar(0))),
348                    prod_of(array_of(Expr::BVar(2), Expr::BVar(1)), Expr::BVar(2)),
349                ),
350            ),
351        ),
352    )?;
353    add_axiom(
354        env,
355        "Array.swap",
356        vec![],
357        implicit_pi(
358            "α",
359            type1(),
360            implicit_pi(
361                "n",
362                nat_ty(),
363                default_pi(
364                    "arr",
365                    array_of(Expr::BVar(1), Expr::BVar(0)),
366                    default_pi(
367                        "i",
368                        fin_of(Expr::BVar(1)),
369                        default_pi(
370                            "j",
371                            fin_of(Expr::BVar(2)),
372                            array_of(Expr::BVar(4), Expr::BVar(3)),
373                        ),
374                    ),
375                ),
376            ),
377        ),
378    )?;
379    add_axiom(
380        env,
381        "Array.map",
382        vec![],
383        implicit_pi(
384            "α",
385            type1(),
386            implicit_pi(
387                "β",
388                type1(),
389                implicit_pi(
390                    "n",
391                    nat_ty(),
392                    default_pi(
393                        "f",
394                        arrow(Expr::BVar(2), Expr::BVar(1)),
395                        default_pi(
396                            "arr",
397                            array_of(Expr::BVar(3), Expr::BVar(1)),
398                            array_of(Expr::BVar(3), Expr::BVar(2)),
399                        ),
400                    ),
401                ),
402            ),
403        ),
404    )?;
405    {
406        let f_ty = arrow(Expr::BVar(1), arrow(Expr::BVar(3), Expr::BVar(3)));
407        add_axiom(
408            env,
409            "Array.foldl",
410            vec![],
411            implicit_pi(
412                "α",
413                type1(),
414                implicit_pi(
415                    "β",
416                    type1(),
417                    implicit_pi(
418                        "n",
419                        nat_ty(),
420                        default_pi(
421                            "f",
422                            f_ty,
423                            default_pi(
424                                "init",
425                                Expr::BVar(2),
426                                default_pi(
427                                    "arr",
428                                    array_of(Expr::BVar(4), Expr::BVar(2)),
429                                    Expr::BVar(4),
430                                ),
431                            ),
432                        ),
433                    ),
434                ),
435            ),
436        )?;
437    }
438    {
439        let f_ty = arrow(Expr::BVar(2), arrow(Expr::BVar(2), Expr::BVar(3)));
440        add_axiom(
441            env,
442            "Array.foldr",
443            vec![],
444            implicit_pi(
445                "α",
446                type1(),
447                implicit_pi(
448                    "β",
449                    type1(),
450                    implicit_pi(
451                        "n",
452                        nat_ty(),
453                        default_pi(
454                            "f",
455                            f_ty,
456                            default_pi(
457                                "init",
458                                Expr::BVar(2),
459                                default_pi(
460                                    "arr",
461                                    array_of(Expr::BVar(4), Expr::BVar(2)),
462                                    Expr::BVar(4),
463                                ),
464                            ),
465                        ),
466                    ),
467                ),
468            ),
469        )?;
470    }
471    add_axiom(
472        env,
473        "Array.filter",
474        vec![],
475        implicit_pi(
476            "α",
477            type1(),
478            implicit_pi(
479                "n",
480                nat_ty(),
481                default_pi(
482                    "p",
483                    arrow(Expr::BVar(1), bool_ty()),
484                    default_pi(
485                        "arr",
486                        array_of(Expr::BVar(2), Expr::BVar(1)),
487                        list_of(Expr::BVar(3)),
488                    ),
489                ),
490            ),
491        ),
492    )?;
493    add_axiom(
494        env,
495        "Array.append",
496        vec![],
497        implicit_pi(
498            "α",
499            type1(),
500            implicit_pi(
501                "n",
502                nat_ty(),
503                implicit_pi(
504                    "m",
505                    nat_ty(),
506                    default_pi(
507                        "a1",
508                        array_of(Expr::BVar(2), Expr::BVar(1)),
509                        default_pi(
510                            "a2",
511                            array_of(Expr::BVar(3), Expr::BVar(1)),
512                            array_of(Expr::BVar(4), nat_add(Expr::BVar(3), Expr::BVar(2))),
513                        ),
514                    ),
515                ),
516            ),
517        ),
518    )?;
519    add_axiom(
520        env,
521        "Array.reverse",
522        vec![],
523        implicit_pi(
524            "α",
525            type1(),
526            implicit_pi(
527                "n",
528                nat_ty(),
529                default_pi(
530                    "arr",
531                    array_of(Expr::BVar(1), Expr::BVar(0)),
532                    array_of(Expr::BVar(2), Expr::BVar(1)),
533                ),
534            ),
535        ),
536    )?;
537    add_axiom(
538        env,
539        "Array.zip",
540        vec![],
541        implicit_pi(
542            "α",
543            type1(),
544            implicit_pi(
545                "β",
546                type1(),
547                implicit_pi(
548                    "n",
549                    nat_ty(),
550                    default_pi(
551                        "a1",
552                        array_of(Expr::BVar(2), Expr::BVar(0)),
553                        default_pi(
554                            "a2",
555                            array_of(Expr::BVar(2), Expr::BVar(1)),
556                            array_of(prod_of(Expr::BVar(4), Expr::BVar(3)), Expr::BVar(2)),
557                        ),
558                    ),
559                ),
560            ),
561        ),
562    )?;
563    add_axiom(
564        env,
565        "Array.enumerate",
566        vec![],
567        implicit_pi(
568            "α",
569            type1(),
570            implicit_pi(
571                "n",
572                nat_ty(),
573                default_pi(
574                    "arr",
575                    array_of(Expr::BVar(1), Expr::BVar(0)),
576                    array_of(prod_of(nat_ty(), Expr::BVar(2)), Expr::BVar(1)),
577                ),
578            ),
579        ),
580    )?;
581    add_axiom(
582        env,
583        "Array.take",
584        vec![],
585        implicit_pi(
586            "α",
587            type1(),
588            implicit_pi(
589                "n",
590                nat_ty(),
591                default_pi(
592                    "k",
593                    nat_ty(),
594                    default_pi(
595                        "arr",
596                        array_of(Expr::BVar(2), Expr::BVar(1)),
597                        array_of(Expr::BVar(3), nat_min(Expr::BVar(1), Expr::BVar(2))),
598                    ),
599                ),
600            ),
601        ),
602    )?;
603    add_axiom(
604        env,
605        "Array.drop",
606        vec![],
607        implicit_pi(
608            "α",
609            type1(),
610            implicit_pi(
611                "n",
612                nat_ty(),
613                default_pi(
614                    "k",
615                    nat_ty(),
616                    default_pi(
617                        "arr",
618                        array_of(Expr::BVar(2), Expr::BVar(1)),
619                        array_of(Expr::BVar(3), nat_sub(Expr::BVar(2), Expr::BVar(1))),
620                    ),
621                ),
622            ),
623        ),
624    )?;
625    add_axiom(
626        env,
627        "Array.any",
628        vec![],
629        implicit_pi(
630            "α",
631            type1(),
632            implicit_pi(
633                "n",
634                nat_ty(),
635                default_pi(
636                    "p",
637                    arrow(Expr::BVar(1), bool_ty()),
638                    default_pi("arr", array_of(Expr::BVar(2), Expr::BVar(1)), bool_ty()),
639                ),
640            ),
641        ),
642    )?;
643    add_axiom(
644        env,
645        "Array.all",
646        vec![],
647        implicit_pi(
648            "α",
649            type1(),
650            implicit_pi(
651                "n",
652                nat_ty(),
653                default_pi(
654                    "p",
655                    arrow(Expr::BVar(1), bool_ty()),
656                    default_pi("arr", array_of(Expr::BVar(2), Expr::BVar(1)), bool_ty()),
657                ),
658            ),
659        ),
660    )?;
661    add_axiom(
662        env,
663        "Array.contains",
664        vec![],
665        implicit_pi(
666            "α",
667            type1(),
668            implicit_pi(
669                "n",
670                nat_ty(),
671                inst_pi(
672                    "inst",
673                    beq_of(Expr::BVar(1)),
674                    default_pi(
675                        "arr",
676                        array_of(Expr::BVar(2), Expr::BVar(1)),
677                        default_pi("a", Expr::BVar(3), bool_ty()),
678                    ),
679                ),
680            ),
681        ),
682    )?;
683    add_axiom(
684        env,
685        "Array.indexOf?",
686        vec![],
687        implicit_pi(
688            "α",
689            type1(),
690            implicit_pi(
691                "n",
692                nat_ty(),
693                inst_pi(
694                    "inst",
695                    beq_of(Expr::BVar(1)),
696                    default_pi(
697                        "arr",
698                        array_of(Expr::BVar(2), Expr::BVar(1)),
699                        default_pi("a", Expr::BVar(3), option_of(fin_of(Expr::BVar(3)))),
700                    ),
701                ),
702            ),
703        ),
704    )?;
705    add_axiom(
706        env,
707        "Array.toList",
708        vec![],
709        implicit_pi(
710            "α",
711            type1(),
712            implicit_pi(
713                "n",
714                nat_ty(),
715                default_pi(
716                    "arr",
717                    array_of(Expr::BVar(1), Expr::BVar(0)),
718                    list_of(Expr::BVar(2)),
719                ),
720            ),
721        ),
722    )?;
723    add_axiom(
724        env,
725        "Array.findSome?",
726        vec![],
727        implicit_pi(
728            "α",
729            type1(),
730            implicit_pi(
731                "β",
732                type1(),
733                implicit_pi(
734                    "n",
735                    nat_ty(),
736                    default_pi(
737                        "f",
738                        arrow(Expr::BVar(2), option_of(Expr::BVar(1))),
739                        default_pi(
740                            "arr",
741                            array_of(Expr::BVar(3), Expr::BVar(1)),
742                            option_of(Expr::BVar(3)),
743                        ),
744                    ),
745                ),
746            ),
747        ),
748    )?;
749    add_axiom(
750        env,
751        "Array.qsort",
752        vec![],
753        implicit_pi(
754            "α",
755            type1(),
756            implicit_pi(
757                "n",
758                nat_ty(),
759                inst_pi(
760                    "inst",
761                    ord_of(Expr::BVar(1)),
762                    default_pi(
763                        "arr",
764                        array_of(Expr::BVar(2), Expr::BVar(1)),
765                        array_of(Expr::BVar(3), Expr::BVar(2)),
766                    ),
767                ),
768            ),
769        ),
770    )?;
771    add_axiom(
772        env,
773        "Array.binSearch",
774        vec![],
775        implicit_pi(
776            "α",
777            type1(),
778            implicit_pi(
779                "n",
780                nat_ty(),
781                inst_pi(
782                    "inst",
783                    ord_of(Expr::BVar(1)),
784                    default_pi(
785                        "arr",
786                        array_of(Expr::BVar(2), Expr::BVar(1)),
787                        default_pi("a", Expr::BVar(3), option_of(fin_of(Expr::BVar(3)))),
788                    ),
789                ),
790            ),
791        ),
792    )?;
793    {
794        let push_expr = app2(
795            Expr::Const(Name::str("Array.push"), vec![]),
796            Expr::BVar(1),
797            Expr::BVar(0),
798        );
799        let size_push = app(Expr::Const(Name::str("Array.size"), vec![]), push_expr);
800        let size_a = app(Expr::Const(Name::str("Array.size"), vec![]), Expr::BVar(1));
801        let succ_size_a = nat_succ(size_a);
802        add_axiom(
803            env,
804            "Array.size_push",
805            vec![],
806            implicit_pi(
807                "α",
808                type1(),
809                implicit_pi(
810                    "n",
811                    nat_ty(),
812                    default_pi(
813                        "a",
814                        array_of(Expr::BVar(1), Expr::BVar(0)),
815                        default_pi(
816                            "x",
817                            Expr::BVar(2),
818                            eq_expr(nat_ty(), size_push, succ_size_a),
819                        ),
820                    ),
821                ),
822            ),
823        )?;
824    }
825    {
826        let set_expr = app3(
827            Expr::Const(Name::str("Array.set"), vec![]),
828            Expr::BVar(2),
829            Expr::BVar(1),
830            Expr::BVar(0),
831        );
832        let get_set = app2(
833            Expr::Const(Name::str("Array.get"), vec![]),
834            set_expr,
835            Expr::BVar(1),
836        );
837        add_axiom(
838            env,
839            "Array.get_set_same",
840            vec![],
841            implicit_pi(
842                "α",
843                type1(),
844                implicit_pi(
845                    "n",
846                    nat_ty(),
847                    default_pi(
848                        "a",
849                        array_of(Expr::BVar(1), Expr::BVar(0)),
850                        default_pi(
851                            "i",
852                            fin_of(Expr::BVar(1)),
853                            default_pi(
854                                "v",
855                                Expr::BVar(3),
856                                eq_expr(Expr::BVar(4), get_set, Expr::BVar(0)),
857                            ),
858                        ),
859                    ),
860                ),
861            ),
862        )?;
863    }
864    {
865        let eq_ij = eq_expr(fin_of(Expr::BVar(4)), Expr::BVar(2), Expr::BVar(1));
866        let not_eq = arrow(eq_ij, Expr::Const(Name::str("False"), vec![]));
867        let set_expr = app3(
868            Expr::Const(Name::str("Array.set"), vec![]),
869            Expr::BVar(4),
870            Expr::BVar(3),
871            Expr::BVar(1),
872        );
873        let get_set_j = app2(
874            Expr::Const(Name::str("Array.get"), vec![]),
875            set_expr,
876            Expr::BVar(2),
877        );
878        let get_a_j = app2(
879            Expr::Const(Name::str("Array.get"), vec![]),
880            Expr::BVar(4),
881            Expr::BVar(2),
882        );
883        add_axiom(
884            env,
885            "Array.get_set_diff",
886            vec![],
887            implicit_pi(
888                "α",
889                type1(),
890                implicit_pi(
891                    "n",
892                    nat_ty(),
893                    default_pi(
894                        "a",
895                        array_of(Expr::BVar(1), Expr::BVar(0)),
896                        default_pi(
897                            "i",
898                            fin_of(Expr::BVar(1)),
899                            default_pi(
900                                "j",
901                                fin_of(Expr::BVar(2)),
902                                default_pi(
903                                    "v",
904                                    Expr::BVar(4),
905                                    default_pi(
906                                        "h",
907                                        not_eq,
908                                        eq_expr(Expr::BVar(6), get_set_j, get_a_j),
909                                    ),
910                                ),
911                            ),
912                        ),
913                    ),
914                ),
915            ),
916        )?;
917    }
918    {
919        let map_fa = app2(
920            Expr::Const(Name::str("Array.map"), vec![]),
921            Expr::BVar(1),
922            Expr::BVar(0),
923        );
924        let size_map = app(Expr::Const(Name::str("Array.size"), vec![]), map_fa);
925        let size_a = app(Expr::Const(Name::str("Array.size"), vec![]), Expr::BVar(0));
926        add_axiom(
927            env,
928            "Array.map_size",
929            vec![],
930            implicit_pi(
931                "α",
932                type1(),
933                implicit_pi(
934                    "β",
935                    type1(),
936                    implicit_pi(
937                        "n",
938                        nat_ty(),
939                        default_pi(
940                            "f",
941                            arrow(Expr::BVar(2), Expr::BVar(1)),
942                            default_pi(
943                                "a",
944                                array_of(Expr::BVar(3), Expr::BVar(1)),
945                                eq_expr(nat_ty(), size_map, size_a),
946                            ),
947                        ),
948                    ),
949                ),
950            ),
951        )?;
952    }
953    {
954        let to_list_a = app(
955            Expr::Const(Name::str("Array.toList"), vec![]),
956            Expr::BVar(0),
957        );
958        let length_tolist = app(Expr::Const(Name::str("List.length"), vec![]), to_list_a);
959        let size_a = app(Expr::Const(Name::str("Array.size"), vec![]), Expr::BVar(0));
960        add_axiom(
961            env,
962            "Array.toList_length",
963            vec![],
964            implicit_pi(
965                "α",
966                type1(),
967                implicit_pi(
968                    "n",
969                    nat_ty(),
970                    default_pi(
971                        "a",
972                        array_of(Expr::BVar(1), Expr::BVar(0)),
973                        eq_expr(nat_ty(), length_tolist, size_a),
974                    ),
975                ),
976            ),
977        )?;
978    }
979    Ok(())
980}
981#[cfg(test)]
982mod tests {
983    use super::*;
984    /// Set up a minimal environment with all prerequisites.
985    fn setup_env() -> Environment {
986        let mut env = Environment::new();
987        for name in &[
988            "Nat", "Bool", "Nat.zero", "Nat.succ", "Nat.add", "Nat.sub", "Nat.min", "Ord", "BEq",
989            "Eq", "False",
990        ] {
991            env.add(Declaration::Axiom {
992                name: Name::str(*name),
993                univ_params: vec![],
994                ty: type1(),
995            })
996            .expect("operation should succeed");
997        }
998        env.add(Declaration::Axiom {
999            name: Name::str("Fin"),
1000            univ_params: vec![],
1001            ty: arrow(nat_ty(), type1()),
1002        })
1003        .expect("operation should succeed");
1004        env.add(Declaration::Axiom {
1005            name: Name::str("Option"),
1006            univ_params: vec![],
1007            ty: arrow(type1(), type1()),
1008        })
1009        .expect("operation should succeed");
1010        env.add(Declaration::Axiom {
1011            name: Name::str("List"),
1012            univ_params: vec![],
1013            ty: arrow(type1(), type1()),
1014        })
1015        .expect("operation should succeed");
1016        env.add(Declaration::Axiom {
1017            name: Name::str("List.length"),
1018            univ_params: vec![],
1019            ty: implicit_pi(
1020                "α",
1021                type1(),
1022                default_pi("l", list_of(Expr::BVar(0)), nat_ty()),
1023            ),
1024        })
1025        .expect("operation should succeed");
1026        env.add(Declaration::Axiom {
1027            name: Name::str("Prod"),
1028            univ_params: vec![],
1029            ty: arrow(type1(), arrow(type1(), type1())),
1030        })
1031        .expect("operation should succeed");
1032        env
1033    }
1034    #[test]
1035    fn test_build_array_env() {
1036        let mut env = setup_env();
1037        assert!(build_array_env(&mut env).is_ok());
1038        assert!(env.get(&Name::str("Array")).is_some());
1039        assert!(env.get(&Name::str("Array.get")).is_some());
1040        assert!(env.get(&Name::str("Array.set")).is_some());
1041    }
1042    #[test]
1043    fn test_array_empty() {
1044        let mut env = setup_env();
1045        build_array_env(&mut env).expect("build_array_env should succeed");
1046        assert!(env.get(&Name::str("Array.empty")).is_some());
1047    }
1048    #[test]
1049    fn test_array_mk() {
1050        let mut env = setup_env();
1051        build_array_env(&mut env).expect("build_array_env should succeed");
1052        assert!(env.get(&Name::str("Array.mk")).is_some());
1053    }
1054    #[test]
1055    fn test_array_mk_empty() {
1056        let mut env = setup_env();
1057        build_array_env(&mut env).expect("build_array_env should succeed");
1058        assert!(env.get(&Name::str("Array.mkEmpty")).is_some());
1059    }
1060    #[test]
1061    fn test_array_size() {
1062        let mut env = setup_env();
1063        build_array_env(&mut env).expect("build_array_env should succeed");
1064        let decl = env
1065            .get(&Name::str("Array.size"))
1066            .expect("declaration 'Array.size' should exist in env");
1067        assert!(decl.ty().is_pi());
1068    }
1069    #[test]
1070    fn test_array_push() {
1071        let mut env = setup_env();
1072        build_array_env(&mut env).expect("build_array_env should succeed");
1073        let decl = env
1074            .get(&Name::str("Array.push"))
1075            .expect("declaration 'Array.push' should exist in env");
1076        assert!(decl.ty().is_pi());
1077    }
1078    #[test]
1079    fn test_array_pop() {
1080        let mut env = setup_env();
1081        build_array_env(&mut env).expect("build_array_env should succeed");
1082        let decl = env
1083            .get(&Name::str("Array.pop"))
1084            .expect("declaration 'Array.pop' should exist in env");
1085        assert!(decl.ty().is_pi());
1086    }
1087    #[test]
1088    fn test_array_swap() {
1089        let mut env = setup_env();
1090        build_array_env(&mut env).expect("build_array_env should succeed");
1091        let decl = env
1092            .get(&Name::str("Array.swap"))
1093            .expect("declaration 'Array.swap' should exist in env");
1094        assert!(decl.ty().is_pi());
1095    }
1096    #[test]
1097    fn test_array_map() {
1098        let mut env = setup_env();
1099        build_array_env(&mut env).expect("build_array_env should succeed");
1100        let decl = env
1101            .get(&Name::str("Array.map"))
1102            .expect("declaration 'Array.map' should exist in env");
1103        assert!(decl.ty().is_pi());
1104    }
1105    #[test]
1106    fn test_array_foldl() {
1107        let mut env = setup_env();
1108        build_array_env(&mut env).expect("build_array_env should succeed");
1109        let decl = env
1110            .get(&Name::str("Array.foldl"))
1111            .expect("declaration 'Array.foldl' should exist in env");
1112        assert!(decl.ty().is_pi());
1113    }
1114    #[test]
1115    fn test_array_foldr() {
1116        let mut env = setup_env();
1117        build_array_env(&mut env).expect("build_array_env should succeed");
1118        let decl = env
1119            .get(&Name::str("Array.foldr"))
1120            .expect("declaration 'Array.foldr' should exist in env");
1121        assert!(decl.ty().is_pi());
1122    }
1123    #[test]
1124    fn test_array_filter() {
1125        let mut env = setup_env();
1126        build_array_env(&mut env).expect("build_array_env should succeed");
1127        assert!(env.get(&Name::str("Array.filter")).is_some());
1128    }
1129    #[test]
1130    fn test_array_append() {
1131        let mut env = setup_env();
1132        build_array_env(&mut env).expect("build_array_env should succeed");
1133        let decl = env
1134            .get(&Name::str("Array.append"))
1135            .expect("declaration 'Array.append' should exist in env");
1136        assert!(decl.ty().is_pi());
1137    }
1138    #[test]
1139    fn test_array_reverse() {
1140        let mut env = setup_env();
1141        build_array_env(&mut env).expect("build_array_env should succeed");
1142        assert!(env.get(&Name::str("Array.reverse")).is_some());
1143    }
1144    #[test]
1145    fn test_array_zip() {
1146        let mut env = setup_env();
1147        build_array_env(&mut env).expect("build_array_env should succeed");
1148        let decl = env
1149            .get(&Name::str("Array.zip"))
1150            .expect("declaration 'Array.zip' should exist in env");
1151        assert!(decl.ty().is_pi());
1152    }
1153    #[test]
1154    fn test_array_enumerate() {
1155        let mut env = setup_env();
1156        build_array_env(&mut env).expect("build_array_env should succeed");
1157        assert!(env.get(&Name::str("Array.enumerate")).is_some());
1158    }
1159    #[test]
1160    fn test_array_take() {
1161        let mut env = setup_env();
1162        build_array_env(&mut env).expect("build_array_env should succeed");
1163        let decl = env
1164            .get(&Name::str("Array.take"))
1165            .expect("declaration 'Array.take' should exist in env");
1166        assert!(decl.ty().is_pi());
1167    }
1168    #[test]
1169    fn test_array_drop() {
1170        let mut env = setup_env();
1171        build_array_env(&mut env).expect("build_array_env should succeed");
1172        assert!(env.get(&Name::str("Array.drop")).is_some());
1173    }
1174    #[test]
1175    fn test_array_any() {
1176        let mut env = setup_env();
1177        build_array_env(&mut env).expect("build_array_env should succeed");
1178        assert!(env.get(&Name::str("Array.any")).is_some());
1179    }
1180    #[test]
1181    fn test_array_all() {
1182        let mut env = setup_env();
1183        build_array_env(&mut env).expect("build_array_env should succeed");
1184        assert!(env.get(&Name::str("Array.all")).is_some());
1185    }
1186    #[test]
1187    fn test_array_contains() {
1188        let mut env = setup_env();
1189        build_array_env(&mut env).expect("build_array_env should succeed");
1190        let decl = env
1191            .get(&Name::str("Array.contains"))
1192            .expect("declaration 'Array.contains' should exist in env");
1193        assert!(decl.ty().is_pi());
1194    }
1195    #[test]
1196    fn test_array_indexof() {
1197        let mut env = setup_env();
1198        build_array_env(&mut env).expect("build_array_env should succeed");
1199        let decl = env
1200            .get(&Name::str("Array.indexOf?"))
1201            .expect("declaration 'Array.indexOf?' should exist in env");
1202        assert!(decl.ty().is_pi());
1203    }
1204    #[test]
1205    fn test_array_tolist() {
1206        let mut env = setup_env();
1207        build_array_env(&mut env).expect("build_array_env should succeed");
1208        assert!(env.get(&Name::str("Array.toList")).is_some());
1209    }
1210    #[test]
1211    fn test_array_findsome() {
1212        let mut env = setup_env();
1213        build_array_env(&mut env).expect("build_array_env should succeed");
1214        let decl = env
1215            .get(&Name::str("Array.findSome?"))
1216            .expect("declaration 'Array.findSome?' should exist in env");
1217        assert!(decl.ty().is_pi());
1218    }
1219    #[test]
1220    fn test_array_qsort() {
1221        let mut env = setup_env();
1222        build_array_env(&mut env).expect("build_array_env should succeed");
1223        let decl = env
1224            .get(&Name::str("Array.qsort"))
1225            .expect("declaration 'Array.qsort' should exist in env");
1226        assert!(decl.ty().is_pi());
1227    }
1228    #[test]
1229    fn test_array_binsearch() {
1230        let mut env = setup_env();
1231        build_array_env(&mut env).expect("build_array_env should succeed");
1232        let decl = env
1233            .get(&Name::str("Array.binSearch"))
1234            .expect("declaration 'Array.binSearch' should exist in env");
1235        assert!(decl.ty().is_pi());
1236    }
1237    #[test]
1238    fn test_size_push_theorem() {
1239        let mut env = setup_env();
1240        build_array_env(&mut env).expect("build_array_env should succeed");
1241        let decl = env
1242            .get(&Name::str("Array.size_push"))
1243            .expect("declaration 'Array.size_push' should exist in env");
1244        assert!(decl.ty().is_pi());
1245    }
1246    #[test]
1247    fn test_get_set_same_theorem() {
1248        let mut env = setup_env();
1249        build_array_env(&mut env).expect("build_array_env should succeed");
1250        let decl = env
1251            .get(&Name::str("Array.get_set_same"))
1252            .expect("declaration 'Array.get_set_same' should exist in env");
1253        assert!(decl.ty().is_pi());
1254    }
1255    #[test]
1256    fn test_get_set_diff_theorem() {
1257        let mut env = setup_env();
1258        build_array_env(&mut env).expect("build_array_env should succeed");
1259        let decl = env
1260            .get(&Name::str("Array.get_set_diff"))
1261            .expect("declaration 'Array.get_set_diff' should exist in env");
1262        assert!(decl.ty().is_pi());
1263    }
1264    #[test]
1265    fn test_map_size_theorem() {
1266        let mut env = setup_env();
1267        build_array_env(&mut env).expect("build_array_env should succeed");
1268        let decl = env
1269            .get(&Name::str("Array.map_size"))
1270            .expect("declaration 'Array.map_size' should exist in env");
1271        assert!(decl.ty().is_pi());
1272    }
1273    #[test]
1274    fn test_tolist_length_theorem() {
1275        let mut env = setup_env();
1276        build_array_env(&mut env).expect("build_array_env should succeed");
1277        let decl = env
1278            .get(&Name::str("Array.toList_length"))
1279            .expect("declaration 'Array.toList_length' should exist in env");
1280        assert!(decl.ty().is_pi());
1281    }
1282    #[test]
1283    fn test_mk_array_ty_expr() {
1284        let t = mk_array_ty(nat_ty(), Expr::Const(Name::str("n"), vec![]));
1285        assert!(matches!(t, Expr::App(_, _)));
1286    }
1287    #[test]
1288    fn test_mk_array_empty_expr() {
1289        let e = mk_array_empty(nat_ty());
1290        assert!(matches!(e, Expr::App(_, _)));
1291    }
1292    #[test]
1293    fn test_mk_array_push_expr() {
1294        let arr = Expr::Const(Name::str("a"), vec![]);
1295        let elem = Expr::Const(Name::str("x"), vec![]);
1296        let expr = mk_array_push(arr, elem);
1297        assert!(matches!(expr, Expr::App(_, _)));
1298    }
1299    #[test]
1300    fn test_mk_array_get_expr() {
1301        let arr = Expr::Const(Name::str("a"), vec![]);
1302        let idx = Expr::Const(Name::str("i"), vec![]);
1303        let expr = mk_array_get(arr, idx);
1304        assert!(matches!(expr, Expr::App(_, _)));
1305    }
1306    #[test]
1307    fn test_mk_array_set_expr() {
1308        let arr = Expr::Const(Name::str("a"), vec![]);
1309        let idx = Expr::Const(Name::str("i"), vec![]);
1310        let val = Expr::Const(Name::str("v"), vec![]);
1311        let expr = mk_array_set(arr, idx, val);
1312        assert!(matches!(expr, Expr::App(_, _)));
1313    }
1314    #[test]
1315    fn test_mk_array_map_expr() {
1316        let f = Expr::Const(Name::str("f"), vec![]);
1317        let arr = Expr::Const(Name::str("a"), vec![]);
1318        let expr = mk_array_map(f, arr);
1319        assert!(matches!(expr, Expr::App(_, _)));
1320    }
1321    #[test]
1322    fn test_mk_array_foldl_expr() {
1323        let f = Expr::Const(Name::str("f"), vec![]);
1324        let init = Expr::Const(Name::str("init"), vec![]);
1325        let arr = Expr::Const(Name::str("a"), vec![]);
1326        let expr = mk_array_foldl(f, init, arr);
1327        assert!(matches!(expr, Expr::App(_, _)));
1328    }
1329    #[test]
1330    fn test_mk_array_tolist_expr() {
1331        let arr = Expr::Const(Name::str("a"), vec![]);
1332        let expr = mk_array_tolist(arr);
1333        assert!(matches!(expr, Expr::App(_, _)));
1334    }
1335    #[test]
1336    fn test_all_array_decls_present() {
1337        let mut env = setup_env();
1338        build_array_env(&mut env).expect("build_array_env should succeed");
1339        let names = [
1340            "Array",
1341            "Array.get",
1342            "Array.set",
1343            "Array.empty",
1344            "Array.mk",
1345            "Array.mkEmpty",
1346            "Array.size",
1347            "Array.push",
1348            "Array.pop",
1349            "Array.swap",
1350            "Array.map",
1351            "Array.foldl",
1352            "Array.foldr",
1353            "Array.filter",
1354            "Array.append",
1355            "Array.reverse",
1356            "Array.zip",
1357            "Array.enumerate",
1358            "Array.take",
1359            "Array.drop",
1360            "Array.any",
1361            "Array.all",
1362            "Array.contains",
1363            "Array.indexOf?",
1364            "Array.toList",
1365            "Array.findSome?",
1366            "Array.qsort",
1367            "Array.binSearch",
1368            "Array.size_push",
1369            "Array.get_set_same",
1370            "Array.get_set_diff",
1371            "Array.map_size",
1372            "Array.toList_length",
1373        ];
1374        for name in &names {
1375            assert!(
1376                env.get(&Name::str(*name)).is_some(),
1377                "missing declaration: {}",
1378                name
1379            );
1380        }
1381    }
1382    #[test]
1383    fn test_all_array_decls_are_axioms() {
1384        let mut env = setup_env();
1385        build_array_env(&mut env).expect("build_array_env should succeed");
1386        let names = [
1387            "Array",
1388            "Array.get",
1389            "Array.set",
1390            "Array.empty",
1391            "Array.mk",
1392            "Array.mkEmpty",
1393            "Array.size",
1394            "Array.push",
1395            "Array.pop",
1396            "Array.swap",
1397            "Array.map",
1398            "Array.foldl",
1399            "Array.foldr",
1400            "Array.filter",
1401            "Array.append",
1402            "Array.reverse",
1403            "Array.zip",
1404            "Array.enumerate",
1405            "Array.take",
1406            "Array.drop",
1407            "Array.any",
1408            "Array.all",
1409            "Array.contains",
1410            "Array.indexOf?",
1411            "Array.toList",
1412            "Array.findSome?",
1413            "Array.qsort",
1414            "Array.binSearch",
1415            "Array.size_push",
1416            "Array.get_set_same",
1417            "Array.get_set_diff",
1418            "Array.map_size",
1419            "Array.toList_length",
1420        ];
1421        for name in &names {
1422            let decl = env
1423                .get(&Name::str(*name))
1424                .expect("operation should succeed");
1425            assert!(
1426                matches!(decl, Declaration::Axiom { .. }),
1427                "{} should be an axiom",
1428                name
1429            );
1430        }
1431    }
1432    #[test]
1433    fn test_array_declaration_count() {
1434        let mut env = setup_env();
1435        let pre = env.len();
1436        build_array_env(&mut env).expect("build_array_env should succeed");
1437        let added = env.len() - pre;
1438        assert!(added >= 30, "expected >= 30 declarations, got {}", added);
1439    }
1440    #[test]
1441    fn test_array_push_type_depth() {
1442        let mut env = setup_env();
1443        build_array_env(&mut env).expect("build_array_env should succeed");
1444        let decl = env
1445            .get(&Name::str("Array.push"))
1446            .expect("declaration 'Array.push' should exist in env");
1447        let mut ty = decl.ty().clone();
1448        let mut depth = 0;
1449        while let Expr::Pi(_, _, _, body) = ty {
1450            depth += 1;
1451            ty = (*body).clone();
1452        }
1453        assert!(depth >= 4, "push should have >= 4 Pi levels, got {}", depth);
1454    }
1455    #[test]
1456    fn test_array_foldl_type_depth() {
1457        let mut env = setup_env();
1458        build_array_env(&mut env).expect("build_array_env should succeed");
1459        let decl = env
1460            .get(&Name::str("Array.foldl"))
1461            .expect("declaration 'Array.foldl' should exist in env");
1462        let mut ty = decl.ty().clone();
1463        let mut depth = 0;
1464        while let Expr::Pi(_, _, _, body) = ty {
1465            depth += 1;
1466            ty = (*body).clone();
1467        }
1468        assert!(
1469            depth >= 6,
1470            "foldl should have >= 6 Pi levels, got {}",
1471            depth
1472        );
1473    }
1474}
1475/// `Array.map_id : ∀ {α n}, Array α n → Prop`
1476///
1477/// Functor identity law: mapping the identity function over an array returns
1478/// the same array. `map id a = a`.
1479#[allow(dead_code)]
1480pub fn arr_ext_map_id_ty() -> Expr {
1481    implicit_pi(
1482        "α",
1483        type1(),
1484        implicit_pi(
1485            "n",
1486            nat_ty(),
1487            default_pi("a", array_of(Expr::BVar(1), Expr::BVar(0)), prop()),
1488        ),
1489    )
1490}
1491/// `Array.map_comp : ∀ {α β γ n}, (β → γ) → (α → β) → Array α n → Prop`
1492///
1493/// Functor composition law: mapping (g ∘ f) over an array equals mapping g
1494/// after mapping f. `map (g ∘ f) a = map g (map f a)`.
1495#[allow(dead_code)]
1496pub fn arr_ext_map_comp_ty() -> Expr {
1497    implicit_pi(
1498        "α",
1499        type1(),
1500        implicit_pi(
1501            "β",
1502            type1(),
1503            implicit_pi(
1504                "γ",
1505                type1(),
1506                implicit_pi(
1507                    "n",
1508                    nat_ty(),
1509                    default_pi(
1510                        "g",
1511                        arrow(Expr::BVar(2), Expr::BVar(1)),
1512                        default_pi(
1513                            "f",
1514                            arrow(Expr::BVar(4), Expr::BVar(3)),
1515                            default_pi("a", array_of(Expr::BVar(5), Expr::BVar(2)), prop()),
1516                        ),
1517                    ),
1518                ),
1519            ),
1520        ),
1521    )
1522}
1523/// `Array.pure_map_size : ∀ {α β n}, (α → β) → Array α n → Prop`
1524///
1525/// Applicative functor preservation of size under pure/map:
1526/// `size (map f a) = size a`.
1527#[allow(dead_code)]
1528pub fn arr_ext_pure_map_size_ty() -> Expr {
1529    implicit_pi(
1530        "α",
1531        type1(),
1532        implicit_pi(
1533            "β",
1534            type1(),
1535            implicit_pi(
1536                "n",
1537                nat_ty(),
1538                default_pi(
1539                    "f",
1540                    arrow(Expr::BVar(2), Expr::BVar(1)),
1541                    default_pi("a", array_of(Expr::BVar(3), Expr::BVar(1)), prop()),
1542                ),
1543            ),
1544        ),
1545    )
1546}
1547/// `Array.bind_assoc : ∀ {α β γ n}, Array α n → (α → Array β n) → (β → Array γ n) → Prop`
1548///
1549/// Monad associativity (kleisli composition): `(a >>= f) >>= g = a >>= (λx, f x >>= g)`.
1550#[allow(dead_code)]
1551pub fn arr_ext_bind_assoc_ty() -> Expr {
1552    implicit_pi(
1553        "α",
1554        type1(),
1555        implicit_pi(
1556            "β",
1557            type1(),
1558            implicit_pi(
1559                "γ",
1560                type1(),
1561                implicit_pi(
1562                    "n",
1563                    nat_ty(),
1564                    default_pi(
1565                        "a",
1566                        array_of(Expr::BVar(3), Expr::BVar(0)),
1567                        default_pi(
1568                            "f",
1569                            arrow(Expr::BVar(4), array_of(Expr::BVar(3), Expr::BVar(2))),
1570                            default_pi(
1571                                "g",
1572                                arrow(Expr::BVar(4), array_of(Expr::BVar(3), Expr::BVar(1))),
1573                                prop(),
1574                            ),
1575                        ),
1576                    ),
1577                ),
1578            ),
1579        ),
1580    )
1581}
1582/// `Array.mergesort : {α : Type} → {n : Nat} → \[Ord α\] → Array α n → Array α n`
1583///
1584/// Merge sort: a stable O(n log n) sorting algorithm that returns a sorted
1585/// permutation of the input array.
1586#[allow(dead_code)]
1587pub fn arr_ext_mergesort_ty() -> Expr {
1588    implicit_pi(
1589        "α",
1590        type1(),
1591        implicit_pi(
1592            "n",
1593            nat_ty(),
1594            inst_pi(
1595                "inst",
1596                ord_of(Expr::BVar(1)),
1597                default_pi(
1598                    "arr",
1599                    array_of(Expr::BVar(2), Expr::BVar(1)),
1600                    array_of(Expr::BVar(3), Expr::BVar(2)),
1601                ),
1602            ),
1603        ),
1604    )
1605}
1606/// `Array.sort_stable : ∀ {α n}, \[Ord α\] → Array α n → Prop`
1607///
1608/// Stability of merge sort: elements with equal keys retain their original
1609/// relative order. A stable sort preserves the original ordering for equal elements.
1610#[allow(dead_code)]
1611pub fn arr_ext_sort_stable_ty() -> Expr {
1612    implicit_pi(
1613        "α",
1614        type1(),
1615        implicit_pi(
1616            "n",
1617            nat_ty(),
1618            inst_pi(
1619                "inst",
1620                ord_of(Expr::BVar(1)),
1621                default_pi("arr", array_of(Expr::BVar(2), Expr::BVar(1)), prop()),
1622            ),
1623        ),
1624    )
1625}
1626/// `Array.sort_perm : ∀ {α n}, \[Ord α\] → Array α n → Prop`
1627///
1628/// Correctness of sort as a permutation: the sorted result is a permutation
1629/// of the input (no elements added or dropped).
1630#[allow(dead_code)]
1631pub fn arr_ext_sort_perm_ty() -> Expr {
1632    implicit_pi(
1633        "α",
1634        type1(),
1635        implicit_pi(
1636            "n",
1637            nat_ty(),
1638            inst_pi(
1639                "inst",
1640                ord_of(Expr::BVar(1)),
1641                default_pi("arr", array_of(Expr::BVar(2), Expr::BVar(1)), prop()),
1642            ),
1643        ),
1644    )
1645}
1646/// `Array.sort_sorted : ∀ {α n}, \[Ord α\] → Array α n → Prop`
1647///
1648/// Output of sort satisfies the sorted predicate: for all i < j,
1649/// `get (sort a) i ≤ get (sort a) j`.
1650#[allow(dead_code)]
1651pub fn arr_ext_sort_sorted_ty() -> Expr {
1652    implicit_pi(
1653        "α",
1654        type1(),
1655        implicit_pi(
1656            "n",
1657            nat_ty(),
1658            inst_pi(
1659                "inst",
1660                ord_of(Expr::BVar(1)),
1661                default_pi("arr", array_of(Expr::BVar(2), Expr::BVar(1)), prop()),
1662            ),
1663        ),
1664    )
1665}
1666/// `Array.qsort_average_case : ∀ {α n}, \[Ord α\] → Array α n → Prop`
1667///
1668/// Quicksort average-case complexity: for a random permutation of n elements,
1669/// expected O(n log n) comparisons with randomized pivot selection.
1670#[allow(dead_code)]
1671pub fn arr_ext_qsort_avg_ty() -> Expr {
1672    implicit_pi(
1673        "α",
1674        type1(),
1675        implicit_pi(
1676            "n",
1677            nat_ty(),
1678            inst_pi(
1679                "inst",
1680                ord_of(Expr::BVar(1)),
1681                default_pi("arr", array_of(Expr::BVar(2), Expr::BVar(1)), prop()),
1682            ),
1683        ),
1684    )
1685}
1686/// `Array.reverse_involution : ∀ {α n}, Array α n → Prop`
1687///
1688/// Reversal is an involution: `reverse (reverse a) = a`.
1689#[allow(dead_code)]
1690pub fn arr_ext_reverse_involution_ty() -> Expr {
1691    implicit_pi(
1692        "α",
1693        type1(),
1694        implicit_pi(
1695            "n",
1696            nat_ty(),
1697            default_pi("a", array_of(Expr::BVar(1), Expr::BVar(0)), prop()),
1698        ),
1699    )
1700}
1701/// `Array.reverse_size : ∀ {α n}, Array α n → Prop`
1702///
1703/// Reversal preserves size: `size (reverse a) = size a`.
1704#[allow(dead_code)]
1705pub fn arr_ext_reverse_size_ty() -> Expr {
1706    implicit_pi(
1707        "α",
1708        type1(),
1709        implicit_pi(
1710            "n",
1711            nat_ty(),
1712            default_pi("a", array_of(Expr::BVar(1), Expr::BVar(0)), prop()),
1713        ),
1714    )
1715}
1716/// `Array.append_assoc : ∀ {α n m k}, Array α n → Array α m → Array α k → Prop`
1717///
1718/// Append is associative: `(a ++ b) ++ c = a ++ (b ++ c)`.
1719#[allow(dead_code)]
1720pub fn arr_ext_append_assoc_ty() -> Expr {
1721    implicit_pi(
1722        "α",
1723        type1(),
1724        implicit_pi(
1725            "n",
1726            nat_ty(),
1727            implicit_pi(
1728                "m",
1729                nat_ty(),
1730                implicit_pi(
1731                    "k",
1732                    nat_ty(),
1733                    default_pi(
1734                        "a",
1735                        array_of(Expr::BVar(3), Expr::BVar(2)),
1736                        default_pi(
1737                            "b",
1738                            array_of(Expr::BVar(4), Expr::BVar(2)),
1739                            default_pi("c", array_of(Expr::BVar(5), Expr::BVar(2)), prop()),
1740                        ),
1741                    ),
1742                ),
1743            ),
1744        ),
1745    )
1746}
1747/// `Array.append_empty_left : ∀ {α n}, Array α n → Prop`
1748///
1749/// Left identity of append: `empty ++ a = a`.
1750#[allow(dead_code)]
1751pub fn arr_ext_append_empty_left_ty() -> Expr {
1752    implicit_pi(
1753        "α",
1754        type1(),
1755        implicit_pi(
1756            "n",
1757            nat_ty(),
1758            default_pi("a", array_of(Expr::BVar(1), Expr::BVar(0)), prop()),
1759        ),
1760    )
1761}
1762/// `Array.append_empty_right : ∀ {α n}, Array α n → Prop`
1763///
1764/// Right identity of append: `a ++ empty = a`.
1765#[allow(dead_code)]
1766pub fn arr_ext_append_empty_right_ty() -> Expr {
1767    implicit_pi(
1768        "α",
1769        type1(),
1770        implicit_pi(
1771            "n",
1772            nat_ty(),
1773            default_pi("a", array_of(Expr::BVar(1), Expr::BVar(0)), prop()),
1774        ),
1775    )
1776}
1777/// `Array.append_size : ∀ {α n m}, Array α n → Array α m → Prop`
1778///
1779/// Size of append equals sum: `size (a ++ b) = size a + size b`.
1780#[allow(dead_code)]
1781pub fn arr_ext_append_size_ty() -> Expr {
1782    implicit_pi(
1783        "α",
1784        type1(),
1785        implicit_pi(
1786            "n",
1787            nat_ty(),
1788            implicit_pi(
1789                "m",
1790                nat_ty(),
1791                default_pi(
1792                    "a",
1793                    array_of(Expr::BVar(2), Expr::BVar(1)),
1794                    default_pi("b", array_of(Expr::BVar(3), Expr::BVar(1)), prop()),
1795                ),
1796            ),
1797        ),
1798    )
1799}
1800/// `Array.slice : {α : Type} → {n : Nat} → Array α n → Nat → Nat → List α`
1801///
1802/// Array slice: extract a sub-array from index `lo` to `hi` (exclusive),
1803/// returning it as a list. Used in range queries and substring operations.
1804#[allow(dead_code)]
1805pub fn arr_ext_slice_ty() -> Expr {
1806    implicit_pi(
1807        "α",
1808        type1(),
1809        implicit_pi(
1810            "n",
1811            nat_ty(),
1812            default_pi(
1813                "arr",
1814                array_of(Expr::BVar(1), Expr::BVar(0)),
1815                default_pi(
1816                    "lo",
1817                    nat_ty(),
1818                    default_pi("hi", nat_ty(), list_of(Expr::BVar(4))),
1819                ),
1820            ),
1821        ),
1822    )
1823}
1824/// `Array.prefix_sum : {α : Type} → {n : Nat} → Array α n → Array α n`
1825///
1826/// Prefix sum (cumulative sum): given an array a, compute b where
1827/// b\[i\] = a\[0\] + a\[1\] + ... + a\[i\]. Enables O(1) range sum queries.
1828#[allow(dead_code)]
1829pub fn arr_ext_prefix_sum_ty() -> Expr {
1830    implicit_pi(
1831        "α",
1832        type1(),
1833        implicit_pi(
1834            "n",
1835            nat_ty(),
1836            default_pi(
1837                "arr",
1838                array_of(Expr::BVar(1), Expr::BVar(0)),
1839                array_of(Expr::BVar(2), Expr::BVar(1)),
1840            ),
1841        ),
1842    )
1843}
oxilean_std/array/functions.rs

oxilean_std/array/
functions.rs
