Unification of equations by simp

Stream: general

[Jannis Limperg]

One of the reviews of the induction' paper pointed out that simp apparently does some first-order unification when simplifying equations, even without any simp lemmas:

example (P : Prop) (n m) (h : nat.succ n = nat.succ m → P) : n = m → P :=
begin
  simp only [] at h,
  guard_hyp h : n = m → P,
  exact h
end

Does anyone know what exactly is going on here? Does simp just use Lean's unification procedure whenever it encounters an equation?

[Reid Barton]

I don't know how it works, but simp does seem to have some built-in knowledge of disjointness and injectivity of constructors

[Rob Lewis]

A little experimenting shows it's the constructor_eq option to simp that allows this.

[Jannis Limperg]

Thanks! That led me to the right place in the C++: library/tactic/simplify.cpp, simplify_core_fn::simplify_constructor_eq_constructor.

With constructor_eq, the simplifier indeed uses a partial implementation of the usual unification algorithm. (This is the third such implementation in Core that I'm aware of. :P) It recognises equations whose LHS and RHS are constructor applications and uses injectivity or no-confusion as appropriate. However, it doesn't do any normalisation, doesn't use the cycle rule (cases also doesn't) and doesn't work with tuples for some reason.

universes u v

structure myprod (α : Type u) (β : Type v) : Type (max u v) :=
(a : α) (y : β)

-- Nested constructor applications work.
example (n n' m m' k k' : ℕ)
  (h : myprod.mk (myprod.mk n m) k = myprod.mk (myprod.mk n' m') k') :
  (n = n' ∧ m = m') ∧ k = k' :=
begin
  simp only [] at h,
  exact h
end

-- Also with different data types.
example (n : ℕ) (h : myprod.mk nat.zero nat.zero = myprod.mk (nat.succ 1) (nat.succ 1)) : false :=
begin
  simp only [] at h,
  guard_hyp h : false ∧ false,
  exact and.elim_left h
end

-- Tuples (`prod`) doesn't work for some reason.
example (n n' m m' : ℕ) (h : (n, m) = (n', m')) : n = n' ∧ m = m' :=
begin
  success_if_fail { simp only [] at h },
  sorry
end

-- Constructors are matched syntactically; no normalisation is performed.
example (n : ℕ) (h : 0 = n + 1) : false :=
begin
  success_if_fail { simp only [] at h },
  sorry
end

-- The cycle rule is not implemented.
example (n : ℕ) (h : n = nat.succ n) : false :=
begin
  success_if_fail { simp only [] at h {} },
  sorry
end