Handling Dependent Constants
Sometimes when mathematicians generalize a constant c, they generalize not just occurrences of c, but also occurrences of other constants in the proof that depend on c.
An Example from Set Theory
For example, consider the following theorem, which bounds the size of the union of two sets.
\textrm{If } |A| = 2\ \textrm{ and } |B|=2 \textrm{, then } |A \cup B| \leq 4.
theorem union_of_finsets
(α : Type) [Fintype α] [DecidableEq α] (A B : Finset α)
(hA : A.card = 2) (hB : B.card = 2) : (A ∪ B).card ≤ 4 :=
α:Typeinst✝¹:Fintype αinst✝:DecidableEq αA:Finset αB:Finset αhA:A.card = 2hB:B.card = 2⊢ (A ∪ B).card ≤ 4
/- Prove it using the fact that |A ∪ B| + |A ∩ B| = |A| + |B|. -/
All goals completed! 🐙
If we wish to generalize the constant 2, it is not enough just to generalize the instances of 2 itself, since we must also recognise that the constant 4 depends on the two 2s in an important way. Thus, any algorithm that generalizes the 2s in the proof will need to generalize the 4 as well.
The algorithm we present recognizes from a proof of the theorem that the two 2s are "independent" and that the 4 depends on both of them, yielding the following natural generalization.
\textrm{Let } n,m \in \mathbb{N}.\\
\textrm{ If } |A|=n\ \textrm{ and } |B|=m \textrm{, then } |A \cup B| \leq n+m.
theorem union_of_finsets_generalized :
∀ (n m : ℕ)
(α : Type) [Fintype α] [DecidableEq α] (A B : Finset α),
A.card = n → B.card = m → (A ∪ B).card ≤ n+m :=
⊢ ∀ (n m : ℕ) (α : Type) [inst : Fintype α] [inst : DecidableEq α] (A B : Finset α),
A.card = n → B.card = m → (A ∪ B).card ≤ n + m
/- Generalize the `2`s in the proof to `n` and `m`,
which automatically generalizes the 4 to `n+m`. -/
union_of_finsets.Gen:∀ (n m : ℕ) (α : Type) [inst : Fintype α] [inst : DecidableEq α] (A B : Finset α),
A.card = n → B.card = m → (A ∪ B).card ≤ n + m :=
fun n m α [Fintype α] [DecidableEq α] A B hA hB =>
hA ▸ hB ▸ Finset.card_union_add_card_inter A B ▸ Nat.le_add_right (A ∪ B).card (A ∩ B).card⊢ ∀ (n m : ℕ) (α : Type) [inst : Fintype α] [inst : DecidableEq α] (A B : Finset α),
A.card = n → B.card = m → (A ∪ B).card ≤ n + m
/- Use the generalization to close the goal. -/
All goals completed! 🐙
An Example from Graph Theory
We can also use this program on more complicated mathematical objects.
Consider the following theorem.
\textrm{There is no } 4\textrm{-vertex graph}\\
\textrm{with degree sequence } (1,3,3,3).
theorem nonexistent_graph (G : SimpleGraph (Fin 4)) [DecidableRel G.Adj] :
¬(∃ (v : Fin 4), G.degree v = 1 ∧ ∀ w ≠ v, G.degree w = 3) :=
G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adj⊢ ¬∃ v, G.degree v = 1 ∧ ∀ (w : Fin 4), w ≠ v → G.degree w = 3
/- We first show that any vertex with degree 3 is adjacent to all other vertices. -/
G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3⊢ False; have hw_card : (Set.toFinset {w : Fin 4 | w ≠ v}).card = 3 := G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3⊢ {w | w ≠ v}.toFinset.card = 3 G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3⊢ {w | w ≠ v}.toFinset.card = 3G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3⊢ Fintype.card ↑{w | w ≠ v} = 3; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3⊢ Fintype.card (Fin 4) - 1 = 3; rewrite [G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3⊢ 4 - 1 = 3]; All goals completed! 🐙}; have neq_imp_adj : {w | w ≠ v} ⊆ {w | G.Adj v w} := G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3⊢ {w | w ≠ v} ⊆ {w | G.Adj v w} G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3⊢ {w | w ≠ v} ⊆ {w | G.Adj v w}G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3⊢ ∀ (a : Fin 4), a ≠ v → G.Adj v a; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3w:Fin 4wneqv:w ≠ v⊢ G.Adj v w; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3w:Fin 4wneqv:w ≠ v⊢ G.degree w = Fintype.card (Fin 4) - 1G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3w:Fin 4wneqv:w ≠ v⊢ v ≠ w; rewrite [G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3w:Fin 4wneqv:w ≠ v⊢ G.degree w = 4 - 1G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3w:Fin 4wneqv:w ≠ v⊢ v ≠ w]; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3w:Fin 4wneqv:w ≠ v⊢ v ≠ w; All goals completed! 🐙};
/- Therefore, the vertex with degree 1 must be adjacent to at least 3 other vertices.-/
have v_deg_geq : 3 ≤ G.degree v := G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}⊢ 3 ≤ G.degree v G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}⊢ 3 ≤ G.degree vG:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}⊢ 3 ≤ (G.neighborFinset v).card; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}⊢ {w | w ≠ v}.toFinset.card ≤ (G.neighborFinset v).card; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}⊢ {w | w ≠ v}.toFinset ⊆ G.neighborFinset v; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}⊢ {w | w ≠ v}.toFinset ⊆ (G.neighborSet v).toFinset; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}⊢ {w | w ≠ v}.toFinset ⊆ {w | G.Adj v w}.toFinset; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}⊢ {w | w ≠ v} ⊆ {w | G.Adj v w}; All goals completed! 🐙}; G:SimpleGraph (Fin 4)inst✝:DecidableRel G.Adjv:Fin 4v_deg:G.degree v = 1w_deg:∀ (w : Fin 4), w ≠ v → G.degree w = 3hw_card:{w | w ≠ v}.toFinset.card = 3neq_imp_adj:{w | w ≠ v} ⊆ {w | G.Adj v w}v_deg_geq:3 ≤ 1⊢ False;
/- But, we know the vertex with degree 1 can be adjacent to at most 1 other vertex. Contradiction.-/
All goals completed! 🐙
Our program recognizes that the 4 is a function of the 3, and so if we generalize 4 to n, we must generalize the 3 to n-1. Note that the outputted generalization isolates the condition that n > 2, since the graph in the n=2 case has degree sequence (1,1), which does actually exist.
\textrm{For } n > 2, \textrm{there is no } n\textrm{-vertex graph}\\
\textrm{with degree sequence } (1,n-1, \dots, n-1).
theorem nonexistent_graph_generalized :
∀ (n : ℕ), 2 < n → ∀ (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
¬(∃ v, G.degree v = 1 ∧ ∀ (w : Fin n), w ≠ v → G.degree w = n - 1) :=
⊢ ∀ (n : ℕ),
2 < n →
∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj],
¬∃ v, G.degree v = 1 ∧ ∀ (w : Fin n), w ≠ v → G.degree w = n - 1
n:ℕhn:2 < n⊢ ∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj],
¬∃ v, G.degree v = 1 ∧ ∀ (w : Fin n), w ≠ v → G.degree w = n - 1
/- Generalize the `4` in the proof to `n`,
which automatically generalizes the `3`s to `n-1`. -/
n:ℕhn:2 < nnonexistent_graph.Gen:∀ (n : ℕ),
1 < n - 1 →
∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj],
(∃ v, G.degree v = 1 ∧ ∀ (w : Fin n), w ≠ v → G.degree w = n - 1) → False :=
fun n gen_one G [DecidableRel G.Adj] a =>
Exists.casesOn a fun v h =>
And.casesOn h fun v_deg w_deg =>
let_fun hw_card :=
Eq.mpr (id (congrArg (fun _a => _a = n - 1) (Set.toFinset_card {w | w ≠ v})))
(Eq.mpr (id (congrArg (fun _a => _a = n - 1) (Set.card_ne_eq v)))
(Eq.mpr (id (congrArg (fun _a => _a - 1 = n - 1) (Fintype.card_fin n))) (Eq.refl (n - 1))));
let_fun neq_imp_adj :=
Eq.mpr (id (congrArg (fun _a => _a) (propext Set.setOf_subset_setOf))) fun w wneqv =>
max_deg_imp_adj_all
(Eq.mpr (id (congrArg (fun _a => G.degree w = _a - 1) (Fintype.card_fin n))) (w_deg w wneqv)) v
(Ne.symm wneqv);
let_fun v_deg_geq :=
Eq.mpr (id (congrArg (fun _a => n - 1 ≤ _a) (Eq.symm (SimpleGraph.card_neighborFinset_eq_degree G v))))
(Eq.mpr (id (congrArg (fun _a => _a ≤ (G.neighborFinset v).card) (Eq.symm hw_card)))
(Finset.card_le_card
(id (id (Eq.mpr (id (congrArg (fun _a => _a) (propext Set.toFinset_subset_toFinset))) neq_imp_adj)))));
Nat.not_lt.mpr (Eq.mp (congrArg (fun _a => n - 1 ≤ _a) v_deg) v_deg_geq) gen_one⊢ ∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj],
¬∃ v, G.degree v = 1 ∧ ∀ (w : Fin n), w ≠ v → G.degree w = n - 1
/- Use the generalization to close the goal. -/
All goals completed! 🐙
For details on the technical implementation of this dependence-detection, please see the paper "Automatically Generalizing Proofs and Statements." At a high level, the program determines when one constant is a function of another by replacing each constant with metavariables, and if a typechecking conflict arises in the proof, the program uses the antiunifier of the conflicting expressions to determine the function that relates the two constants.