## Stream: maths

### Topic: ring bug? use bug?

#### Kevin Buzzard (Oct 08 2019 at 09:23):

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 (Oct 08 2019 at 09:24):

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 (Oct 08 2019 at 09:24):

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

#### Rob Lewis (Oct 08 2019 at 09:31):

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 (Oct 08 2019 at 09:31):

existsi instead of use works.

#### Kevin Buzzard (Oct 08 2019 at 09:33):

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

Thanks Rob.

#### Rob Lewis (Oct 08 2019 at 09:41):

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 (Oct 08 2019 at 09:42):

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 (Oct 08 2019 at 09:46):

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 (Oct 08 2019 at 10:03):

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 (Oct 08 2019 at 11:31):

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 (Oct 08 2019 at 11:43):

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 (Oct 08 2019 at 11:44):

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

#### Rob Lewis (Oct 08 2019 at 11:44):

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

#### Keeley Hoek (Oct 08 2019 at 11:53):

Has this turned into a pull request?

#### Keeley Hoek (Oct 08 2019 at 11:53):

Oh damn it was like 10mins ago

#### Rob Lewis (Oct 08 2019 at 11:55):

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 (Oct 08 2019 at 11:55):

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

#### Rob Lewis (Oct 08 2019 at 11:55):

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

#### Patrick Massot (Oct 08 2019 at 11:56):

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 (Oct 08 2019 at 11:58):

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 (Oct 08 2019 at 11:59):

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 (Oct 08 2019 at 12:00):

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

#### Rob Lewis (Oct 08 2019 at 12:01):

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

#### Rob Lewis (Oct 08 2019 at 12:01):

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 (Oct 08 2019 at 12:01):

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

#### Keeley Hoek (Oct 08 2019 at 12:20):

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 (Oct 08 2019 at 12:26):

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 (Oct 08 2019 at 14:11):

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

#### Patrick Massot (Oct 08 2019 at 14:12):

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

#### Rob Lewis (Oct 08 2019 at 14:14):

It should be negligible.

#### Keeley Hoek (Oct 08 2019 at 14:21):

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 (Oct 08 2019 at 14:34):

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 (Oct 08 2019 at 14:37):

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

#### Reid Barton (Oct 08 2019 at 15:21):

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 (Oct 12 2019 at 10:51):

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 (Oct 12 2019 at 10:54):

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 (Oct 12 2019 at 10:57):

I don't think that was ever supposed to work

#### Mario Carneiro (Oct 12 2019 at 10:58):

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 (Oct 12 2019 at 10:58):

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 (Oct 12 2019 at 10:59):

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

#### Mario Carneiro (Oct 12 2019 at 10:59):

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

Last updated: May 14 2021 at 19:21 UTC