deptypes/int/
sub.rs

1use crate::{ops::{Add, Sub}, term::{Term, ValueEq}, type_eq::refl};
2
3use super::{add::{a_plus_0_eq_a, a_plus_s_b_eq_s_add_a_b, add_0_a_eq_a, add_associative, add_commutative, add_eq_to_left_eq, s_a_plus_b_eq_s_add_a_b}, succ_eq_to_eq, Int, Succ, Zero};
4
5/// Axiom (definition of subtraction): (a - b) + b = a
6pub fn a_minus_b_plus_b_eq_a<N, A: Term<Type = N>, B: Term<Type = N>>(
7    ) -> ValueEq<Add<Sub<A, B>, B>, A>
8    where N: Int
9{
10    // SAFETY: this is true for mathematical integers and thus for all types that implement Int by the requirements of Int
11    unsafe {ValueEq::axiom()}
12}
13
14/// Theorem: a + (b - c) = (a + b) - c
15pub fn add_sub_associative<N, A: Term<Type = N>, B: Term<Type = N>, C: Term<Type = N>>(
16    ) -> ValueEq<Add<A, Sub<B, C>>, Sub<Add<A, B>, C>>
17    where N: Int
18{
19    // (a + (b - c)) + c = a + ((b - c) + c) = a + b = (a + b)  - c + c
20    let lemma = -add_associative() + Add::eq(refl(), a_minus_b_plus_b_eq_a()) - a_minus_b_plus_b_eq_a();
21
22    add_eq_to_left_eq(lemma, refl())
23}
24
25// a + b - b + b = a + b
26// a + b - b + b - b = a + b - b
27
28/// Theorem: (a + b) - b = a
29#[allow(non_snake_case)]
30pub fn a_plus_b_minus_b_eq_a<N, A: Term<Type = N>, B: Term<Type = N>>(
31    ) -> ValueEq<Sub<Add<A, B>, B>, A>
32    where N: Int
33{
34    // (a + b) - b == a + (b - b) == a + 0 == a
35    //-add_sub_associative() + Add::eq(ValueEq::refl(), a_minus_a_eq_0()) + a_plus_0_eq_a()
36
37    add_eq_to_left_eq(a_minus_b_plus_b_eq_a(), refl())
38}
39
40/// Theorem: a - (b + c) = (a - b) - c
41pub fn sub_add_associative<N, A: Term<Type = N>, B: Term<Type = N>, C: Term<Type = N>>(
42) -> ValueEq<Sub<A, Add<B, C>>, Sub<Sub<A, B>, C>>
43where N: Int
44{
45    // a - (b + c) + (b + c) = a == a - b + b == (((a - b) - c) + c) + b == ((a - b) - c) + (c + b) = ((a - b) - c) + (b + c)
46    let lemma = a_minus_b_plus_b_eq_a() - a_minus_b_plus_b_eq_a() + Add::eq(-a_minus_b_plus_b_eq_a(), refl()) - add_associative() + Add::eq(refl(), add_commutative());
47
48    add_eq_to_left_eq(lemma, refl())
49}
50
51/// Theorem: (a - b) + c = (a + c) - b
52pub fn add_sub_commutative<N, A: Term<Type = N>, B: Term<Type = N>, C: Term<Type = N>>(
53) -> ValueEq<Add<Sub<A, B>, C>, Sub<Add<A, C>, B>>
54where N: Int
55{
56    // ((a - b) + c) + b == (a - b) + (c + b) == (a - b) + (b + c) == ((a - b) + b) + c == a + c == ((a + c) - b) + b
57    let lemma = -add_associative() + Add::eq(refl(), add_commutative()) + add_associative() + Add::eq(a_minus_b_plus_b_eq_a(), refl()) - a_minus_b_plus_b_eq_a();
58
59    add_eq_to_left_eq(lemma, refl())
60}
61
62/// Theorem: a - (b - c) == a + (c - b)
63pub fn a_minus_sub_b_c_eq_a_plus_sub_c_b<N, A: Term<Type = N>, B: Term<Type = N>, C: Term<Type = N>>(
64    ) -> ValueEq<Sub<A, Sub<B, C>>, Add<A, Sub<C, B>>>
65    where N: Int
66{
67    // (a - (b - c)) + ((b - c) + c) == a - (b - c) + (b - c) + c == a + c == a + ((c - b) + b) == (a + (c - b)) + b == a + (c - b) + ((b - c) + c)
68    let lemma = add_associative() + Add::eq(a_minus_b_plus_b_eq_a(), refl()) + Add::eq(refl(), -a_minus_b_plus_b_eq_a()) + add_associative() + Add::eq(refl(), -a_minus_b_plus_b_eq_a());
69
70    add_eq_to_left_eq(lemma, refl())
71}
72
73/// Theorem: a - (b - c) = (a - b) + c
74pub fn sub_sub_associative<N, A: Term<Type = N>, B: Term<Type = N>, C: Term<Type = N>>(
75) -> ValueEq<Sub<A, Sub<B, C>>, Add<Sub<A, B>, C>>
76where N: Int
77{
78    // a - (b - c) == a + (c - b) == (a + c) - b == (a - b) + c
79    a_minus_sub_b_c_eq_a_plus_sub_c_b() + add_sub_associative() - add_sub_commutative()
80}
81
82/// Theorem: a - a = 0
83pub fn a_minus_a_eq_0<N, A: Term<Type = N>>(
84    ) -> ValueEq<Sub<A, A>, Zero<N>>
85    where N: Int
86{
87    // (a - a) + a == a == a + 0 == 0 + a
88    let lemma = a_minus_b_plus_b_eq_a() - a_plus_0_eq_a() + add_commutative();
89
90    add_eq_to_left_eq(lemma, refl())
91}
92
93/// Theorem: a - 0 = a
94pub fn a_minus_0_eq_a<N, A: Term<Type = N>>(
95    ) -> ValueEq<Sub<A, Zero<N>>, A>
96where N: Int
97{
98    // a - 0 + 0 == a == a + 0
99    let lemma = a_minus_b_plus_b_eq_a() - a_plus_0_eq_a();
100
101    add_eq_to_left_eq(lemma, refl())
102}
103
104/// Theorem: S(a) - S(b) = a - b
105pub fn s_a_minus_s_b_eq_a_minus_b<N, A: Term<Type = N>, B: Term<Type = N>>(
106    ) -> ValueEq<Sub<Succ<A>, Succ<B>>, Sub<A, B>>
107    where N: Int
108{
109    // S(S(a) - S(b) + b) == (S(a) - S(b)) + S(b) == S(a)
110    // S(a) - S(b) + b == a
111    let lemma = succ_eq_to_eq(-a_plus_s_b_eq_s_add_a_b() + a_minus_b_plus_b_eq_a());
112
113    // S(a) - S(b) == (S(a) - S(b) + b) - b == a - b
114    -a_plus_b_minus_b_eq_a() + Sub::eq(lemma, refl())
115}
116
117/// Theorem: S(a) - b = S(a - b)
118#[allow(non_snake_case)]
119pub fn s_a_minus_b_eq_s_sub_a_b<N, A: Term<Type = N>, B: Term<Type = N>>(
120    ) -> ValueEq<Sub<Succ<A>, B>, Succ<Sub<A, B>>>
121    where N: Int
122{
123    // S(a - b) + b == S(a - b + b) == S(a)
124    let lemma = s_a_plus_b_eq_s_add_a_b() + Succ::eq(a_minus_b_plus_b_eq_a());
125
126    // S(a) - b == S(a - b) + b - b == S(a - b)
127    -Sub::eq(lemma, refl()) + a_plus_b_minus_b_eq_a()
128}
129
130/// Theorem: S(a) - S(0) = a
131pub fn s_a_minus_s_0_eq_a<N, A: Term<Type = N>>(
132    ) -> ValueEq<Sub<Succ<A>, Succ<Zero<N>>>, A>
133    where N: Int
134{
135    // S(a) - S(0) == a - 0 == a
136    s_a_minus_s_b_eq_a_minus_b() + a_minus_0_eq_a()
137}
138
139/// Theorem: S(a - S(b)) = a - b
140pub fn s_sub_a_s_b_eq_a_minus_b<N, A: Term<Type = N>, B: Term<Type = N>>(
141    ) -> ValueEq<Succ<Sub<A, Succ<B>>>, Sub<A, B>>
142    where N: Int
143{
144    // S(a - S(b)) == S(a) - S(b) == a - b
145    -s_a_minus_b_eq_s_sub_a_b() + s_a_minus_s_b_eq_a_minus_b()
146}
147
148/// Theorem: S(a - S(0)) = a
149pub fn s_sub_a_s_0_eq_a<N, A: Term<Type = N>>(
150    ) -> ValueEq<Succ<Sub<A, Succ<Zero<N>>>>, A>
151    where N: Int
152{
153    // S(a - S(0)) == a - 0 == a
154    s_sub_a_s_b_eq_a_minus_b() + a_minus_0_eq_a()
155}
156
157/// a - c == b - d && c == d => a == b
158pub fn sub_eq_to_left_eq<N, A: Term<Type = N>, B: Term<Type = N>, C: Term<Type = N>, D: Term<Type = N>>(
159    eq: ValueEq<Sub<A, C>, Sub<B, D>>,
160    c_eq_d: ValueEq<C, D>
161    ) -> ValueEq<A, B>
162    where N: Int
163{
164    // a == a - c + c == b - d + d == b
165    -a_minus_b_plus_b_eq_a() + Add::eq(eq, c_eq_d) + a_minus_b_plus_b_eq_a()
166}
167
168/// Theorem: a - (a - b) = b
169pub fn a_minus_sub_a_b_eq_b<N, A: Term<Type = N>, B: Term<Type = N>>(
170) -> ValueEq<Sub<A, Sub<A, B>>, B>
171where N: Int
172{
173    // a - (a - b) = (a - a) + b = 0 + b = b
174    sub_sub_associative() + Add::eq(a_minus_a_eq_0(), refl()) + add_0_a_eq_a()
175}
176
177/// a - c == b - d && a == b => c == d
178pub fn sub_eq_to_right_eq<N, A: Term<Type = N>, B: Term<Type = N>, C: Term<Type = N>, D: Term<Type = N>>(
179    eq: ValueEq<Sub<A, C>, Sub<B, D>>,
180    a_eq_b: ValueEq<A, B>
181    ) -> ValueEq<C, D>
182    where N: Int
183{
184    // c == a - (a - c) == b - (b - d) == d
185    -a_minus_sub_a_b_eq_b() + Sub::eq(a_eq_b, eq) + a_minus_sub_a_b_eq_b()
186}
deptypes/int/sub.rs

deptypes/int/
sub.rs
