prop/fun/
natc.rs

1//! # Closed natural numbers
2
3//! Closed natural numbers is a theory of natural numbers where 0 is both the first and the last
4//! natural number. For more information, see
5//! [reading sequence about closed natural numbers](https://github.com/advancedresearch/path_semantics/blob/master/sequences.md#closed-natural-numbers).
6//!
7//! Closed natural numbers occur frequently in computer science as modular arithmetic.
8//! The difference between closed natural numbers and modular arithmetic is that in closed natural
9//! numbers, you might have numbers that are infinite.
10//!
11//! For example, an infinite number `1 + 1 + 1 + 1 + ...` does not change identity by adding `1`
12//! in front of it. Now, it is impossible to construct a such number without any assumptions.
13//! However, one can assume that a such number exist with `n ~~ s_c(n)` and then
14//! prove that this number equals 0 ([eq_last_zeroc]).
15//!
16//! Closed natural numbers is a [Robinson arithmetic](https://en.wikipedia.org/wiki/Robinson_arithmetic)
17//! minus the first axiom that 0 is not the successor of any number `(s(x) == 0)  =>  false`,
18//! plus a new axiom describing the closed property of addition ([addc_closed]):
19//!
20//! ```text
21//! (n : nat_c) ⋀ (m : nat_c) ⋀ (n ~~ add_c(s_c(n), m))  =>  (n == m)
22//! ```
23//!
24//! Using symbolic distinction (see [sd]), one can show that it is not possible to construct such
25//! numbers without making assumptions. Symbolic distinction can be used safely to extend logic,
26//! but symbolic indistinction is not safe. Since this axiom implies symbolic distinction,
27//! it is safe to use when reasoning about infinite series.
28
29use super::*;
30
31/// The type of closed natural numbers.
32#[derive(Copy, Clone)]
33pub struct Natc(());
34
35/// `nat_c : type(0)`.
36pub fn natc_ty() -> Ty<Natc, Type<Z>> {unimplemented!()}
37
38/// `n : nat_c  =>  (n == 0_c) ⋁ ∃ m : nat_c { s_c(m) == n }`.
39pub fn natc_def<N: Prop, M: Prop>(
40    _: Ty<N, Natc>
41) -> Or<Eq<N, Zc>, Exists<Ty<M, Natc>, Eq<Sc<M>, N>>> {unimplemented!()}
42
43/// Closed zero.
44#[derive(Copy, Clone)]
45pub struct Zc(());
46
47/// `0_c : nat_c`.
48pub fn zeroc_ty() -> Ty<Zc, Natc> {unimplemented!()}
49
50/// Closed successor function.
51#[derive(Copy, Clone)]
52pub struct FSc(());
53
54/// `s_c(n)`.
55pub type Sc<N> = App<FSc, N>;
56
57/// `s_c : nat_c -> nat_c`.
58pub fn sc_ty() -> Ty<FSc, Pow<Natc, Natc>> {unimplemented!()}
59
60/// `n : nat_c  =>  s_c(n) : nat_c`.
61pub fn sc_def<N: Prop>(_ty_n: Ty<N, Natc>) -> Ty<Sc<N>, Natc> {unimplemented!()}
62
63/// `(s_c(n) == s_c(m))  =>  (n == m)`.
64pub fn sc_eq_rev<N: Prop, M: Prop>(_: Eq<Sc<N>, Sc<M>>) -> Eq<N, M> {unimplemented!()}
65
66/// Closed addition.
67#[derive(Copy, Clone)]
68pub struct FAddc(());
69
70/// `add_c(a, b)`.
71pub type Addc<A, B> = App<FAddc, Tup<A, B>>;
72
73/// `add_c : (nat_c, nat_c) -> nat_c`.
74pub fn addc_ty() -> Ty<FAddc, Pow<Natc, Tup<Natc, Natc>>> {unimplemented!()}
75
76/// `n : nat_c  =>  add_c(n, 0_c) = n`.
77pub fn addc_zeroc<N: Prop>(_ty_n: Ty<N, Natc>) -> Eq<Addc<N, Zc>, N> {unimplemented!()}
78
79/// `(s_c(n) : nat_c) ⋀ (m : nat_c)  =>  add_c(n, s_c(m)) = s_c(add_c(n, m))`.
80pub fn addc_sc<N: Prop, M: Prop>(
81    _ty_sc_n: Ty<Sc<N>, Natc>,
82    _ty_m: Ty<M, Natc>
83) -> Eq<Addc<N, Sc<M>>, Sc<Addc<N, M>>> {unimplemented!()}
84
85/// `(n : nat_c) ⋀ (m : nat_c) ⋀ (n ~~ add_c(s_c(n), m))  =>  (n == m)`.
86pub fn addc_closed<N: Prop, M: Prop>(
87    _ty_n: Ty<N, Natc>,
88    _ty_m: Ty<M, Natc>,
89    _: Q<N, Addc<Sc<N>, M>>
90) -> Eq<N, M> {unimplemented!()}
91
92/// Closed multiplication.
93#[derive(Copy, Clone)]
94pub struct FMulc(());
95
96/// `mul_c(a, b)`.
97pub type Mulc<A, B> = App<FMulc, Tup<A, B>>;
98
99/// `mul_c : (nat_c, nat_c) -> nat_c`.
100pub fn mulc_ty() -> Ty<FMulc, Pow<Natc, Tup<Natc, Natc>>> {unimplemented!()}
101
102/// `n : nat_c  =>  mul_c(n, 0_c) = 0_c`.
103pub fn mulc_zc<N: Prop>(_ty_n: Ty<N, Natc>) -> Eq<Mulc<N, Zc>, Zc> {unimplemented!()}
104
105/// `(n : nat_c) ⋀ (m : nat_c) ⋀ mul_c(n, s_c(m)) = add_c(mul_c(n, m), n)`.
106pub fn mulc_sc<N: Prop, M: Prop>(
107    _ty_n: Ty<N, Natc>,
108    _ty_m: Ty<M, Natc>,
109) -> Eq<Mulc<N, Sc<M>>, Addc<Mulc<N, M>, N>> {unimplemented!()}
110
111/// `(n : nat_c)^true ⋀ (n ~~ s_c(n))  =>  (n == 0_c)`.
112pub fn eq_last_zeroc<N: Prop>(
113    tauto_ty_n: Tauto<Ty<N, Natc>>,
114    theory_x: Q<N, Sc<N>>
115) -> Eq<N, Zc> {
116    fn f<N: Prop>(ty_n: Ty<N, Natc>) -> Eq<Sc<N>, Addc<Sc<N>, Zc>> {
117        eq::symmetry(addc_zeroc(sc_def(ty_n)))
118    }
119    let theory_x = hooo::q_in_right_arg(theory_x, tauto_ty_n.trans(f));
120    addc_closed(tauto_ty_n(True), zeroc_ty(), theory_x)
121}
prop/fun/natc.rs

prop/fun/
natc.rs
