Automatic insertion of `show` tactic for VSCode?

Stream: metaprogramming / tactics

[Ben Selfridge]

Hello,

I'm doing a proof, and noticing that it's really helpful to add show tactics periodically to illustrate what the current goal is. Below is a snippet:

example : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
  apply le_antisymm
  . show a ⊓ b ⊓ c ≤ a ⊓ (b ⊓ c)
    apply le_min
    . show a ⊓ b ⊓ c ≤ a
      calc a ⊓ b ⊓ c ≤ a ⊓ b := by apply min_le_left
           _         ≤ a     := by apply min_le_left
    . show a ⊓ b ⊓ c ≤ b ⊓ c
      apply le_min
      . show a ⊓ b ⊓ c ≤ b
        have h₁ : min (min a b) c ≤ min a b := by apply min_le_left
        have h₂ : min a b ≤ b := by apply min_le_right
        exact le_trans h₁ h₂
...

This seems automatable. I'm just copy + pasting the current goal into a show tactic. Is there a keystroke in VSCode for this? If not, does it seem like something that would be useful? It might be fun to try to add something like that.

[Damiano Testa]

Does this discussion do something like what you have in mind?

[Joachim Breitner]

You should be able to define a show? tactic that uses the code actions / suggestions mechanism to replace itself with show relatively easily. maybe a nice project to play with metaprogramming?