Generalizing Higher-Order Constants

Since both our algorithm and its predecessor assume type-theoretic foundations, generalizing constants like \mathbb{ℤ} (integers) or + (addition) works just as well as generalizing numerical constants.

Generalizing Integer Addition

As an example, consider the following result proving left-cancellation on the integers from more basic axioms.

\textrm{For any } a,b,c \in ℤ, \textrm{ if } a+b=a+c, \textrm{ then } b=c.

theorem Int.left_cancellation (a b c : ℤ) (h : a + b = a + c) : b = c := a:ℤb:ℤc:ℤh:a + b = a + c⊢ b = c /- Add '-a' to both sides. -/ replace h : -a + (a + b) = -a + (a + c) := a:ℤb:ℤc:ℤh:a + b = a + c⊢ b = c All goals completed! 🐙 /- Apply associativity and cancel. -/ rwa [← Int.add_assoc, Int.add_left_neg, ← Int.add_assoc, Int.add_left_neg, Int.zero_add, a:ℤb:ℤc:ℤh:b = c⊢ b = ca:ℤb:ℤc:ℤh:b = c⊢ b = c at h

We prove it by adding -a to both sides (on the left), applying associativity, noting that a+-a=0, and using the fact that 0 is an additive identity.

Our program will recognize that each step of the argument works just as well in an arbitrary semigroup with an identity and left inverse, so in fact the proof gives the following result.

\textrm{Let } (G, \cdot) \textrm{ be a semigroup with an identity and left inverse.}\\ \textrm{For any } a,b,c \in G, \textrm{ if } a \cdot b=a \cdot c, \textrm{ then } b=c.

example : ∀ (G : Type) -- If you have an arbitrary set [inverse : Neg G] -- with a symbol representing the inverse, (e : G) -- and a symbol representing the identity, (f : G → G → G), -- and a binary operation (∀ (a : G), f e a = a) → -- s.t. the identity element is left-neutral w.r.t. the operation (∀ (a : G), f (-a) a = e) → -- and every element has a left inverse under the operation (∀ (a b c : G), f (f a b) c = f a (f b c)) → -- and the operation is associative, ∀ (a b c : G), f a b = f a c → b = c -- then the operation is left-cancellative. := ⊢ ∀ (G : Type) [inverse : Neg G] (e : G) (f : G → G → G), (∀ (a : G), f e a = a) → (∀ (a : G), f (-a) a = e) → (∀ (a b c : G), f (f a b) c = f a (f b c)) → ∀ (a b c : G), f a b = f a c → b = c /- Generalize addition to an arbitrary binary operation. -/ Int.left_cancellation.Gen:∀ (f : ℤ → ℤ → ℤ), (∀ (a : ℤ), f 0 a = a) → (∀ (a : ℤ), f (-a) a = 0) → (∀ (a b c : ℤ), f (f a b) c = f a (f b c)) → ∀ (a b c : ℤ), f a b = f a c → b = c := fun f gen_zero gen_add gen_add_1 a b c h => let_fun h := Eq.mpr (id (congrArg (fun _a => f (-a) _a = f (-a) (f a c)) h)) (Eq.refl (f (-a) (f a c))); Eq.mp (congrArg (fun _a => b = _a) (gen_zero c)) (Eq.mp (congrArg (fun _a => _a = f 0 c) (gen_zero b)) (Eq.mp (congrArg (fun _a => f 0 b = f _a c) (gen_add a)) (Eq.mp (congrArg (fun _a => f 0 b = _a) (Eq.symm (gen_add_1 (-a) a c))) (Eq.mp (congrArg (fun _a => f _a b = f (-a) (f a c)) (gen_add a)) (Eq.mp (congrArg (fun _a => _a = f (-a) (f a c)) (Eq.symm (gen_add_1 (-a) a b))) h)))))⊢ ∀ (G : Type) [inverse : Neg G] (e : G) (f : G → G → G), (∀ (a : G), f e a = a) → (∀ (a : G), f (-a) a = e) → (∀ (a b c : G), f (f a b) c = f a (f b c)) → ∀ (a b c : G), f a b = f a c → b = c /- Generalize 0 to an arbitrary identity element. -/ Int.left_cancellation.Gen:∀ (f : ℤ → ℤ → ℤ), (∀ (a : ℤ), f 0 a = a) → (∀ (a : ℤ), f (-a) a = 0) → (∀ (a b c : ℤ), f (f a b) c = f a (f b c)) → ∀ (a b c : ℤ), f a b = f a c → b = c := fun f gen_zero gen_add gen_add_1 a b c h => let_fun h := Eq.mpr (id (congrArg (fun _a => f (-a) _a = f (-a) (f a c)) h)) (Eq.refl (f (-a) (f a c))); Eq.mp (congrArg (fun _a => b = _a) (gen_zero c)) (Eq.mp (congrArg (fun _a => _a = f 0 c) (gen_zero b)) (Eq.mp (congrArg (fun _a => f 0 b = f _a c) (gen_add a)) (Eq.mp (congrArg (fun _a => f 0 b = _a) (Eq.symm (gen_add_1 (-a) a c))) (Eq.mp (congrArg (fun _a => f _a b = f (-a) (f a c)) (gen_add a)) (Eq.mp (congrArg (fun _a => _a = f (-a) (f a c)) (Eq.symm (gen_add_1 (-a) a b))) h)))))Int.left_cancellation.Gen.Gen:∀ (e : ℤ) (f : ℤ → ℤ → ℤ), (∀ (a : ℤ), f e a = a) → (∀ (a : ℤ), f (-a) a = e) → (∀ (a b c : ℤ), f (f a b) c = f a (f b c)) → ∀ (a b c : ℤ), f a b = f a c → b = c := fun e f gen_zero gen_add gen_add_1 a b c h => let_fun h := Eq.mpr (id (congrArg (fun _a => f (-a) _a = f (-a) (f a c)) h)) (Eq.refl (f (-a) (f a c))); Eq.mp (congrArg (fun _a => b = _a) (gen_zero c)) (Eq.mp (congrArg (fun _a => _a = f e c) (gen_zero b)) (Eq.mp (congrArg (fun _a => f e b = f _a c) (gen_add a)) (Eq.mp (congrArg (fun _a => f e b = _a) (Eq.symm (gen_add_1 (-a) a c))) (Eq.mp (congrArg (fun _a => f _a b = f (-a) (f a c)) (gen_add a)) (Eq.mp (congrArg (fun _a => _a = f (-a) (f a c)) (Eq.symm (gen_add_1 (-a) a b))) h)))))⊢ ∀ (G : Type) [inverse : Neg G] (e : G) (f : G → G → G), (∀ (a : G), f e a = a) → (∀ (a : G), f (-a) a = e) → (∀ (a b c : G), f (f a b) c = f a (f b c)) → ∀ (a b c : G), f a b = f a c → b = c /- Generalize ℤ to an arbitrary semigroup. -/ Int.left_cancellation.Gen:∀ (f : ℤ → ℤ → ℤ), (∀ (a : ℤ), f 0 a = a) → (∀ (a : ℤ), f (-a) a = 0) → (∀ (a b c : ℤ), f (f a b) c = f a (f b c)) → ∀ (a b c : ℤ), f a b = f a c → b = c := fun f gen_zero gen_add gen_add_1 a b c h => let_fun h := Eq.mpr (id (congrArg (fun _a => f (-a) _a = f (-a) (f a c)) h)) (Eq.refl (f (-a) (f a c))); Eq.mp (congrArg (fun _a => b = _a) (gen_zero c)) (Eq.mp (congrArg (fun _a => _a = f 0 c) (gen_zero b)) (Eq.mp (congrArg (fun _a => f 0 b = f _a c) (gen_add a)) (Eq.mp (congrArg (fun _a => f 0 b = _a) (Eq.symm (gen_add_1 (-a) a c))) (Eq.mp (congrArg (fun _a => f _a b = f (-a) (f a c)) (gen_add a)) (Eq.mp (congrArg (fun _a => _a = f (-a) (f a c)) (Eq.symm (gen_add_1 (-a) a b))) h)))))Int.left_cancellation.Gen.Gen:∀ (e : ℤ) (f : ℤ → ℤ → ℤ), (∀ (a : ℤ), f e a = a) → (∀ (a : ℤ), f (-a) a = e) → (∀ (a b c : ℤ), f (f a b) c = f a (f b c)) → ∀ (a b c : ℤ), f a b = f a c → b = c := fun e f gen_zero gen_add gen_add_1 a b c h => let_fun h := Eq.mpr (id (congrArg (fun _a => f (-a) _a = f (-a) (f a c)) h)) (Eq.refl (f (-a) (f a c))); Eq.mp (congrArg (fun _a => b = _a) (gen_zero c)) (Eq.mp (congrArg (fun _a => _a = f e c) (gen_zero b)) (Eq.mp (congrArg (fun _a => f e b = f _a c) (gen_add a)) (Eq.mp (congrArg (fun _a => f e b = _a) (Eq.symm (gen_add_1 (-a) a c))) (Eq.mp (congrArg (fun _a => f _a b = f (-a) (f a c)) (gen_add a)) (Eq.mp (congrArg (fun _a => _a = f (-a) (f a c)) (Eq.symm (gen_add_1 (-a) a b))) h)))))Int.left_cancellation.Gen.Gen.Gen:∀ (G : Type) (gen_instNegInt : Neg G) (e : G) (f : G → G → G), (∀ (a : G), f e a = a) → (∀ (a : G), f (-a) a = e) → (∀ (a b c : G), f (f a b) c = f a (f b c)) → ∀ (a b c : G), f a b = f a c → b = c := fun G gen_instNegInt e f gen_zero gen_add gen_add_1 a b c h => let_fun h := Eq.mpr (id (congrArg (fun _a => f (-a) _a = f (-a) (f a c)) h)) (Eq.refl (f (-a) (f a c))); Eq.mp (congrArg (fun _a => b = _a) (gen_zero c)) (Eq.mp (congrArg (fun _a => _a = f e c) (gen_zero b)) (Eq.mp (congrArg (fun _a => f e b = f _a c) (gen_add a)) (Eq.mp (congrArg (fun _a => f e b = _a) (Eq.symm (gen_add_1 (-a) a c))) (Eq.mp (congrArg (fun _a => f _a b = f (-a) (f a c)) (gen_add a)) (Eq.mp (congrArg (fun _a => _a = f (-a) (f a c)) (Eq.symm (gen_add_1 (-a) a b))) h)))))⊢ ∀ (G : Type) [inverse : Neg G] (e : G) (f : G → G → G), (∀ (a : G), f e a = a) → (∀ (a : G), f (-a) a = e) → (∀ (a b c : G), f (f a b) c = f a (f b c)) → ∀ (a b c : G), f a b = f a c → b = c /- Use the generalization to close the goal. -/ All goals completed! 🐙

Thus, by generalizing the constants +, 0, and \mathbb{Z}, the algorithm has found that the conclusion holds in a semigroup with an identity and left inverses. Importantly, the algorithm does not need to have prior knowledge of these more abstract concepts: it discovers the abstractions for itself.

Generalizing ℤ in Bézout's Identity

A more complicated example of this kind is provided by Bézout's identity from elementary number theory. Our algorithm is capable of generalizing the non-numerical constant \mathbb{Z} in a standard proof of this theorem.

\textrm{Let } x,y \in \mathbb{Z}, \textrm{ where } y \neq 0.\\ \textrm{There exist } h,k \in \mathbb{Z} \textrm{ such that } hx + ky = \gcd(x,y).

bezout_identity : ∀ (x y : ℤ), y ≠ 0 → ∃ h k, isGCD (h * x + k * y) x y#check (bezout_identity : ∀ x y : ℤ, y ≠ 0 → ∃ h k, isGCD (h * x + k * y) x y)

Generalizing the integers in this proof produces a definition broadly similar to that of a Euclidean domain from ring theory, i.e. roughly speaking, an integral domain with a measure of size that allows one to run the Euclidean algorithm and guarantees that it will terminate.

example := ⊢ ∀ (R : Type) (gen_instOfNat : {n : ℕ} → OfNat R n) (gen_instAddGroup : AddGroup R) (gen_instMul : Mul R) (gen_instDvd : Dvd R), (∀ (a b c : R), a + b + c = a + (b + c)) → (∀ (a b c : R), a + (b + c) = b + (a + c)) → (∀ (a b c : R), (a + b) * c = a * c + b * c) → (∀ (a b c : R), a * (b + c) = a * b + a * c) → (∀ (a b c : R), a * b * c = a * (b * c)) → ∀ (gen_natAbs : R → ℕ), (∀ (a : R), 0 * a = 0) → (∀ (a : R), 1 * a = a) → (∀ (a : R), 0 + a = a) → (∀ {a : R}, gen_natAbs a = 0 ↔ a = 0) → ∀ (gen_instDiv : Div R) (gen_instMod : Mod R), (∀ (a b : R), a / b * b + a % b = a) → ∀ (gen_instNegInt : Neg R), (∀ (a b : R), -(a * b) = -a * b) → (∀ (a : R) {b : R}, gen_natAbs b ≠ 0 → gen_natAbs (a % b) < gen_natAbs b) → (∀ (a : R), a + 0 = a) → (∀ (a b : R), b ∣ a * b) → (∀ (a b : R), (a ∣ b) = ∃ c, b = a * c) → (∀ (a b c : R), a * (b * c) = b * (a * c)) → ∀ (x y : R), y ≠ 0 → ∃ h k, isGCD (h * x + k * y) x y /- Generalize ℤ in Bezout's identity -/ bezout_identity.Gen:∀ (R : Type) (gen_instOfNat : {n : ℕ} → OfNat R n) (gen_instAddGroup : AddGroup R) (gen_instMul : Mul R) (gen_instDvd : Dvd R), (∀ (a b c : R), a + b + c = a + (b + c)) → (∀ (a b c : R), a + (b + c) = b + (a + c)) → (∀ (a b c : R), (a + b) * c = a * c + b * c) → (∀ (a b c : R), a * (b + c) = a * b + a * c) → (∀ (a b c : R), a * b * c = a * (b * c)) → ∀ (gen_natAbs : R → ℕ), (∀ (a : R), 0 * a = 0) → (∀ (a : R), 1 * a = a) → (∀ (a : R), 0 + a = a) → (∀ {a : R}, gen_natAbs a = 0 ↔ a = 0) → ∀ (gen_instDiv : Div R) (gen_instMod : Mod R), (∀ (a b : R), a / b * b + a % b = a) → ∀ (gen_instNegInt : Neg R), (∀ (a b : R), -(a * b) = -a * b) → (∀ (a : R) {b : R}, gen_natAbs b ≠ 0 → gen_natAbs (a % b) < gen_natAbs b) → (∀ (a : R), a + 0 = a) → (∀ (a b : R), b ∣ a * b) → (∀ (a b : R), (a ∣ b) = ∃ c, b = a * c) → (∀ (a b c : R), a * (b * c) = b * (a * c)) → ∀ (x y : R), y ≠ 0 → ∃ h k, isGCD (h * x + k * y) x y := fun R gen_instOfNat gen_instAddGroup gen_instMul gen_instDvd gen_add gen_add_1 gen_add_2 gen_mul gen_mul_1 gen_natAbs gen_zero gen_one gen_zero_1 gen_natAbs_1 gen_instDiv gen_instMod gen_ediv gen_instNegInt gen_neg gen_emod gen_add_3 gen_dvd gen_dvd_1 gen_mul_2 x y y_neq_0 => let A := {z | ∃ h k, z = h * x + k * y}; let_fun A_add := fun a a_1 => Exists.casesOn (motive := fun x => ∀ b ∈ A, a + b ∈ A) a_1 fun h h_1 => Exists.casesOn (motive := fun x => ∀ b ∈ A, a + b ∈ A) h_1 fun k a_eq b a_2 => Exists.casesOn a_2 fun h' h_2 => Exists.casesOn h_2 fun k' b_eq => Exists.intro (h + h') (Exists.intro (k + k') (Eq.mpr (id (congrArg ⋯ a_eq)) (Eq.mpr (id ⋯) (Eq.mpr ⋯ ⋯)))); let_fun A_mul := fun a a_1 => Exists.casesOn (motive := fun x => ∀ (z : R), z * a ∈ A) a_1 fun h h_1 => Exists.casesOn (motive := fun x => ∀ (z : R), z * a ∈ A) h_1 fun k a_eq z => Exists.intro (z * h) (Exists.intro (z * k) (Eq.mpr (id (congrArg (fun _a => z * _a = z * h * x + z * k * y) a_eq)) (Eq.mpr (id (congrArg (fun _a => _a = z * h * x + z * k * y) (gen_mul z (h * x) (k * y)))) (Eq.mpr (id (congrArg (fun _a => _a + z * (k * y) = z * h * x + z * k * y) (Eq.symm (gen_mul_1 z h x)))) (Eq.mpr (id (congrArg (fun _a => z * h * x + _a = z * h * x + z * k * y) (Eq.symm (gen_mul_1 z k y)))) (Eq.refl (z * h * x + z * k * y))))))); let B := gen_natAbs '' A \ {0}; let_fun hB_nonempty := Exists.intro (gen_natAbs (0 * x + 1 * y)) (id (Eq.mpr (id (congrArg (fun _a => _a) (propext Set.mem_diff_singleton))) ⟨Set.mem_image_of_mem gen_natAbs (Exists.intro 0 (Exists.intro 1 (Eq.refl (0 * x + 1 * y)))), Eq.mpr (id (congrArg (fun _a => gen_natAbs (_a + 1 * y) ≠ 0) (gen_zero x))) (Eq.mpr (id (congrArg (fun _a => gen_natAbs (0 + _a) ≠ 0) (gen_one y))) (Eq.mpr (id (congrArg (fun _a => gen_natAbs _a ≠ 0) (gen_zero_1 y))) (Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_def (gen_natAbs y) 0))) (Eq.mpr (id (congrArg (fun _a => ¬_a) (propext gen_natAbs_1))) y_neq_0))))⟩)); let Bmin := Nat.find hB_nonempty; let_fun hBmin_spec := Nat.find_spec hB_nonempty; Exists.casesOn hBmin_spec.left fun d hd => let_fun hdA := hd.left; let_fun hdAbs_eq_Bmin := hd.right; let_fun hBmin_neq_0 := hBmin_spec.right; let_fun hdAbs_neq_0 := Eq.mp (congrArg (fun _a => _a ≠ 0) (Eq.symm hdAbs_eq_Bmin)) hBmin_neq_0; let_fun hd_min := fun z hz => if hzAbs : gen_natAbs z = 0 then Or.inl hzAbs else Or.inr (let_fun hBmin_min := Nat.find_min' hB_nonempty ⟨Set.mem_image_of_mem gen_natAbs hz, hzAbs⟩; Eq.mpr (id (congrArg (fun _a => _a ≤ gen_natAbs z) hdAbs_eq_Bmin)) hBmin_min); let_fun hd_div_A := fun a ha_A => let q := a / d; let r := a % d; let_fun a_eq_quotRem := Eq.symm (gen_ediv a d); let_fun r_eq := Eq.symm ⋯; let_fun rAbs_lt_dAbs := gen_emod a hdAbs_neq_0; ⋯; let_fun hxA := Exists.intro 1 (Exists.intro 0 (of_eq_true (Eq.trans (congrArg (Eq x) (Eq.trans ⋯ (gen_add_3 x))) (eq_self x)))); let_fun d_dvd_x := hd_div_A x hxA; let_fun hyA := Exists.intro 0 (Exists.intro 1 (of_eq_true (Eq.trans ⋯ (eq_self y)))); let_fun d_dvd_y := hd_div_A y hyA; Exists.casesOn hdA fun h h_1 => ⋯⊢ ∀ (R : Type) (gen_instOfNat : {n : ℕ} → OfNat R n) (gen_instAddGroup : AddGroup R) (gen_instMul : Mul R) (gen_instDvd : Dvd R), (∀ (a b c : R), a + b + c = a + (b + c)) → (∀ (a b c : R), a + (b + c) = b + (a + c)) → (∀ (a b c : R), (a + b) * c = a * c + b * c) → (∀ (a b c : R), a * (b + c) = a * b + a * c) → (∀ (a b c : R), a * b * c = a * (b * c)) → ∀ (gen_natAbs : R → ℕ), (∀ (a : R), 0 * a = 0) → (∀ (a : R), 1 * a = a) → (∀ (a : R), 0 + a = a) → (∀ {a : R}, gen_natAbs a = 0 ↔ a = 0) → ∀ (gen_instDiv : Div R) (gen_instMod : Mod R), (∀ (a b : R), a / b * b + a % b = a) → ∀ (gen_instNegInt : Neg R), (∀ (a b : R), -(a * b) = -a * b) → (∀ (a : R) {b : R}, gen_natAbs b ≠ 0 → gen_natAbs (a % b) < gen_natAbs b) → (∀ (a : R), a + 0 = a) → (∀ (a b : R), b ∣ a * b) → (∀ (a b : R), (a ∣ b) = ∃ c, b = a * c) → (∀ (a b c : R), a * (b * c) = b * (a * c)) → ∀ (x y : R), y ≠ 0 → ∃ h k, isGCD (h * x + k * y) x y -- <- click to see the generalization All goals completed! 🐙

That is, the program identifies, among others, the following conditions under which the theorem holds for an arbitrary set R.

  • The set has the appropriate additive and multiplicative structure (in particular, R must be a group under addition, and multiplication must distribute over addition).

  • The set comes equipped with a function R \to \mathbb{N} (the "size function"), which is the generalization of the absolute value function on the integers.

  • The only element in R of size 0 is the additive identity 0.

  • There are functions q, r : R \times R \to R, generalizations of the quotient and remainder, respectively, that satisfy the property a = q(a, b)\cdot b + r(a, b) for elements a, b \in R.

  • For any a, b \in R such that b \neq 0, the size of r(a, b) is strictly less than the size of b.