Closing `⊢` goals in `conv` mode

Stream: general

[Eric Wieser]

After running rw in conv mode with docs#finsupp.sum_map_domain_index (which requires two assumptions), I end up with one | goal and two ⊢ goals.

I already know how to handle the | goal, and can discard it with skip. I'm then left with two ⊢ goals, but:

• I'm still in conv mode, so don't have any tactics to help me
• If I leave conv mode, the | goal does not take effect

Is there a way to drop back into tactic mode in conv mode?

[Johan Commelin]

Good question! Does conv mode have an exact tactic?

[Eric Wieser]

No!

[Johan Commelin]

If not, I guess it should get it for situations like these.

[Eric Wieser]

But indeed, then I could use exact by { } which would hopefully do the trick

[Eric Wieser]

Furthermore, if I attempt a term-mode proof as an argument to sum_map_domain_index, if I get it wrong the error is silenced and the conv does nothing

[Eric Wieser]

almost- #mwe (needs some variables from monoid_algebra.lean):

-- in master shortly
def to_add_equiv : multiplicative G ≃ G := ⟨multiplicative.to_add, multiplicative.of_add, of_add_to_add, to_add_of_add⟩

def add_monoid_algebra.to_multiplicative :
  add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G) :=
{ map_mul' := λ x y, by {
    unfold finsupp.dom_congr to_add_equiv,
    simp [mul_def],
    simp_rw map_domain_sum,
    simp_rw map_domain_single,
    conv_rhs {
      for (finsupp.sum _ _) [1, 2] {
        rw finsupp.sum_map_domain_index,
        skip,
      },
    },
    sorry },
  map_add' := λ x y, by {
    simp [finsupp.dom_congr, map_domain_add],
  },
  ..finsupp.dom_congr to_add_equiv }

[Eric Wieser]

meta def conv.interactive.exact (q : interactive.parse interactive.types.texpr) : conv unit := tactic.interactive.exact q

seems to do the job, although I wonder if it warrants some special casing to only allow its use on ⊢ goals

[Eric Wieser]

In fact even this works:

meta def conv.interactive.exact := tactic.interactive.exact

[Eric Wieser]

Should I PR the above?

Or should we change conv so that unsolved goals remain outside of the conv block?

[Eric Wieser]

And If I did use the above definition of exact, is there anything to stop the user closing a | goal with it nonsensically?

[Eric Wieser]

Here's a contrived #mwe showing when exact can be needed in conv mode:

import algebra.ring

meta def conv.interactive.tactic_exact := tactic.interactive.exact

variables {α : Type*} [ring α] {a b c : α}

lemma obvious : c = 1 → (a * b) * c = a * b := λ h, by {rw [h, mul_one]}

example (hc : c = 1) (hb : b = 1) : (a * b) * c = a := begin
  conv_lhs {
    rw obvious,
    skip,
    -- goal is `| c`, which is nonsense
    tactic_exact by {
      -- goal is `⊢ c = 1`
      assumption,
    }
  },
  rw [hb, mul_one],
end

It seems that conv gets confused about the goal state after the rw.

[Gabriel Ebner]

In this case you could also use rw hc, skip instead of the tactic_exact.

[Gabriel Ebner]

conv doesn't really get confused here. Remember that conv is just a light wrapper around the standard tactic state that prints subgoals a = b as | a, and where the tactics operate on the left-hand side (a) of the equation.

[Eric Wieser]

Right, hence this example being contrived. The one earlier in this thread I can't work out any way to solve without tactic_exact.

[Eric Wieser]

I was not aware that was how conv works

[Eric Wieser]

But I feel like new goals introduced by rw should never be treated as | goals

[Eric Wieser]

Gabriel Ebner said:

that prints subgoals a = b as | a

Where does this actually happen? tactic.interactive_expr has some code to print ⊢ g as HTML, but I can't see where the rules for printing conv mode are.

[Gabriel Ebner]

It's implemented in conv.save_info (by passing a boolean flag to the C++ code..). This is a magic name. When Lean sees begin[conv] ... end, it looks for conv.save_info, conv.istep, etc.

[Eric Wieser]

I've never seen the syntax begin[...] before

[Bryan Gin-ge Chen]

It's not documented anywhere but that's how you enter a custom tactic mode.

[Bryan Gin-ge Chen]

There was some discussion on custom tactic modes in this thread.

[Eric Wieser]

Does that mean I can use begin[tactic] to switch back to tactic mode from conv mode?

[Eric Wieser]

Oh, I guess I need to be in an expression context

[Eric Wieser]

Gabriel Ebner said:

It's implemented in conv.save_info (by passing a boolean flag to the C++ code..). This is a magic name. When Lean sees begin[conv] ... end, it looks for conv.save_info, conv.istep, etc.

I don't see where that boolean flag is, conv.save_info looks like it just calls regular tactic code.

[Gabriel Ebner]

The boolean flag is in tactic_state.to_format.

[Gabriel Ebner]

I thought this works:

begin  begin[smt]  end end

Maybe this works as well?

by conv { begin[tactic] end }

[Kevin Buzzard]

@Eric Wieser the natural number game uses this begin [natnumgame] trick and that's how I stopped rw from closing refl goals

[Eric Wieser]

save_info is run automatically between conv tactics I assume?

[Eric Wieser]

I think what I'd like to happen, is that after rw runs, any new goals are marked with some kind of "not conv" flag

[Eric Wieser]

Which both:

• Adjusts tactic state rendering
• Allows exact to be used to close those goals (and those goals only)

[Eric Wieser]

But perhaps the simpler alternative is to make rw in conv mode take an extra argument, a tactic block

[Eric Wieser]

And have it use that tactic block to close any goals it creates.

[Eric Wieser]

Alright, I almost have this - but I'm stuck writing the tactic parser - I can't work out how to combine parse (tk ...) with itactic:

meta def rw2 (q : parse rw_rules) (cfg : rewrite_cfg := {}) (p : parse (tk "with" *> itactic)) : conv unit

fails with a type error, and I can't find any examples to follow

[Eric Wieser]

I've pushed the parts I can do to https://github.com/leanprover-community/lean/pull/475 - I'd appreciate help ironing out the details