simp only []

Stream: general

[Kevin Buzzard]

I have a proof which finishes with simp, exact h, which is not ideal. The goal is the equality of two structures, and one of the fields is another structure; everything is a prop other than two non-defeq terms, which are equal because of h. I never quite know how to prove these things (I'm proving an ext lemma for G-module homomorphisms) so I tried squeeze_simp and it told me to use simp only []. And lo and behold, simp only [] does work. What does it do?

[Simon Hudon]

You can have a look at the proof term by replacing simp with this:

  do { g ← tactic.main_goal,
       `[simp only []],
       tactic.trace g },

It will tell you what rules it uses without being asked to.

[Patrick Massot]

I have a proof which finishes with simp, exact h

Doesn't simpa work here?

[Kevin Buzzard]

Simon Hudon said:

You can have a look at the proof term by replacing simp with this:

  do { g ← tactic.main_goal,
       `[simp only []],
       tactic.trace g },

It will tell you what rules it uses without being asked to.

eq.mpr (id (eq.trans mk.inj_eq add_monoid_hom.mk.inj_eq)) ?m_1

That function is not in []!

[Kevin Buzzard]

Patrick Massot said:

I have a proof which finishes with simp, exact h

Doesn't simpa work here?

It does -- thanks. simp [h] didn't.

[Gabriel Ebner]

The simplifier has built-in support to simplify constructor equalities, which should work for arbitrary inductive types (but in practice it sometimes fails so we have extra simp lemmas in mathlib):

example (a b c d : ℕ) :
  [a, b] = [c, d] ↔ a = c ∧ b = d :=
by simp