ring bug? use bug?

Stream: maths

[Kevin Buzzard]

Whatever's going on here?

import data.real.basic -- real numbers

lemma Sht2Question5a :
  ∀ x : ℝ, ∃ y : ℝ, x + y = 2 :=
begin
  intro x,
  use 2 - x,
  -- ⊢ x + (2 - x) = 2
  ring, -- nothing happened?
  ring, -- normal service resumed, goal closed
end

If I'd not tried this out beforehand then I would have looked very silly in front of 300 people.

[Kevin Buzzard]

Even with pp.all true I cannot figure out the problem. The first ring seems to not change the tactic state at all.

[Kevin Buzzard]

example (x : ℝ) : x + (2 - x) = 2 := by ring works fine

[Rob Lewis]

I think use is leaving uninstantiated metavars in the goal. The first ring call is instantiating them but doing nothing else, then the second finishes the job.

[Rob Lewis]

existsi instead of use works.

[Kevin Buzzard]

I thought use would be the culprit. I was surprised the metavars didn't manifest themselves in some way in the tactic state though.

[Kevin Buzzard]

Thanks Rob.

[Rob Lewis]

I don't see anything suspicious in use that would cause this. It's basically just a wrapper around refine and fconstructor. It feels a little hackish to just make use clean up the goal afterward, but I'm not sure how else to fix it.

[Rob Lewis]

Is there a "clean up metavars in the goal" tactic already? Something like this?

meta def fix_goal : tactic unit :=
target >>= instantiate_mvars >>= change

[Rob Lewis]

I thought use would be the culprit. I was surprised the metavars didn't manifest themselves in some way in the tactic state though.

The pretty printer instantiates metavars by default, you can disable it with set_option pp.instantiate_mvars false to see what's happening.

[Rob Lewis]

Hmm, maybe it's not so hackish. The alternative is asking ring to clean up the goal before it starts. I'm not sure there's a well-defined policy on whose job it is to instantiate metavars. Some tactics don't care if they're present, but it matters for things like ring that look at the structure of the target expression.

[Kevin Buzzard]

All this under-the-hood stuff that I as a non-meta person have very little understanding of. Still so much to learn!

[Rob Lewis]

It's actually pretty simple to understand in this case. You're starting with one goal ∃ n : T, P n. use begins by splitting this into two goals. The first goal is T, the second is to show that P holds of whatever value of T you give in the first goal. This missing value is represented with a metavariable ?m. When you solve the first goal with k : T the metavariable gets assigned to k. For anything working "up to defeq," the second goal is P k. But syntactically it's still P ?m, which confuses ring.

[Johan Commelin]

This sound like it's definitely uses job to clean up after itself... :stuck_out_tongue_wink:

[Rob Lewis]

If you were just solving the second goal by applying a proof of P k, it wouldn't matter.

[Keeley Hoek]

Has this turned into a pull request?

[Keeley Hoek]

Oh damn it was like 10mins ago

[Rob Lewis]

Heh. The PR should be adding

meta def fix_goal : tactic unit :=
target >>= instantiate_mvars >>= change

and applying it to all goals after a successful application of use.

[Patrick Massot]

Do you understand why existsi doesn't have this issue?

[Rob Lewis]

It also might not be a bad idea to make ring instantiate mvars in the goal before it starts.

[Patrick Massot]

I find it very annoying that sometimes use doesn't work while existsi works. It means we have to keep both in our heads.

[Patrick Massot]

I may be partly guilty, because I was on the side which pushed for use to try to close stupid goals after doing its main job. But I changed my mind. Now I'm ready to sacrifice this in favor or reliability and getting rid of existsi entirely.

[Rob Lewis]

Unlike use, existsi t doesn't create any new goals under the hood. It's possible to hit this same problem with existsi too:

lemma Sht2Question5a' :
  ∀ x : ℝ, ∃ y : ℝ, x + y = 2 :=
begin
  intro x,
  existsi _,
  swap,
  exact 2 - x,
  ring,
  ring
end

[Rob Lewis]

Assuming this issue with use is fixed, what are the other problems?

[Rob Lewis]

use is somewhat more general than existsi because it supports things like this:

[Rob Lewis]

example : ∃ p : ℕ × ℕ, true :=
begin
  use [1, 2], -- good
  -- existsi [1, 2] -- fails
end

example : ∃ p : ℕ × ℕ, true :=
begin
  use 1,
/-
2 goals
⊢ ℕ

⊢ true-/
end

[Patrick Massot]

I'll try to grep for existsi in the perfectoid project, and see if I can get a minimized version

[Keeley Hoek]

So long as there aren't really any core tactics which are big metavariable offenders, it seems reasonable to me that a convention to clean up after yourself is optimal. On the other hand, unless tactics are being called automatically (as in by another tactic lots of times), probably instantiate_mvars can't be thaaat expensive to pointlessly run?

Oh, but I see your example makes existsi mess up ring. Gotcha.

[Rob Lewis]

Yeah, the problem is it's not always possible to clean up, as in the existsi example. I think it's reasonable to ask interactive tactics to clean up as much as they can. But that's not a guarantee.

[Rob Lewis]

https://github.com/leanprover-community/mathlib/pull/1520

[Patrick Massot]

Did you try to figure out the performance impact on ring?

[Rob Lewis]

It should be negligible.

[Keeley Hoek]

I guess it'd be O(number of verts in the expression tree) if the number of metavariables is low, and there are some pretty cray cray typeclass-related expression traces, but probably not in a goal ring should eat I guess.

[Rob Lewis]

The calls to instantiate_mvars_in_target take at most half a millisecond each. I'll keep going and see if there are any weird long ones, but I bet this adds under half a second total.

[Rob Lewis]

It does actually add a few ms to complex.exp_add.

[Reid Barton]

Oh I need to look at this thread again later, but this is very interesting. I've seen the ring, ring thing before and I never imagined it could be the fault of something other than ring itself

[Kevin Buzzard]

import data.real.basic tactic.ring

example (a b l m : ℝ) :
  abs(a + (b + (-l - m))) = abs(a + (-l + (b - m))) :=
-- by ring -- I think this used to work but now it doesn't
by congr' 1; ring

Did ring change as a result of this conversation and now this? Or was this some other change? A project which I'm pretty sure used to compile now no longer does.

[Kevin Buzzard]

Similarly lam n, [a thing] = lam n, [a thing which ring can prove is equal] can no longer be closed by ring. Am I just behind the times? If this is a design decision I'm fine.

[Mario Carneiro]

I don't think that was ever supposed to work

[Mario Carneiro]

ring will rewrite in subterms if it isn't facing an equality of rings, but that's mostly for viewing purposes so you know why ring isn't working

[Kevin Buzzard]

OK then no worries. I have an old project written before update-mathlib and I bumped mathlib to get update-mathlib working and it broke the project.

[Kevin Buzzard]

All the fixes are easy. I neither know nor care why it broke.

[Mario Carneiro]

I would actually expect in the abs example that ring sees it as two atoms and tries to prove x = y