Zulip Chat Archive

Stream: lean4

Topic: tactic which is just a combination of other tactics

Kevin Buzzard (Oct 19 2023 at 18:11):

I want to prove lots of things (all the one-variable axioms for a commutative ring defined as a quotient) using this sequence of tactics:

  intro x
  refine Quot.induction_on x ?_
  rintro ⟨a, b⟩
  apply Quot.sound
  simp
  try ring

How do I write one tactic which does this? I knew how to do this in Lean 3 and it's useful for teaching gimmicks.

Alex J. Best (Oct 19 2023 at 18:15):

Here is one way

import Mathlib.Tactic

macro "foo" : tactic => `(tactic|
  · intro a
    exact a)

example (h : 1= 1): 1= 1:= by
  revert h
  foo

Alex J. Best (Oct 19 2023 at 18:16):

Actually this isn't good, I'll try and make a better version

Kyle Miller (Oct 19 2023 at 18:17):

macro "buzzardify" : tactic =>
  `(tactic|
    intro x
    refine Quot.induction_on x ?_
    rintro ⟨a, b⟩
    apply Quot.sound
    simp
    try ring)

Alex J. Best (Oct 19 2023 at 18:28):

I don't think that does what you think it does kyle, or at least I have no idea what that would do,
Look at the state after

macro "buzzardify" : tactic =>
  `(tactic|
    intro x
    ring)

example (h a s : 1= 1): 1= 1:= by
  revert h a s
  buzzardify

Alex J. Best (Oct 19 2023 at 18:33):

I think

macro "buzzardify" : tactic =>
  `(tactic|
  focus
    intro x
    refine Quot.induction_on x ?_
    rintro ⟨a, b⟩
    apply Quot.sound
    simp
    try ring)

works

Kyle Miller (Oct 19 2023 at 18:35):

Oh, oops, should have tested more carefully (i.e., at all). You can use parentheses to group tactics:

