oxilean_std/list/
functions.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{
6    BinderInfo, Declaration, Environment, Expr, InductiveEnv, InductiveType, IntroRule, Level, Name,
7};
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/// `List` applied to a type argument.
30#[allow(dead_code)]
31pub fn list_of(elem_ty: Expr) -> Expr {
32    app(Expr::Const(Name::str("List"), vec![]), elem_ty)
33}
34/// `Option` applied to a type argument.
35#[allow(dead_code)]
36pub fn option_of(elem_ty: Expr) -> Expr {
37    app(Expr::Const(Name::str("Option"), vec![]), elem_ty)
38}
39/// `Prod` applied to two type arguments.
40#[allow(dead_code)]
41pub fn prod_of(a: Expr, b: Expr) -> Expr {
42    app2(Expr::Const(Name::str("Prod"), vec![]), a, b)
43}
44/// Build a non-dependent arrow `A -> B`.
45#[allow(dead_code)]
46pub fn arrow(a: Expr, b: Expr) -> Expr {
47    Expr::Pi(
48        BinderInfo::Default,
49        Name::str("_"),
50        Box::new(a),
51        Box::new(b),
52    )
53}
54/// Function application `f a`.
55#[allow(dead_code)]
56pub fn app(f: Expr, a: Expr) -> Expr {
57    Expr::App(Box::new(f), Box::new(a))
58}
59/// Function application `f a b`.
60#[allow(dead_code)]
61pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
62    app(app(f, a), b)
63}
64/// Function application `f a b c`.
65#[allow(dead_code)]
66pub fn app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
67    app(app2(f, a, b), c)
68}
69/// An implicit Pi binder.
70#[allow(dead_code)]
71pub fn implicit_pi(name: &str, ty: Expr, body: Expr) -> Expr {
72    Expr::Pi(
73        BinderInfo::Implicit,
74        Name::str(name),
75        Box::new(ty),
76        Box::new(body),
77    )
78}
79/// A default (explicit) Pi binder.
80#[allow(dead_code)]
81pub fn default_pi(name: &str, ty: Expr, body: Expr) -> Expr {
82    Expr::Pi(
83        BinderInfo::Default,
84        Name::str(name),
85        Box::new(ty),
86        Box::new(body),
87    )
88}
89/// Build `Eq @{} ty a b`.
90#[allow(dead_code)]
91pub fn eq_expr(ty: Expr, a: Expr, b: Expr) -> Expr {
92    app(app(app(Expr::Const(Name::str("Eq"), vec![]), ty), a), b)
93}
94/// Shorthand to add an axiom to env.
95#[allow(dead_code)]
96pub fn add_axiom(
97    env: &mut Environment,
98    name: &str,
99    univ_params: Vec<Name>,
100    ty: Expr,
101) -> Result<(), String> {
102    env.add(Declaration::Axiom {
103        name: Name::str(name),
104        univ_params,
105        ty,
106    })
107    .map_err(|e| e.to_string())
108}
109/// Build the List type and all standard operations, adding them to the
110/// environment.
111///
112/// Assumes that `Nat`, `Bool`, `Option`, `Prod`, and `Eq` are already in
113/// the environment (or will be referenced by name).
114pub fn build_list_env(env: &mut Environment, ind_env: &mut InductiveEnv) -> Result<(), String> {
115    let list_ty = arrow(type1(), type1());
116    let nil_ty = implicit_pi("alpha", type1(), list_of(Expr::BVar(0)));
117    let cons_ty = implicit_pi(
118        "alpha",
119        type1(),
120        default_pi(
121            "hd",
122            Expr::BVar(0),
123            default_pi("tl", list_of(Expr::BVar(1)), list_of(Expr::BVar(2))),
124        ),
125    );
126    let list_ind = InductiveType::new(
127        Name::str("List"),
128        vec![],
129        1,
130        0,
131        list_ty.clone(),
132        vec![
133            IntroRule {
134                name: Name::str("List.nil"),
135                ty: nil_ty.clone(),
136            },
137            IntroRule {
138                name: Name::str("List.cons"),
139                ty: cons_ty.clone(),
140            },
141        ],
142    );
143    ind_env.add(list_ind).map_err(|e| format!("{}", e))?;
144    add_axiom(env, "List", vec![], list_ty)?;
145    add_axiom(env, "List.nil", vec![], nil_ty)?;
146    add_axiom(env, "List.cons", vec![], cons_ty)?;
147    let u = Name::str("u");
148    let sort_u = Expr::Sort(Level::Param(u.clone()));
149    let c_ty = arrow(list_of(Expr::BVar(0)), sort_u);
150    let nil_case_ty = app(
151        Expr::BVar(1),
152        app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(2)),
153    );
154    let cons_case_ty = default_pi(
155        "hd",
156        Expr::BVar(2),
157        default_pi(
158            "tl",
159            list_of(Expr::BVar(3)),
160            default_pi(
161                "ih",
162                app(Expr::BVar(3), Expr::BVar(0)),
163                app(
164                    Expr::BVar(4),
165                    app2(
166                        Expr::Const(Name::str("List.cons"), vec![]),
167                        Expr::BVar(2),
168                        Expr::BVar(1),
169                    ),
170                ),
171            ),
172        ),
173    );
174    let target = default_pi(
175        "l",
176        list_of(Expr::BVar(3)),
177        app(Expr::BVar(4), Expr::BVar(0)),
178    );
179    let rec_ty = implicit_pi(
180        "alpha",
181        type1(),
182        implicit_pi(
183            "C",
184            c_ty,
185            default_pi(
186                "nil_case",
187                nil_case_ty,
188                default_pi("cons_case", cons_case_ty, target),
189            ),
190        ),
191    );
192    add_axiom(env, "List.rec", vec![u], rec_ty)?;
193    add_axiom(
194        env,
195        "List.map",
196        vec![],
197        implicit_pi(
198            "alpha",
199            type1(),
200            implicit_pi(
201                "beta",
202                type1(),
203                default_pi(
204                    "f",
205                    arrow(Expr::BVar(1), Expr::BVar(0)),
206                    default_pi("l", list_of(Expr::BVar(2)), list_of(Expr::BVar(2))),
207                ),
208            ),
209        ),
210    )?;
211    add_axiom(
212        env,
213        "List.filter",
214        vec![],
215        implicit_pi(
216            "alpha",
217            type1(),
218            default_pi(
219                "p",
220                arrow(Expr::BVar(0), bool_ty()),
221                default_pi("l", list_of(Expr::BVar(1)), list_of(Expr::BVar(2))),
222            ),
223        ),
224    )?;
225    {
226        let f_ty = Expr::Pi(
227            BinderInfo::Default,
228            Name::str("_"),
229            Box::new(Expr::BVar(1)),
230            Box::new(Expr::Pi(
231                BinderInfo::Default,
232                Name::str("_"),
233                Box::new(Expr::BVar(1)),
234                Box::new(Expr::BVar(2)),
235            )),
236        );
237        add_axiom(
238            env,
239            "List.foldr",
240            vec![],
241            implicit_pi(
242                "alpha",
243                type1(),
244                implicit_pi(
245                    "beta",
246                    type1(),
247                    default_pi(
248                        "f",
249                        f_ty,
250                        default_pi(
251                            "init",
252                            Expr::BVar(1),
253                            default_pi("l", list_of(Expr::BVar(3)), Expr::BVar(3)),
254                        ),
255                    ),
256                ),
257            ),
258        )?;
259    }
260    {
261        let f_ty = Expr::Pi(
262            BinderInfo::Default,
263            Name::str("_"),
264            Box::new(Expr::BVar(0)),
265            Box::new(Expr::Pi(
266                BinderInfo::Default,
267                Name::str("_"),
268                Box::new(Expr::BVar(2)),
269                Box::new(Expr::BVar(2)),
270            )),
271        );
272        add_axiom(
273            env,
274            "List.foldl",
275            vec![],
276            implicit_pi(
277                "alpha",
278                type1(),
279                implicit_pi(
280                    "beta",
281                    type1(),
282                    default_pi(
283                        "f",
284                        f_ty,
285                        default_pi(
286                            "init",
287                            Expr::BVar(1),
288                            default_pi("l", list_of(Expr::BVar(3)), Expr::BVar(3)),
289                        ),
290                    ),
291                ),
292            ),
293        )?;
294    }
295    add_axiom(
296        env,
297        "List.reverse",
298        vec![],
299        implicit_pi(
300            "alpha",
301            type1(),
302            default_pi("l", list_of(Expr::BVar(0)), list_of(Expr::BVar(1))),
303        ),
304    )?;
305    add_axiom(
306        env,
307        "List.length",
308        vec![],
309        implicit_pi(
310            "alpha",
311            type1(),
312            default_pi("l", list_of(Expr::BVar(0)), nat_ty()),
313        ),
314    )?;
315    add_axiom(
316        env,
317        "List.append",
318        vec![],
319        implicit_pi(
320            "alpha",
321            type1(),
322            default_pi(
323                "l1",
324                list_of(Expr::BVar(0)),
325                default_pi("l2", list_of(Expr::BVar(1)), list_of(Expr::BVar(2))),
326            ),
327        ),
328    )?;
329    add_axiom(
330        env,
331        "List.head?",
332        vec![],
333        implicit_pi(
334            "alpha",
335            type1(),
336            default_pi("l", list_of(Expr::BVar(0)), option_of(Expr::BVar(1))),
337        ),
338    )?;
339    add_axiom(
340        env,
341        "List.tail",
342        vec![],
343        implicit_pi(
344            "alpha",
345            type1(),
346            default_pi("l", list_of(Expr::BVar(0)), list_of(Expr::BVar(1))),
347        ),
348    )?;
349    add_axiom(
350        env,
351        "List.nth?",
352        vec![],
353        implicit_pi(
354            "alpha",
355            type1(),
356            default_pi(
357                "l",
358                list_of(Expr::BVar(0)),
359                default_pi("n", nat_ty(), option_of(Expr::BVar(2))),
360            ),
361        ),
362    )?;
363    add_axiom(
364        env,
365        "List.zip",
366        vec![],
367        implicit_pi(
368            "alpha",
369            type1(),
370            implicit_pi(
371                "beta",
372                type1(),
373                default_pi(
374                    "l1",
375                    list_of(Expr::BVar(1)),
376                    default_pi(
377                        "l2",
378                        list_of(Expr::BVar(1)),
379                        list_of(prod_of(Expr::BVar(3), Expr::BVar(2))),
380                    ),
381                ),
382            ),
383        ),
384    )?;
385    add_axiom(
386        env,
387        "List.take",
388        vec![],
389        implicit_pi(
390            "alpha",
391            type1(),
392            default_pi(
393                "n",
394                nat_ty(),
395                default_pi("l", list_of(Expr::BVar(1)), list_of(Expr::BVar(2))),
396            ),
397        ),
398    )?;
399    add_axiom(
400        env,
401        "List.drop",
402        vec![],
403        implicit_pi(
404            "alpha",
405            type1(),
406            default_pi(
407                "n",
408                nat_ty(),
409                default_pi("l", list_of(Expr::BVar(1)), list_of(Expr::BVar(2))),
410            ),
411        ),
412    )?;
413    add_axiom(
414        env,
415        "List.any",
416        vec![],
417        implicit_pi(
418            "alpha",
419            type1(),
420            default_pi(
421                "p",
422                arrow(Expr::BVar(0), bool_ty()),
423                default_pi("l", list_of(Expr::BVar(1)), bool_ty()),
424            ),
425        ),
426    )?;
427    add_axiom(
428        env,
429        "List.all",
430        vec![],
431        implicit_pi(
432            "alpha",
433            type1(),
434            default_pi(
435                "p",
436                arrow(Expr::BVar(0), bool_ty()),
437                default_pi("l", list_of(Expr::BVar(1)), bool_ty()),
438            ),
439        ),
440    )?;
441    add_axiom(
442        env,
443        "List.replicate",
444        vec![],
445        implicit_pi(
446            "alpha",
447            type1(),
448            default_pi(
449                "n",
450                nat_ty(),
451                default_pi("x", Expr::BVar(1), list_of(Expr::BVar(2))),
452            ),
453        ),
454    )?;
455    add_axiom(
456        env,
457        "List.join",
458        vec![],
459        implicit_pi(
460            "alpha",
461            type1(),
462            default_pi(
463                "ll",
464                list_of(list_of(Expr::BVar(0))),
465                list_of(Expr::BVar(1)),
466            ),
467        ),
468    )?;
469    add_axiom(env, "List.iota", vec![], arrow(nat_ty(), list_of(nat_ty())))?;
470    add_axiom(
471        env,
472        "List.range",
473        vec![],
474        arrow(nat_ty(), list_of(nat_ty())),
475    )?;
476    add_axiom(
477        env,
478        "List.enumFrom",
479        vec![],
480        implicit_pi(
481            "alpha",
482            type1(),
483            default_pi(
484                "start",
485                nat_ty(),
486                default_pi(
487                    "l",
488                    list_of(Expr::BVar(1)),
489                    list_of(prod_of(nat_ty(), Expr::BVar(2))),
490                ),
491            ),
492        ),
493    )?;
494    add_axiom(
495        env,
496        "List.nil_append",
497        vec![],
498        implicit_pi(
499            "alpha",
500            type1(),
501            default_pi(
502                "l",
503                list_of(Expr::BVar(0)),
504                eq_expr(
505                    list_of(Expr::BVar(1)),
506                    app2(
507                        Expr::Const(Name::str("List.append"), vec![]),
508                        app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(1)),
509                        Expr::BVar(0),
510                    ),
511                    Expr::BVar(0),
512                ),
513            ),
514        ),
515    )?;
516    add_axiom(
517        env,
518        "List.append_nil",
519        vec![],
520        implicit_pi(
521            "alpha",
522            type1(),
523            default_pi(
524                "l",
525                list_of(Expr::BVar(0)),
526                eq_expr(
527                    list_of(Expr::BVar(1)),
528                    app2(
529                        Expr::Const(Name::str("List.append"), vec![]),
530                        Expr::BVar(0),
531                        app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(1)),
532                    ),
533                    Expr::BVar(0),
534                ),
535            ),
536        ),
537    )?;
538    {
539        let append = Expr::Const(Name::str("List.append"), vec![]);
540        add_axiom(
541            env,
542            "List.append_assoc",
543            vec![],
544            implicit_pi(
545                "alpha",
546                type1(),
547                default_pi(
548                    "l1",
549                    list_of(Expr::BVar(0)),
550                    default_pi(
551                        "l2",
552                        list_of(Expr::BVar(1)),
553                        default_pi(
554                            "l3",
555                            list_of(Expr::BVar(2)),
556                            eq_expr(
557                                list_of(Expr::BVar(3)),
558                                app2(
559                                    append.clone(),
560                                    app2(append.clone(), Expr::BVar(2), Expr::BVar(1)),
561                                    Expr::BVar(0),
562                                ),
563                                app2(
564                                    append.clone(),
565                                    Expr::BVar(2),
566                                    app2(append, Expr::BVar(1), Expr::BVar(0)),
567                                ),
568                            ),
569                        ),
570                    ),
571                ),
572            ),
573        )?;
574    }
575    add_axiom(
576        env,
577        "List.length_nil",
578        vec![],
579        implicit_pi(
580            "alpha",
581            type1(),
582            eq_expr(
583                nat_ty(),
584                app(
585                    Expr::Const(Name::str("List.length"), vec![]),
586                    app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(0)),
587                ),
588                Expr::Const(Name::str("Nat.zero"), vec![]),
589            ),
590        ),
591    )?;
592    add_axiom(
593        env,
594        "List.length_cons",
595        vec![],
596        implicit_pi(
597            "alpha",
598            type1(),
599            default_pi(
600                "a",
601                Expr::BVar(0),
602                default_pi(
603                    "l",
604                    list_of(Expr::BVar(1)),
605                    eq_expr(
606                        nat_ty(),
607                        app(
608                            Expr::Const(Name::str("List.length"), vec![]),
609                            app2(
610                                Expr::Const(Name::str("List.cons"), vec![]),
611                                Expr::BVar(1),
612                                Expr::BVar(0),
613                            ),
614                        ),
615                        app(
616                            Expr::Const(Name::str("Nat.succ"), vec![]),
617                            app(Expr::Const(Name::str("List.length"), vec![]), Expr::BVar(0)),
618                        ),
619                    ),
620                ),
621            ),
622        ),
623    )?;
624    {
625        let length = Expr::Const(Name::str("List.length"), vec![]);
626        let append_c = Expr::Const(Name::str("List.append"), vec![]);
627        let add_c = Expr::Const(Name::str("Nat.add"), vec![]);
628        add_axiom(
629            env,
630            "List.length_append",
631            vec![],
632            implicit_pi(
633                "alpha",
634                type1(),
635                default_pi(
636                    "l1",
637                    list_of(Expr::BVar(0)),
638                    default_pi(
639                        "l2",
640                        list_of(Expr::BVar(1)),
641                        eq_expr(
642                            nat_ty(),
643                            app(length.clone(), app2(append_c, Expr::BVar(1), Expr::BVar(0))),
644                            app2(
645                                add_c,
646                                app(length.clone(), Expr::BVar(1)),
647                                app(length, Expr::BVar(0)),
648                            ),
649                        ),
650                    ),
651                ),
652            ),
653        )?;
654    }
655    add_axiom(
656        env,
657        "List.map_nil",
658        vec![],
659        implicit_pi(
660            "alpha",
661            type1(),
662            implicit_pi(
663                "beta",
664                type1(),
665                default_pi(
666                    "f",
667                    arrow(Expr::BVar(1), Expr::BVar(0)),
668                    eq_expr(
669                        list_of(Expr::BVar(1)),
670                        app2(
671                            Expr::Const(Name::str("List.map"), vec![]),
672                            Expr::BVar(0),
673                            app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(2)),
674                        ),
675                        app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(1)),
676                    ),
677                ),
678            ),
679        ),
680    )?;
681    add_axiom(
682        env,
683        "List.map_cons",
684        vec![],
685        implicit_pi(
686            "alpha",
687            type1(),
688            implicit_pi(
689                "beta",
690                type1(),
691                default_pi(
692                    "f",
693                    arrow(Expr::BVar(1), Expr::BVar(0)),
694                    default_pi(
695                        "a",
696                        Expr::BVar(2),
697                        default_pi(
698                            "l",
699                            list_of(Expr::BVar(3)),
700                            eq_expr(
701                                list_of(Expr::BVar(3)),
702                                app2(
703                                    Expr::Const(Name::str("List.map"), vec![]),
704                                    Expr::BVar(2),
705                                    app2(
706                                        Expr::Const(Name::str("List.cons"), vec![]),
707                                        Expr::BVar(1),
708                                        Expr::BVar(0),
709                                    ),
710                                ),
711                                app2(
712                                    Expr::Const(Name::str("List.cons"), vec![]),
713                                    app(Expr::BVar(2), Expr::BVar(1)),
714                                    app2(
715                                        Expr::Const(Name::str("List.map"), vec![]),
716                                        Expr::BVar(2),
717                                        Expr::BVar(0),
718                                    ),
719                                ),
720                            ),
721                        ),
722                    ),
723                ),
724            ),
725        ),
726    )?;
727    add_axiom(
728        env,
729        "List.map_map",
730        vec![],
731        implicit_pi(
732            "alpha",
733            type1(),
734            implicit_pi(
735                "beta",
736                type1(),
737                implicit_pi(
738                    "gamma",
739                    type1(),
740                    default_pi(
741                        "f",
742                        arrow(Expr::BVar(2), Expr::BVar(1)),
743                        default_pi(
744                            "g",
745                            arrow(Expr::BVar(2), Expr::BVar(1)),
746                            default_pi(
747                                "l",
748                                list_of(Expr::BVar(4)),
749                                eq_expr(
750                                    list_of(Expr::BVar(3)),
751                                    app2(
752                                        Expr::Const(Name::str("List.map"), vec![]),
753                                        Expr::BVar(1),
754                                        app2(
755                                            Expr::Const(Name::str("List.map"), vec![]),
756                                            Expr::BVar(2),
757                                            Expr::BVar(0),
758                                        ),
759                                    ),
760                                    app2(
761                                        Expr::Const(Name::str("List.map"), vec![]),
762                                        Expr::Lam(
763                                            BinderInfo::Default,
764                                            Name::str("x"),
765                                            Box::new(Expr::BVar(5)),
766                                            Box::new(app(
767                                                Expr::BVar(2),
768                                                app(Expr::BVar(3), Expr::BVar(0)),
769                                            )),
770                                        ),
771                                        Expr::BVar(0),
772                                    ),
773                                ),
774                            ),
775                        ),
776                    ),
777                ),
778            ),
779        ),
780    )?;
781    add_axiom(
782        env,
783        "List.map_id",
784        vec![],
785        implicit_pi(
786            "alpha",
787            type1(),
788            default_pi(
789                "l",
790                list_of(Expr::BVar(0)),
791                eq_expr(
792                    list_of(Expr::BVar(1)),
793                    app2(
794                        Expr::Const(Name::str("List.map"), vec![]),
795                        Expr::Lam(
796                            BinderInfo::Default,
797                            Name::str("x"),
798                            Box::new(Expr::BVar(1)),
799                            Box::new(Expr::BVar(0)),
800                        ),
801                        Expr::BVar(0),
802                    ),
803                    Expr::BVar(0),
804                ),
805            ),
806        ),
807    )?;
808    add_axiom(
809        env,
810        "List.reverse_nil",
811        vec![],
812        implicit_pi(
813            "alpha",
814            type1(),
815            eq_expr(
816                list_of(Expr::BVar(0)),
817                app(
818                    Expr::Const(Name::str("List.reverse"), vec![]),
819                    app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(0)),
820                ),
821                app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(0)),
822            ),
823        ),
824    )?;
825    add_axiom(
826        env,
827        "List.reverse_cons",
828        vec![],
829        implicit_pi(
830            "alpha",
831            type1(),
832            default_pi(
833                "a",
834                Expr::BVar(0),
835                default_pi(
836                    "l",
837                    list_of(Expr::BVar(1)),
838                    eq_expr(
839                        list_of(Expr::BVar(2)),
840                        app(
841                            Expr::Const(Name::str("List.reverse"), vec![]),
842                            app2(
843                                Expr::Const(Name::str("List.cons"), vec![]),
844                                Expr::BVar(1),
845                                Expr::BVar(0),
846                            ),
847                        ),
848                        app2(
849                            Expr::Const(Name::str("List.append"), vec![]),
850                            app(
851                                Expr::Const(Name::str("List.reverse"), vec![]),
852                                Expr::BVar(0),
853                            ),
854                            app2(
855                                Expr::Const(Name::str("List.cons"), vec![]),
856                                Expr::BVar(1),
857                                app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(2)),
858                            ),
859                        ),
860                    ),
861                ),
862            ),
863        ),
864    )?;
865    add_axiom(
866        env,
867        "List.reverse_reverse",
868        vec![],
869        implicit_pi(
870            "alpha",
871            type1(),
872            default_pi(
873                "l",
874                list_of(Expr::BVar(0)),
875                eq_expr(
876                    list_of(Expr::BVar(1)),
877                    app(
878                        Expr::Const(Name::str("List.reverse"), vec![]),
879                        app(
880                            Expr::Const(Name::str("List.reverse"), vec![]),
881                            Expr::BVar(0),
882                        ),
883                    ),
884                    Expr::BVar(0),
885                ),
886            ),
887        ),
888    )?;
889    add_axiom(
890        env,
891        "List.filter_nil",
892        vec![],
893        implicit_pi(
894            "alpha",
895            type1(),
896            default_pi(
897                "p",
898                arrow(Expr::BVar(0), bool_ty()),
899                eq_expr(
900                    list_of(Expr::BVar(1)),
901                    app2(
902                        Expr::Const(Name::str("List.filter"), vec![]),
903                        Expr::BVar(0),
904                        app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(1)),
905                    ),
906                    app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(1)),
907                ),
908            ),
909        ),
910    )?;
911    add_axiom(
912        env,
913        "List.foldr_nil",
914        vec![],
915        implicit_pi(
916            "alpha",
917            type1(),
918            implicit_pi(
919                "beta",
920                type1(),
921                default_pi(
922                    "f",
923                    arrow(Expr::BVar(1), arrow(Expr::BVar(1), Expr::BVar(1))),
924                    default_pi(
925                        "b",
926                        Expr::BVar(1),
927                        eq_expr(
928                            Expr::BVar(2),
929                            app3(
930                                Expr::Const(Name::str("List.foldr"), vec![]),
931                                Expr::BVar(1),
932                                Expr::BVar(0),
933                                app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(3)),
934                            ),
935                            Expr::BVar(0),
936                        ),
937                    ),
938                ),
939            ),
940        ),
941    )?;
942    add_axiom(
943        env,
944        "List.foldl_nil",
945        vec![],
946        implicit_pi(
947            "alpha",
948            type1(),
949            implicit_pi(
950                "beta",
951                type1(),
952                default_pi(
953                    "f",
954                    arrow(Expr::BVar(0), arrow(Expr::BVar(2), Expr::BVar(1))),
955                    default_pi(
956                        "b",
957                        Expr::BVar(1),
958                        eq_expr(
959                            Expr::BVar(2),
960                            app3(
961                                Expr::Const(Name::str("List.foldl"), vec![]),
962                                Expr::BVar(1),
963                                Expr::BVar(0),
964                                app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(3)),
965                            ),
966                            Expr::BVar(0),
967                        ),
968                    ),
969                ),
970            ),
971        ),
972    )?;
973    {
974        let length = Expr::Const(Name::str("List.length"), vec![]);
975        let reverse = Expr::Const(Name::str("List.reverse"), vec![]);
976        add_axiom(
977            env,
978            "List.length_reverse",
979            vec![],
980            implicit_pi(
981                "alpha",
982                type1(),
983                default_pi(
984                    "l",
985                    list_of(Expr::BVar(0)),
986                    eq_expr(
987                        nat_ty(),
988                        app(length.clone(), app(reverse, Expr::BVar(0))),
989                        app(length, Expr::BVar(0)),
990                    ),
991                ),
992            ),
993        )?;
994    }
995    {
996        let length = Expr::Const(Name::str("List.length"), vec![]);
997        let map_c = Expr::Const(Name::str("List.map"), vec![]);
998        add_axiom(
999            env,
1000            "List.length_map",
1001            vec![],
1002            implicit_pi(
1003                "alpha",
1004                type1(),
1005                implicit_pi(
1006                    "beta",
1007                    type1(),
1008                    default_pi(
1009                        "f",
1010                        arrow(Expr::BVar(1), Expr::BVar(0)),
1011                        default_pi(
1012                            "l",
1013                            list_of(Expr::BVar(2)),
1014                            eq_expr(
1015                                nat_ty(),
1016                                app(length.clone(), app2(map_c, Expr::BVar(1), Expr::BVar(0))),
1017                                app(length, Expr::BVar(0)),
1018                            ),
1019                        ),
1020                    ),
1021                ),
1022            ),
1023        )?;
1024    }
1025    {
1026        let length = Expr::Const(Name::str("List.length"), vec![]);
1027        let filter_c = Expr::Const(Name::str("List.filter"), vec![]);
1028        let le_c = Expr::Const(Name::str("Nat.le"), vec![]);
1029        add_axiom(
1030            env,
1031            "List.length_filter_le",
1032            vec![],
1033            implicit_pi(
1034                "alpha",
1035                type1(),
1036                default_pi(
1037                    "p",
1038                    arrow(Expr::BVar(0), bool_ty()),
1039                    default_pi(
1040                        "l",
1041                        list_of(Expr::BVar(1)),
1042                        app2(
1043                            le_c,
1044                            app(length.clone(), app2(filter_c, Expr::BVar(1), Expr::BVar(0))),
1045                            app(length, Expr::BVar(0)),
1046                        ),
1047                    ),
1048                ),
1049            ),
1050        )?;
1051    }
1052    add_axiom(
1053        env,
1054        "List.mem_nil",
1055        vec![],
1056        implicit_pi(
1057            "alpha",
1058            type1(),
1059            default_pi(
1060                "a",
1061                Expr::BVar(0),
1062                arrow(
1063                    app2(
1064                        Expr::Const(Name::str("List.Mem"), vec![]),
1065                        Expr::BVar(0),
1066                        app(Expr::Const(Name::str("List.nil"), vec![]), Expr::BVar(1)),
1067                    ),
1068                    Expr::Const(Name::str("False"), vec![]),
1069                ),
1070            ),
1071        ),
1072    )?;
1073    add_axiom(
1074        env,
1075        "List.mem_cons",
1076        vec![],
1077        implicit_pi(
1078            "alpha",
1079            type1(),
1080            default_pi(
1081                "a",
1082                Expr::BVar(0),
1083                default_pi(
1084                    "b",
1085                    Expr::BVar(1),
1086                    default_pi(
1087                        "l",
1088                        list_of(Expr::BVar(2)),
1089                        app2(
1090                            Expr::Const(Name::str("Iff"), vec![]),
1091                            app2(
1092                                Expr::Const(Name::str("List.Mem"), vec![]),
1093                                Expr::BVar(2),
1094                                app2(
1095                                    Expr::Const(Name::str("List.cons"), vec![]),
1096                                    Expr::BVar(1),
1097                                    Expr::BVar(0),
1098                                ),
1099                            ),
1100                            app2(
1101                                Expr::Const(Name::str("Or"), vec![]),
1102                                eq_expr(Expr::BVar(3), Expr::BVar(2), Expr::BVar(1)),
1103                                app2(
1104                                    Expr::Const(Name::str("List.Mem"), vec![]),
1105                                    Expr::BVar(2),
1106                                    Expr::BVar(0),
1107                                ),
1108                            ),
1109                        ),
1110                    ),
1111                ),
1112            ),
1113        ),
1114    )?;
1115    add_axiom(
1116        env,
1117        "List.unzip",
1118        vec![],
1119        implicit_pi(
1120            "alpha",
1121            type1(),
1122            implicit_pi(
1123                "beta",
1124                type1(),
1125                default_pi(
1126                    "l",
1127                    list_of(prod_of(Expr::BVar(1), Expr::BVar(0))),
1128                    prod_of(list_of(Expr::BVar(2)), list_of(Expr::BVar(1))),
1129                ),
1130            ),
1131        ),
1132    )?;
1133    add_axiom(
1134        env,
1135        "List.partition",
1136        vec![],
1137        implicit_pi(
1138            "alpha",
1139            type1(),
1140            default_pi(
1141                "p",
1142                arrow(Expr::BVar(0), bool_ty()),
1143                default_pi(
1144                    "l",
1145                    list_of(Expr::BVar(1)),
1146                    prod_of(list_of(Expr::BVar(2)), list_of(Expr::BVar(2))),
1147                ),
1148            ),
1149        ),
1150    )?;
1151    add_axiom(
1152        env,
1153        "List.span",
1154        vec![],
1155        implicit_pi(
1156            "alpha",
1157            type1(),
1158            default_pi(
1159                "p",
1160                arrow(Expr::BVar(0), bool_ty()),
1161                default_pi(
1162                    "l",
1163                    list_of(Expr::BVar(1)),
1164                    prod_of(list_of(Expr::BVar(2)), list_of(Expr::BVar(2))),
1165                ),
1166            ),
1167        ),
1168    )?;
1169    add_axiom(
1170        env,
1171        "List.find?",
1172        vec![],
1173        implicit_pi(
1174            "alpha",
1175            type1(),
1176            default_pi(
1177                "p",
1178                arrow(Expr::BVar(0), bool_ty()),
1179                default_pi("l", list_of(Expr::BVar(1)), option_of(Expr::BVar(2))),
1180            ),
1181        ),
1182    )?;
1183    add_axiom(
1184        env,
1185        "List.count",
1186        vec![],
1187        implicit_pi(
1188            "alpha",
1189            type1(),
1190            default_pi(
1191                "p",
1192                arrow(Expr::BVar(0), bool_ty()),
1193                default_pi("l", list_of(Expr::BVar(1)), nat_ty()),
1194            ),
1195        ),
1196    )?;
1197    add_axiom(
1198        env,
1199        "List.intersperse",
1200        vec![],
1201        implicit_pi(
1202            "alpha",
1203            type1(),
1204            default_pi(
1205                "sep",
1206                Expr::BVar(0),
1207                default_pi("l", list_of(Expr::BVar(1)), list_of(Expr::BVar(2))),
1208            ),
1209        ),
1210    )?;
1211    add_axiom(
1212        env,
1213        "List.transpose",
1214        vec![],
1215        implicit_pi(
1216            "alpha",
1217            type1(),
1218            default_pi(
1219                "ll",
1220                list_of(list_of(Expr::BVar(0))),
1221                list_of(list_of(Expr::BVar(1))),
1222            ),
1223        ),
1224    )?;
1225    add_axiom(
1226        env,
1227        "List.Perm",
1228        vec![],
1229        implicit_pi(
1230            "alpha",
1231            type1(),
1232            default_pi(
1233                "l1",
1234                list_of(Expr::BVar(0)),
1235                default_pi("l2", list_of(Expr::BVar(1)), prop()),
1236            ),
1237        ),
1238    )?;
1239    add_axiom(
1240        env,
1241        "List.Perm.refl",
1242        vec![],
1243        implicit_pi(
1244            "alpha",
1245            type1(),
1246            default_pi(
1247                "l",
1248                list_of(Expr::BVar(0)),
1249                app2(
1250                    Expr::Const(Name::str("List.Perm"), vec![]),
1251                    Expr::BVar(0),
1252                    Expr::BVar(0),
1253                ),
1254            ),
1255        ),
1256    )?;
1257    add_axiom(
1258        env,
1259        "List.Perm.symm",
1260        vec![],
1261        implicit_pi(
1262            "alpha",
1263            type1(),
1264            default_pi(
1265                "l1",
1266                list_of(Expr::BVar(0)),
1267                default_pi(
1268                    "l2",
1269                    list_of(Expr::BVar(1)),
1270                    arrow(
1271                        app2(
1272                            Expr::Const(Name::str("List.Perm"), vec![]),
1273                            Expr::BVar(1),
1274                            Expr::BVar(0),
1275                        ),
1276                        app2(
1277                            Expr::Const(Name::str("List.Perm"), vec![]),
1278                            Expr::BVar(0),
1279                            Expr::BVar(1),
1280                        ),
1281                    ),
1282                ),
1283            ),
1284        ),
1285    )?;
1286    add_axiom(
1287        env,
1288        "List.Perm.trans",
1289        vec![],
1290        implicit_pi(
1291            "alpha",
1292            type1(),
1293            default_pi(
1294                "l1",
1295                list_of(Expr::BVar(0)),
1296                default_pi(
1297                    "l2",
1298                    list_of(Expr::BVar(1)),
1299                    default_pi(
1300                        "l3",
1301                        list_of(Expr::BVar(2)),
1302                        arrow(
1303                            app2(
1304                                Expr::Const(Name::str("List.Perm"), vec![]),
1305                                Expr::BVar(2),
1306                                Expr::BVar(1),
1307                            ),
1308                            arrow(
1309                                app2(
1310                                    Expr::Const(Name::str("List.Perm"), vec![]),
1311                                    Expr::BVar(1),
1312                                    Expr::BVar(0),
1313                                ),
1314                                app2(
1315                                    Expr::Const(Name::str("List.Perm"), vec![]),
1316                                    Expr::BVar(2),
1317                                    Expr::BVar(0),
1318                                ),
1319                            ),
1320                        ),
1321                    ),
1322                ),
1323            ),
1324        ),
1325    )?;
1326    add_axiom(
1327        env,
1328        "List.Sublist",
1329        vec![],
1330        implicit_pi(
1331            "alpha",
1332            type1(),
1333            default_pi(
1334                "l1",
1335                list_of(Expr::BVar(0)),
1336                default_pi("l2", list_of(Expr::BVar(1)), prop()),
1337            ),
1338        ),
1339    )?;
1340    add_axiom(
1341        env,
1342        "List.Sublist.refl",
1343        vec![],
1344        implicit_pi(
1345            "alpha",
1346            type1(),
1347            default_pi(
1348                "l",
1349                list_of(Expr::BVar(0)),
1350                app2(
1351                    Expr::Const(Name::str("List.Sublist"), vec![]),
1352                    Expr::BVar(0),
1353                    Expr::BVar(0),
1354                ),
1355            ),
1356        ),
1357    )?;
1358    add_axiom(
1359        env,
1360        "List.Sublist.trans",
1361        vec![],
1362        implicit_pi(
1363            "alpha",
1364            type1(),
1365            default_pi(
1366                "l1",
1367                list_of(Expr::BVar(0)),
1368                default_pi(
1369                    "l2",
1370                    list_of(Expr::BVar(1)),
1371                    default_pi(
1372                        "l3",
1373                        list_of(Expr::BVar(2)),
1374                        arrow(
1375                            app2(
1376                                Expr::Const(Name::str("List.Sublist"), vec![]),
1377                                Expr::BVar(2),
1378                                Expr::BVar(1),
1379                            ),
1380                            arrow(
1381                                app2(
1382                                    Expr::Const(Name::str("List.Sublist"), vec![]),
1383                                    Expr::BVar(1),
1384                                    Expr::BVar(0),
1385                                ),
1386                                app2(
1387                                    Expr::Const(Name::str("List.Sublist"), vec![]),
1388                                    Expr::BVar(2),
1389                                    Expr::BVar(0),
1390                                ),
1391                            ),
1392                        ),
1393                    ),
1394                ),
1395            ),
1396        ),
1397    )?;
1398    add_axiom(
1399        env,
1400        "List.Decidable.mem",
1401        vec![],
1402        implicit_pi(
1403            "alpha",
1404            type1(),
1405            default_pi(
1406                "a",
1407                Expr::BVar(0),
1408                default_pi(
1409                    "l",
1410                    list_of(Expr::BVar(1)),
1411                    app(
1412                        Expr::Const(Name::str("Decidable"), vec![]),
1413                        app2(
1414                            Expr::Const(Name::str("List.Mem"), vec![]),
1415                            Expr::BVar(1),
1416                            Expr::BVar(0),
1417                        ),
1418                    ),
1419                ),
1420            ),
1421        ),
1422    )?;
1423    {
1424        let take_c = Expr::Const(Name::str("List.take"), vec![]);
1425        let append_c = Expr::Const(Name::str("List.append"), vec![]);
1426        let length_c = Expr::Const(Name::str("List.length"), vec![]);
1427        let sub_c = Expr::Const(Name::str("Nat.sub"), vec![]);
1428        add_axiom(
1429            env,
1430            "List.take_append",
1431            vec![],
1432            implicit_pi(
1433                "alpha",
1434                type1(),
1435                default_pi(
1436                    "n",
1437                    nat_ty(),
1438                    default_pi(
1439                        "l1",
1440                        list_of(Expr::BVar(1)),
1441                        default_pi(
1442                            "l2",
1443                            list_of(Expr::BVar(2)),
1444                            eq_expr(
1445                                list_of(Expr::BVar(3)),
1446                                app2(
1447                                    take_c.clone(),
1448                                    Expr::BVar(2),
1449                                    app2(append_c.clone(), Expr::BVar(1), Expr::BVar(0)),
1450                                ),
1451                                app2(
1452                                    append_c,
1453                                    app2(take_c.clone(), Expr::BVar(2), Expr::BVar(1)),
1454                                    app2(
1455                                        take_c,
1456                                        app2(sub_c, Expr::BVar(2), app(length_c, Expr::BVar(1))),
1457                                        Expr::BVar(0),
1458                                    ),
1459                                ),
1460                            ),
1461                        ),
1462                    ),
1463                ),
1464            ),
1465        )?;
1466    }
1467    {
1468        let drop_c = Expr::Const(Name::str("List.drop"), vec![]);
1469        let append_c = Expr::Const(Name::str("List.append"), vec![]);
1470        let length_c = Expr::Const(Name::str("List.length"), vec![]);
1471        let sub_c = Expr::Const(Name::str("Nat.sub"), vec![]);
1472        add_axiom(
1473            env,
1474            "List.drop_append",
1475            vec![],
1476            implicit_pi(
1477                "alpha",
1478                type1(),
1479                default_pi(
1480                    "n",
1481                    nat_ty(),
1482                    default_pi(
1483                        "l1",
1484                        list_of(Expr::BVar(1)),
1485                        default_pi(
1486                            "l2",
1487                            list_of(Expr::BVar(2)),
1488                            eq_expr(
1489                                list_of(Expr::BVar(3)),
1490                                app2(
1491                                    drop_c.clone(),
1492                                    Expr::BVar(2),
1493                                    app2(append_c.clone(), Expr::BVar(1), Expr::BVar(0)),
1494                                ),
1495                                app2(
1496                                    append_c,
1497                                    app2(drop_c.clone(), Expr::BVar(2), Expr::BVar(1)),
1498                                    app2(
1499                                        drop_c,
1500                                        app2(sub_c, Expr::BVar(2), app(length_c, Expr::BVar(1))),
1501                                        Expr::BVar(0),
1502                                    ),
1503                                ),
1504                            ),
1505                        ),
1506                    ),
1507                ),
1508            ),
1509        )?;
1510    }
1511    {
1512        let count_c = Expr::Const(Name::str("List.count"), vec![]);
1513        let length_c = Expr::Const(Name::str("List.length"), vec![]);
1514        let le_c = Expr::Const(Name::str("Nat.le"), vec![]);
1515        add_axiom(
1516            env,
1517            "List.count_le_length",
1518            vec![],
1519            implicit_pi(
1520                "alpha",
1521                type1(),
1522                default_pi(
1523                    "p",
1524                    arrow(Expr::BVar(0), bool_ty()),
1525                    default_pi(
1526                        "l",
1527                        list_of(Expr::BVar(1)),
1528                        app2(
1529                            le_c,
1530                            app2(count_c, Expr::BVar(1), Expr::BVar(0)),
1531                            app(length_c, Expr::BVar(0)),
1532                        ),
1533                    ),
1534                ),
1535            ),
1536        )?;
1537    }
1538    Ok(())
1539}
1540/// Create a `List` type expression applied to an element type.
1541pub fn list_type(elem_ty: Expr) -> Expr {
1542    app(Expr::Const(Name::str("List"), vec![]), elem_ty)
1543}
1544/// Create an empty list (nil) for a given element type.
1545pub fn list_nil(elem_ty: Expr) -> Expr {
1546    app(Expr::Const(Name::str("List.nil"), vec![]), elem_ty)
1547}
1548/// Create a cons cell: `List.cons head tail`.
1549pub fn list_cons(head: Expr, tail: Expr) -> Expr {
1550    app2(Expr::Const(Name::str("List.cons"), vec![]), head, tail)
1551}
1552/// Create a `List.map f l` expression.
1553#[allow(dead_code)]
1554pub fn list_map(f: Expr, l: Expr) -> Expr {
1555    app2(Expr::Const(Name::str("List.map"), vec![]), f, l)
1556}
1557/// Create a `List.filter pred l` expression.
1558#[allow(dead_code)]
1559pub fn list_filter(pred: Expr, l: Expr) -> Expr {
1560    app2(Expr::Const(Name::str("List.filter"), vec![]), pred, l)
1561}
1562/// Create a `List.foldr f init l` expression.
1563#[allow(dead_code)]
1564pub fn list_foldr(f: Expr, init: Expr, l: Expr) -> Expr {
1565    app3(Expr::Const(Name::str("List.foldr"), vec![]), f, init, l)
1566}
1567/// Create a `List.foldl f init l` expression.
1568#[allow(dead_code)]
1569pub fn list_foldl(f: Expr, init: Expr, l: Expr) -> Expr {
1570    app3(Expr::Const(Name::str("List.foldl"), vec![]), f, init, l)
1571}
1572/// Create a `List.reverse l` expression.
1573#[allow(dead_code)]
1574pub fn list_reverse(l: Expr) -> Expr {
1575    app(Expr::Const(Name::str("List.reverse"), vec![]), l)
1576}
1577/// Create a `List.length l` expression.
1578#[allow(dead_code)]
1579pub fn list_length(l: Expr) -> Expr {
1580    app(Expr::Const(Name::str("List.length"), vec![]), l)
1581}
1582/// Create a `List.append l1 l2` expression.
1583#[allow(dead_code)]
1584pub fn list_append(l1: Expr, l2: Expr) -> Expr {
1585    app2(Expr::Const(Name::str("List.append"), vec![]), l1, l2)
1586}
1587/// Create a `List.head? l` expression.
1588#[allow(dead_code)]
1589pub fn list_head(l: Expr) -> Expr {
1590    app(Expr::Const(Name::str("List.head?"), vec![]), l)
1591}
1592/// Create a `List.tail l` expression.
1593#[allow(dead_code)]
1594pub fn list_tail(l: Expr) -> Expr {
1595    app(Expr::Const(Name::str("List.tail"), vec![]), l)
1596}
1597/// Create a `List.take n l` expression.
1598#[allow(dead_code)]
1599pub fn list_take(n: Expr, l: Expr) -> Expr {
1600    app2(Expr::Const(Name::str("List.take"), vec![]), n, l)
1601}
1602/// Create a `List.drop n l` expression.
1603#[allow(dead_code)]
1604pub fn list_drop(n: Expr, l: Expr) -> Expr {
1605    app2(Expr::Const(Name::str("List.drop"), vec![]), n, l)
1606}
1607/// Create a `List.replicate n x` expression.
1608#[allow(dead_code)]
1609pub fn list_replicate(n: Expr, x: Expr) -> Expr {
1610    app2(Expr::Const(Name::str("List.replicate"), vec![]), n, x)
1611}
1612/// Create a `List.join ll` expression.
1613#[allow(dead_code)]
1614pub fn list_join(ll: Expr) -> Expr {
1615    app(Expr::Const(Name::str("List.join"), vec![]), ll)
1616}
1617/// Create a `List.range n` expression.
1618#[allow(dead_code)]
1619pub fn list_range(n: Expr) -> Expr {
1620    app(Expr::Const(Name::str("List.range"), vec![]), n)
1621}
1622/// Build a list expression from a Rust Vec of element expressions.
1623///
1624/// `mk_list_from_vec(elem_ty, vec![a, b, c])` produces
1625/// `List.cons a (List.cons b (List.cons c (List.nil elem_ty)))`.
1626#[allow(dead_code)]
1627pub fn mk_list_from_vec(elem_ty: Expr, elems: Vec<Expr>) -> Expr {
1628    let mut result = list_nil(elem_ty);
1629    for e in elems.into_iter().rev() {
1630        result = list_cons(e, result);
1631    }
1632    result
1633}
oxilean_std/list/functions.rs

oxilean_std/list/
functions.rs
