Tactic simp term order

Stream: lean4

[Yicheng Qian]

What order does simp use to compare terms? For example,

set_option pp.all true

theorem sdf : Nat.add (Nat.add a b) c = Nat.add (Nat.add b c) a := by
  simp

/- => @Eq.{1} Nat
  (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
    (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) a b) c)
  (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
    (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) b c) a)
-/

why will it consider @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat, which is a non-whnf, to be simpler than Nat.add?

[Notification Bot]

Yicheng Qian has marked this topic as resolved.

[Notification Bot]

Yicheng Qian has marked this topic as unresolved.

[Yicheng Qian]

This makes me worried because I think that in some cases this will make the tactic rw fail to work. Consider this example

structure Semigroup where
  carrier : Type u
  mul : carrier → carrier → carrier
  mul_assoc (a b c : carrier) : mul (mul a b) c = mul a (mul b c)

instance (S : Semigroup) : Mul S.carrier where
  mul a b := S.mul a b

instance : CoeSort Semigroup (Type u) where
  coe S := S.carrier

structure Morphism (S1 S2 : Semigroup) where
  mor : S1 → S2
  resp_mul : ∀ a b : S1, mor (a * b) = (mor a) * (mor b)

instance : CoeFun (Morphism S1 S2) (fun _ => S1 -> S2) where
  coe f := f.mor

To prove the following theorem, the simplest way seems to involve unfolding of HMul.hMul and Mul.mul (I consier this necessary because otherwise rw [S2.mul_assoc] won't work)

example {S1 S2 : Semigroup} (f : Morphism S1 S2) (a : S1) :
  f ((a * a) * (a * a)) = f a * ((f a * f a) * f a) := by
    simp [f.resp_mul]; simp [HMul.hMul, Mul.mul]; simp [S2.mul_assoc]

[Yicheng Qian]

If we refuse to unfold HMul.hMul and Mul.mul, then the simplest way I can come up with is to enter the conversion tactic mode

example {S1 S2 : Semigroup} (f : Morphism S1 S2) (a : S1) :
  f ((a * a) * (a * a)) = f a * ((f a * f a) * f a) :=
  calc
    f ((a * a) * (a * a)) = f (a * a) * f (a * a)     := by rw [f.resp_mul]
               _          = (f a * f a) * (f a * f a) := by rw [f.resp_mul]
               _          = S2.2 (S2.2 (f a) (f a)) (S2.2 (f a) (f a)) :=
                               by conv =>
                                  lhs; whnf
                                  args whnf whnf
               _          = S2.2 (f a) (S2.2 (S2.2 (f a) (f a)) (f a)) := by simp [S2.mul_assoc]

[Mario Carneiro]

The direction of simp rewrites is a library design question. We generally prefer a + b over Nat.add a b because the former will have more theorems about it: for example we would have an associativity theorem add_assoc which applies to any additive semigroup rather than just Nat.