prop/fun/
list.rs

1//! List.
2
3use super::*;
4use natp::{FAdd, Nat, Succ, Zero};
5
6/// A list.
7#[derive(Copy, Clone)]
8pub struct FList(());
9
10/// `list(a)`.
11pub type List<A> = App<FList, A>;
12
13/// `head(a)`.
14pub struct Head<A>(A);
15
16/// `tail(a)`.
17pub struct Tail<A>(A);
18
19/// `(a : type(0))  =>  (list : a -> type(0))`.
20pub fn list_ty<A: Prop>(_a_ty: Ty<A, Type<Z>>) -> Ty<FList, Pow<Type<Z>, A>> {unimplemented!()}
21/// `a : list(b)  =>  (a == nil{b}) ⋁ (a == cons{b}(head(a), tail(a)))`.
22pub fn list_def<A: Prop, B: Prop>(
23    _: Ty<A, List<B>>
24) -> Or<Eq<A, Nil<B>>, Eq<A, Cons<B, Head<A>, Tail<A>>>> {
25    unimplemented!()
26}
27/// `(a : list(b)) ⋀ ¬(a == nil{b})  =>  head(a) : b`.
28pub fn head_ty<A: Prop, B: Prop>(_: Ty<A, List<B>>, _: Not<Eq<A, Nil<B>>>) -> Ty<Head<A>, B> {
29    unimplemented!()
30}
31/// `(a : list(b)) ⋀ ¬(a == nil{b})  =>  tail(a) : list(b)`.
32pub fn tail_ty<A: Prop, B: Prop>(
33    _: Ty<A, List<B>>,
34    _: Not<Eq<A, Nil<B>>>
35) -> Ty<Tail<A>, List<B>> {
36    unimplemented!()
37}
38/// `∃ nil{a} : list(a) { x } ⋀ ∃ cons{a}(b, c) : list(a) { x }  =>  x`.
39pub fn list_exists<A: Prop, B: VProp, C: VProp, X: Prop>(
40    _: Exists<Ty<Nil<A>, List<A>>, X>,
41    _: Exists<Ty<Cons<A, B, Nil<A>>, List<A>>, X>
42) -> X {unimplemented!()}
43
44/// An empty list.
45#[derive(Copy, Clone)]
46pub struct FNil(());
47
48/// `nil{a}`.
49pub type Nil<A> = App<FNil, A>;
50
51/// `(a : type(0))  =>  (nil{a} : list(a))`.
52pub fn nil_ty<A: Prop>(_a_ty: Ty<A, Type<Z>>) -> Ty<Nil<A>, List<A>> {unimplemented!()}
53
54/// A non-empty list.
55#[derive(Copy, Clone)]
56pub struct FCons(());
57
58/// `cons{x}(a, b)`.
59pub type Cons<X, A, B> = App<App<FCons, X>, Tup<A, B>>;
60
61/// `a : type(0)  =>  cons{a} : (a, list(a)) -> list(a)`.
62pub fn cons_ty<A: Prop>() -> Ty<App<FCons, A>, Pow<List<A>, Tup<A, List<A>>>> {
63    unimplemented!()
64}
65
66/// List concatenation.
67#[derive(Copy, Clone)]
68pub struct FConcat(());
69
70/// `concat{x}(a, b)`.
71pub type Concat<X, A, B> = App<App<FConcat, X>, Tup<A, B>>;
72
73/// `(a : type(0))  =>  (concat{a} : (list(a), list(a)) -> list(a))`.
74pub fn concat_ty<A: Prop>(
75    _a_ty: Ty<A, Type<Z>>
76) -> Ty<App<FConcat, A>, Pow<List<A>, Tup<List<A>, List<A>>>> {unimplemented!()}
77/// `(nil{x} : list(x)) ⋀ (a : list(x))  =>  concat{x}(nil{x}, a) == a`.
78pub fn concat_nil<X: Prop, A: Prop>(
79    _ty_nil: Ty<Nil<X>, List<X>>,
80    _ty_a: Ty<A, List<X>>
81) -> Eq<Concat<X, Nil<X>, A>, A> {unimplemented!()}
82/// `(cons{x}(a, b) : list(x)) ⋀ (c : list(x))  =>
83///  concat{x}(cons{x}(a, b), c) == cons{x}(a, concat{x}(b, c))`.
84pub fn concat_cons<X: Prop, A: Prop, B: Prop, C: Prop>(
85    _ty_cons: Ty<Cons<X, A, B>, List<X>>,
86    _ty_c: Ty<C, List<X>>
87) -> Eq<Concat<X, Cons<X, A, B>, C>, Cons<X, A, Concat<X, B, C>>> {unimplemented!()}
88/// `concat{x}[len{x}]  == add`.
89pub fn norm1_concat_len<X: Prop>() -> Eq<SymNorm2<App<FConcat, X>, App<FLen, X>>, FAdd> {
90    unimplemented!()
91}
92
93/// Length of list.
94#[derive(Copy, Clone)]
95pub struct FLen(());
96
97/// `len{x}(a)`.
98pub type Len<X, A> = App<App<FLen, X>, A>;
99
100/// `(a : type(0))  =>  (len{a} : list(a) -> nat)`.
101pub fn len_ty<A: Prop>(_a: Ty<A, Type<Z>>) -> Ty<App<FLen, A>, Pow<Nat, List<A>>> {
102    unimplemented!()
103}
104/// `nil{a} : list(a)  =>  len(nil{a}) == 0`.
105pub fn len_nil<A: Prop>(_: Ty<Nil<A>, List<A>>) -> Eq<Len<A, Nil<A>>, Zero> {unimplemented!()}
106/// `cons{x}(a, b) : list(a)  =>  len{x}(cons{x}(a, b)) == succ(len{x}(b))`.
107pub fn len_cons<X: Prop, A: Prop, B: Prop>(
108    _: Ty<Cons<X, A, B>, List<A>>
109) -> Eq<Len<X, Cons<X, A, B>>, Succ<Len<X, B>>> {
110    unimplemented!()
111}
prop/fun/list.rs

prop/fun/
list.rs
