Comment: num_thy_1_summary
Elementary divisibility theory over the integers.
Gcd function and relation introduced. Chinese remainder
theorem proven.
Comment: num_thy_1_intro
Some elementary number theory is developed. Theory
demonstrates rewriter handling multiple equality and
inequality relations over the integers.
The approach taken here is similar to that taken in
the factor_1 theory in the algebra theory collection.
Definition: divides
b | a == ∃c:ℤ. (a = (b * c) ∈ ℤ)
Lemma: divides_wf
∀[a,b:ℤ]. (a | b ∈ ℙ)
Lemma: comb_for_divides_wf
λa,b,z. (a | b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ
Lemma: zero_divs_only_zero
∀[a:ℤ]. a = 0 ∈ ℤ supposing 0 | a
Lemma: one_divs_any
∀a:ℤ. (1 | a)
Lemma: any_divs_zero
∀b:ℤ. (b | 0)
Lemma: divides_invar_1
∀a,b:ℤ. (a | b ⇐⇒ (-a) | b)
Lemma: divides_invar_2
∀a,b:ℤ. (a | b ⇐⇒ a | (-b))
Lemma: divisors_bound
∀[a:ℕ]. ∀[b:ℕ+]. a ≤ b supposing a | b
Lemma: only_pm_one_divs_one
∀b:ℤ. ((b | 1) ⇒ b = ± 1)
Lemma: divides_of_absvals
∀a,b:ℤ. (|a| | |b| ⇐⇒ a | b)
Lemma: absval-divides
∀a,b:ℤ. (|a| | b ⇐⇒ a | b)
Lemma: divides_reflexivity
∀a:ℤ. (a | a)
Lemma: divides_transitivity
∀a,b,c:ℤ. ((a | b) ⇒ (b | c) ⇒ (a | c))
Lemma: divides_preorder
Preorder(ℤ;x,y.x | y)
Lemma: divides_anti_sym_n
∀[a,b:ℕ]. (a = b ∈ ℤ) supposing ((b | a) and (a | b))
Lemma: divides_anti_sym
∀a,b:ℤ. ((a | b) ⇒ (b | a) ⇒ a = ± b)
Lemma: assoc_reln
∀a,b:ℤ. ((a | b) ∧ (b | a) ⇐⇒ a = ± b)
Lemma: divisor_of_sum
∀a,b1,b2:ℤ. ((a | b1) ⇒ (a | b2) ⇒ (a | (b1 + b2)))
Lemma: divisor_of_minus
∀a,b:ℤ. ((a | b) ⇒ (a | (-b)))
Lemma: divisor_of_mul
∀a,b,c:ℤ. ((a | b) ⇒ (a | (b * c)))
Lemma: divides_mul
∀a,b:ℤ. ((a | b) ⇒ (∀n:ℤ. ((n * a) | (n * b))))
Lemma: divides_add
∀x,y,z:ℤ. ((x | y) ⇒ (x | z) ⇒ (x | (y + z)))
Lemma: divides_subtract
∀x,y,z:ℤ. ((x | y) ⇒ (x | z) ⇒ (x | (y - z)))
Lemma: divides_product
∀x,y,z:ℤ. (((x | y) ∨ (x | z)) ⇒ (x | (y * z)))
Lemma: divisor_bound
∀[a:ℕ]. ∀[b:ℕ+]. a ≤ b supposing a | b
Lemma: divides_iff_rem_zero
∀a:ℤ. ∀b:ℤ-o. (b | a ⇐⇒ (a rem b) = 0 ∈ ℤ)
Lemma: divides_iff_div_exact
∀a:ℤ. ∀n:ℤ-o. (n | a ⇐⇒ ((a ÷ n) * n) = a ∈ ℤ)
Lemma: decidable__divides
∀a,b:ℤ. Dec(a | b)
Lemma: decidable__divides_ext
∀a,b:ℤ. Dec(a | b)
Lemma: decidable__exists-divisor
∀n:ℕ+. ∀P:ℕ ⟶ ℙ. ((∀d:ℕ. Dec(P[d])) ⇒ Dec(∃d:ℕ. ((d | n) ∧ P[d])))
Lemma: add-div-when-divides
∀a,b:ℤ. ∀c:ℤ-o. (((a ÷ c) + (b ÷ c)) = ((a + b) ÷ c) ∈ ℤ) supposing ((c | a) and (c | b))
Lemma: add-div-when-divides2
∀a,b,x,y:ℤ. ∀c:ℤ-o. ((((a ÷ c) * x) + ((b ÷ c) * y)) = (((a * x) + (b * y)) ÷ c) ∈ ℤ) supposing ((c | a) and (c | b))
Comment: divides_instance_com
The proof here illustrates how the evaluation
of the extract of one theorem (decidable__divides)
can help to prove another theorem.
For neatness, the pattern of proof here could easily
be incorporated into a tactic.
Lemma: divides_instance
3 | 6
Lemma: orbit-size-divides-order
∀[T:Type]. ∀f:T ⟶ T. ∀n:ℕ. ∀L:T List. ||L|| | n supposing orbit(T;f;L) supposing ∀x:T. ((f^n x) = x ∈ T)
Comment: gcd_p_com
Should redo this not using uncurried antecedents.
Makes forward chaining a lot easier.
Definition: assoced
a ~ b == (a | b) ∧ (b | a)
Lemma: assoced_wf
∀[a,b:ℤ]. (a ~ b ∈ ℙ)
Lemma: comb_for_assoced_wf
λa,b,z. (a ~ b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ
Lemma: assoced_equiv_rel
EquivRel(ℤ;x,y.x ~ y)
Lemma: decidable__assoced
∀a,b:ℤ. Dec(a ~ b)
Lemma: divides_functionality_wrt_assoced
∀a,a',b,b':ℤ. ((a ~ a') ⇒ (b ~ b') ⇒ (a | b ⇐⇒ a' | b'))
Lemma: divides_weakening
∀a,b:ℤ. ((a ~ b) ⇒ (a | b))
Lemma: assoced_weakening
∀a,b:ℤ. a ~ b supposing a = b ∈ ℤ
Lemma: assoced_transitivity
∀a,b,c:ℤ. ((a ~ b) ⇒ (b ~ c) ⇒ (a ~ c))
Lemma: multiply_functionality_wrt_assoced
∀a,a',b,b':ℤ. ((a ~ a') ⇒ (b ~ b') ⇒ ((a * b) ~ (a' * b')))
Lemma: assoced_inversion
∀a,b:ℤ. ((a ~ b) ⇒ (b ~ a))
Lemma: assoced_functionality_wrt_assoced
∀a,b,a',b':ℤ. ((a ~ a') ⇒ (b ~ b') ⇒ (a ~ b ⇐⇒ a' ~ b'))
Lemma: assoced_elim
∀a,b:ℤ. (a ~ b ⇐⇒ (a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ))
Lemma: mul_cancel_in_assoced
∀a,b:ℤ. ∀n:ℤ-o. (((n * a) ~ (n * b)) ⇒ (a ~ b))
Lemma: neg_assoced
∀a:ℤ. ((-a) ~ a)
Lemma: absval_assoced
∀a:ℤ. (|a| ~ a)
Lemma: unit_chars
∀a:ℤ. (a | 1 ⇐⇒ a ~ 1)
Lemma: assoced_nelim
∀a,b:ℕ. (a ~ b ⇐⇒ a = b ∈ ℤ)
Lemma: pdivisor_bound
∀a:ℕ. ∀b:ℕ+. ((a | b) ∧ (¬(b | a)) ⇐⇒ a < b ∧ (a | b))
Lemma: divides_nchar
∀a,b:ℕ+. (a | b ⇐⇒ ∃c:ℕ+. (b = (a * c) ∈ ℕ+))
Definition: gcd_p
GCD(a;b;y) == (y | a) ∧ (y | b) ∧ (∀z:ℤ. (((z | a) ∧ (z | b)) ⇒ (z | y)))
Lemma: gcd_p_wf
∀[a,b,y:ℤ]. (GCD(a;b;y) ∈ ℙ)
Lemma: comb_for_gcd_p_wf
λa,b,y,z. GCD(a;b;y) ∈ a:ℤ ⟶ b:ℤ ⟶ y:ℤ ⟶ (↓True) ⟶ ℙ
Lemma: gcd_p_functionality_wrt_assoced
∀a,a',b,b',y,y':ℤ. ((a ~ a') ⇒ (b ~ b') ⇒ (y ~ y') ⇒ (GCD(a;b;y) ⇐⇒ GCD(a';b';y')))
Lemma: gcd_p_eq_args
∀a:ℤ. GCD(a;a;a)
Lemma: gcd_p_zero
∀a:ℤ. GCD(a;0;a)
Lemma: gcd_p_one
∀a:ℤ. GCD(a;1;1)
Lemma: gcd_p_zero_rel
∀a,b:ℤ. (GCD(a;0;b) ⇒ ((a = b ∈ ℤ) ∨ (a = (-b) ∈ ℤ)))
Lemma: gcd_p_sym
∀a,b,y:ℤ. (GCD(a;b;y) ⇒ GCD(b;a;y))
Lemma: gcd_p_sym_a
∀a,b,y:ℤ. (GCD(a;b;y) ⇒ GCD(b;a;y))
Lemma: gcd_p_neg_arg
∀a,b,y:ℤ. (GCD(a;b;y) ⇒ GCD(a;-b;y))
Lemma: gcd_p_neg_arg_a
∀a,b,y:ℤ. (GCD(a;b;y) ⇒ GCD(-a;b;y))
Lemma: gcd_p_neg_arg_2
∀a,b,y:ℤ. (GCD(a;b;y) ⇐⇒ GCD(a;-b;y))
Lemma: gcd_p_shift
∀a,b,y,k:ℤ. (GCD(a;b;y) ⇒ GCD(a;b + (k * a);y))
Lemma: gcd_unique
∀a,b,y1,y2:ℤ. (GCD(a;b;y1) ⇒ GCD(a;b;y2) ⇒ (y1 ~ y2))
Lemma: gcd_of_triple
∀a,b,c,x,y:ℤ.
(GCD(a;b;x) ⇒ GCD(x;c;y) ⇒ (((y | a) ∧ (y | b) ∧ (y | c)) ∧ (∀z:ℤ. ((z | a) ⇒ (z | b) ⇒ (z | c) ⇒ (z | y)))))
Lemma: gcd_sat_gcd_p
∀a,b:ℤ. GCD(a;b;gcd(a;b))
Lemma: gcd_sat_pred
∀a,b:ℤ. GCD(a;b;gcd(a;b))
Lemma: gcd_elim
∀a,b:ℤ. ∃y:ℤ. (GCD(a;b;y) ∧ (gcd(a;b) = y ∈ ℤ))
Lemma: gcd_sym
∀a,b:ℤ. (gcd(a;b) ~ gcd(b;a))
Lemma: gcd_eq_args
∀a:ℤ. (gcd(a;a) ~ a)
Lemma: gcd_is_divisor_1
∀a,b:ℤ. (gcd(a;b) | a)
Lemma: gcd_is_divisor_2
∀a,b:ℤ. (gcd(a;b) | b)
Lemma: gcd_is_gcd
∀a,b,c:ℤ. ((c | a) ⇒ (c | b) ⇒ (c | gcd(a;b)))
Lemma: gcd_properties
∀a,b:ℤ. (((gcd(a;b) | a) ∧ (gcd(a;b) | b)) ∧ (∀c:ℤ. ((c | a) ⇒ (c | b) ⇒ (c | gcd(a;b)))))
Comment: quot_rem_exists_com
The q and r computed by the extracts of these theorems are
not the same as those returned by the divides(a;b) and
remainder(a;b) built-in arithmetic functions: with those
functions, the sign of r follows the sign of a and div
has simple symmetry properties. Here, things are set up
so that the same inequalities for r are satisfied over
2 adjacent quadrants of a,b: r is closer to the `mod'
function. This makes the gcd_exists and bezout_ident_
theorems simpler to prove, since two quadrants can be
easily taken care of on the first induction.
Lemma: quot_rem_exists_n
∀a:ℕ. ∀b:ℕ+. ∃q:ℕ. ∃r:ℕb. (a = ((q * b) + r) ∈ ℤ)
Lemma: quot_rem_exists
∀a:ℤ. ∀b:ℕ+. ∃q:ℤ. ∃r:ℕb. (a = ((q * b) + r) ∈ ℤ)
Lemma: gcd_exists_n
∀b:ℕ. ∀a:ℤ. ∃y:ℤ. GCD(a;b;y)
Lemma: gcd_ex_n
∀b:ℕ. ∀a:ℤ. (∃y:ℤ [GCD(a;b;y)])
Lemma: gcd_exists
∀a,b:ℤ. ∃y:ℤ. GCD(a;b;y)
Lemma: bezout_ident_n
∀b:ℕ. ∀a:ℤ. ∃u,v:ℤ. GCD(a;b;(u * a) + (v * b))
Lemma: bezout_ident
∀a,b:ℤ. ∃u,v:ℤ. GCD(a;b;(u * a) + (v * b))
Lemma: gcd_p_mul
∀a,b,y,n:ℤ. (GCD(a;b;y) ⇒ GCD(n * a;n * b;n * y))
Lemma: gcd_mul
∀a,b,n:ℤ. ((n * gcd(a;b)) ~ gcd(n * a;n * b))
Lemma: gcd_assoc
∀a,b,c:ℤ. (gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c)))
Definition: coprime
CoPrime(a,b) == GCD(a;b;1)
Lemma: coprime_wf
∀[a,b:ℤ]. (CoPrime(a,b) ∈ ℙ)
Lemma: coprime_inversion
∀a,b:ℤ. (CoPrime(a,b) ⇐⇒ CoPrime(b,a))
Lemma: comb_for_coprime_wf
λa,b,z. CoPrime(a,b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ
Lemma: sq_stable__coprime
∀i,j:ℤ. SqStable(CoPrime(i,j))
Comment: prime_com
We follow a more abstract characterization of primeness here,
defining separately notions of primeness and irreducibility.
See algebra/factor_1 theory for more details of this.
Approach here to dealing with 0 in lemmas and definitions has
been a bit ad-hoc. Is there something more principled that
could be done?
Definition: reducible
reducible(a) == ∃b,c:ℤ-o. ((¬(b ~ 1)) ∧ (¬(c ~ 1)) ∧ (a = (b * c) ∈ ℤ))
Lemma: reducible_wf
∀[a:ℤ]. (reducible(a) ∈ ℙ)
Definition: atomic
atomic(a) == (¬(a = 0 ∈ ℤ)) ∧ (¬(a ~ 1)) ∧ (¬reducible(a))
Lemma: atomic_wf
∀[a:ℤ]. (atomic(a) ∈ ℙ)
Comment: atomic_char_com
This theorem was quite tedious to prove.
Could the proof be simpler?
7/7/98 Proof changed to avoid use of
sq_stable_iff_stable which has inappropriate
use of Xmiddle. The first tactic proving the first
subgoal was modified. See theory not_good for old
proof.
Lemma: atomic_char
∀a:ℤ. (atomic(a) ⇐⇒ {(¬(a ~ 1)) ∧ (∀b:ℤ. ((b | a) ⇒ ((b ~ 1) ∨ (b ~ a))))})
Definition: prime
prime(a) == (¬(a = 0 ∈ ℤ)) ∧ (¬(a ~ 1)) ∧ (∀b,c:ℤ. ((a | (b * c)) ⇒ ((a | b) ∨ (a | c))))
Lemma: prime_wf
∀[a:ℤ]. (prime(a) ∈ ℙ)
Lemma: self_divisor_mul
∀a:ℤ-o. ∀b:ℤ. (((a * b) | a) ⇒ (b ~ 1))
Lemma: prime_imp_atomic
∀[a:ℤ]. atomic(a) supposing prime(a)
Lemma: prime_elim
∀p:ℤ. (prime(p) ⇒ ((¬(p = 0 ∈ ℤ)) ∧ (¬(p ~ 1)) ∧ (∀a:ℤ. ((a | p) ⇒ ((a ~ 1) ∨ (a ~ p))))))
Lemma: assoced-prime
∀p,q:ℤ. ((p ~ q) ⇒ prime(p) ⇒ prime(q))
Lemma: prime-mul
∀x,y:ℤ. (prime(x * y) ⇒ ((x ~ 1) ∨ (y ~ 1)))
Lemma: prime-mult
∀n:{2...}. ∀x:ℤ. (prime(n * x) ⇒ (prime(n) ∧ (x ~ 1)))
Lemma: not-prime-mult
∀[n,m:{2...}]. ∀[x:ℤ]. (¬prime((n * m) * x))
Lemma: not-prime-square
∀[x:ℤ]. (¬prime(x * x))
Lemma: coprime_intro
∀a,b:ℤ. ((∀c:ℤ. ((c | a) ⇒ (c | b) ⇒ (c | 1))) ⇒ CoPrime(a,b))
Lemma: coprime_elim
∀a,b:ℤ. (CoPrime(a,b) ⇐⇒ ∀c:ℤ. ((c | a) ⇒ (c | b) ⇒ (c ~ 1)))
Lemma: coprime_elim_a
∀a,b:ℤ. (CoPrime(a,b) ⇐⇒ gcd(a;b) ~ 1)
Lemma: coprime_iff_ndivides
∀a,p:ℤ. (prime(p) ⇒ (CoPrime(p,a) ⇐⇒ ¬(p | a)))
Lemma: coprime_bezout_id0
∀a,b:ℤ. (CoPrime(a,b) ⇒ (∃x,y:ℤ. (((a * x) + (b * y)) ~ 1)))
Lemma: coprime_bezout_id1
∀a,b:ℤ. (CoPrime(a,b) ⇒ (∃x,y:ℤ. (((a * x) + (b * y)) = 1 ∈ ℤ)))
Lemma: coprime_bezout_id2
∀a,b:ℤ. ((∃x,y:ℤ. (((a * x) + (b * y)) = 1 ∈ ℤ)) ⇒ CoPrime(a,b))
Lemma: coprime_bezout_id
∀a,b:ℤ. (CoPrime(a,b) ⇐⇒ ∃x,y:ℤ. (((a * x) + (b * y)) = 1 ∈ ℤ))
Lemma: coprime_prod
∀a,b1,b2:ℤ. (CoPrime(a,b1) ⇒ CoPrime(a,b2) ⇒ CoPrime(a,b1 * b2))
Lemma: coprime-exp1
∀a,b:ℤ. (CoPrime(a,b) ⇒ (∀n:ℕ. CoPrime(a,b^n)))
Lemma: coprime_divisors_prod
∀a1,a2,b:ℤ. (CoPrime(a1,a2) ⇒ (a1 | b) ⇒ (a2 | b) ⇒ ((a1 * a2) | b))
Lemma: coprime_divides_prod
∀a1,a2,b:ℤ. ((b | (a1 * a2)) ⇒ CoPrime(b,a1) ⇒ (b | a2))
Lemma: atomic_imp_prime
∀a:ℤ. prime(a) supposing atomic(a)
Lemma: prime_divs_prod
∀p:ℤ. (prime(p) ⇒ (∀a1,a2:ℤ. ((p | (a1 * a2)) ⇒ ((p | a1) ∨ (p | a2)))))
Lemma: decidable__reducible
∀n:ℕ. Dec(reducible(n))
Lemma: decidable__prime
∀n:ℕ. Dec(prime(n))
Lemma: mul_assoc
∀[a,b,c:ℤ]. ((a * b * c) = ((a * b) * c) ∈ ℤ)
Definition: eqmod
a ≡ b mod m == m | (a - b)
Lemma: eqmod_wf
∀[m,a,b:ℤ]. (a ≡ b mod m ∈ ℙ)
Lemma: rem-eqmod
∀a:ℤ. ∀m:ℤ-o. ((a rem m) ≡ a mod m)
Lemma: decidable__eqmod
∀m,a,b:ℤ. Dec(a ≡ b mod m)
Lemma: sq_stable__eqmod
∀m,a,b:ℤ. SqStable(a ≡ b mod m)
Lemma: comb_for_eqmod_wf
λm,a,b,z. (a ≡ b mod m) ∈ m:ℤ ⟶ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℙ
Lemma: eqmod_weakening
∀m,a,b:ℤ. a ≡ b mod m supposing a = b ∈ ℤ
Lemma: eqmod_refl
∀m,a:ℤ. (a ≡ a mod m)
Lemma: eqmod_transitivity
∀m,a,b,c:ℤ. ((a ≡ b mod m) ⇒ (b ≡ c mod m) ⇒ (a ≡ c mod m))
Lemma: eqmod_inversion
∀m,a,b:ℤ. ((a ≡ b mod m) ⇒ (b ≡ a mod m))
Lemma: eqmod-eqmod-div
∀m,m',a,a',b,b':ℤ. ((m' | m) ⇒ (a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ (a ≡ b mod m' ⇐⇒ a' ≡ b' mod m'))
Lemma: eqmod-divides-implies
∀m,m':ℤ. ((m' | m) ⇒ {∀a,b:ℤ. ((a ≡ b mod m) ⇒ (a ≡ b mod m'))})
Lemma: eqmod_functionality_wrt_eqmod
∀m,m',a,a',b,b':ℤ. (a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ (a ≡ b mod m ⇐⇒ a' ≡ b' mod m') supposing m = m' ∈ ℤ
Lemma: eqmod_fun
∀m,a,a',b,b':ℤ. ((a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ (a ≡ b mod m ⇐⇒ a' ≡ b' mod m))
Lemma: eqmod_equiv_rel
∀n:ℤ. EquivRel(ℤ;x,y.x ≡ y mod n)
Lemma: eqmod-zero
∀m:ℤ. (m ≡ 0 mod m)
Lemma: add_functionality_wrt_eqmod
∀m,a,a',b,b':ℤ. ((a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ ((a + b) ≡ (a' + b') mod m))
Lemma: add_reduce_eqmod
∀m,x,y:ℤ. ((x + y) ≡ x mod m ⇐⇒ y ≡ 0 mod m)
Lemma: add_eqmod_zero
∀m,x,y:ℤ. ((x ≡ 0 mod m) ⇒ (y ≡ 0 mod m) ⇒ ((x + y) ≡ 0 mod m))
Lemma: minus_functionality_wrt_eqmod
∀m,a,a':ℤ. ((a ≡ a' mod m) ⇒ ((-a) ≡ (-a') mod m))
Lemma: subtract-elim
∀[x,y:ℤ]. (x - y ~ x + (-y))
Lemma: subtract_functionality_wrt_eqmod
∀m,a,a',b,b':ℤ. ((a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ ((a - b) ≡ (a' - b') mod m))
Lemma: multiply_functionality_wrt_eqmod
∀m,a,a',b,b':ℤ. ((a ≡ a' mod m) ⇒ (b ≡ b' mod m) ⇒ ((a * b) ≡ (a' * b') mod m))
Lemma: small-eqmod
∀m:ℕ+. ∀a:ℤ. ∃b:ℤ. (((2 * |b|) ≤ m) ∧ (b ≡ a mod m))
Lemma: multiply_eqmod_zero_left
∀m,x,y:ℤ. ((x ≡ 0 mod m) ⇒ ((x * y) ≡ 0 mod m))
Lemma: gcd_functionality_wrt_eqmod
∀a,a',m:ℤ. ((a' ≡ a mod m) ⇒ (gcd(a';m) ~ gcd(a;m)))
Lemma: coprime_functionality_wrt_eqmod
∀a,a',m:ℤ. ((a' ≡ a mod m) ⇒ (CoPrime(a',m) ⇐⇒ CoPrime(a,m)))
Lemma: coprime_functionality_wrt_eqmod2
∀a,a',m:ℤ. ((a' ≡ a mod m) ⇒ (CoPrime(m,a') ⇐⇒ CoPrime(m,a)))
Lemma: eqmod_cancellation
∀m,x,a,b:ℤ. (CoPrime(x,m) ⇒ ((x * a) ≡ (x * b) mod m) ⇒ (a ≡ b mod m))
Lemma: product-eq-0-mod-prime
∀p,a,b:ℤ. (prime(p) ⇒ ((a * b) ≡ 0 mod p) ⇒ ((a ≡ 0 mod p) ∨ (b ≡ 0 mod p)))
Lemma: modulus-idempotent
∀x:ℤ. ∀m:ℕ+. (((x mod m) mod m) = (x mod m) ∈ ℤ)
Lemma: modulus-equal
∀x,y:ℤ. ∀m:ℕ+. ((x mod m) = (y mod m) ∈ ℤ ⇐⇒ m | (x - y))
Lemma: modulus-equal-iff-eqmod
∀x,y:ℤ. ∀m:ℕ+. ((x mod m) = (y mod m) ∈ ℤ ⇐⇒ x ≡ y mod m)
Lemma: mod-eqmod
∀x:ℤ. ∀m:ℕ+. ((x mod m) ≡ x mod m)
Lemma: modulus_functionality_wrt_eqmod
∀[m:ℕ+]. ∀[x,y:ℤ]. (x mod m) = (y mod m) ∈ ℤ supposing x ≡ y mod m
Lemma: add-one-mod-2
∀[x:ℤ]. (((x + 1) mod 2) = (1 - x mod 2) ∈ ℤ)
Lemma: impossible-equation-by-eqmod
∀[x,z,a:ℤ]. (¬(((27 * x) + (z + z) + (3 * x * z) + z) = (1 + (999 * a)) ∈ ℤ))
Definition: isOdd
isOdd(n) == (n mod 2 =z 1)
Lemma: isOdd_wf
∀[n:ℤ]. (isOdd(n) ∈ 𝔹)
Definition: isEven
isEven(n) == (n mod 2 =z 0)
Lemma: isEven_wf
∀[n:ℤ]. (isEven(n) ∈ 𝔹)
Lemma: assert-isOdd
∀n:ℤ. (↑isOdd(n) ⇐⇒ ∃k:ℤ. (n = ((2 * k) + 1) ∈ ℤ))
Lemma: isOdd-2n+1
∀n:ℤ. (isOdd((2 * n) + 1) ~ tt)
Lemma: assert-isEven
∀n:ℤ. (↑isEven(n) ⇐⇒ ∃k:ℤ. (n = (2 * k) ∈ ℤ))
Lemma: isEven-2n
∀n:ℤ. (isEven(2 * n) ~ tt)
Lemma: rem-zero-implies-minus
∀x:ℤ. ∀y:ℤ-o. (((x rem y) = 0 ∈ ℤ) ⇒ ((-x rem y) = 0 ∈ ℤ))
Lemma: not-even-succ-implies-even
∀n:ℤ. ((¬↑isEven(n + 1)) ⇒ (↑isEven(n)))
Lemma: even-succ-implies-not-even
∀n:ℤ. ((↑isEven(n + 1)) ⇒ (¬↑isEven(n)))
Lemma: even-implies-two-times
∀n:ℕ. ((↑isEven(n)) ⇒ (∃k:ℕ. (n = (2 * k) ∈ ℤ)))
Lemma: odd-implies-succ-two-times
∀n:ℕ. ((↑isOdd(n)) ⇒ (∃k:ℕ. (n = ((2 * k) + 1) ∈ ℤ)))
Lemma: odd-or-even
∀n:ℤ. (↑(isOdd(n) ∨bisEven(n)))
Lemma: odd-implies
∀n:ℤ. ((↑isOdd(n)) ⇒ {((↑isEven(n - 1)) ∧ (¬↑isEven(n))) ∧ (↑isEven(n + 1))})
Lemma: even-implies
∀n:ℤ. ((↑isEven(n)) ⇒ {((↑isOdd(n - 1)) ∧ (¬↑isOdd(n))) ∧ (↑isOdd(n + 1))})
Lemma: even-iff-not-odd
∀[n:ℤ]. uiff(↑isEven(n);¬↑isOdd(n))
Lemma: odd-iff-not-even
∀[n:ℤ]. uiff(↑isOdd(n);¬↑isEven(n))
Lemma: small-eqmod-odd
∀m:ℕ+. ((↑isOdd(m)) ⇒ (∀a:ℤ. ∃b:ℤ. (2 * |b| < m ∧ (b ≡ a mod m))))
Definition: same-parity
same-parity(n;m) == if isEven(n) then isEven(m) else isOdd(m) fi
Lemma: same-parity_wf
∀[n,m:ℤ]. (same-parity(n;m) ∈ 𝔹)
Lemma: same-parity-implies
∀[n,m:ℤ]. ((↑same-parity(n;m)) ⇒ {(¬↑same-parity(n;m - 1)) ∧ (¬↑same-parity(n;m + 1))})
Lemma: not-same-parity-implies
∀[n,m:ℤ]. ((¬↑same-parity(n;m)) ⇒ {(↑same-parity(n;m - 1)) ∧ (↑same-parity(n;m + 1))})
Lemma: same-parity-implies-even-odd
∀n,m:ℤ. ((↑same-parity(n;m)) ⇒ (((↑isEven(n)) ∧ (↑isEven(m))) ∨ ((↑isOdd(n)) ∧ (↑isOdd(m)))))
Lemma: not-same-parity-implies-even-odd
∀n,m:ℤ. ((¬↑same-parity(n;m)) ⇒ (((↑isEven(n)) ∧ (↑isOdd(m))) ∨ ((↑isOdd(n)) ∧ (↑isEven(m)))))
Lemma: isOdd-isEven-add
∀[n,m:ℤ]. (uiff(↑isOdd(n + m);¬↑same-parity(n;m)) ∧ uiff(↑isEven(n + m);↑same-parity(n;m)))
Lemma: isEven-add
∀[n,m:ℤ]. uiff(↑isEven(n + m);↑same-parity(n;m))
Lemma: isOdd-add
∀[n,m:ℤ]. uiff(↑isOdd(n + m);¬↑same-parity(n;m))
Lemma: odd-plus-even
∀[n,m:ℤ]. ↑isOdd(n + m) supposing (↑isOdd(n)) ∧ (↑isEven(m))
Lemma: odd-plus-odd
∀[n,m:ℤ]. ↑isEven(n + m) supposing (↑isOdd(n)) ∧ (↑isOdd(m))
Lemma: even-plus-odd
∀[n,m:ℤ]. ↑isOdd(n + m) supposing (↑isOdd(m)) ∧ (↑isEven(n))
Lemma: even-plus-even
∀[n,m:ℤ]. ↑isEven(n + m) supposing (↑isEven(m)) ∧ (↑isEven(n))
Lemma: isOdd-sum
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. uiff(↑isOdd(Σ(f[x] | x < n));↑isOdd(||filter(λx.isOdd(f[x]);upto(n))||))
Lemma: isEven-sum
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. uiff(↑isEven(Σ(f[x] | x < n));↑isEven(||filter(λx.isOdd(f[x]);upto(n))||))
Lemma: lsum-of-even
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)} ⟶ ℤ]. ↑isEven(Σ(f[x] | x ∈ L)) supposing (∀x∈L.↑isEven(f[x]))
Lemma: odd-lsum-of-odd
∀[T:Type]. ∀[L:T List].
∀[f:{x:T| (x ∈ L)} ⟶ ℤ]. ↑isOdd(Σ(f[x] | x ∈ L)) supposing (∀x∈L.↑isOdd(f[x])) supposing ↑isOdd(||L||)
Lemma: odd-l_sum
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)} ⟶ ℤ]. uiff(↑isOdd(l_sum(map(f;L)));↑isOdd(||filter(λx.isOdd(f x);L)||))
Lemma: all-even-implies-sum-even
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ↑isEven(Σ(f[x] | x < n)) supposing ∀x:ℕn. (↑isEven(f[x]))
Comment: chrem_com
Here is the existential half of the chinese remainder theorem for
pairs of integers.
Missing is the proof of uniqueness mod (r * s)
Theorems with _a extensions are proved with extraction in mind.
Lemma: chrem_exists_aux
∀r,s:ℕ+. (CoPrime(r,s) ⇒ (∃x:ℤ. ((x ≡ 1 mod r) ∧ (x ≡ 0 mod s))))
Lemma: chrem_exists_aux_a
∀r:ℕ+. ∀s:{s':ℕ+| CoPrime(r,s')} . (∃x:ℤ [((x ≡ 1 mod r) ∧ (x ≡ 0 mod s))])
Lemma: chrem_exists
∀r,s:ℕ+. (CoPrime(r,s) ⇒ (∀a,b:ℤ. ∃x:ℤ. ((x ≡ a mod r) ∧ (x ≡ b mod s))))
Lemma: chrem_exists_a
∀r:ℕ+. ∀s:{s':ℕ+| CoPrime(r,s')} . ∀a,b:ℤ. (∃x:ℤ [((x ≡ a mod r) ∧ (x ≡ b mod s))])
Definition: fib
fib(n) == fix((λfib,n. if (n =z 0) ∨b(n =z 1) then 1 else (fib (n - 1)) + (fib (n - 2)) fi )) n
Lemma: fib_wf
∀[n:ℕ]. (fib(n) ∈ ℕ)
Lemma: comb_for_fib_wf
λn,z. fib(n) ∈ n:ℕ ⟶ (↓True) ⟶ ℕ
Lemma: fib_coprime
∀n:ℕ. CoPrime(fib(n),fib(n + 1))
Lemma: fib-exists
∀n:ℕ. (∃m:ℕ [(m = fib(n) ∈ ℕ)])
Lemma: fast-fib
∀n:ℕ. (∃m:ℕ [(m = fib(n) ∈ ℕ)])
Lemma: fast-fib-ext
∀n:ℕ. (∃m:ℕ [(m = fib(n) ∈ ℕ)])
Definition: fastfib
fastfib(n) == TERMOF{fast-fib-ext:o, 1:l} n
Lemma: less-fast-fib
∀n:ℕ. {m:ℕ| m = fib(n) ∈ ℕ}
Lemma: less-fast-fib-ext
∀n:ℕ. {m:ℕ| m = fib(n) ∈ ℕ}
Lemma: assert-pushdownC-test
∀a,b,c:ℤ.
((↑(((a =z c) ∧b c <z b) ∧b (¬b((a =z b) ∨b(b + 2 =z c)))))
⇒ {(¬(a = b ∈ ℤ)) ∧ (¬((b + 2) = c ∈ ℤ)) ∧ c < b ∧ (a = c ∈ ℤ)})
Definition: slowfib
slowfib(n) == TERMOF{less-fast-fib-ext:o, 1:l} n
Definition: genfact
genfact(n;b;m.f[m]) ==
if (n) < (1) then b else eval x = f[n] in eval b' = b * x in eval n' = n - 1 in genfact(n';b';m.f[m])
Lemma: genfact_wf
∀[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ]. (genfact(n;b;m.f[m]) ∈ ℤ)
Lemma: genfact-base-linear
∀[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ]. (genfact(n;b;m.f[m]) = (b * genfact(n;1;m.f[m])) ∈ ℤ)
Lemma: genfact-step
∀[n:ℤ]. ∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℤ]. (genfact(n;b;m.f[m]) = if n <z 1 then b else f[n] * genfact(n - 1;b;m.f[m]) fi ∈ ℤ)
Lemma: genfact-unbounded
∀f:ℕ+ ⟶ ℤ. ∀b:ℕ+. ∀N:ℤ. (∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]) supposing ∀m:ℕ+. 1 < f[m]
Lemma: genfact-unbounded-ext
∀f:ℕ+ ⟶ ℤ. ∀b:ℕ+. ∀N:ℤ. (∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]) supposing ∀m:ℕ+. 1 < f[m]
Definition: genfact-inv
genfact-inv(N;b;m.f[m]) ==
eval M = N in
letrec g(k)=λx.if (x) < (M) then eval k' = k + 1 in eval z = f[k'] in eval x' = z * x in g k' x' else k in g(0) b
Lemma: genfact-inv_wf
∀[f:ℕ+ ⟶ ℤ]. ∀[b:ℕ+]. ∀[N:ℤ]. (genfact-inv(N;b;m.f[m]) ∈ {n:ℕ| N ≤ genfact(n;b;m.f[m])} ) supposing ∀m:ℕ+. 1 < f[m]
Lemma: exp-as-genfact
∀[x:ℤ]. ∀[n:ℕ]. (x^n ~ genfact(n;1;m.x))
Lemma: exp_functionality_wrt_eqmod
∀m,i,j:ℤ. ((i ≡ j mod m) ⇒ (∀n:ℕ. (i^n ≡ j^n mod m)))
Lemma: cube-mod-9
∀n:ℤ. ((n^3 ≡ 0 mod 9) ∨ (n^3 ≡ 1 mod 9) ∨ (n^3 ≡ (-1) mod 9))
Lemma: three-cubes-mod-9
∀a,b,c,k:ℤ. (((a^3 + b^3 + c^3) = k ∈ ℤ) ⇒ ((¬(k ≡ 4 mod 9)) ∧ (¬(k ≡ 5 mod 9))))
Lemma: three-cubes-3-mod-9
∀a,b,c,k:ℤ. (((a^3 + b^3 + c^3) = k ∈ ℤ) ⇒ (k ≡ 3 mod 9) ⇒ ((a^3 ≡ 1 mod 9) ∧ (b^3 ≡ 1 mod 9) ∧ (c^3 ≡ 1 mod 9)))
Lemma: three-cubes-6-mod-9
∀a,b,c,k:ℤ.
(((a^3 + b^3 + c^3) = k ∈ ℤ) ⇒ (k ≡ 6 mod 9) ⇒ ((a^3 ≡ (-1) mod 9) ∧ (b^3 ≡ (-1) mod 9) ∧ (c^3 ≡ (-1) mod 9)))
Lemma: exp-of-mul
∀[x,y:ℤ]. ∀[n:ℕ]. ((x * y)^n = (x^n * y^n) ∈ ℤ)
Lemma: exp-divides
∀x,y:ℤ. ((x | y) ⇒ (∀n:ℕ. (x^n | y^n)))
Lemma: exp-one
∀[n:ℕ]. (1^n = 1 ∈ ℤ)
Lemma: exp-zero
∀[n:ℕ+]. (0^n = 0 ∈ ℤ)
Lemma: exp_mul
∀[i:ℤ]. ∀[n,m:ℕ]. (i^(m * n) = i^m^n ∈ ℤ)
Lemma: exp_preserves_le
∀[n,x,y:ℕ]. x^n ≤ y^n supposing x ≤ y
Lemma: exp_preserves_lt
∀[n:ℕ+]. ∀[x,y:ℕ]. x^n < y^n supposing x < y
Lemma: exp-le-iff
∀[n:ℕ+]. ∀[x,y:ℕ]. uiff(x ≤ y;x^n ≤ y^n)
Lemma: exp-greater
∀[x:{2...}]. ∀[n:ℕ]. n < x^n
Lemma: exp-positive
∀[n,x:ℕ+]. 0 < x^n
Lemma: exp-non-neg
∀[n,x:ℕ]. (0 ≤ x^n)
Lemma: exp-positive-stronger
∀n:ℕ. ∀x:ℕ+. 0 < x^n
Lemma: exp-is-zero
∀[x:ℤ]. ∀[n:ℕ]. uiff(x^n = 0 ∈ ℤ;0 < n ∧ (x = 0 ∈ ℤ))
Lemma: exp-non-zero
∀[n:ℕ]. ∀[x:ℤ]. ¬(x^n = 0 ∈ ℤ) supposing ¬(x = 0 ∈ ℤ)
Lemma: exp_functionality_wrt_le_1
∀[b:ℕ+]. ∀[x,y:ℕ]. b^x ≤ b^y supposing x ≤ y
Lemma: divides-prime
∀p,q:ℤ. (prime(q) ⇒ (p | q) ⇒ ((p ~ q) ∨ (p ~ 1) ∨ (p = 0 ∈ ℤ)))
Lemma: prime-divides-prime
∀p,q:ℤ. (prime(p) ⇒ prime(q) ⇒ (p | q) ⇒ (p ~ q))
Lemma: prime-power-divides-product
∀p:ℕ. (prime(p) ⇒ (∀n:ℕ+. ∀x,y:ℤ. ((¬(p | x)) ⇒ (p^n | (x * y)) ⇒ (p^n | y))))
Lemma: prime-isOdd
∀p:ℕ. (prime(p) ⇒ (¬(p = 2 ∈ ℤ)) ⇒ (↑isOdd(p)))
Lemma: positive-prime-divides-prime
∀[p,q:ℕ]. (p = q ∈ ℕ) supposing ((p | q) and prime(q) and prime(p))
Lemma: positive-prime-divides-product
∀p:{p:ℕ| prime(p)} . ∀qs:{p:ℕ| prime(p)} List. ((p | reduce(λx,y. (x * y);1;qs)) ⇒ (p ∈ qs))
Definition: quadratic-residue
a is a quadratic residue mod p == ∃x:ℤ. ((x * x) ≡ a mod p)
Lemma: quadratic-residue_wf
∀[a,p:ℤ]. (a is a quadratic residue mod p ∈ ℙ)
Lemma: quadratic-residue_functionality
∀a,a',p:ℤ. ((a' ≡ a mod p) ⇒ (a' is a quadratic residue mod p ⇐⇒ a is a quadratic residue mod p))
Lemma: mul_wf_nzero
∀[a,b:ℤ-o]. (a * b ∈ ℤ-o)
Lemma: mul_nzero
∀[a,b:ℤ-o]. a * b ≠ 0
Lemma: mul_add_distrib
∀[a,b,c:ℤ]. (((a + b) * c) = ((a * c) + (b * c)) ∈ ℤ)
Lemma: left_mul_add_distrib
∀[a,b,c:ℤ]. ((c * (a + b)) = ((c * a) + (c * b)) ∈ ℤ)
Lemma: left_mul_subtract_distrib
∀[a,b,c:ℤ]. ((c * (a - b)) = ((c * a) - c * b) ∈ ℤ)
Lemma: exp_difference_factor
∀[n:ℕ+]. ∀[x,y:ℤ]. ((x^n - y^n) = (Σ(x^(n - i + 1) * y^i | i < n) * (x - y)) ∈ ℤ)
Lemma: absval_exp
∀[x:ℤ]. ∀[n:ℕ]. (|x^n| ~ |x|^n)
Lemma: exp_difference_bound
∀[n:ℕ+]. ∀[M:ℕ]. ∀[x,y:ℤ]. |x^n - y^n| ≤ ((n * M^(n - 1)) * |x - y|) supposing (|x| ≤ M) ∧ (|y| ≤ M)
Definition: sign
sign(x) == if 0 ≤z x then 1 else -1 fi
Lemma: sign_wf
∀[x:ℤ]. (sign(x) ∈ ℤ)
Lemma: sign-absval
∀[x:ℤ]. ((sign(x) * |x|) = x ∈ ℤ)
Lemma: sign-squared
∀[x:ℤ]. ((sign(x) * sign(x)) = 1 ∈ ℤ)
Definition: permutation-sign
The sign of a permutation can be defined in various ways.
The crucial properties are
1) permutation-sign-id (sign of identity = 1)
2) sign-flip (sign of a transposition = -1)
3) permutation-sign-compose (sign of f o g = sign(f)*sign(g))
Properties 1 and 3 make sign a character of the group of permutations on
ℕn (the symmetric group Sn).
The definition used here suffices to prove these properties,
so it is equivalent to any other definition -- e.g parity of the number
of transpositons in a decompositon, etc.⋅
permutation-sign(n;f) == Π(Π(sign((f j) - f i) | i < j) | j < n)
Lemma: permutation-sign_wf
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕn]. (permutation-sign(n;f) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
Lemma: permutation-sign-id
∀[n:ℕ]. (permutation-sign(n;λx.x) ~ 1)
Lemma: permutation-sign-flip-adjacent
∀[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[u:ℕn - 1].
(permutation-sign(n;f o (u, u + 1)) = (-permutation-sign(n;f)) ∈ ℤ)
Lemma: permutation-sign-flip
∀[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[u,v:ℕn].
permutation-sign(n;f o (u, v)) = (-permutation-sign(n;f)) ∈ ℤ supposing ¬(u = v ∈ ℤ)
Lemma: sign-flip
∀[n:ℕ]. ∀[u,v:ℕn]. permutation-sign(n;(u, v)) = (-1) ∈ ℤ supposing ¬(u = v ∈ ℤ)
Lemma: permutation-sign-compose
∀[n:ℕ]. ∀[f,g:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ].
(permutation-sign(n;f o g) = (permutation-sign(n;f) * permutation-sign(n;g)) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
Lemma: sign-inverse
∀[n:ℕ]. ∀[f:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ]. (permutation-sign(n;inv(f)) = permutation-sign(n;f) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
Lemma: divides-add
∀x,y,z:ℤ. ((z | x) ⇒ (z | y) ⇒ (z | (x + y)))
Lemma: divides-mul
∀x,y,z:ℤ. (((z | x) ∨ (z | y)) ⇒ (z | (x * y)))
Lemma: gcd-property
∀x,y:ℤ. ∃a,b:ℤ. (CoPrime(a,b) ∧ (x = (gcd(x;y) * a) ∈ ℤ) ∧ (y = (gcd(x;y) * b) ∈ ℤ))
Lemma: gcd-positive
∀[y,x:ℕ]. (0 < gcd(x;y)) supposing ((0 ≤ y) and 0 < x)
Lemma: gcd-non-neg
∀[y,x:ℕ]. (0 ≤ gcd(x;y))
Lemma: gcd_sym_nat
∀a,b:ℕ. (gcd(a;b) ~ gcd(b;a))
Lemma: gcd_assoc_nat
∀a,b,c:ℕ. (gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c)))
Lemma: gcd_subtract
∀a,b:ℕ. gcd(a - b;b) ~ gcd(a;b) supposing b ≤ a
Lemma: gcd-reduce
∀p,q:ℤ. ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
Lemma: gcd-reduce-ext
∀p,q:ℤ. ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
Lemma: gcd-reduce-coprime
∀p,q:ℤ. ∃x,y:ℤ. (((x * p) + (y * q)) = 1 ∈ ℤ) supposing CoPrime(p,q)
Lemma: gcd-reduce-prime
∀p,q:ℤ. ∃x,y:ℤ. (((x * p) + (y * q)) = 1 ∈ ℤ) supposing prime(p) ∧ (¬(p | q))
Definition: gcd_reduce
gcd_reduce(p;q) == let g,a,b,rest = TERMOF{gcd-reduce-ext:o, 1:l} p q in <g, a, b>
Lemma: gcd_reduce_wf
∀[p,q:ℤ]. (gcd_reduce(p;q) ∈ ℕ × ℤ × ℤ)
Lemma: gcd_reduce_property
∀p,q:ℤ. let g,a,b = gcd_reduce(p;q) in (p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ CoPrime(a,b) ∧ ((p * b) = (a * q) ∈ ℤ)
Lemma: gcd_com
∀[n,m:ℕ]. (gcd(n;m) ~ gcd(m;n))
Lemma: gcd-non-zero
∀a,b:ℤ. ((a ≠ 0 ∨ b ≠ 0) ⇒ gcd(a;b) ≠ 0)
Definition: lcm
lcm(a;b) ==
eval a' = a in
eval b' = b in
if (a' =z 0) then 0
if (b' =z 0) then 0
else eval g = gcd(a';b') in
(a' * b') ÷ g
fi
Lemma: lcm_wf
∀[a,b:ℤ]. (lcm(a;b) ∈ ℤ)
Lemma: lcm-positive
∀[a,b:ℕ+]. 0 < lcm(a;b)
Lemma: lcm-property
∀x,y:ℤ. ∃a,b:ℤ. (CoPrime(a,b) ∧ ((x * b) = lcm(x;y) ∈ ℤ) ∧ ((y * a) = lcm(x;y) ∈ ℤ))
Lemma: lcm-is-lcm
∀n,m:ℕ+. (((n | lcm(n;m)) ∧ (m | lcm(n;m))) ∧ (∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (lcm(n;m) | v))))
Lemma: lcm-is-lcm-nat
∀n,m:ℕ. (((n | lcm(n;m)) ∧ (m | lcm(n;m))) ∧ (∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (lcm(n;m) | v))))
Lemma: lcm-unique
∀n,m,l:ℕ+. ((((n | l) ∧ (m | l)) ∧ (∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (l | v)))) ⇒ (l = lcm(n;m) ∈ ℤ))
Lemma: lcm-unique-nat
∀n,m,l:ℕ. ((((n | l) ∧ (m | l)) ∧ (∀v:ℤ. ((n | v) ⇒ (m | v) ⇒ (l | v)))) ⇒ (l = lcm(n;m) ∈ ℤ))
Lemma: gcd-unique-nat
∀n,m,g:ℕ. ((((g | n) ∧ (g | m)) ∧ (∀v:ℤ. ((v | n) ⇒ (v | m) ⇒ (v | g)))) ⇒ (g = gcd(n;m) ∈ ℤ))
Lemma: lcm_wf_nat
∀[n,m:ℕ]. (lcm(n;m) ∈ ℕ)
Lemma: lcm-com-nat
∀n,m:ℕ. (lcm(n;m) = lcm(m;n) ∈ ℤ)
Lemma: lcm-assoc-nat
∀[n,m,k:ℕ]. (lcm(n;lcm(m;k)) = lcm(lcm(n;m);k) ∈ ℤ)
Lemma: lcm-gcd-absorption
∀[n,m:ℕ]. (lcm(n;gcd(n;m)) = n ∈ ℤ)
Lemma: gcd-lcm-absorption
∀[n,m:ℕ]. (gcd(n;lcm(n;m)) = n ∈ ℤ)
Definition: int_mod
ℤ_n == x,y:ℤ//(x ≡ y mod n)
Lemma: int_mod_wf
∀[n:ℤ]. (ℤ_n ∈ Type)
Lemma: int-subtype-int_mod
∀[n:ℤ]. (ℤ ⊆r ℤ_n)
Lemma: modulus_wf_int_mod
∀[n:ℕ+]. ∀[x:ℤ_n]. (x mod n ∈ ℕn)
Lemma: modulus-int_mod-nonzero
∀[n:ℕ+]. ∀[x:ℤ_n]. x mod n ∈ ℕ+n supposing x ≠ 0 ∈ ℤ_n
Lemma: equal_int_mod_iff_modulus
∀[n:ℕ+]. ∀[x,y:ℤ_n]. uiff((x mod n) = (y mod n) ∈ ℤ;x = y ∈ ℤ_n)
Lemma: minus_wf_int_mod
∀[n:ℤ]. ∀[x:ℤ_n]. (-x ∈ ℤ_n)
Lemma: add_wf_int_mod
∀[n:ℤ]. ∀[x,y:ℤ_n]. (x + y ∈ ℤ_n)
Lemma: add_is_int_counterexample
∀[n:ℤ]. ∀[x:ℤ_n]. (x + (-x) ∈ ℤ)
Lemma: add_com_int_mod
∀[n:ℤ]. ∀[x,y:ℤ_n]. ((x + y) = (y + x) ∈ ℤ_n)
Lemma: add_zero_int_mod
∀[n:ℤ]. ∀[x:ℤ_n]. ((x + 0) = x ∈ ℤ_n)
Lemma: add_inverse_int_mod
∀[n:ℤ]. ∀[x:ℤ_n]. ((x + (-x)) = 0 ∈ ℤ_n)
Lemma: add_assoc_int_mod
∀[n:ℤ]. ∀[x,y,z:ℤ_n]. (((x + y) + z) = (x + y + z) ∈ ℤ_n)
Lemma: multiply_wf_int_mod
∀[n:ℤ]. ∀[x,y:ℤ_n]. (x * y ∈ ℤ_n)
Lemma: multiply_com_int_mod
∀[n:ℤ]. ∀[x,y:ℤ_n]. ((x * y) = (y * x) ∈ ℤ_n)
Lemma: multiply_one_int_mod
∀[n:ℤ]. ∀[x:ℤ_n]. ((x * 1) = x ∈ ℤ_n)
Lemma: multiply_assoc_int_mod
∀[n:ℤ]. ∀[x,y,z:ℤ_n]. (((x * y) * z) = (x * y * z) ∈ ℤ_n)
Lemma: multiply_distrib_int_mod
∀[n:ℤ]. ∀[a,x,y:ℤ_n]. ((a * (x + y)) = ((a * x) + (a * y)) ∈ ℤ_n)
Lemma: multiply_distrib2_int_mod
∀[n:ℤ]. ∀[a,x,y:ℤ_n]. (((x + y) * a) = ((x * a) + (y * a)) ∈ ℤ_n)
Lemma: subtype_rel_int_mod
∀[a,b:ℤ]. ((a | b) ⇒ (ℤ_b ⊆r ℤ_a))
Lemma: int_mod_union_int_mod
∀[n,m:ℕ+]. ℤ_n ⋃ ℤ_m ≡ ℤ_gcd(n;m)
Lemma: int_mod_isect_int_mod
∀[n,m:ℕ+]. ℤ_n ⋂ ℤ_m ≡ ℤ_lcm(n;m)
Lemma: int_mod_2_union_int_mod_3
ℤ_2 ⋃ ℤ_3 ≡ ⇃(ℤ)
Lemma: int_mod_2_isect_int_mod_3
ℤ_2 ⋂ ℤ_3 ≡ ℤ_6
Lemma: equipollent-int_mod
∀m:ℕ+. ℤ_m ~ ℕm
Comment: fibs and nats as streams
Here are some examples about the "stream" of fibonacci numbers.
They would be part of the streams theory (part of co-recursion)
except that the definition of the fibonacci numbers is in
num_thy_1.⋅
Definition: fibs
fibs() == fix((λfibs.1.1.stream-zip(λx,y. (x + y);fibs;s-tl(fibs))))
Lemma: fibs_wf
fibs() ∈ stream(ℕ)
Lemma: nth-fibs
∀n:ℕ. (s-nth(n;fibs()) = fib(n) ∈ ℤ)
Lemma: fibs-equal-map
fibs() = stream-map(λn.fib(n);nats()) ∈ stream(ℕ)
Definition: better-fibs
better-fibs() == stream-map(λp.(fst(p));mk-stream(λp.let a,b = p in eval c = a + b in <b, c>;<1, 1>))
Lemma: better-fibs_wf
better-fibs() ∈ stream(ℕ)
Lemma: nth-better-fibs
∀n:ℕ. (s-nth(n;better-fibs()) = fib(n) ∈ ℤ)
Lemma: better-fibs-equal-map
better-fibs() = stream-map(λn.fib(n);nats()) ∈ stream(ℕ)
Lemma: eqmod-by-orbits
∀n,k,p:ℕ.
((∃T:Type
∃f:T ⟶ T
(T ~ ℕn
∧ Inj(T;T;f)
∧ {x:T| (f x) = x ∈ T} ~ ℕk
∧ (∀L:T List. (||L|| = 1 ∈ ℤ) ∨ (p | ||L||) supposing orbit(T;f;L))))
⇒ (n ≡ k mod p))
Lemma: eqmod-prime-order-fixedpoints
∀n,k,p:ℕ.
(prime(p)
⇒ (∃T:Type. ∃f:T ⟶ T. (T ~ ℕn ∧ Inj(T;T;f) ∧ {x:T| (f x) = x ∈ T} ~ ℕk ∧ (∀x:T. ((f^p x) = x ∈ T))))
⇒ (n ≡ k mod p))
Lemma: fermat-little
∀p:ℕ. (prime(p) ⇒ (∀x:ℕ. (x^p ≡ x mod p)))
Lemma: fermat-little2
∀p:ℕ. (prime(p) ⇒ (∀x:ℕ. x^(p - 1) ≡ 1 mod p supposing ¬(p | x)))
Definition: nondecreasing
nondecreasing(f;k) == ∀i:ℕk - 1. ((f i) ≤ (f (i + 1)))
Lemma: nondecreasing_wf
∀[k:ℕ]. ∀[f:ℕk ⟶ ℤ]. (nondecreasing(f;k) ∈ ℙ)
Lemma: const_nondecreasing
∀[k:ℕ]. ∀[x:ℤ]. nondecreasing(λi.x;k)
Definition: fadd
fadd(f;g) == λi.((f i) + (g i))
Lemma: fadd_wf
∀[n,m,k:ℕ]. ∀[f:ℕn ⟶ ℕm]. ∀[g:ℕn ⟶ ℕk + 1]. (fadd(f;g) ∈ ℕn ⟶ ℕm + k)
Lemma: fadd_increasing
∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ]. (increasing(fadd(f;g);n)) supposing (nondecreasing(g;n) and increasing(f;n))
Definition: fshift
fshift(f;x) == λi.if (i =z 0) then x else f (i - 1) fi
Lemma: fshift_wf
∀[n,k:ℕ]. ∀[f:ℕn ⟶ ℕk]. ∀[x:ℕk]. (fshift(f;x) ∈ ℕn + 1 ⟶ ℕk)
Lemma: fshift_increasing
∀[n:ℕ]. ∀[x:ℤ]. ∀[f:ℕn ⟶ ℤ]. (increasing(fshift(f;x);n + 1)) supposing (x < f 0 and 0 < n and increasing(f;n))
Definition: fappend
f[n:=x] == λi.if (i =z n) then x else f i fi
Lemma: fappend_wf
∀[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm]. ∀[x:ℕm]. (f[n:=x] ∈ ℕn + 1 ⟶ ℕm)
Lemma: increasing_split
∀m:ℕ
∀[P:ℕm ⟶ ℙ]
((∀i:ℕm. Dec(P i))
⇒ (∃n,k:ℕ
∃f:ℕn ⟶ ℕm
∃g:ℕk ⟶ ℕm
(increasing(f;n)
∧ increasing(g;k)
∧ (∀i:ℕn. (P (f i)))
∧ (∀j:ℕk. (¬(P (g j))))
∧ (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))))))
Lemma: pair_support
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m,k:ℕn].
(Σ(f[x] | x < n) = (f[m] + f[k]) ∈ ℤ) supposing
((∀x:ℕn. ((¬(x = m ∈ ℤ)) ⇒ (¬(x = k ∈ ℤ)) ⇒ (f[x] = 0 ∈ ℤ))) and
(¬(m = k ∈ ℤ)))
Definition: double_sum
sum(f[x; y] | x < n; y < m) == Σ(Σ(f[x; y] | y < m) | x < n)
Lemma: double_sum_wf
∀[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm ⟶ ℤ]. (sum(f[x;y] | x < n; y < m) ∈ ℤ)
Lemma: pair_support_double_sum
∀[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm ⟶ ℤ]. ∀[x1,x2:ℕn]. ∀[y1,y2:ℕm].
(sum(f[x;y] | x < n; y < m) = (f[x1;y1] + f[x2;y2]) ∈ ℤ) supposing
((∀x:ℕn. ∀y:ℕm. ((¬((x = x1 ∈ ℤ) ∧ (y = y1 ∈ ℤ))) ⇒ (¬((x = x2 ∈ ℤ) ∧ (y = y2 ∈ ℤ))) ⇒ (f[x;y] = 0 ∈ ℤ))) and
((¬(x1 = x2 ∈ ℤ)) ∨ (¬(y1 = y2 ∈ ℤ))))
Lemma: double_sum_difference
∀[n,m:ℕ]. ∀[f,g:ℕn ⟶ ℕm ⟶ ℤ]. ∀[d:ℤ].
sum(f[x;y] | x < n; y < m) = (sum(g[x;y] | x < n; y < m) + d) ∈ ℤ
supposing sum(f[x;y] - g[x;y] | x < n; y < m) = d ∈ ℤ
Lemma: double_sum_functionality
∀[n,m:ℕ]. ∀[f,g:ℕn ⟶ ℕm ⟶ ℤ].
sum(f[x;y] | x < n; y < m) = sum(g[x;y] | x < n; y < m) ∈ ℤ supposing ∀x:ℕn. ∀y:ℕm. (f[x;y] = g[x;y] ∈ ℤ)
Lemma: sum_switch
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[i:ℕn - 1]. (Σ(f[(i, i + 1) x] | x < n) = Σ(f[x] | x < n) ∈ ℤ)
Definition: fact
(n)! == primrec(n;1;λi,j. ((i + 1) * j))
Lemma: fact0_redex_lemma
(0)! ~ 1
Lemma: fact_unroll
∀[n:ℤ]. ((n)! ~ if n <z 1 then 1 else n * (n - 1)! fi )
Lemma: fact_unroll_1
∀[n:ℤ]. (n)! ~ n * (n - 1)! supposing ¬n < 1
Lemma: fact-as-genfact
∀[n:ℕ]. ((n)! ~ genfact(n;1;m.m))
Lemma: fact_wf
∀[n:ℕ]. ((n)! ∈ ℕ+)
Lemma: exp-fact-as-genfact
∀[a,x:ℤ]. ∀[n:ℕ]. (a * x^n * (n)! ~ genfact(n;a;m.x * m))
Lemma: fact_add1
∀[n:ℕ]. ((n + 1)! ~ (n + 1) * (n)!)
Lemma: fact_add2
∀[n:ℕ]. ((n + 2)! ~ (n + 2) * (n + 1) * (n)!)
Lemma: fact-increasing
∀[m:ℕ]. ∀[n:ℕ+]. (n < m ⇒ (n)! < (m)!)
Lemma: fact-non-decreasing
∀[m,n:ℕ]. ((n ≤ m) ⇒ ((n)! ≤ (m)!))
Lemma: fact-positive
∀[m:ℕ]. (1 ≤ (m)!)
Lemma: fact-non-zero
∀[m:ℕ]. (¬((m)! = 0 ∈ ℤ))
Lemma: fact-greater-exp
∀k,n:ℕ. ∃m:ℕ. n * k^m < (m)!
Definition: expfact
expfact(n;x;p;b)
==r if p ≤z b then n else eval n' = n + 1 in eval p' = x * p in eval b' = n' * b in expfact(n';x;p';b') fi
Lemma: expfact_wf
∀[m:ℕ+]. ∀[k:ℕ]. ∀[n:ℕ+]. ∀b:{b:ℕ| n * k^b < (b)!} . ((m ≤ b) ⇒ (expfact(m;k;n * k^m;(m)!) ∈ {b:ℕ+| (n * k^b) ≤ (b)!} \000C))
Lemma: expfact-property
∀k:ℕ. ∀n:ℕ+. ∃m:ℕ+. ((n * k^m) ≤ (m)!)
Definition: exp-ratio
exp-ratio(a;b;n;p;q)
==r if p <z q then n else eval n' = n + 1 in eval p' = a * p in eval q' = b * q in exp-ratio(a;b;n';p';q') fi
Lemma: exp-ratio_wf
∀[a:ℕ]. ∀[b:{a + 1...}]. ∀[k:ℕ].
∀c:{n:ℕ| k * a^n < b^n} . ∀n:ℕ. ((n ≤ c) ⇒ (exp-ratio(a;b;n;k * a^n;b^n) ∈ {n:ℕ| k * a^n < b^n} ))
Lemma: exp-ratio_wf2
∀b:{2...}. ∀k:ℕ. ∀M:ℕ+. (exp-ratio(1;b;0;k;M) ∈ {n:ℕ| k < M * b^n} )
Lemma: exp-ratio-property
∀a:ℕ. ∀b:{a + 1...}. ∀k:ℕ. (exp-ratio(a;b;0;k;1) ∈ {n:ℕ| k * a^n < b^n} )
Lemma: exp-ratio-property2
∀M:ℕ+. ∀b:{2...}. ∀k:ℕ. (exp-ratio(1;b;0;k;M) ∈ {n:ℕ| k < M * b^n} )
Definition: super-fact
(n)!! == primrec(n;1;λi,j. ((i + 1)! * j))
Lemma: super-fact_wf
∀[n:ℕ]. ((n)!! ∈ ℕ+)
Lemma: super-fact-unroll
∀[n:ℕ+]. ((n)!! ~ (n)! * (n - 1)!!)
Lemma: super-fact-int-prod-exp
∀[k:ℕ]. ((k)!! = Π((k - i)^(i + 1) | i < k) ∈ ℤ)
Lemma: fact-bound
∀n:ℕ. ((n)! ≤ n^n)
Comment: xxxxx
*
No Annotations
[-]
∀n:ℕ. ((n)! ≤ n^n)
* BY ](InductionOnNat THEN Auto)[
* 1
.....upcase.....
[-]
1. n : ℤ
2. 0 < n
3. (n - 1)! ≤ (n - 1)^(n - 1)
[-]
⊢ (n)! ≤ n^n
* BY ](RWO "exp_step fact_unroll_1" 0 THEN Auto)[
* 11
[-]
⊢ (n * (n - 1)!) ≤ (n * n^(n - 1))
* BY ](InstLemma `exp_preserves_le` [⌜n - 1⌝;⌜n - 1⌝;⌜n⌝]⋅ THEN Auto)[
* 111
[+],
[-]
⊢ (n * (n - 1)!) ≤ (n * n^(n - 1))
* BY ](RWW "-2 -1" 0 THEN Auto)[
*
No Annotations
[+]∀n:ℕ. ((n)! ≤ n^n)
* BY ]((InductionOnNat THEN Auto)
THEN (RWO "exp_step fact_unroll_1" 0 THEN Auto)
THEN (InstLemma `exp_preserves_le` [⌜n - 1⌝;⌜n - 1⌝;⌜n⌝]⋅ THEN Auto)
THEN RWW "-2 -1" 0
THEN Auto)[
⋅
Definition: doublefact
doublefact(n) == if n <z 2 then 1 else n * doublefact(n - 2) fi
Lemma: doublefact_wf
∀[n:ℤ]. (doublefact(n) ∈ ℕ+)
Lemma: add-plus-1-div-2-implies-lt
∀[n,m:ℕ]. n < m supposing n < ((n + m) + 1) ÷ 2
Lemma: exp-minusone
∀[n:ℕ]. ((-1)^n = if (n mod 2 =z 0) then 1 else -1 fi ∈ ℤ)
Lemma: exp-minusone-2n-add
∀[n,k:ℕ]. ((-1)^((2 * n) + k) = (-1)^k ∈ ℤ)
Lemma: exp-minus
∀[n:ℕ]. ∀[x:ℤ]. ((-x)^n = if (n mod 2 =z 0) then x^n else -x^n fi ∈ ℤ)
Lemma: exp-convex
∀[a,b,c:ℕ]. ∀[n:ℕ+]. |a - b| ≤ c supposing |a^n - b^n| ≤ c^n
Lemma: exp-convex2
∀[a,b:ℤ]. ∀[c:ℕ]. ∀[n:ℕ+]. |a - b| ≤ c supposing (|a^n - b^n| ≤ c^n) ∧ (0 ≤ a ⇐⇒ 0 ≤ b)
Lemma: mul-assoced-one
∀x,y:ℤ. (((x * y) ~ 1) ⇒ (x ~ 1))
Lemma: exp-assoced-one
∀x:ℤ. ∀n:ℕ+. ((x^n ~ 1) ⇒ (x ~ 1))
Lemma: exp-equal-one
∀x:ℤ. ∀n:ℕ. (x^n = 1 ∈ ℤ ⇐⇒ (x = 1 ∈ ℤ) ∨ (n = 0 ∈ ℤ) ∨ ((x = (-1) ∈ ℤ) ∧ ((n mod 2) = 0 ∈ ℤ)))
Lemma: exp-equal-minusone
∀[x:ℤ]. ∀[n:ℕ]. uiff(x^n = (-1) ∈ ℤ;(x = (-1) ∈ ℤ) ∧ ((n mod 2) = 1 ∈ ℤ))
Lemma: div_mono1
∀[i,k:ℕ]. (i ÷ k < i) supposing (1 < k and 0 < i)
Lemma: efficient-exp
∀i:ℤ. ∀n:ℕ. (∃j:ℤ [(j = i^n ∈ ℤ)])
Lemma: less-efficient-exp
∀i:ℤ. ∀n:ℕ. (∃j:ℤ [(j = i^n ∈ ℤ)])
Lemma: efficient-exp-ext
∀i:ℤ. ∀n:ℕ. (∃j:ℤ [(j = i^n ∈ ℤ)])
Definition: fastexp
i^n == TERMOF{efficient-exp-ext:o, 1:l} i n
Lemma: fastexp_wf
∀[i:ℤ]. ∀[n:ℕ]. (i^n ∈ ℤ)
Lemma: less-efficient-exp-ext
∀i:ℤ. ∀n:ℕ. (∃j:ℤ [(j = i^n ∈ ℤ)])
Lemma: exp-fastexp
∀[i:ℤ]. ∀[n:ℕ]. (i^n ~ i^n)
Definition: exp-rem
exp-rem(i;n;m) ==
fix((λexp-rem,n. if n=1
then i rem m
else if n=0
then 1 rem m
else eval n' = n ÷ 2 in
eval x = exp-rem n' in
if n rem 2=0 then x * x rem m else (i * x * x rem m)))
n
Lemma: exp-rem_wf
∀[m:ℕ+]. ∀[i:ℤ]. ∀[n:ℕ]. (exp-rem(i;n;m) ∈ ℤ)
Lemma: rem_mul
∀[x,y:ℕ]. ∀[m:ℕ+]. ((x * y rem m) = ((x rem m) * (y rem m) rem m) ∈ ℤ)
Lemma: rem_mul2
∀[x,y:ℕ]. ∀[m:ℕ+]. ((x * y rem m) = ((x rem m) * y rem m) ∈ ℤ)
Lemma: thm_1a
∀n:ℕ. (↑isEven((n * n) + n))
Lemma: exp-rem-property
∀[m:ℕ+]. ∀[n,i:ℕ]. (exp-rem(i;n;m) ~ i^n rem m)
Definition: log
log(b;n) == genfact-inv(n;1;x.b)
Lemma: log_wf
∀[b:{i:ℤ| 1 < i} ]. ∀[x:ℤ]. (log(b;x) ∈ ℕ)
Lemma: log-property
∀[b:{i:ℤ| 1 < i} ]. ∀[x:ℤ]. (x ≤ b^log(b;x))
Lemma: coprime_symmetry
∀a,b:ℤ. (CoPrime(a,b) ⇒ CoPrime(b,a))
Lemma: coprime-mod
∀n:ℕ+. ∀x:ℤ. (CoPrime(n,x) ⇐⇒ CoPrime(n,x mod n))
Lemma: coprime-exp
∀a,b:ℤ. (CoPrime(a,b) ⇒ (∀n,m:ℕ. CoPrime(a^m,b^n)))
Lemma: gcd-exp
∀x,y:ℤ. ∀n:ℕ. (gcd(x^n;y^n) ~ gcd(x;y)^n)
Lemma: divides-iff-gcd
∀x,y:ℤ. (x | y ⇐⇒ gcd(y;x) = x ∈ ℤ)
Lemma: divides-iff-gcd-assoced
∀x,y:ℤ. (x | y ⇐⇒ gcd(x;y) ~ x)
Lemma: exp_functionality_wrt_assoced
∀n:ℕ. ∀x,y:ℤ. ((x ~ y) ⇒ (x^n ~ y^n))
Lemma: exp-divides-exp
∀x,y:ℤ. (x | y ⇐⇒ ∀n:ℕ+. (x^n | y^n))
Lemma: exp-divides-exp2
∀x,y:ℤ. (x | y ⇐⇒ ∃n:ℕ+. (x^n | y^n))
Lemma: exp_assoced
∀n:ℕ+. ∀x,y:ℤ. (x^n ~ y^n ⇐⇒ x ~ y)
Lemma: div_induction
∀b:{b:ℤ| 1 < b} . ∀[P:ℤ ⟶ ℙ]. (P[0] ⇒ (∀i:ℤ-o. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℤ. P[i]))
Lemma: div_induction-ext
∀b:{b:ℤ| 1 < b} . ∀[P:ℤ ⟶ ℙ]. (P[0] ⇒ (∀i:ℤ-o. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℤ. P[i]))
Lemma: div_nat_induction
∀b:{b:ℤ| 1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0] ⇒ (∀i:ℕ+. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
Lemma: div_nat_induction-ext
∀b:{b:ℤ| 1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0] ⇒ (∀i:ℕ+. (P[i ÷ b] ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
Lemma: int-sq-root
∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
Lemma: int-sqrt-ext
∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
Lemma: integer-nth-root
∀n:ℕ+. ∀x:ℕ. (∃r:ℕ [((r^n ≤ x) ∧ x < (r + 1)^n)])
Lemma: integer-nth-root-ext
∀n:ℕ+. ∀x:ℕ. (∃r:ℕ [((r^n ≤ x) ∧ x < (r + 1)^n)])
Lemma: integer-nth-root2
∀n:{n:ℕ+| (n mod 2) = 1 ∈ ℤ} . ∀x:{...0}. (∃r:{...0} [((r - 1)^n < x ∧ (x ≤ r^n))])
Definition: iroot
iroot(n;x) == TERMOF{integer-nth-root-ext:o, 1:l} n x
Lemma: iroot_wf
∀[n:ℕ+]. ∀[x:ℕ]. (iroot(n;x) ∈ ℕ)
Lemma: iroot-property
∀[n:ℕ+]. ∀[x:ℕ]. ((iroot(n;x)^n ≤ x) ∧ x < (iroot(n;x) + 1)^n)
Definition: is-power
is-power(n;x) == eval r = iroot(n;x) in (r^n =z x)
Lemma: is-power_wf
∀[n:ℕ+]. ∀[x:ℕ]. (is-power(n;x) ∈ 𝔹)
Lemma: assert-is-power
∀n:ℕ+. ∀x:ℕ. (↑is-power(n;x) ⇐⇒ ∃r:ℕ. (x = r^n ∈ ℤ))
Definition: is_power
is_power(n;z) == if (z) < (0) then (n mod 2 =z 1) ∧b is-power(n;-z) else is-power(n;z)
Lemma: is_power_wf
∀[n:ℕ+]. ∀[x:ℤ]. (is_power(n;x) ∈ 𝔹)
Lemma: assert-is_power
∀n:ℕ+. ∀x:ℤ. (↑is_power(n;x) ⇐⇒ ∃r:ℤ. (x = r^n ∈ ℤ))
Lemma: iroot-zero
∀[n:ℕ+]. (iroot(n;0) ~ 0)
Lemma: iroot-positive
∀[n,x:ℕ+]. (1 ≤ iroot(n;x))
Definition: general-iroot
general-iroot(n;x) ==
eval m = n in
eval y = x in
if (y) < (0) then if m mod 2=1 then TERMOF{integer-nth-root2:o, 1:l} m y else 0 else iroot(m;y)
Lemma: general-iroot_wf
∀[n:ℕ+]. ∀[x:ℤ]. (general-iroot(n;x) ∈ ℤ)
Lemma: general-iroot-property
∀[n:ℕ+]. ∀[x:ℤ].
(((0 ≤ x) ⇒ ((general-iroot(n;x)^n ≤ x) ∧ x < (general-iroot(n;x) + 1)^n))
∧ ((x < 0 ∧ ((n mod 2) = 1 ∈ ℤ)) ⇒ ((x ≤ general-iroot(n;x)^n) ∧ (general-iroot(n;x) - 1)^n < x))
∧ ((x < 0 ∧ ((n mod 2) = 0 ∈ ℤ)) ⇒ (general-iroot(n;x) = 0 ∈ ℤ)))
Lemma: isqrrrt
∀n:ℕ. (∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))])
Lemma: isqrrrt-program
∀n:ℕ. (∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))])
Lemma: integer-sqrt
∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
Lemma: integer-sqrt-xover
∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
Lemma: integer-sqrt-bin-search
∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
Definition: isqrt_newton
isqrt_newton(n;x)
==r eval s = x + (n ÷ x) in
eval z = s ÷ 2 in
if z=x then z else if (x) < (z) then x else isqrt_newton(n;z)
Lemma: isqrt_newton_wf
∀n,x:ℕ+. isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))] supposing n < (x + 1) * (x + 1)
Lemma: integer-sqrt-newton
∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
Lemma: integer-sqrt-newton-ext
∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
Definition: isqrtn
isqrtn(x) == TERMOF{integer-sqrt-newton-ext:o, 1:l} x
Lemma: isqrtn_wf
∀x:ℕ. (isqrtn(x) ∈ {r:ℕ| ((r * r) ≤ x) ∧ x < (r + 1) * (r + 1)} )
Lemma: integer-sqrt-ext
∀x:ℕ. (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
Definition: isqrt
isqrt(x) == TERMOF{integer-sqrt-ext:o, 1:l} x
Lemma: isqrt_wf
∀[x:ℕ]. (isqrt(x) ∈ ℕ)
Lemma: isqrt-property
∀[x:ℕ]. (((isqrt(x) * isqrt(x)) ≤ x) ∧ x < (isqrt(x) + 1) * (isqrt(x) + 1))
Lemma: isqrt-non-decreasing
∀[x,y:ℕ]. isqrt(x) ≤ isqrt(y) supposing x ≤ y
Lemma: square-iff-isqrt
∀x:ℕ. (∃y:ℕ. ((y * y) = x ∈ ℤ) ⇐⇒ (isqrt(x) * isqrt(x)) = x ∈ ℤ)
Lemma: isqrt-of-square
∀[z:ℕ]. (isqrt(z * z) = z ∈ ℤ)
Lemma: two-squares-iff
∀x:ℕ
(∃y,z:ℕ. (((y * y) + (z * z)) = x ∈ ℤ)
⇐⇒ ∃y:ℕisqrt(x) + 1. ((isqrt(x - y * y) * isqrt(x - y * y)) = (x - y * y) ∈ ℤ))
Lemma: isqrt-convex
∀a,b:ℕ. (|isqrt(a) - isqrt(b)| ≤ isqrt(|a - b|))
Lemma: int-between
∀i,j:ℤ. ∃k:ℤ. ((i ≤ k) ∧ k < j) supposing i < j
Definition: triangular-num
t(n) == (n * (n + 1)) ÷ 2
Lemma: triangular-num_wf
∀[n:ℕ]. (t(n) ∈ ℕ)
Lemma: triangular-num-alt
∀[n:ℕ]. (t(n) = (((n ÷ 2) + (n rem 2)) * ((2 * (n ÷ 2)) + 1)) ∈ ℤ)
Lemma: triangular-num-add1
∀[n:ℕ]. (t(n + 1) = (t(n) + n + 1) ∈ ℤ)
Lemma: triangular-num-le
∀[n,m:ℕ]. t(n) ≤ t(m) supposing n ≤ m
Lemma: twice-triangular
∀[n:ℕ]. ((2 * t(n)) = ((n * n) + n) ∈ ℤ)
Definition: tsqrt
tsqrt(n) == eval r = isqrt(2 * n) in if (r * r) + r ≤z 2 * n then r else r - 1 fi
Lemma: tsqrt_wf
∀[n:ℕ]. (tsqrt(n) ∈ ℕ)
Lemma: tsqrt-property
∀[n:ℕ]. ((t(tsqrt(n)) ≤ n) ∧ n < t(tsqrt(n) + 1))
Lemma: tsqrt-unique
∀[n,x:ℕ]. (((t(x) ≤ n) ∧ n < t(x + 1)) ⇒ (x = tsqrt(n) ∈ ℤ))
Definition: coded-pair
coded-pair(m) == eval n = m in eval x = tsqrt(n) in eval a = n - t(x) in eval b = x - a in <a, b>
Lemma: coded-pair_wf
∀[n:ℕ]. (coded-pair(n) ∈ ℕ × ℕ)
Definition: code-pair
code-pair(a;b) == t(a + b) + a
Lemma: code-pair_wf
∀[a,b:ℕ]. (code-pair(a;b) ∈ ℕ)
Lemma: coded-code-pair
∀[a,b:ℕ]. (coded-pair(code-pair(a;b)) = <a, b> ∈ (ℕ × ℕ))
Lemma: code-coded-pair
∀n:ℕ. (let a,b = coded-pair(n) in code-pair(a;b) = n ∈ ℤ)
Lemma: code-pair-bijection
Bij(ℕ;ℕ × ℕ;λx.coded-pair(x))
Definition: code-seq1
code-seq1(k;s) == primrec(k;0;λi,x. if (i =z 0) then s i else code-pair(x;s i) fi )
Lemma: code-seq1_wf
∀[k:ℕ]. ∀[s:ℕk ⟶ ℕ]. (code-seq1(k;s) ∈ ℕ)
Definition: coded-seq1
coded-seq1(k;x;n)
==r if (k =z 0) then x else let y,m = coded-pair(x) in if (n =z k) then m else coded-seq1(k - 1;y;n) fi fi
Lemma: coded-seq1_wf
∀[k:ℕ]. ∀[n:ℕk + 1]. ∀[x:ℕ]. (coded-seq1(k;x;n) ∈ ℕ)
Lemma: coded-code-seq1
∀[k:ℕ+]. ∀s:ℕk ⟶ ℕ. ∀[n:ℕk]. (coded-seq1(k - 1;code-seq1(k;s);n) = (s n) ∈ ℤ)
Lemma: code-coded-seq1
∀[k:ℕ+]. ∀[x:ℕ]. (code-seq1(k;λn.coded-seq1(k - 1;x;n)) = x ∈ ℤ)
Definition: code-seq
code-seq(k;s) == if (k =z 0) then 0 else code-pair(k - 1;code-seq1(k;s)) + 1 fi
Lemma: code-seq_wf
∀[k:ℕ]. ∀[s:ℕk ⟶ ℕ]. (code-seq(k;s) ∈ ℕ)
Definition: coded-seq
coded-seq(x) == if (x =z 0) then <0, λx.x> else let a,b = coded-pair(x - 1) in <a + 1, λn.coded-seq1(a;b;n)> fi
Lemma: coded-seq_wf
∀x:ℕ. (coded-seq(x) ∈ k:ℕ × (ℕk ⟶ ℕ))
Lemma: code-coded-seq
∀x:ℕ. (let k,s = coded-seq(x) in code-seq(k;s) = x ∈ ℤ)
Lemma: coded-code-seq
∀k:ℕ. ∀s:ℕk ⟶ ℕ. (coded-seq(code-seq(k;s)) = <k, s> ∈ (k:ℕ × (ℕk ⟶ ℕ)))
Lemma: code-seq-bijection
Bij(ℕ;k:ℕ × (ℕk ⟶ ℕ);λx.coded-seq(x))
Lemma: countable-nsub-family
∀B:ℕ ⟶ ℕ+. ∃g:ℕ ⟶ (i:ℕ × ℕB[i]). Surj(ℕ;i:ℕ × ℕB[i];g)
Definition: twosquareinv
This function defines an involution on the type
x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} where p is a prime.
It is used in
"A One-Sentence Proof that Every Prime p == 1 (mod 4) Is a Sum of Two Squares"
by D. Zaiger.
He says that it is a simplification of an argument by Heath-Brown.⋅
twosquareinv(t) ==
let x,y,z = t in
if x <z y - z then <x + z + z, z, y - z - x>
if x <z y + y then <(y + y) - x, y, (x - y) + z>
else <x - y + y, (x - y) + z, y>
fi
Lemma: twosquareinv_wf
∀[p:{2...}]. ∀[t:x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} ].
(twosquareinv(t) ∈ x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )
Lemma: twosquareinv-involution
∀p:{p:{2...}| prime(p)} . ∀t:x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} . (twosquareinv(twosquareinv(t)) ~ t)
Lemma: twosquareinv-fixpoint
∀p:{p:{2...}| prime(p)} . ∀t:x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} .
((twosquareinv(t) = t ∈ (ℕ × ℕ × ℕ)) ⇒ (t ~ <1, 1, (p - 1) ÷ 4>))
Lemma: twosquare-type-finite
∀p:{p:{2...}| prime(p)} . finite(x:ℕ × y:ℕ × {z:ℕ| ((x * x) + (4 * y * z)) = p ∈ ℤ} )
Lemma: prime-sum-of-two-squares-if-one-mod-four
This proof that every prime p that is 1 mod 4 is the sum of two squares
comes from the article by D. Zagier called
"A One-Sentence Proof that Every Prime p == 1 (mod 4) Is a Sum of Two Squares".
It uses the properties
twosquareinv-involution and
twosquareinv-fixpoint
that a certain involution has a unique fixed point to deduce
that the given finite set (see twosquare-type-finite)
has odd cardinality
(see involution-with-unique-fixpoint) ,
so every invoulution has a fixed point (see involution-has-fixpoint),
and this proves the theorem.
⋅
∀p:{p:{2...}| prime(p)} . ((∃k:ℤ. (p = (1 + (4 * k)) ∈ ℤ)) ⇒ (∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ)))
Lemma: prime-sum-of-two-squares-iff-one-mod-four
∀p:{p:{2...}| prime(p)} . ((p = 2 ∈ ℤ) ∨ (∃k:ℤ. (p = (1 + (4 * k)) ∈ ℤ)) ⇐⇒ ∃a,b:ℤ. (p = ((a * a) + (b * b)) ∈ ℤ))
Lemma: three-cubes-lemma
∀d,e:ℤ.
(∃a,b:ℤ. ((((a * a) + ((b * b) - a * b)) = e ∈ ℤ) ∧ ((a + b) = d ∈ ℤ))
⇐⇒ ∃n:ℕ. (((4 * e) - d * d) = (3 * n * n) ∈ ℤ))
Lemma: sum-of-three-cubes-iff-1
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.
The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅
∀k:ℕ. ∀a,b,c:ℤ.
((0 ≤ (a + b))
⇒ ((((a * a * a) + (b * b * b)) + (c * c * c)) = k ∈ ℤ
⇐⇒ ∃d:ℕ
(((a + b) = d ∈ ℤ)
∧ (((d = 0 ∈ ℤ) ∧ ((c * c * c) = k ∈ ℤ))
∨ ((¬(d = 0 ∈ ℤ))
∧ ((k - c * c * c rem d) = 0 ∈ ℤ)
∧ (((a * a) + ((b * b) - a * b)) = ((k - c * c * c) ÷ d) ∈ ℤ))))))
Lemma: sum-of-three-cubes-iff-2
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.
The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅
∀k:ℕ
(∃a,b,c:ℤ. (((a * a * a) + (b * b * b) + (c * c * c)) = k ∈ ℤ)
⇐⇒ ∃c:ℤ
(((c * c * c) = k ∈ ℤ)
∨ (∃d:ℕ
((¬(d = 0 ∈ ℤ))
∧ ((k - c * c * c rem d) = 0 ∈ ℤ)
∧ (∃n:ℕ. (((4 * ((k - c * c * c) ÷ d)) - d * d) = (3 * n * n) ∈ ℤ))))))
Lemma: sum-of-three-cubes-iff-3
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.
The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅
∀k:ℕ
(∃a,b,c:ℤ. (((a * a * a) + (b * b * b) + (c * c * c)) = k ∈ ℤ)
⇐⇒ ∃d:ℕ. ∃e:ℤ. ((∃c:ℤ. (((d * e) - k) = (c * c * c) ∈ ℤ)) ∧ (∃n:ℕ. (((4 * e) - d * d) = (3 * n * n) ∈ ℤ))))
Lemma: sum-of-three-cubes-iff-4
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.
The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅
∀k:ℕ
(∃a,b,c:ℤ. (((a * a * a) + (b * b * b) + (c * c * c)) = k ∈ ℤ)
⇐⇒ ∃d,n:ℕ
((((d * d) + (3 * n * n) rem 4) = 0 ∈ ℤ)
∧ (∃c:ℤ. (((d * (((d * d) + (3 * n * n)) ÷ 4)) - k) = (c * c * c) ∈ ℤ))))
Lemma: sum-of-three-cubes-iff
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.
The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅
∀k:ℕ
(∃a,b,c:ℤ. (((a * a * a) + (b * b * b) + (c * c * c)) = k ∈ ℤ)
⇐⇒ ∃d,n:ℕ
((↑is_power(3;((2 * d) * ((d * d) + (3 * n * n))) - k))
∨ (↑is_power(3;(((2 * d) + 1) * (((d * (d + 1)) + (3 * n * (n + 1))) + 1)) - k))))
Lemma: 33-is-sum-of-three-cubes
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.
The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅
∃a,b,c:ℤ. (((a * a * a) + (b * b * b) + (c * c * c)) = 33 ∈ ℤ)
Lemma: 33-is-sum-of-three-cubes-implies
This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.
The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅
∃d,n:ℕ
((∃c:ℤ. ((((2 * d) * ((d * d) + (3 * n * n))) - 33) = (c * c * c) ∈ ℤ))
∨ (∃c:ℤ. (((((2 * d) + 1) * (((d * (d + 1)) + (3 * n * (n + 1))) + 1)) - 33) = (c * c * c) ∈ ℤ)))
Lemma: 2-is-sum-of-three-cubes
According to wikipedia, as of 2018 these are the only
known ways of writing 2 as the sum of three cubes .⋅
(∀x:ℤ
let a = 1 + (6 * x * x * x) in
let b = 1 - 6 * x * x * x in
let c = -(6 * x * x) in
((a * a * a) + (b * b * b) + (c * c * c)) = 2 ∈ ℤ)
∧ let a = 1214928 in
let b = 3480205 in
let c = -3528875 in
((a * a * a) + (b * b * b) + (c * c * c)) = 2 ∈ ℤ
Lemma: olympiad-problem-six
∀k:ℤ. ∀a,b:ℕ. ((((a * a) + (b * b)) = (k * ((a * b) + 1)) ∈ ℤ) ⇒ (∃n:ℤ. (k = (n * n) ∈ ℤ)))
Lemma: Vieta-jumping-example2
∀k:ℤ. ∀a,b:ℕ. (((((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ) ⇒ (k = 3 ∈ ℤ))
Definition: vexample
vexample(n;a;b) == if n=0 then <a, b> else eval b' = (3 * b) - a in eval m = n - 1 in vexample(m;b;b')
Lemma: vexample_wf
∀n,a:ℕ. ∀b:{b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} .
(vexample(n;a;b) ∈ a:ℕ × {b:ℕ| (((a * a) + (b * b)) + 1) = ((a * b) * 3) ∈ ℤ} )
Lemma: Vieta-jumping-example2-corollary
∀k:ℤ. ∀a,b:ℕ. (((((a * a) + (b * b)) + 1) = (k * a * b) ∈ ℤ) ⇒ (a ≤ b) ⇒ (∃n:ℕ. (<a, b> = vexample(n;1;1) ∈ (ℤ × ℤ)))\000C)
Lemma: ab-divides-a^2+b^2+1
∀a,b:ℤ.
((a * b) | (((a * a) + (b * b)) + 1)
⇐⇒ ∃n:ℕ. ((<|a|, |b|> = vexample(n;1;1) ∈ (ℤ × ℤ)) ∨ (<|b|, |a|> = vexample(n;1;1) ∈ (ℤ × ℤ))))
Definition: search
search(k;P) == primrec(k;0;λi,j. if 0 <z j then j if P i then i + 1 else 0 fi )
Lemma: search_wf
∀[k:ℕ]. ∀[P:ℕk ⟶ 𝔹]. (search(k;P) ∈ ℕk + 1)
Lemma: search_property
∀k:ℕ. ∀P:ℕk ⟶ 𝔹.
((∃i:ℕk. (↑(P i)) ⇐⇒ 0 < search(k;P))
∧ (↑(P (search(k;P) - 1))) ∧ (∀j:ℕk. ¬↑(P j) supposing j < search(k;P) - 1) supposing 0 < search(k;P))
Lemma: search_succ
∀[k:ℕ]. ∀[P:ℕk + 1 ⟶ 𝔹].
(search(k + 1;P) = if P 0 then 1 if 0 <z search(k;λi.(P (i + 1))) then search(k;λi.(P (i + 1))) + 1 else 0 fi ∈ ℤ)
Comment: parametricity (theorems for free)
Parametricity or "theorems for free" allows one to deduce
certain facts about functions with a polymorphic type.
Those polymorphic types are often expressed in a type system
with impredicative quantification over all types.
But we can often get the same results using predicative quantification
over the types in a universe.
So, for example, instead of the type
(FORALL alpha. alpha-> alpha) in an impredicative system,
we can consider the type ⌜⋂A:Type. (A ⟶ A)⌝.
Since the universe ⌜Type⌝ (note that it is just our display for Universe{i})
contains "enough" types, in particular singleton types and types that
contain bottom, we can get many of the results of parametricity theory.
For example:
polymorphic-id-unique
polymorphic-id-unique-sq
polymorphic-constant
polymorphic-constant-bool
The only functions of type alpha->alpha->alpha
are \x y. x and \x y. y, see polymorphic-choice.
The only functions of type alpha->List(alpha) are
\x. repn(n,x) see polymorphic-list
⋅
Lemma: polymorphic-id-unique
∀f,g:⋂T:Type. (T ⟶ T). (f = g ∈ (⋂T:Type. (T ⟶ T)))
Lemma: polymorphic-id-unique-sq
∀f:⋂T:Type. (T ⟶ T). (f ~ λx.x)
Lemma: polymorphic-constant-base
∀[T:Type]. ∀f:Base ⟶ T. ∃t:T. ∀x:Base. ((f x) = t ∈ T) supposing mono(T) ∧ value-type(T)
Lemma: polymorphic-constant
∀[T:Type]. ∀f:⋂A:Type. (A ⟶ T). ∃t:T. ∀A:Type. ∀x:A. ((f x) = t ∈ T) supposing mono(T) ∧ value-type(T)
Lemma: polymorphic-constant-bool
∀f:⋂A:Type. (A ⟶ 𝔹). ∃t:𝔹. ∀A:Type. ∀x:A. f x = t
Lemma: polymorphic-constant-nat
∀f:⋂A:Type. (A ⟶ ℕ). ∃n:ℕ. ∀A:Type. ∀x:A. ((f x) = n ∈ ℕ)
Lemma: polymorphic-list
∀f:⋂A:Type. (A ⟶ (A List)). ∃n:ℕ. (f = (λx.repn(n;x)) ∈ (⋂A:Type. (A ⟶ (A List))))
Lemma: type-equating-some
∀T:Type. ∀P:T ⟶ ℙ.
∃T':Type
((T ⊆r T') ∧ (∀x,y:T. (P[x] ⇒ P[y] ⇒ (x = y ∈ T'))) ∧ (∀x,y:T. ((¬P[x]) ⇒ (x = y ∈ T ⇐⇒ x = y ∈ T'))))
Lemma: exists-type-equating-ints
∀x,y,n,m:ℤ.
((¬(x = y ∈ ℤ))
⇒ (¬(n = m ∈ ℤ))
⇒ (¬(x = m ∈ ℤ))
⇒ (¬(y = n ∈ ℤ))
⇒ (∃T:Type. ((x = n ∈ T) ∧ (y = m ∈ T) ∧ (¬(x = y ∈ T)))))
Definition: EquatePairs
EquatePairs(x;n;y;m) ==
pertype(λ2a b.(a = b ∈ Base)
∨ (((x = a ∈ Base) ∧ (n = b ∈ Base)) ∨ ((x = b ∈ Base) ∧ (n = a ∈ Base)))
∨ (((y = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((y = b ∈ Base) ∧ (m = a ∈ Base)))
∨ ((x = y ∈ Base) ∧ (((n = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((n = b ∈ Base) ∧ (m = a ∈ Base)))))
Lemma: EquatePairs_wf
∀[x,y,n,m:Base].
(EquatePairs(x;n;y;m) ∈ Type) supposing ((¬(n = m ∈ Base)) and (¬(x = m ∈ Base)) and (¬(y = n ∈ Base)))
Lemma: EquatePairs-equality
∀[x,y,n,m:Base].
(∀a,b:Base.
(a = b ∈ EquatePairs(x;n;y;m)
⇐⇒ ↓(a = b ∈ Base)
∨ (((x = a ∈ Base) ∧ (n = b ∈ Base)) ∨ ((x = b ∈ Base) ∧ (n = a ∈ Base)))
∨ (((y = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((y = b ∈ Base) ∧ (m = a ∈ Base)))
∨ ((x = y ∈ Base) ∧ (((n = a ∈ Base) ∧ (m = b ∈ Base)) ∨ ((n = b ∈ Base) ∧ (m = a ∈ Base)))))) supposing
((¬(n = m ∈ Base)) and
(¬(x = m ∈ Base)) and
(¬(y = n ∈ Base)))
Lemma: type-separation
∀x,y:Base.
(((x)↓ ∨ is-exception(x))
⇒ ((y)↓ ∨ is-exception(y))
⇒ (∀n,m:ℤ. ∀T:Type. ((x = n ∈ T) ⇒ (y = m ∈ T) ⇒ (x = y ∈ T)))
⇒ (x = y ∈ Base))
Lemma: polymorphic-choice-int
∀f:⋂A:Type. (A ⟶ A ⟶ A). ((∀x,y:ℤ. ((f x y) = x ∈ ℤ)) ∨ (∀x,y:ℤ. ((f x y) = y ∈ ℤ)))
Lemma: type-with-x=0-y=1
∀x,y:Base. ∃T:Type. ((x = 0 ∈ T) ∧ (y = 1 ∈ T) ∧ ((0 = 1 ∈ T) ⇒ (↓(x = y ∈ Base) ∨ (x = 1 ∈ Base) ∨ (y = 0 ∈ Base))))
Lemma: type-with-y=n
∀n,m:ℤ. ((¬(n = m ∈ ℤ)) ⇒ (∀y:Base. ∃T:Type. ((y = n ∈ T) ∧ (m = m ∈ T) ∧ ((n = m ∈ T) ⇒ (y = m ∈ Base)))))
Lemma: polymorphic-choice-base
∀f:⋂A:Type. (A ⟶ A ⟶ A). ((∀x,y:Base. ((f x y) = x ∈ Base)) ∨ (∀x,y:Base. ((f x y) = y ∈ Base)))
Lemma: polymorphic-choice
∀f:⋂A:Type. (A ⟶ A ⟶ A). ((f = (λx,y. x) ∈ (⋂A:Type. (A ⟶ A ⟶ A))) ∨ (f = (λx,y. y) ∈ (⋂A:Type. (A ⟶ A ⟶ A))))
Lemma: poly-choice-eta-1
∀f:Base. ((∀x,y:Base. ((f x y) = y ∈ Base)) ⇒ (f ~ λx,y. y))
Lemma: not-poly-choice-eta-2
¬(∀f:Base. ((∀x,y:Base. ((f x y) = x ∈ Base)) ⇒ (f ~ λx,y. (f x y))))
Lemma: not-poly-choice-eta-2'
¬(∀f:Base. ((∀x,y:Base. ((f x y) = x ∈ Base)) ⇒ (f ~ λx,y. x)))
Lemma: poly-choice-eta-2
∀f:Base. ((∀x,y:Base. ((f x y) = x ∈ Base)) ⇒ (f ~ λx.if f x is lambda then λy.x otherwise ⊥))
Lemma: polymorphic-choice-base-sq
∀f:Base. ((f ∈ ⋂A:Type. (A ⟶ A ⟶ A)) ⇒ ((f ~ λx.if f x is lambda then λy.x otherwise ⊥) ∨ (f ~ λx,y. y)))
Lemma: polymorphic-choice-sq
∀f:⋂A:Type. (A ⟶ A ⟶ A). ((f ~ λx.if f x is lambda then λy.x otherwise ⊥) ∨ (f ~ λx,y. y))
Lemma: base-is-base-list
∀[T:Type]. ∀[x:Base]. ((x ∈ T List) ⇒ (x ∈ Base List))
Definition: testxx
testxx(x;y)==r if (x =z 0) then y else testxx(x - 1;y) fi
Home
Index