The following is a simple proof that 2
cannot be expressed as the ratio of two integers; that is, for every two integers
p and q,
(p/q)2 ≠ 2.
This is a simplified version of a similar
proof by Milad Niqui.
Use Alt+↓/↑ to step through the proof,
and observe the proof state on the right panel.
First, we simplify the goal a bit by inlining the
definition of ⃞2.
The gist of the proof is realizing that it can be obtained by
instantiating the induction hypothesis with values
3q–2p and
3p–4q.
The rest follows from simpler inequalities,
2p < 3q
< 2p+q
and
4q < 3p.
These are not included in the example; for details, see
the full proof below.
Special thanks to Karl Palmskog for
writing up this version.
sqrt_2
Irrationality of the square root of two
The original problem on the square root of two arose when
comparing the side with the diagonal of a square,
which reduces to considering an isosceles right triangle.
Below, we prove a statement in Coq of the irrationality
of the square root of two that is expressed only in terms
of natural numbers (Coq's nat). The proof is a simplified
version of a proof by Milad Niqui.
We begin by loading results on arithmetic on natural numbers,
and the lia arithmetic solver tactic.
FromCoqRequireImportUtf8ArithLia.
Arithmetic utility results
Lemmalt_monotonic_inverse : forallf : nat -> nat,
(forallxy : nat, x < y -> fx < fy) -> forallxy : nat, fx < fy -> x < y. Proof. introsfHmonxyHlt; case (le_gt_decyx); auto. introsHle; elim (le_lt_or_eq__Hle). introsHlt'; elim (lt_asym__Hlt); applyHmon; auto. introsHeq; elim (Nat.lt_neq__Hlt); rewriteHeq; auto. Qed.
The lia tactic easily proves linear arithmetic statements.
Lemmasub_square_identity : forallab : nat, b <= a -> (a - b) * (a - b) = a * a + b * b - 2 * (a * b). Proof. introsabH. rewrite <- (Nat.sub_addbaH). lia. Qed.
Lemmaroot_monotonic : forallxy : nat, x * x < y * y -> x < y. Proof. apply (lt_monotonic_inverse (funx => x * x)). applyNat.square_lt_mono. Qed.
Lemmasquare_recompose : forallxy : nat, x * y * (x * y) = x * x * (y * y). Proof. lia. Qed.
Key arithmetic lemmas
Sectionsqrt2_decrease.
We use sections to simplify lemmas that use the same assumptions.
After the `End` command, lemmas inside the section are generalized
with the variables and hypotheses they depend on.
Endsqrt2_decrease.
The Main Action: Statement and Proof
The proof proceeds by well-founded induction on q.
We apply the induction hypothesis with the numbers 3 * q - 2 * p
and 3 * p - 4 * q. This leaves two key proof goals:
3 * q - 2 * p <> 0, which we prove using arithmetic and the
comparison2 lemma above.
(3 * p - 4 * q) * (3 * p - 4 * q) = 2 * ((3 * q - 2 * p) * (3 * q - 2 * p)),
which we prove using the new_equality lemma above.