Automation with grind🔗

The factorization of the difference of two squares can be proven by grind.

example (x y : ℝ)
  : x^2 - y^2 = (x + y) * (x - y)
:= byx:ℝy:ℝ⊢ x ^ 2 - y ^ 2 = (x + y) * (x - y)
  grindAll goals completed! 🐙

When the elaborator encounters by, signifying a tactic block, it runs the tactic interpreter. Tactics are imperative programs. Within a tactic block they manipulate the proof state consisting of the hypotheses and the goal, and the block as a whole must produce an expression having the proposition as its type.

Above, grind is the only tactic in the block. It produces an expression of type x^2 - y^2 = (x + y) * (x - y).

We can give a name to a proven proposition in several ways, and use it in subsequent proofs.

def diff_sq₁ (x y : ℝ) : x^2 - y^2 = (x + y) * (x - y)
:= byx:ℝy:ℝ⊢ x ^ 2 - y ^ 2 = (x + y) * (x - y) grindAll goals completed! 🐙

lemma diff_sq₂ (x y : ℝ) : x^2 - y^2 = (x + y) * (x - y)
:= byx:ℝy:ℝ⊢ x ^ 2 - y ^ 2 = (x + y) * (x - y) grindAll goals completed! 🐙

theorem diff_sq₃ (x y : ℝ) : x^2 - y^2 = (x + y) * (x - y)
:= diff_sq₁ x y

Despite the syntactic differences, all these define the same function.

The expression produced by grind can be inspected using #print. The actual proof has an auto-generated name.

theorem Document.Tactic_proofs.diff_sq₂ : ∀ (x y : ℝ), x ^ 2 - y ^ 2 = (x + y) * (x - y) :=
fun x y ↦ diff_sq₁._proof_1 x y#print diff_sq₂
theorem Document.Tactic_proofs.diff_sq₁._proof_1 : ∀ (x y : ℝ), x ^ 2 - y ^ 2 = (x + y) * (x - y) :=
fun x y ↦
  Classical.byContradiction fun h ↦
    id
      (let ctx := Lean.RArray.branch 1 (Lean.RArray.leaf x) (Lean.RArray.leaf y);
      let e_1 := ((Lean.Grind.CommRing.Expr.var 0).pow 2).sub ((Lean.Grind.CommRing.Expr.var 1).pow 2);
      let e_2 :=
        ((Lean.Grind.CommRing.Expr.var 0).add (Lean.Grind.CommRing.Expr.var 1)).mul
          ((Lean.Grind.CommRing.Expr.var 0).sub (Lean.Grind.CommRing.Expr.var 1));
      let p_1 := Lean.Grind.CommRing.Poly.num 0;
      h
        (Lean.Grind.CommRing.Stepwise.imp_1eq ctx e_1 e_2 p_1 p_1 (eagerReduce (Eq.refl true))
          (Lean.Grind.CommRing.Stepwise.d_init ctx p_1)))#print diff_sq₁._proof_1

The proof refers to several functions and is already long even without expanding them. Writing just grind amounts to significant compression. This is achieved by using algorithms inspired by modern SMT solvers.

Rewriting with simp🔗

Semigroup is a set with an associative binary operation. In Lean, semigroups are defined as a type class.[…]Type classes are inductive types with special elaboration-level features. We return to them later.

Here is a fact about a semigroup together with a commutativity hypothesis.

example (G : Type) [Semigroup G] (a b c : G)
  (h : ∀ x y : G, x * y = y * x)
  : a * b * c = b * c * a
:= byG:Typeinst✝:Semigroup Ga:Gb:Gc:Gh:∀ (x y : G), x * y = y * x⊢ a * b * c = b * c * a
  calc
    (a * b) * c
    _ = (b * a) * c := byG:Typeinst✝:Semigroup Ga:Gb:Gc:Gh:∀ (x y : G), x * y = y * x⊢ a * b * c = b * a * c simp [h]All goals completed! 🐙
    _ = b * (a * c) := byG:Typeinst✝:Semigroup Ga:Gb:Gc:Gh:∀ (x y : G), x * y = y * x⊢ b * a * c = b * (a * c) grindAll goals completed! 🐙
    _ = b * (c * a) := byG:Typeinst✝:Semigroup Ga:Gb:Gc:Gh:∀ (x y : G), x * y = y * x⊢ b * (a * c) = b * (c * a) simp [h]All goals completed! 🐙
    _ = (b * c) * a := byG:Typeinst✝:Semigroup Ga:Gb:Gc:Gh:∀ (x y : G), x * y = y * x⊢ b * (c * a) = b * c * a grindAll goals completed! 🐙

We use the grind and simp tactics to prove the steps in the calc block.[…]The calc block chains equalities and other transitive relations. The simp tactic uses the commutativity hypothesis h as a rewrite rule.

Further proofs🔗

example : diff_sq₁ = diff_sq₂ := rfl
example : diff_sq₁ = diff_sq₃ := rfl