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

oxilean_std/array/
functions.rs
