3. The Digit Layer
This chapter contains all the digit-level arithmetic of the proof. The infinitude of both residue classes is the only place Dirichlet's theorem on primes in arithmetic progressions enters; the eventual-periodicity argument is a self-contained binary-tail argument that deliberately dodges any general "rational iff eventually periodic digits" library, which Mathlib does not currently have.
Theorembits_infinite_ones
The set \{k \mid b_k = 1\} is infinite.
Lean code for Theorem bits_infinite_ones
-
≈
theorem bits_infinite_ones : {k | bit k = 1}.Infinite
theorem bits_infinite_ones : {k | bit k = 1}.Infinite
By Dirichlet's theorem at modulus 4 — in Mathlib's form, the primes \equiv 3 \pmod 4
form an infinite set — infinitely many primes lie in the class 3 \bmod 4. These transfer to
bit indices along the injection sending a prime p to the number of primes below p, minus
one; its inverse is the odd-prime enumeration k \mapsto p_k, and 2 is excluded since
2 \not\equiv 3 \pmod 4. So infinitely many indices k have p_k \equiv 3 \pmod 4, i.e.
b_k = 1. \blacksquare
≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.
haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
where `_` stands for the tactics that follow this one.
It is convenient for types that have only one applicable constructor.
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
which adds the equation `h : e = pat` to the local context.
The tactic supports all the same syntax variants and options as the `have` term.
## Properties and relations
* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
which may be important for performance reasons.
Consider using the equivalent `let +nondep` to indicate the intent.
hidx := infinite_oddPrime_index infinite_primes_three_mod_four
(fun p hp ↦ hp.1) (fun h ↦ absurd h.2 (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. decide`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
and then reducing that instance to evaluate the truth value of `p`.
If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
The target is not allowed to contain local variables or metavariables.
If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target,
or you can use the `+revert` option, described below.
Options:
- `decide +revert` begins by reverting local variables that the target depends on,
after cleaning up the local context of irrelevant variables.
A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
or if it is a proposition that refers to a relevant variable.
- `decide +kernel` uses kernel for reduction instead of the elaborator.
It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything,
and (2) it reduces the `Decidable` instance only once instead of twice.
- `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance,
admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
of the trusted code base.
Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute.
Like with `+kernel`, the `Decidable` instance is evaluated only once.
Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term,
`Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs.
Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms.
These can appear in instances defined using tactics (such as `rw` and `simp`).
To avoid this, create such instances using definitions such as `decidable_of_iff` instead.
## Examples
Proving inequalities:
```lean
example : 2 + 2 ≠ 5 := by decide
```
Trying to prove a false proposition:
```lean
example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
1 ≠ 1
is false
-/
```
Trying to prove a proposition whose `Decidable` instance fails to reduce
```lean
opaque unknownProp : Prop
open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
unknownProp
since its 'Decidable' instance reduced to
Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/
```
## Properties and relations
For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
```lean
example : 1 + 1 = 2 := by decide
example : 1 + 1 = 2 := by rfl
```
))
refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
hidx.mono fun k hk ↦ ?_
exact`exact e` closes the main goal if its target type matches that of `e`.
bit_eq_one_iff.mpr hk.2
Theorembits_infinite_zeros
The set \{k \mid b_k = 0\} is infinite. Together with the previous theorem: the digit
sequence is neither eventually all ones nor eventually all zeros, which is exactly what the
eventual-periodicity argument needs to keep the binary tails strictly between 0 and 1.
Lean code for Theorem bits_infinite_zeros
-
≈
theorem bits_infinite_zeros : {k | bit k = 0}.Infinite
theorem bits_infinite_zeros : {k | bit k = 0}.Infinite
The same argument as the previous theorem, applied to the residue class 1 \bmod 4:
Dirichlet's theorem supplies infinitely many primes \equiv 1 \pmod 4, the odd-prime
enumeration injects them into the index set, and for such an index k, p_k \equiv 1 \pmod 4
is in particular \not\equiv 3 \pmod 4, so b_k = 0. \blacksquare
≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.
haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
where `_` stands for the tactics that follow this one.
It is convenient for types that have only one applicable constructor.
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
which adds the equation `h : e = pat` to the local context.
The tactic supports all the same syntax variants and options as the `have` term.
## Properties and relations
* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
which may be important for performance reasons.
Consider using the equivalent `let +nondep` to indicate the intent.
hidx := infinite_oddPrime_index infinite_primes_one_mod_four
(fun p hp ↦ hp.1) (fun h ↦ absurd h.2 (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. decide`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`
and then reducing that instance to evaluate the truth value of `p`.
If it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.
The target is not allowed to contain local variables or metavariables.
If there are local variables, you can first try using the `revert` tactic with these local variables to move them into the target,
or you can use the `+revert` option, described below.
Options:
- `decide +revert` begins by reverting local variables that the target depends on,
after cleaning up the local context of irrelevant variables.
A variable is *relevant* if it appears in the target, if it appears in a relevant variable,
or if it is a proposition that refers to a relevant variable.
- `decide +kernel` uses kernel for reduction instead of the elaborator.
It has two key properties: (1) since it uses the kernel, it ignores transparency and can unfold everything,
and (2) it reduces the `Decidable` instance only once instead of twice.
- `decide +native` uses the native code compiler (`#eval`) to evaluate the `Decidable` instance,
admitting the result via an axiom. This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
This can be significantly more efficient than using reduction, but it is at the cost of increasing the size
of the trusted code base.
Namely, it depends on the correctness of the Lean compiler and all definitions with an `@[implemented_by]` attribute.
Like with `+kernel`, the `Decidable` instance is evaluated only once.
Limitation: In the default mode or `+kernel` mode, since `decide` uses reduction to evaluate the term,
`Decidable` instances defined by well-founded recursion might not work because evaluating them requires reducing proofs.
Reduction can also get stuck on `Decidable` instances with `Eq.rec` terms.
These can appear in instances defined using tactics (such as `rw` and `simp`).
To avoid this, create such instances using definitions such as `decidable_of_iff` instead.
## Examples
Proving inequalities:
```lean
example : 2 + 2 ≠ 5 := by decide
```
Trying to prove a false proposition:
```lean
example : 1 ≠ 1 := by decide
/-
tactic 'decide' proved that the proposition
1 ≠ 1
is false
-/
```
Trying to prove a proposition whose `Decidable` instance fails to reduce
```lean
opaque unknownProp : Prop
open scoped Classical in
example : unknownProp := by decide
/-
tactic 'decide' failed for proposition
unknownProp
since its 'Decidable' instance reduced to
Classical.choice ⋯
rather than to the 'isTrue' constructor.
-/
```
## Properties and relations
For equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.
```lean
example : 1 + 1 = 2 := by decide
example : 1 + 1 = 2 := by rfl
```
))
refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
hidx.mono fun k hk ↦ ?_
haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
where `_` stands for the tactics that follow this one.
It is convenient for types that have only one applicable constructor.
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
which adds the equation `h : e = pat` to the local context.
The tactic supports all the same syntax variants and options as the `have` term.
## Properties and relations
* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
which may be important for performance reasons.
Consider using the equivalent `let +nondep` to indicate the intent.
h1 : oddPrime k % 4 = 1 := hk.2
exact`exact e` closes the main goal if its target type matches that of `e`.
bit_eq_zero_iff.mpr (by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.
We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
)
TheoremeventuallyPeriodic_of_not_irrational
If \varrho is not irrational, then the bit sequence is eventually periodic: there
exist N and P > 0 with b_{k+P} = b_k for all k \ge N.
Lean code for Theorem eventuallyPeriodic_of_not_irrational
-
≈
theorem eventuallyPeriodic_of_not_irrational : ¬ Irrational ϱ → ∃ N P, 0 < P ∧ ∀ k ≥ N, bit (k + P) = bit k
theorem eventuallyPeriodic_of_not_irrational : ¬ Irrational ϱ → ∃ N P, 0 < P ∧ ∀ k ≥ N, bit (k + P) = bit k
Define the binary tails t_k := \sum_{j \ge 0} b_{k+j}\, 2^{-(j+1)}, so that t_0 = \varrho;
the argument runs through the tails, in the Lean file's zero-based indexing.
First, t_k \in (0,1) strictly for every k: infinitely many later ones force
t_k > 0, and infinitely many later zeros force t_k < 1. Next, the recurrence
t_k = (b_k + t_{k+1})/2 holds by splitting off the first term of the tail, so if b_k = 1
then t_k \in (1/2, 1) and if b_k = 0 then t_k \in (0, 1/2). In particular
t_k \ne 1/2 always, so t_k determines b_k (b_k = 1 \iff t_k > 1/2) and hence
also t_{k+1} = 2 t_k - b_k.
Because 2^k \varrho is an integer plus t_k and t_k \in (0,1), we have
t_k = \operatorname{fract}(2^k \varrho). If \varrho is rational with denominator b,
then each t_k = \operatorname{fract}(2^k \varrho) lies in the finite set
\{0, 1/b, \ldots, (b-1)/b\} — in Lean, the denominator of the rational witness produced by
unfolding "not irrational" — so by pigeonhole there are m < n with t_m = t_n. Since
t_k determines both b_k and t_{k+1}, induction propagates the collision:
t_{m+i} = t_{n+i} and b_{m+i} = b_{n+i} for all i \ge 0. Hence the bits are periodic
with period P = n - m from index m. \blacksquare
≈by`by tac` constructs a term of the expected type by running the tactic(s) `tac`.
introIntroduces one or more hypotheses, optionally naming and/or pattern-matching them.
For each hypothesis to be introduced, the remaining main goal's target type must
be a `let` or function type.
* `intro` by itself introduces one anonymous hypothesis, which can be accessed
by e.g. `assumption`. It is equivalent to `intro _`.
* `intro x y` introduces two hypotheses and names them. Individual hypotheses
can be anonymized via `_`, given a type ascription, or matched against a pattern:
```lean
-- ... ⊢ α × β → ...
intro (a, b)
-- ..., a : α, b : β ⊢ ...
```
* `intro rfl` is short for `intro h; subst h`, if `h` is an equality where the left-hand or right-hand side
is a variable.
* Alternatively, `intro` can be combined with pattern matching much like `fun`:
```lean
intro
| n + 1, 0 => tac
| ...
```
h
obtainThe `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.
```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```
If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.
If `type` is omitted, `:= proof` is required.
⟨m, n, hmn, ht⟩ := exists_t_collision h
refine`refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
⟨m, n - m, by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.
We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
, fun k hk ↦ ?_⟩
obtainThe `obtain` tactic is a combination of `have` and `rcases`. See `rcases` for
a description of supported patterns.
```lean
obtain ⟨patt⟩ : type := proof
```
is equivalent to
```lean
have h : type := proof
rcases h with ⟨patt⟩
```
If `⟨patt⟩` is omitted, `rcases` will try to infer the pattern.
If `type` is omitted, `:= proof` is required.
⟨i, rfl⟩ : ∃ i, k = m + i := ⟨k - m, by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.
We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
⟩
haveThe `have` tactic is for adding opaque definitions and hypotheses to the local context of the main goal.
The definitions forget their associated value and cannot be unfolded, unlike definitions added by the `let` tactic.
* `have h : t := e` adds the hypothesis `h : t` if `e` is a term of type `t`.
* `have h := e` uses the type of `e` for `t`.
* `have : t := e` and `have := e` use `this` for the name of the hypothesis.
* `have pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
where `_` stands for the tactics that follow this one.
It is convenient for types that have only one applicable constructor.
For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the
hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`.
* The syntax `have (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
which adds the equation `h : e = pat` to the local context.
The tactic supports all the same syntax variants and options as the `have` term.
## Properties and relations
* It is not possible to unfold a variable introduced using `have`, since the definition's value is forgotten.
The `let` tactic introduces definitions that can be unfolded.
* The `have h : t := e` is like doing `let h : t := e; clear_value h`.
* The `have` tactic is preferred for propositions, and `let` is preferred for non-propositions.
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
which may be important for performance reasons.
Consider using the equivalent `let +nondep` to indicate the intent.
hbi : bit (m + i) = bit (n + i) := bit_eq_of_t_eq (t_eq_add ht i)
rw`rw` is like `rewrite`, but also tries to close the goal by "cheap" (reducible) `rfl` afterwards.
[show m + i + (n - m) = n + i from by`by tac` constructs a term of the expected type by running the tactic(s) `tac`. omegaThe `omega` tactic, for resolving integer and natural linear arithmetic problems.
It is not yet a full decision procedure (no "dark" or "grey" shadows),
but should be effective on many problems.
We handle hypotheses of the form `x = y`, `x < y`, `x ≤ y`, and `k ∣ x` for `x y` in `Nat` or `Int`
(and `k` a literal), along with negations of these statements.
We decompose the sides of the inequalities as linear combinations of atoms.
If we encounter `x / k` or `x % k` for literal integers `k` we introduce new auxiliary variables
and the relevant inequalities.
On the first pass, we do not perform case splits on natural subtraction.
If `omega` fails, we recursively perform a case split on
a natural subtraction appearing in a hypothesis, and try again.
The options
```
omega +splitDisjunctions +splitNatSub +splitNatAbs +splitMinMax
```
can be used to:
* `splitDisjunctions`: split any disjunctions found in the context,
if the problem is not otherwise solvable.
* `splitNatSub`: for each appearance of `((a - b : Nat) : Int)`, split on `a ≤ b` if necessary.
* `splitNatAbs`: for each appearance of `Int.natAbs a`, split on `0 ≤ a` if necessary.
* `splitMinMax`: for each occurrence of `min a b`, split on `min a b = a ∨ min a b = b`
Currently, all of these are on by default.
, ← hbi]