Handling Repeated Constants
Often, a proof will contain the same constant multiple times. When we generalize, the proof should tell us whether these instances of the constant must necessarily be equal for the proof to go through, or whether each instance plays a different role in the proof.
Generalizing Instances Separately
So, in a proof where a constant appears multiple times, the algorithm can determine when to generalize each occurrence separately.
Consider the following proof.
17 + \sqrt{17} \textrm{ is irrational.}
theorem irrat_sum:
Irrational (17 + Real.sqrt (17:ℕ)) :=
⊢ Irrational (17 + √↑17)
/- It suffices to show that `√17` is irrational,
since a natural number plus an irrational is irrational. -/
⊢ Irrational √↑17
/- The rest of the proof shows that √17 is irrational. -/
⊢ ¬∃ a b, a.gcd b = 1 ∧ a * a = 17 * b * b
a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * b⊢ False; have a_div : 17 ∣ a := a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * b⊢ 17 ∣ a a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * b⊢ 17 ∣ ahave c : 17 ∣ a * a := a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * b⊢ 17 ∣ a * a a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * b⊢ 17 ∣ a * aa:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * b⊢ 17 ∣ 17 * (b * b); All goals completed! 🐙}; a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * bc:17 ∣ a ∨ 17 ∣ a⊢ 17 ∣ a; a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * bh✝:17 ∣ a⊢ 17 ∣ aa:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * bh✝:17 ∣ a⊢ 17 ∣ a a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * bh✝:17 ∣ a⊢ 17 ∣ aa:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * bh✝:17 ∣ a⊢ 17 ∣ a All goals completed! 🐙}
a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * ba_div:17 ∣ aa_is_pk:∃ k, a = 17 * k⊢ False
a:ℕb:ℕcopr:a.gcd b = 1h:a * a = 17 * b * ba_div:17 ∣ ak:ℕhk:a = 17 * k⊢ False; a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕh:17 * k * (17 * k) = 17 * b * bhk:a = 17 * k⊢ False; a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕh:17 * b * b = 17 * k * (17 * k)hk:a = 17 * k⊢ False; a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕh:b * b = k * k * 17 ∨ 17 = 0hk:a = 17 * k⊢ False; a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17⊢ False
have b_div : 17 ∣ b := a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17⊢ 17 ∣ b a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17⊢ 17 ∣ bhave c : 17 ∣ b * b := a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17⊢ 17 ∣ b * b a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17⊢ 17 ∣ b * ba:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17⊢ 17 ∣ k * k * 17; All goals completed! 🐙}; a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17c:17 ∣ b ∨ 17 ∣ b⊢ 17 ∣ b; a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17h✝:17 ∣ b⊢ 17 ∣ ba:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17h✝:17 ∣ b⊢ 17 ∣ b a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17h✝:17 ∣ b⊢ 17 ∣ ba:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17h✝:17 ∣ b⊢ 17 ∣ b All goals completed! 🐙}
a:ℕb:ℕcopr:a.gcd b = 1a_div:17 ∣ ak:ℕhk:a = 17 * kh:b * b = k * k * 17b_div:17 ∣ bp_dvd_gcd:17 ∣ a.gcd b⊢ False; a:ℕb:ℕcopr:a.gcd b = 1k:ℕhk:a = 17 * kh:b * b = k * k * 17p_dvd_gcd:17 ∣ a.gcd b⊢ False; a:ℕb:ℕcopr:a.gcd b = 1k:ℕhk:a = 17 * kh:b * b = k * k * 17p_dvd_gcd:17 ∣ 1⊢ False; All goals completed! 🐙
We would not want the generalization to place the primality assumption on both occurences of 17, yielding the overly-specific generalization that p+\sqrt{p} is irrational for any prime p.
Happily, our algorithm yields the stronger generalization:
\textrm{For any natural number }n \textrm{ and prime } p,\\
n+\sqrt{p} \textrm{ is irrational.}
theorem irrat_sum_generalized:
∀ (p : ℕ), Nat.Prime p → ∀ (n : ℕ), Irrational (n + √p) :=
⊢ ∀ (p : ℕ), Nat.Prime p → ∀ (n : ℕ), Irrational (↑n + √↑p)
/- Generalize the `17` in the proof,
then add the generalization `irrat_sum.Gen` as a hypothesis. -/
irrat_sum.Gen:∀ (n : ℕ), Nat.Prime n → ∀ (m : ℕ), Irrational (↑m + √↑n) :=
fun n gen_prime m =>
Irrational.nat_add
(irrat_def n fun a =>
Exists.casesOn a fun a h =>
Exists.casesOn h fun b h =>
And.casesOn h fun copr h =>
let_fun a_div :=
let_fun c :=
Eq.mpr (id (congrArg (fun _a => n ∣ _a) h))
(Eq.mpr (id (congrArg (fun _a => n ∣ _a) (mul_assoc n b b))) (Nat.dvd_mul_right n (b * b)));
Or.casesOn (motive := fun t =>
Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c = t → n ∣ a)
(Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c) (fun h h_1 => h)
(fun h h_1 => h) (Eq.refl (Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c));
let_fun a_is_pk := dvd_iff_exists_eq_mul_right.mp a_div;
Exists.casesOn a_is_pk fun k hk =>
let_fun b_div :=
let_fun c :=
Eq.mpr
(id
(congrArg (fun _a => n ∣ _a)
(Eq.mp
(Eq.trans (congrArg (Or (b * b = k * k * n)) (eq_false (Nat.Prime.ne_zero gen_prime)))
(or_false (b * b = k * k * n)))
(Eq.mp (congrArg (fun _a => b * b = _a ∨ n = 0) (Eq.symm (mul_assoc k k n)))
(Eq.mp (congrArg (fun _a => _a) (propext mul_eq_mul_left_iff))
(Eq.mp (congrArg (fun _a => n * (b * b) = n * (k * _a)) (mul_comm n k))
(Eq.mp (congrArg (fun _a => n * (b * b) = _a) (mul_assoc n k (n * k)))
(Eq.mp (congrArg (fun _a => _a = n * k * (n * k)) (mul_assoc n b b))
(id (Eq.symm (Eq.mp (congrArg (fun _a => _a * _a = n * b * b) hk) h)))))))))))
(Nat.dvd_mul_left n (k * k));
Or.casesOn (motive := fun t =>
Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c = t → n ∣ b)
(Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c) (fun h h_1 => h)
(fun h h_1 => h)
(Eq.refl (Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c));
let_fun p_dvd_gcd := Nat.dvd_gcd_iff.mpr ⟨a_div, b_div⟩;
Nat.Prime.not_dvd_one gen_prime (Eq.mp (congrArg (fun _a => n ∣ _a) copr) p_dvd_gcd))
m⊢ ∀ (p : ℕ), Nat.Prime p → ∀ (n : ℕ), Irrational (↑n + √↑p)
/- Use the generalization to close the goal.-/
All goals completed! 🐙
We can also choose to selectively generalize a particular occurrence of a constant. Below, we only generalize the occurrence of 17 under the square root, yielding the generalization that 17+\sqrt{p} is irrational for any prime p.
theorem irrat_sum_semigeneralized:
∀ (p : ℕ), Nat.Prime p → Irrational (17 + √p) :=
⊢ ∀ (p : ℕ), Nat.Prime p → Irrational (17 + √↑p)
/- Selectively generalize the occurrence of `17` under the square root,
then add the generalization `irrat_sum.Gen` as a hypothesis. -/
irrat_sum.Gen:∀ (n : ℕ), Nat.Prime n → Irrational (↑17 + √↑n) :=
fun n gen_prime =>
Irrational.nat_add
(irrat_def n fun a =>
Exists.casesOn a fun a h =>
Exists.casesOn h fun b h =>
And.casesOn h fun copr h =>
let_fun a_div :=
let_fun c :=
Eq.mpr (id (congrArg (fun _a => n ∣ _a) h))
(Eq.mpr (id (congrArg (fun _a => n ∣ _a) (mul_assoc n b b))) (Nat.dvd_mul_right n (b * b)));
Or.casesOn (motive := fun t =>
Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c = t → n ∣ a)
(Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c) (fun h h_1 => h)
(fun h h_1 => h) (Eq.refl (Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c));
let_fun a_is_pk := dvd_iff_exists_eq_mul_right.mp a_div;
Exists.casesOn a_is_pk fun k hk =>
let_fun b_div :=
let_fun c :=
Eq.mpr
(id
(congrArg (fun _a => n ∣ _a)
(Eq.mp
(Eq.trans (congrArg (Or (b * b = k * k * n)) (eq_false (Nat.Prime.ne_zero gen_prime)))
(or_false (b * b = k * k * n)))
(Eq.mp (congrArg (fun _a => b * b = _a ∨ n = 0) (Eq.symm (mul_assoc k k n)))
(Eq.mp (congrArg (fun _a => _a) (propext mul_eq_mul_left_iff))
(Eq.mp (congrArg (fun _a => n * (b * b) = n * (k * _a)) (mul_comm n k))
(Eq.mp (congrArg (fun _a => n * (b * b) = _a) (mul_assoc n k (n * k)))
(Eq.mp (congrArg (fun _a => _a = n * k * (n * k)) (mul_assoc n b b))
(id (Eq.symm (Eq.mp (congrArg (fun _a => _a * _a = n * b * b) hk) h)))))))))))
(Nat.dvd_mul_left n (k * k));
Or.casesOn (motive := fun t =>
Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c = t → n ∣ b)
(Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c) (fun h h_1 => h)
(fun h h_1 => h)
(Eq.refl (Eq.mp (congrArg (fun _a => _a) (propext (Nat.Prime.dvd_mul gen_prime))) c));
let_fun p_dvd_gcd := Nat.dvd_gcd_iff.mpr ⟨a_div, b_div⟩;
Nat.Prime.not_dvd_one gen_prime (Eq.mp (congrArg (fun _a => n ∣ _a) copr) p_dvd_gcd))
17⊢ ∀ (p : ℕ), Nat.Prime p → Irrational (17 + √↑p)
/- Use the generalization to close the goal.-/
All goals completed! 🐙
Generalizing Instances Together
If different occurrences of a constant play the same role in the proof, the program automatically detects this and generalizes them as the same constant.
For example, consider the following theorem which proves that the number of functions between two sets of size 3 is 3 ^ 3.
\textrm{If } |A| = 3\ \textrm{ and } |B|=3 \textrm{, then } |f:A \to B| = 3^3.
theorem fun_set
{A B : Type} [Fintype A] [Fintype B] [DecidableEq A]
(A_card : Fintype.card A = 3) (B_card : Fintype.card B = 3) :
Fintype.card (A → B) = 3 ^ 3 :=
A:TypeB:Typeinst✝²:Fintype Ainst✝¹:Fintype Binst✝:DecidableEq AA_card:Fintype.card A = 3B_card:Fintype.card B = 3⊢ Fintype.card (A → B) = 3 ^ 3
A:TypeB:Typeinst✝²:Fintype Ainst✝¹:Fintype Binst✝:DecidableEq AA_card:Fintype.card A = 3B_card:Fintype.card B = 3⊢ Fintype.card B ^ Finset.univ.card = 3 ^ 3; All goals completed! 🐙
Generalizing each of the four instances of 3 to a different variable here would yield an incorrect statement. Rather, the cardinality of A is linked to the base of the exponent 3^3, and the cardinality of A is linked to the power of the exponent 3^3. Generalizing all four instances of 3 in this proof creates only two variables, one for each pair of linked occurrences. The result is the generalization that if |A| = n and |B| = m, then the number of functions f : A → B is m^n.
\textrm{Let } n,m \in \mathbb{N}.\\
\textrm{If } |A| = n\ \textrm{ and } |B|=m \textrm{, then } |f: A \to B| = m^n.
theorem fun_set_generalized :
∀ (n m : ℕ)
{A B : Type} [Fintype A] [Fintype B] [DecidableEq A],
Fintype.card A = n → Fintype.card B = m →
Fintype.card (A → B) = m ^ n:=
⊢ ∀ (n m : ℕ) {A B : Type} [inst : Fintype A] [inst_1 : Fintype B] [inst_2 : DecidableEq A],
Fintype.card A = n → Fintype.card B = m → Fintype.card (A → B) = m ^ n
/- Generalize all occurrences of `3` in the proof,
then add the generalization `fun_set.Gen` as a hypothesis. -/
fun_set.Gen:∀ (n m : ℕ) {A B : Type} [inst : Fintype A] [inst_1 : Fintype B] [inst_2 : DecidableEq A],
Fintype.card A = n → Fintype.card B = m → Fintype.card (A → B) = m ^ n :=
fun n m {A B} [Fintype A] [Fintype B] [DecidableEq A] A_card B_card =>
Eq.mpr (id (congrArg (fun _a => _a = m ^ n) Fintype.card_pi))
(Eq.mpr (id (congrArg (fun _a => _a = m ^ n) (Finset.prod_const (Fintype.card B))))
((fun {α β γ} [HPow α β γ] a a_1 e_a =>
Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a ^ a_3 = a_2 ^ a_4)
(fun a_2 a_3 e_a => e_a ▸ Eq.refl (a ^ a_2)) e_a)
(Fintype.card B) m B_card Finset.univ.card n A_card))⊢ ∀ (n m : ℕ) {A B : Type} [inst : Fintype A] [inst_1 : Fintype B] [inst_2 : DecidableEq A],
Fintype.card A = n → Fintype.card B = m → Fintype.card (A → B) = m ^ n
/- Use the generalization to close the goal.-/
All goals completed! 🐙
For details on the technical implementation handling repeated constants, please see the paper "Automatically Generalizing Proofs and Statements." At a high level, the program determines whether two occurrences of a constant play the same role in a proof by replacing both with metavariables, then checking if the two metavariables unify after typechecking the proof (which tries to unify metavariables so that inferred statements in the proof match up with the expected ones).