oxilean_std/vec/
functions_2.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use oxilean_kernel::{
7    BinderInfo, Declaration, Environment, Expr, InductiveEnv, InductiveType, IntroRule, Level, Name,
8};
9
10/// Register Vec.zip axioms: zip two vectors of the same length element-wise.
11#[allow(dead_code)]
12pub fn register_vec_zip_axioms(env: &mut Environment) {
13    use oxilean_kernel::{BinderInfo, Declaration, Expr, Level, Name};
14    let type1 = Expr::Sort(Level::succ(Level::zero()));
15    let nat_ty = Expr::Const(Name::str("Nat"), vec![]);
16    let zip_ty = Expr::Pi(
17        BinderInfo::Implicit,
18        Name::str("α"),
19        Box::new(type1.clone()),
20        Box::new(Expr::Pi(
21            BinderInfo::Implicit,
22            Name::str("β"),
23            Box::new(type1.clone()),
24            Box::new(Expr::Pi(
25                BinderInfo::Implicit,
26                Name::str("n"),
27                Box::new(nat_ty.clone()),
28                Box::new(Expr::Pi(
29                    BinderInfo::Default,
30                    Name::str("xs"),
31                    Box::new(Expr::App(
32                        Box::new(Expr::App(
33                            Box::new(Expr::Const(Name::str("Vec"), vec![])),
34                            Box::new(Expr::BVar(2)),
35                        )),
36                        Box::new(Expr::BVar(0)),
37                    )),
38                    Box::new(Expr::Pi(
39                        BinderInfo::Default,
40                        Name::str("ys"),
41                        Box::new(Expr::App(
42                            Box::new(Expr::App(
43                                Box::new(Expr::Const(Name::str("Vec"), vec![])),
44                                Box::new(Expr::BVar(3)),
45                            )),
46                            Box::new(Expr::BVar(1)),
47                        )),
48                        Box::new(Expr::Const(Name::str("Unit"), vec![])),
49                    )),
50                )),
51            )),
52        )),
53    );
54    let zip_decl = Declaration::Axiom {
55        name: Name::str("Vec.zip"),
56        univ_params: vec![],
57        ty: zip_ty,
58    };
59    let _ = env.add(zip_decl);
60    let zip_nil_ty = Expr::Pi(
61        BinderInfo::Implicit,
62        Name::str("α"),
63        Box::new(type1.clone()),
64        Box::new(Expr::Pi(
65            BinderInfo::Implicit,
66            Name::str("β"),
67            Box::new(type1.clone()),
68            Box::new(Expr::Const(Name::str("True"), vec![])),
69        )),
70    );
71    let zip_nil_decl = Declaration::Axiom {
72        name: Name::str("Vec.zip_nil"),
73        univ_params: vec![],
74        ty: zip_nil_ty,
75    };
76    let _ = env.add(zip_nil_decl);
77    let zip_length_ty = Expr::Pi(
78        BinderInfo::Implicit,
79        Name::str("α"),
80        Box::new(type1.clone()),
81        Box::new(Expr::Pi(
82            BinderInfo::Implicit,
83            Name::str("β"),
84            Box::new(type1.clone()),
85            Box::new(Expr::Pi(
86                BinderInfo::Implicit,
87                Name::str("n"),
88                Box::new(nat_ty.clone()),
89                Box::new(Expr::Const(Name::str("True"), vec![])),
90            )),
91        )),
92    );
93    let zip_length_decl = Declaration::Axiom {
94        name: Name::str("Vec.zip_length"),
95        univ_params: vec![],
96        ty: zip_length_ty,
97    };
98    let _ = env.add(zip_length_decl);
99}
100/// Register Vec.unzip axioms: unzip a vector of pairs into two vectors.
101#[allow(dead_code)]
102pub fn register_vec_unzip_axioms(env: &mut Environment) {
103    use oxilean_kernel::{BinderInfo, Declaration, Expr, Level, Name};
104    let type1 = Expr::Sort(Level::succ(Level::zero()));
105    let nat_ty = Expr::Const(Name::str("Nat"), vec![]);
106    let unzip_ty = Expr::Pi(
107        BinderInfo::Implicit,
108        Name::str("α"),
109        Box::new(type1.clone()),
110        Box::new(Expr::Pi(
111            BinderInfo::Implicit,
112            Name::str("β"),
113            Box::new(type1.clone()),
114            Box::new(Expr::Pi(
115                BinderInfo::Implicit,
116                Name::str("n"),
117                Box::new(nat_ty.clone()),
118                Box::new(Expr::Pi(
119                    BinderInfo::Default,
120                    Name::str("xs"),
121                    Box::new(Expr::Const(Name::str("Unit"), vec![])),
122                    Box::new(Expr::Const(Name::str("Unit"), vec![])),
123                )),
124            )),
125        )),
126    );
127    let unzip_decl = Declaration::Axiom {
128        name: Name::str("Vec.unzip"),
129        univ_params: vec![],
130        ty: unzip_ty,
131    };
132    let _ = env.add(unzip_decl);
133    let zip_unzip_ty = Expr::Pi(
134        BinderInfo::Implicit,
135        Name::str("α"),
136        Box::new(type1.clone()),
137        Box::new(Expr::Pi(
138            BinderInfo::Implicit,
139            Name::str("β"),
140            Box::new(type1.clone()),
141            Box::new(Expr::Pi(
142                BinderInfo::Implicit,
143                Name::str("n"),
144                Box::new(nat_ty.clone()),
145                Box::new(Expr::Const(Name::str("True"), vec![])),
146            )),
147        )),
148    );
149    let zip_unzip_decl = Declaration::Axiom {
150        name: Name::str("Vec.zip_unzip"),
151        univ_params: vec![],
152        ty: zip_unzip_ty,
153    };
154    let _ = env.add(zip_unzip_decl);
155}
156/// Register Vec.foldl and Vec.foldr axioms.
157#[allow(dead_code)]
158pub fn register_vec_fold_axioms(env: &mut Environment) {
159    use oxilean_kernel::{BinderInfo, Declaration, Expr, Level, Name};
160    let type1 = Expr::Sort(Level::succ(Level::zero()));
161    let nat_ty = Expr::Const(Name::str("Nat"), vec![]);
162    let foldl_ty = Expr::Pi(
163        BinderInfo::Implicit,
164        Name::str("α"),
165        Box::new(type1.clone()),
166        Box::new(Expr::Pi(
167            BinderInfo::Implicit,
168            Name::str("β"),
169            Box::new(type1.clone()),
170            Box::new(Expr::Pi(
171                BinderInfo::Default,
172                Name::str("f"),
173                Box::new(Expr::Pi(
174                    BinderInfo::Default,
175                    Name::str("_acc"),
176                    Box::new(Expr::BVar(1)),
177                    Box::new(Expr::Pi(
178                        BinderInfo::Default,
179                        Name::str("_x"),
180                        Box::new(Expr::BVar(2)),
181                        Box::new(Expr::BVar(3)),
182                    )),
183                )),
184                Box::new(Expr::Pi(
185                    BinderInfo::Default,
186                    Name::str("init"),
187                    Box::new(Expr::BVar(2)),
188                    Box::new(Expr::Pi(
189                        BinderInfo::Implicit,
190                        Name::str("n"),
191                        Box::new(nat_ty.clone()),
192                        Box::new(Expr::Pi(
193                            BinderInfo::Default,
194                            Name::str("_xs"),
195                            Box::new(Expr::Const(Name::str("Unit"), vec![])),
196                            Box::new(Expr::BVar(4)),
197                        )),
198                    )),
199                )),
200            )),
201        )),
202    );
203    let foldl_decl = Declaration::Axiom {
204        name: Name::str("Vec.foldl"),
205        univ_params: vec![],
206        ty: foldl_ty,
207    };
208    let _ = env.add(foldl_decl);
209    let foldl_nil_ty = Expr::Pi(
210        BinderInfo::Implicit,
211        Name::str("α"),
212        Box::new(type1.clone()),
213        Box::new(Expr::Pi(
214            BinderInfo::Implicit,
215            Name::str("β"),
216            Box::new(type1.clone()),
217            Box::new(Expr::Const(Name::str("True"), vec![])),
218        )),
219    );
220    let foldl_nil_decl = Declaration::Axiom {
221        name: Name::str("Vec.foldl_nil"),
222        univ_params: vec![],
223        ty: foldl_nil_ty,
224    };
225    let _ = env.add(foldl_nil_decl);
226    let foldl_cons_ty = Expr::Pi(
227        BinderInfo::Implicit,
228        Name::str("α"),
229        Box::new(type1.clone()),
230        Box::new(Expr::Pi(
231            BinderInfo::Implicit,
232            Name::str("β"),
233            Box::new(type1.clone()),
234            Box::new(Expr::Const(Name::str("True"), vec![])),
235        )),
236    );
237    let foldl_cons_decl = Declaration::Axiom {
238        name: Name::str("Vec.foldl_cons"),
239        univ_params: vec![],
240        ty: foldl_cons_ty,
241    };
242    let _ = env.add(foldl_cons_decl);
243    let foldr_ty = Expr::Pi(
244        BinderInfo::Implicit,
245        Name::str("α"),
246        Box::new(type1.clone()),
247        Box::new(Expr::Pi(
248            BinderInfo::Implicit,
249            Name::str("β"),
250            Box::new(type1.clone()),
251            Box::new(Expr::Pi(
252                BinderInfo::Default,
253                Name::str("_f"),
254                Box::new(Expr::Const(Name::str("Unit"), vec![])),
255                Box::new(Expr::Pi(
256                    BinderInfo::Default,
257                    Name::str("_init"),
258                    Box::new(Expr::BVar(2)),
259                    Box::new(Expr::Pi(
260                        BinderInfo::Implicit,
261                        Name::str("n"),
262                        Box::new(nat_ty.clone()),
263                        Box::new(Expr::Pi(
264                            BinderInfo::Default,
265                            Name::str("_xs"),
266                            Box::new(Expr::Const(Name::str("Unit"), vec![])),
267                            Box::new(Expr::BVar(4)),
268                        )),
269                    )),
270                )),
271            )),
272        )),
273    );
274    let foldr_decl = Declaration::Axiom {
275        name: Name::str("Vec.foldr"),
276        univ_params: vec![],
277        ty: foldr_ty,
278    };
279    let _ = env.add(foldr_decl);
280}
281/// Register Vec.all and Vec.any axioms.
282#[allow(dead_code)]
283pub fn register_vec_predicate_axioms(env: &mut Environment) {
284    use oxilean_kernel::{BinderInfo, Declaration, Expr, Level, Name};
285    let type1 = Expr::Sort(Level::succ(Level::zero()));
286    let nat_ty = Expr::Const(Name::str("Nat"), vec![]);
287    let all_ty = Expr::Pi(
288        BinderInfo::Implicit,
289        Name::str("α"),
290        Box::new(type1.clone()),
291        Box::new(Expr::Pi(
292            BinderInfo::Implicit,
293            Name::str("n"),
294            Box::new(nat_ty.clone()),
295            Box::new(Expr::Pi(
296                BinderInfo::Default,
297                Name::str("_p"),
298                Box::new(Expr::Pi(
299                    BinderInfo::Default,
300                    Name::str("_x"),
301                    Box::new(Expr::BVar(1)),
302                    Box::new(Expr::Const(Name::str("Bool"), vec![])),
303                )),
304                Box::new(Expr::Pi(
305                    BinderInfo::Default,
306                    Name::str("_xs"),
307                    Box::new(Expr::Const(Name::str("Unit"), vec![])),
308                    Box::new(Expr::Const(Name::str("Bool"), vec![])),
309                )),
310            )),
311        )),
312    );
313    let all_decl = Declaration::Axiom {
314        name: Name::str("Vec.all"),
315        univ_params: vec![],
316        ty: all_ty,
317    };
318    let _ = env.add(all_decl);
319    let any_ty = Expr::Pi(
320        BinderInfo::Implicit,
321        Name::str("α"),
322        Box::new(type1.clone()),
323        Box::new(Expr::Pi(
324            BinderInfo::Implicit,
325            Name::str("n"),
326            Box::new(nat_ty.clone()),
327            Box::new(Expr::Pi(
328                BinderInfo::Default,
329                Name::str("_p"),
330                Box::new(Expr::Pi(
331                    BinderInfo::Default,
332                    Name::str("_x"),
333                    Box::new(Expr::BVar(1)),
334                    Box::new(Expr::Const(Name::str("Bool"), vec![])),
335                )),
336                Box::new(Expr::Pi(
337                    BinderInfo::Default,
338                    Name::str("_xs"),
339                    Box::new(Expr::Const(Name::str("Unit"), vec![])),
340                    Box::new(Expr::Const(Name::str("Bool"), vec![])),
341                )),
342            )),
343        )),
344    );
345    let any_decl = Declaration::Axiom {
346        name: Name::str("Vec.any"),
347        univ_params: vec![],
348        ty: any_ty,
349    };
350    let _ = env.add(any_decl);
351    let all_true_ty = Expr::Pi(
352        BinderInfo::Implicit,
353        Name::str("α"),
354        Box::new(type1.clone()),
355        Box::new(Expr::Pi(
356            BinderInfo::Implicit,
357            Name::str("n"),
358            Box::new(nat_ty.clone()),
359            Box::new(Expr::Const(Name::str("True"), vec![])),
360        )),
361    );
362    let all_true_decl = Declaration::Axiom {
363        name: Name::str("Vec.all_true"),
364        univ_params: vec![],
365        ty: all_true_ty,
366    };
367    let _ = env.add(all_true_decl);
368}
369/// Register Vec.scanl axiom: prefix sums generalization.
370#[allow(dead_code)]
371pub fn register_vec_scan_axioms(env: &mut Environment) {
372    use oxilean_kernel::{BinderInfo, Declaration, Expr, Level, Name};
373    let type1 = Expr::Sort(Level::succ(Level::zero()));
374    let nat_ty = Expr::Const(Name::str("Nat"), vec![]);
375    let scanl_ty = Expr::Pi(
376        BinderInfo::Implicit,
377        Name::str("α"),
378        Box::new(type1.clone()),
379        Box::new(Expr::Pi(
380            BinderInfo::Implicit,
381            Name::str("β"),
382            Box::new(type1.clone()),
383            Box::new(Expr::Pi(
384                BinderInfo::Default,
385                Name::str("_f"),
386                Box::new(Expr::Const(Name::str("Unit"), vec![])),
387                Box::new(Expr::Pi(
388                    BinderInfo::Default,
389                    Name::str("_init"),
390                    Box::new(Expr::BVar(2)),
391                    Box::new(Expr::Pi(
392                        BinderInfo::Implicit,
393                        Name::str("n"),
394                        Box::new(nat_ty.clone()),
395                        Box::new(Expr::Pi(
396                            BinderInfo::Default,
397                            Name::str("_xs"),
398                            Box::new(Expr::Const(Name::str("Unit"), vec![])),
399                            Box::new(Expr::Const(Name::str("Unit"), vec![])),
400                        )),
401                    )),
402                )),
403            )),
404        )),
405    );
406    let scanl_decl = Declaration::Axiom {
407        name: Name::str("Vec.scanl"),
408        univ_params: vec![],
409        ty: scanl_ty,
410    };
411    let _ = env.add(scanl_decl);
412    let scanl_length_ty = Expr::Pi(
413        BinderInfo::Implicit,
414        Name::str("α"),
415        Box::new(type1.clone()),
416        Box::new(Expr::Pi(
417            BinderInfo::Implicit,
418            Name::str("β"),
419            Box::new(type1.clone()),
420            Box::new(Expr::Pi(
421                BinderInfo::Implicit,
422                Name::str("n"),
423                Box::new(nat_ty.clone()),
424                Box::new(Expr::Const(Name::str("True"), vec![])),
425            )),
426        )),
427    );
428    let scanl_length_decl = Declaration::Axiom {
429        name: Name::str("Vec.scanl_length"),
430        univ_params: vec![],
431        ty: scanl_length_ty,
432    };
433    let _ = env.add(scanl_length_decl);
434}
435/// Register Vec.replicate axiom: create a vector of n copies of a value.
436#[allow(dead_code)]
437pub fn register_vec_replicate_axioms(env: &mut Environment) {
438    use oxilean_kernel::{BinderInfo, Declaration, Expr, Level, Name};
439    let type1 = Expr::Sort(Level::succ(Level::zero()));
440    let nat_ty = Expr::Const(Name::str("Nat"), vec![]);
441    let replicate_ty = Expr::Pi(
442        BinderInfo::Implicit,
443        Name::str("α"),
444        Box::new(type1.clone()),
445        Box::new(Expr::Pi(
446            BinderInfo::Default,
447            Name::str("n"),
448            Box::new(nat_ty.clone()),
449            Box::new(Expr::Pi(
450                BinderInfo::Default,
451                Name::str("_x"),
452                Box::new(Expr::BVar(1)),
453                Box::new(Expr::App(
454                    Box::new(Expr::App(
455                        Box::new(Expr::Const(Name::str("Vec"), vec![])),
456                        Box::new(Expr::BVar(2)),
457                    )),
458                    Box::new(Expr::BVar(1)),
459                )),
460            )),
461        )),
462    );
463    let replicate_decl = Declaration::Axiom {
464        name: Name::str("Vec.replicate"),
465        univ_params: vec![],
466        ty: replicate_ty,
467    };
468    let _ = env.add(replicate_decl);
469    let rep_zero_ty = Expr::Pi(
470        BinderInfo::Implicit,
471        Name::str("α"),
472        Box::new(type1.clone()),
473        Box::new(Expr::Pi(
474            BinderInfo::Default,
475            Name::str("_x"),
476            Box::new(Expr::BVar(0)),
477            Box::new(Expr::Const(Name::str("True"), vec![])),
478        )),
479    );
480    let rep_zero_decl = Declaration::Axiom {
481        name: Name::str("Vec.replicate_zero"),
482        univ_params: vec![],
483        ty: rep_zero_ty,
484    };
485    let _ = env.add(rep_zero_decl);
486    let rep_succ_ty = Expr::Pi(
487        BinderInfo::Implicit,
488        Name::str("α"),
489        Box::new(type1.clone()),
490        Box::new(Expr::Pi(
491            BinderInfo::Default,
492            Name::str("n"),
493            Box::new(nat_ty.clone()),
494            Box::new(Expr::Pi(
495                BinderInfo::Default,
496                Name::str("_x"),
497                Box::new(Expr::BVar(1)),
498                Box::new(Expr::Const(Name::str("True"), vec![])),
499            )),
500        )),
501    );
502    let rep_succ_decl = Declaration::Axiom {
503        name: Name::str("Vec.replicate_succ"),
504        univ_params: vec![],
505        ty: rep_succ_ty,
506    };
507    let _ = env.add(rep_succ_decl);
508    let map_rep_ty = Expr::Pi(
509        BinderInfo::Implicit,
510        Name::str("α"),
511        Box::new(type1.clone()),
512        Box::new(Expr::Pi(
513            BinderInfo::Implicit,
514            Name::str("β"),
515            Box::new(type1.clone()),
516            Box::new(Expr::Pi(
517                BinderInfo::Default,
518                Name::str("_f"),
519                Box::new(Expr::Pi(
520                    BinderInfo::Default,
521                    Name::str("_x"),
522                    Box::new(Expr::BVar(1)),
523                    Box::new(Expr::BVar(2)),
524                )),
525                Box::new(Expr::Pi(
526                    BinderInfo::Default,
527                    Name::str("n"),
528                    Box::new(nat_ty.clone()),
529                    Box::new(Expr::Pi(
530                        BinderInfo::Default,
531                        Name::str("_x"),
532                        Box::new(Expr::BVar(3)),
533                        Box::new(Expr::Const(Name::str("True"), vec![])),
534                    )),
535                )),
536            )),
537        )),
538    );
539    let map_rep_decl = Declaration::Axiom {
540        name: Name::str("Vec.map_replicate"),
541        univ_params: vec![],
542        ty: map_rep_ty,
543    };
544    let _ = env.add(map_rep_decl);
545}
546#[cfg(test)]
547mod tests_vec_extended {
548    use super::*;
549    use oxilean_kernel::{Environment, InductiveEnv, Name};
550    #[test]
551    fn test_vec_zip_axioms_registered() {
552        let mut env = Environment::new();
553        let mut ind_env = InductiveEnv::new();
554        let _ = build_vec_env(&mut env, &mut ind_env);
555        register_vec_zip_axioms(&mut env);
556        assert!(env.get(&Name::str("Vec.zip")).is_some());
557        assert!(env.get(&Name::str("Vec.zip_nil")).is_some());
558        assert!(env.get(&Name::str("Vec.zip_length")).is_some());
559    }
560    #[test]
561    fn test_vec_unzip_axioms_registered() {
562        let mut env = Environment::new();
563        let mut ind_env = InductiveEnv::new();
564        let _ = build_vec_env(&mut env, &mut ind_env);
565        register_vec_unzip_axioms(&mut env);
566        assert!(env.get(&Name::str("Vec.unzip")).is_some());
567        assert!(env.get(&Name::str("Vec.zip_unzip")).is_some());
568    }
569    #[test]
570    fn test_vec_fold_axioms_registered() {
571        let mut env = Environment::new();
572        let mut ind_env = InductiveEnv::new();
573        let _ = build_vec_env(&mut env, &mut ind_env);
574        register_vec_fold_axioms(&mut env);
575        assert!(env.get(&Name::str("Vec.foldl")).is_some());
576        assert!(env.get(&Name::str("Vec.foldl_nil")).is_some());
577        assert!(env.get(&Name::str("Vec.foldl_cons")).is_some());
578        assert!(env.get(&Name::str("Vec.foldr")).is_some());
579    }
580    #[test]
581    fn test_vec_predicate_axioms_registered() {
582        let mut env = Environment::new();
583        let mut ind_env = InductiveEnv::new();
584        let _ = build_vec_env(&mut env, &mut ind_env);
585        register_vec_predicate_axioms(&mut env);
586        assert!(env.get(&Name::str("Vec.all")).is_some());
587        assert!(env.get(&Name::str("Vec.any")).is_some());
588        assert!(env.get(&Name::str("Vec.all_true")).is_some());
589    }
590    #[test]
591    fn test_vec_scan_axioms_registered() {
592        let mut env = Environment::new();
593        let mut ind_env = InductiveEnv::new();
594        let _ = build_vec_env(&mut env, &mut ind_env);
595        register_vec_scan_axioms(&mut env);
596        assert!(env.get(&Name::str("Vec.scanl")).is_some());
597        assert!(env.get(&Name::str("Vec.scanl_length")).is_some());
598    }
599    #[test]
600    fn test_vec_replicate_axioms_registered() {
601        let mut env = Environment::new();
602        let mut ind_env = InductiveEnv::new();
603        let _ = build_vec_env(&mut env, &mut ind_env);
604        register_vec_replicate_axioms(&mut env);
605        assert!(env.get(&Name::str("Vec.replicate")).is_some());
606        assert!(env.get(&Name::str("Vec.replicate_zero")).is_some());
607        assert!(env.get(&Name::str("Vec.replicate_succ")).is_some());
608        assert!(env.get(&Name::str("Vec.map_replicate")).is_some());
609    }
610}
oxilean_std/vec/functions_2.rs

oxilean_std/vec/
functions_2.rs
