convert_to

Stream: mathlib4

[Moritz Doll]

Ok, the macro works, but the issue is that

import Mathlib.Tactic.Convert
import Mathlib.Algebra.Group.Basic

example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
  convert (_ : c + d = d + c) using 2
  sorry

fails. I think the issue is that the old convert used the assumption in the context, but the Lean 4 version does not do that.

In fact in mathlib3 this works:

import tactic.congr
import algebra.group.defs

example {α} [add_comm_monoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c :=
begin
  convert (_ : c + d = _) using 2,
  rw [add_comm],
end

[Mario Carneiro]

Can you isolate the issue to something that congr is doing?

[Moritz Doll]

I can try it, but I don't think I'll have the time for that today.

[Moritz Doll]

I don't think that congr is the issue here:

import Mathlib.Tactic.Convert
import Mathlib.Algebra.Group.Basic

example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
  convert (_ : c + d = d + c) using 0
  congr 2

example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
  convert (_ : c + d = d + c) using 2

example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
  have h : c + d = d + c := by
    rw [add_comm]
  convert h using 0
  congr 2

example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
  have h : c + d = d + c := by
    rw [add_comm]
  convert h using 2

example {α} [AddCommMonoid α] {a b c d : α} (H : a = c) (H' : b = d) : a + b = d + c := by
  have h : c + d = d + c := by
    rw [add_comm]
  rw [H, H', h]

[Moritz Doll]

the first two fail, the last three succeed

[Kyle Miller]

Moritz Doll said:

I think the issue is that the old convert used the assumption in the context, but the Lean 4 version does not do that.

Just to give a bit of information about the internals of convert/convert_to in mathlib3, they use a special version of congr called docs#tactic.congr' that uses assumption among other things.

[Moritz Doll]

but does convert .. using 0 use congr' at all?

[Kyle Miller]

Yes, it's always used

[Kyle Miller]

And the number controls how many times tactic.congr_core' is recursively run. Even if it's using 0 it will at least try assumption <|> reflexivity transparency.none <|> by_proof_irrel first.

[Moritz Doll]

convert is definitively not the issue: commenting that part out in the tactic is does help

[Moritz Doll]

(maybe not too unexpected since it is completely in try-catch blocks)

[Moritz Doll]

the issue seems to be elabTermWithHoles in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Convert.lean#L107

[Moritz Doll]

setting allowNaturalHolesto true in elabTermWithHoles solves the issue

[Moritz Doll]

now the question is why was false used and what is the correct thing for convert?

[Moritz Doll]

other question: there is an explanation of allowNaturalHoles in the file ElabTerm, but it feels to me that this explanation should be in the docstring of elabTermWithHoles as well. any objections to adding that?

[Moritz Doll]

I've made a new PR for this, too mathlib4#527 this time as a branch on leanprover-community.

[Mario Carneiro]

The difference between allowNaturalHoles and not is the difference between refine' and refine

[Mario Carneiro]

when it is true, you get a behavior closer to lean 3 where all _ (including automatically generated ones from implicit args) are turned into subgoals

[Mario Carneiro]

We would like to migrate to the lean 4 behavior where subgoals are explicitly marked in the syntax with ?_

[Moritz Doll]

thanks for explanation, I saw that ?_ was a thing in Lean 4, but I did not know what it was exactly about.