What does `simpa using foo` do?

Stream: mathlib4

[Arien Malec]

I'm trying to unwind a misbehaving simpa using foo tactic (red squiggly + "no goals to be solved" + "Goals accomplished :tada:"), and would like to see where the more primitive simplification is getting to...

[Riccardo Brasca]

If you get both "goal accomplished" and an error it can be a bug. Can you provide a #mwe?

[Arien Malec]

Doesn't feel like it -- I'm deep in the bowels of a port that's secondary to another port. Let me see if I can sorry some stuff to make an #mwe

[Arien Malec]

I get the error on both simpas here:

import Mathlib.Data.Option.Basic
import Mathlib.Data.Subtype
import Mathlib.Logic.Equiv.Defs

variable (e : Option α ≃ Option β)

private def remove_none_aux (x : α) : β := sorry

private theorem remove_none_aux_some {x : α} (h : ∃ x', e (some x) = some x') :
    some (remove_none_aux e x) = e (some x) := sorry

private theorem remove_none_aux_none {x : α} (h : e (some x) = none) :
    some (remove_none_aux e x) = e none := sorry

private theorem remove_none_aux_inv (x : α) : remove_none_aux e.symm (remove_none_aux e x) = x :=
  Option.some_injective _
    (by
      cases h1 : e.symm (some (remove_none_aux e x)) <;> cases h2 : e (some x)
      · rw [remove_none_aux_none _ h1]
        exact (e.eq_symm_apply.mpr h2).symm

      · rw [remove_none_aux_some _ ⟨_, h2⟩] at h1
        simpa using h1

      · rw [remove_none_aux_none _ h2] at h1
        simpa using h1

      · rw [remove_none_aux_some _ ⟨_, h1⟩]
        rw [remove_none_aux_some _ ⟨_, h2⟩]
        simp
        )

But figuring out how to trigger this with a minimum of dependencies is going to be tricky. Let me work on it...

[Junyan Xu]

simpa using h1 is like simp followed by exact h1, so it's possible that simp already solves the goal and so exact h1 produce an error that there's "no goals to be solved".

[Riccardo Brasca]

What happen if you remove all the private?

[Arien Malec]

simp doesn't solve the goal, sadly

[Riccardo Brasca]

Also, a sorried def is always dangerous.

[Junyan Xu]

What does simp at h1 ⊢ gives you?

[Arien Malec]

No effect on removing the private declarations.

[Riccardo Brasca]

Can you remove the first sorry?

[Arien Malec]

I just sorryd to de-dependency the beast...

[Arien Malec]

Unfortunately the first sorry depends on a file that's as yet unported....

[Arien Malec]

@Junyan Xu 's suggestion gives the :tada:

[Mario Carneiro]

make them opaque instead of sorry

[Mario Carneiro]

or axiom

[Arien Malec]

OK, this repros.

import Mathlib.Data.Option.Basic
import Mathlib.Data.Subtype
import Mathlib.Logic.Equiv.Defs

variable (e : Option α ≃ Option β)

def remove_none_aux (x : α) : β :=
  if h : (e (some x)).isSome then Option.get _ h
  else
    Option.get _ <|
      show (e none).isSome by
        rw [← Option.ne_none_iff_isSome]
        intro hn
        rw [Option.not_isSome_iff_eq_none, ← hn] at h
        exact Option.some_ne_none _ (e.injective h)


theorem remove_none_aux_some {x : α} (h : ∃ x', e (some x) = some x') :
    some (remove_none_aux e x) = e (some x) :=
  by simp [remove_none_aux, Option.isSome_iff_exists.mpr h]

theorem remove_none_aux_none {x : α} (h : e (some x) = none) :
    some (remove_none_aux e x) = e none := by
  simp [remove_none_aux, Option.not_isSome_iff_eq_none.mpr h]

theorem remove_none_aux_inv (x : α) : remove_none_aux e.symm (remove_none_aux e x) = x :=
  Option.some_injective _
    (by
      cases h1 : e.symm (some (remove_none_aux e x)) <;> cases h2 : e (some x)
      · rw [remove_none_aux_none _ h1]
        exact (e.eq_symm_apply.mpr h2).symm

      · rw [remove_none_aux_some _ ⟨_, h2⟩] at h1
        simpa using h1

      · rw [remove_none_aux_none _ h2] at h1
        simpa using h1

      · rw [remove_none_aux_some _ ⟨_, h1⟩]
        rw [remove_none_aux_some _ ⟨_, h2⟩]
        simp
        )

[Ruben Van de Velde]

When I've hit that, replacing simpa using foo by simp at foo was sufficient

[Arien Malec]

So interestingly, when I replace
simpa using h1
with
simp at h1 exact h1

I get the same behavior (red squiggly + :tada:)

[Mario Carneiro]

what it macro expands to is:

have' h := h1
simp at h1
exact h

and the exact line fails. As Ruben says, the solution is to just use simp at h1, the error message should be fixed to indicate this

[Mario Carneiro]

The red squiggly + :tada: situation isn't that unusual, the tactic state is generally empty at the end of a proof and that's when the :tada: shows up

[Mario Carneiro]

in particular, almost all tactics give an error if used when there are no goals, and that's when you get the :tada:

[Arien Malec]

It's just that h1is the goal....

[Mario Carneiro]

?

[Arien Malec]

so exact h1 should work?

[Mario Carneiro]

no, h1 is not the goal

[Mario Carneiro]

h1 is some ... = none after simplification which is why simp can close the goal itself

[Arien Malec]

If I take the #mwe above, replace simpa using h1 with simp at h1, h1 is the goal...

[Mario Carneiro]

I think you must be confused by the "expected type" printout

[Mario Carneiro]

the tactic state is empty (i.e. there are no goals and you get a :tada:)

[Mario Carneiro]

that's the first bit

[Mario Carneiro]

the expected type is the type of h1

[Mario Carneiro]

because your cursor is on h1

[Arien Malec]

You are exactly correct