Zulip Chat Archive

Stream: maths

Topic: ring bug? use bug?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 08 2019 at 09:24):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Oct 08 2019 at 09:31):

existsi instead of use works.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 08 2019 at 09:33):

Thanks Rob.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Keeley Hoek (Oct 08 2019 at 11:53):

Has this turned into a pull request?

view this post on Zulip Keeley Hoek (Oct 08 2019 at 11:53):

Oh damn it was like 10mins ago

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 08 2019 at 11:55):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Rob Lewis (Oct 08 2019 at 12:00):

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

view this post on Zulip Rob Lewis (Oct 08 2019 at 12:01):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Oct 08 2019 at 14:11):

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

view this post on Zulip Patrick Massot (Oct 08 2019 at 14:12):

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

view this post on Zulip Rob Lewis (Oct 08 2019 at 14:14):

It should be negligible.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Oct 08 2019 at 14:37):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 12 2019 at 10:57):

I don't think that was ever supposed to work

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 12 2019 at 10:59):

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

view this post on Zulip 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