macro "buzzardify" : tactic => `(tactic|(
  intro x
  refine Quot.induction_on x ?_
  rintro ⟨a, b⟩
  apply Quot.sound
  simp
  try ring))

Kevin Buzzard (Oct 19 2023 at 18:46):

Works in my use case! Thanks both of you! This is something I've been teaching this week.

import Mathlib.Tactic

-- A "pre-integer" is just a pair of naturals.
abbrev MyPreint := ℕ × ℕ

namespace MyPreint

/-- The equivalence relation on pre-integers, which we'll quotient out
by to get integers. -/
def R (x y : MyPreint) : Prop := x.1 + y.2 = x.2 + y.1

-- Lemma saying what definition of `R` is on ordered pairs
lemma R_def (a b c d : ℕ) : R (a,b) (c,d) ↔ a + d = b + c := by
  rfl

-- `linarith` tactic can do all the calculations to prove it's an equiv reln
lemma R_refl : Reflexive R := by
  rintro ⟨a, b⟩
  simp only [R_def] at *
  linarith

lemma R_symm : Symmetric R := by
  rintro ⟨a, b⟩ ⟨c, d⟩ h
  simp only [R_def] at *
  linarith

lemma R_trans : Transitive R := by
  rintro ⟨a, b⟩ ⟨c, d⟩ ⟨e, f⟩ h1 h2
  simp only [R_def] at *
  linarith

/-- Enable `≈` notation for `R` and ability to quotient by it  -/
instance R_equiv : Setoid MyPreint where
  r := R
  iseqv := ⟨@R_refl, @R_symm, @R_trans⟩

-- Teach the definition of `≈` to the simplifier
@[simp] lemma equiv_def (a b c d : ℕ) : (a, b) ≈ (c, d) ↔ a + d = b + c := R_def a b c d

-- Teach the definition of `Setoid.r` to the simplifier
@[simp] lemma equiv_def' (a b c d : ℕ) : Setoid.r (a, b) (c, d) ↔ a + d = b + c := equiv_def a b c d

/-- Negation on pre-integers. -/
def neg (ab : MyPreint) : MyPreint := (ab.2, ab.1)

-- teach it to the simplifier
@[simp] lemma neg_def (a b : ℕ) : neg (a, b) = (b, a) := rfl

/-- Addition on pre-integers. -/
def add (ab cd : MyPreint) : MyPreint := (ab.1 + cd.1, ab.2 + cd.2)

-- teach it to the simplifier
@[simp] lemma add_def (a b c d : ℕ) : add (a, b) (c, d) = (a + c, b + d) := rfl

/-- Multiplication on pre-integers. -/
def mul (ab cd : MyPreint) : MyPreint := (ab.1 * cd.1 + ab.2 * cd.2, ab.1 * cd.2 + ab.2 * cd.1)

-- teach it to the simplifier
@[simp] lemma mul_def (a b c d : ℕ) : mul (a, b) (c, d) = (a * c + b * d, a * d + b * c) := rfl

end MyPreint

open MyPreint

/-- Make the integers as a quotient of preintegers. -/
def MyInt := Quotient R_equiv

namespace MyInt

-- `0` notation (the equiv class of (0,0))
instance : Zero MyInt where zero := ⟦(0, 0)⟧

-- `1` notation (the equiv class of (1,0))
instance : One MyInt where one := ⟦(1, 0)⟧

/-- Negation on integers. -/
def neg : MyInt → MyInt := Quotient.map MyPreint.neg <| by
  -- to prove this is well-defined, we need to
  -- show some lemma or other
  rintro ⟨a, b⟩ ⟨c, d⟩ (h : a + d = b + c)
  simp [MyPreint.neg]
  -- So prove this lemma
  linarith

-- unary `-` notation
instance : Neg MyInt where neg := neg

/-- Addition on integers. -/
def add : MyInt → MyInt → MyInt  := Quotient.map₂ MyPreint.add <| by
  -- to show this is well-defined, we need to
  -- show some lemma or other
  rintro ⟨a, b⟩ ⟨c, d⟩ (h1 : a + d = b + c)
         ⟨e, f⟩ ⟨g, h⟩ (h2 : e + h = f + g)
  simp [MyPreint.add]
  -- So prove this lemma
  linarith

-- `+` notation
instance : Add MyInt where add := add

/-- Multiplication on integers. -/
def mul : MyInt → MyInt → MyInt  := Quotient.map₂ MyPreint.mul <| by
  -- to show this is well-defined, we need to show some lemma or other
  rintro ⟨a, b⟩ ⟨c, d⟩ (h1 : a + d = b + c)
         ⟨e, f⟩ ⟨g, h⟩ (h2 : e + h = f + g)
  simp [MyPreint.mul]
  -- so prove this lemma (which in this case is nonlinear)
  nlinarith

-- `*` notation
instance : Mul MyInt where mul := mul

open MyPreint

-- Every single proof of every single axiom is: "replace all integers with
-- pairs of naturals, turn the question into a question about naturals,
-- and then get the `ring` tactic to prove it if it's not already proved by accident"

macro "int_proof₁" : tactic =>
  `(tactic|
  focus
    intro x
    refine Quot.induction_on x ?_
    rintro ⟨a, b⟩
    apply Quot.sound
    simp
    try ring)

macro "int_proof₂" : tactic =>
  `(tactic|
  focus
    intro x y
    refine Quot.induction_on₂ x y ?_
    rintro ⟨a, b⟩ ⟨c, d⟩
    apply Quot.sound
    simp
    try ring)

macro "int_proof₃" : tactic =>
  `(tactic|
  focus
    intro x y z
    refine Quot.induction_on₃ x y z ?_
    rintro ⟨a, b⟩ ⟨c, d⟩ ⟨e, f⟩
    apply Quot.sound
    simp
    try ring)

instance : CommRing MyInt where
  add := (. + .)
  add_assoc := by int_proof₃
  zero := 0
  zero_add := by int_proof₁
  add_zero := by int_proof₁
  add_comm := by int_proof₂
  mul := (. * .)
  left_distrib := by int_proof₃
  right_distrib := by int_proof₃
  zero_mul := by int_proof₁
  mul_zero := by int_proof₁
  mul_assoc := by int_proof₃
  one := 1
  one_mul := by int_proof₁
  mul_one := by int_proof₁
  neg := (- .)
  add_left_neg := by int_proof₁
  mul_comm := by int_proof₂

What's the next trick? Figure out just one int_proof tactic that counts the number of inputs?

Damiano Testa (Oct 19 2023 at 19:54):

If you do not expect to need more than the three arguments, you can simply combine them by trying them each, until one succeeds...

Kevin Buzzard (Oct 19 2023 at 20:30):

So then the only question left is whether lean 4 has a version of the refine_struct tactic meaning that I will be able to solve them all in one line