Zulip Chat Archive

Stream: mathlib4

Topic: use


Heather Macbeth (Oct 28 2022 at 20:56):

I don't know if it's been noticed that the mathlib4 use behaves differently than the mathlib3 one: it seems to behave effectively as use; try { refl }. So this is a full proof in mathlib4:

import Mathlib.Init.Data.Nat.Basic
import Mathlib.Tactic.Use

example :  a : , 3 * a = 15 := by
  use 5

whereas the corresponding mathlib3 proof is

import tactic.interactive

example :  a : , 3 * a = 15 :=
begin
  use 5,
  refl
end

Heather Macbeth (Oct 28 2022 at 21:13):

I would like to advocate for the old behaviour -- use is disproportionately used by novices (power users being more likely to use refine) and novices might find it easier to understand the single-purpose version of the tactic. (I remember @Kevin Buzzard has the NNG disable a similar behaviour in rw, for the same reason.)

If the consensus is for the new behaviour, would anyone mind at least having an option to toggle the old behaviour?

Gabriel Ebner (Oct 28 2022 at 21:38):

We've had a discussion about this some time ago. See the messages around https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20status.3F/near/270894463

Junyan Xu (Oct 28 2022 at 21:40):

The following closes the goal. So probably the Lean 3 use only closes syntactic equalities (just like Lean 3 rw), but Lean 4 goes one step further?

import tactic.interactive

example :  a : , a = 5 :=
begin
  use 5,
end

Gabriel Ebner (Oct 28 2022 at 21:40):

My take on this is that we should change the use behavior anhow. As I've mentioned there, the current behavior is way too magic and nondeterministic, which also prevents us from producing useful error messages.

Gabriel Ebner (Oct 28 2022 at 21:41):

I think both using and not using rfl have arguments going for it. Other tactics like rw do rfl automatically, others don't.

Gabriel Ebner (Oct 28 2022 at 21:44):

use is disproportionately used by novices (power users being more likely to use refine)

I really don't think we should have special tactics for novices in mathlib. This just increases the amount of tactics users have to learn (since you'll have to learn the "grown-up" versions anyhow).

Gabriel Ebner (Oct 28 2022 at 21:45):

(I can see the point of simplified/restricted versions of tactics for courses though.)

Heather Macbeth (Oct 28 2022 at 21:49):

Gabriel Ebner said:

use is disproportionately used by novices (power users being more likely to use refine)

I really don't think we should have special tactics for novices in mathlib. This just increases the amount of tactics users have to learn (since you'll have to learn the "grown-up" versions anyhow).

@Gabriel Ebner To clarify -- are you saying we should get rid of use altogether?

Gabriel Ebner (Oct 28 2022 at 21:49):

Relatedly, I don't think that the power user / novice split for refine / use is because use is simpler. It's because use breaks very easily. For example you can't do use _.

Gabriel Ebner (Oct 28 2022 at 21:50):

are you saying we should get rid of use altogether?

No, I think that a simpler use would be much more useful. One where use foo simply means refine ⟨foo, ?_⟩.

Damiano Testa (Oct 28 2022 at 21:53):

This had never occurred to me: can you use use on iffs?

Damiano Testa (Oct 28 2022 at 21:54):

(either the Lean3 or Lean4 version)

Damiano Testa (Oct 28 2022 at 21:55):

E.g. Gabriel's last suggestion seems to make use _ a possibile alternative to split.

Damiano Testa (Oct 28 2022 at 21:56):

Yes, I'm also so curious that I'm tempted to turn on the computer and try it!

I'll go to sleep instead... :smile:

Gabriel Ebner (Oct 28 2022 at 22:04):

This works in Lean 3:

import tactic.interactive
example : true  true := by use true.intro

Gabriel Ebner (Oct 28 2022 at 22:06):

I think this is very much intentional so that you can use x hx on ∃ y, 0 < y ∧ p y.

Adam Topaz (Oct 28 2022 at 22:07):

I use use pretty frequently. For example, it's useful if you have a goal that's an existential and the term that you need to provide is some complicated deeply nested structure that's eventually just, say, a natural number with various properties at each layer. It's much quicker to write use 37 and have the tactic add all the sidegoals as opposed to refine <<<<37,_>,_>,_>,...>

Damiano Testa (Oct 28 2022 at 22:09):

I was more curious about use h when the goal is P ↔ Q and h : P → Q. Does it work?

Adam Topaz (Oct 28 2022 at 22:09):

I think it does?

Gabriel Ebner (Oct 28 2022 at 22:10):

example : true  true := by use id; exact id

Damiano Testa (Oct 28 2022 at 22:12):

Never, until this discussion, had I thought that use could work in this case!

Adam Topaz (Oct 28 2022 at 22:12):

Here is what I have in mind:

import tactic

structure A :=
(n : )
(p : n = n)

structure B :=
(n : A)
(p : n = n)

structure C :=
(n : B)
(p : n = n)

structure D :=
(n : C)
(p : n = n)

structure E :=
(n : D)
(p : n = n)

example :  q : E, q = q :=
begin
  use 37,
end

Adam Topaz (Oct 28 2022 at 22:12):

I would rather not use refine in this case

Gabriel Ebner (Oct 28 2022 at 22:17):

That is an interesting application.. do we use this often in mathlib? I would have never guessed that you can use use for that (and I guess it only works on the first field).

Adam Topaz (Oct 28 2022 at 22:18):

right it only works for the first field.

Adam Topaz (Oct 28 2022 at 22:18):

I've certainly used it somewhere... I don't remember exactly where (either mathlib or LTE)

Adam Topaz (Oct 28 2022 at 22:23):

What I would really like is to be able to write use A _ B and have it behave as refine <<A,_>,B,_,_,...> (with the obvious generalizations)

Kevin Buzzard (Oct 28 2022 at 22:33):

As Gabriel may remember, use exists because the core Lean 3 existsi was poor at type unification (eg I think things like existsi 37 wouldn't make progress on exists n : int, ...) and Rob wrote use as a more user-friendly version. IIRC existsi _ works though.

Junyan Xu (Oct 28 2022 at 22:39):

I think the reason for not allowing placeholders in use is the expected type is unknown; for example in ⟨⟨A,B⟩,C⟩, use _ could match either the first field of the first field (A) or the entire first field ⟨A,B⟩. Maybe it could fallback to either destruct nothing or destruct everything? use [A, B, C] is allowed though.

Moritz Doll (Oct 29 2022 at 00:47):

existsi in mathlib4 is defined as refine <e, _>, see https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Existsi.lean
which is use without trying trivial

Mario Carneiro (Oct 29 2022 at 00:49):

I thought that we were already aligning existsi to the exists tactic in lean 4?

Moritz Doll (Oct 29 2022 at 00:55):

I cannot remember having a discussion about something like that, maybe that was before I was porting existsi?

Moritz Doll (Oct 29 2022 at 00:59):

Also it seems that use and exists are literally the same tactic.

Moritz Doll (Oct 29 2022 at 01:01):

macro "use " es:term,+ : tactic =>
  `(tactic|(refine $es,*, ?_; try trivial))

and

macro "exists " es:term,+ : tactic =>
  `(tactic| (refine $es,*, ?_; try trivial))

Kevin Buzzard (Oct 29 2022 at 05:44):

Can you prove that two tactics are equal with rfl?

Mario Carneiro (Oct 29 2022 at 05:59):

You can state it, but it's not true:

example :
    Mathlib.Tactic.«_aux_Mathlib_Tactic_Use___macroRules_Mathlib_Tactic_tacticUse_,,_1» =
    Lean.Parser.Tactic.«_aux_Init_Tactics___macroRules_Lean_Parser_Tactic_tacticExists_,,_1» := rfl

the reason being that one of them replaces applications of use ... with stuff and the other replaces exists ...

Damiano Testa (Oct 29 2022 at 06:29):

I never cease to be surprised by how literal computers are... :man_facepalming:

Adam Topaz (Oct 29 2022 at 14:17):

Is there a simple way to obtain the actual name of a tactic/macro, like the ones that Mario used above?

Kyle Miller (Oct 29 2022 at 14:41):

@Gabriel Ebner I use use relatively frequently to instantiate an existential over a subtype, to get two proof obligations (that the term is in the subtype and also the body of the existential). This is a simpler version of Adam's example.

Scott Morrison (Oct 29 2022 at 22:14):

Adam Topaz said:

Is there a simple way to obtain the actual name of a tactic/macro, like the ones that Mario used above?

Probably inserting a whatsnew in before the macro.

Mario Carneiro (Oct 29 2022 at 23:56):

I reused some tricks from the #help command implementation: you can get the name of a macro_rules by searching for uses of the macro attribute corresponding to the syntax:

#eval show MetaM _ from do
  for i in macroAttribute.getEntries ( getEnv) ``Lean.Parser.Tactic.«tacticExists_,,» do
    println! i.declName

The name of the syntax itself can be found by hovering on the macro in macro "exists " ...

Heather Macbeth (Dec 21 2022 at 16:42):

I'd like to reopen this discussion from October about the use tactic. The old use had many features, some advocated for by Adam and Kyle upthread, some considered

Gabriel Ebner said:

way too magic and nondeterministic

by Gabriel. Personally I don't mind whether we implement all the features of the old use or not, but I would really like to get rid of the rfl after filling the existential, since in addition to succeeding or failing by apparent "magic" this could get quite slow.

Two options:

  • get rid of the rfl check entirely, so the tactic is literally refine ⟨foo, ?_⟩ as Gabriel suggested
  • use only equality up to reducible, the way we had in mathlib3 by having it invoke the trivial' tactic rather than the trivial tactic

Heather Macbeth (Dec 21 2022 at 16:59):

I've opened mathlib4#1153 implementing the first option. If we prefer the second option, it will take a tiny bit more work, because we don't seem to have trivial' implemented yet.

Moritz Doll (Dec 21 2022 at 23:05):

We have existsi as refine ⟨foo, ?_⟩ already

Heather Macbeth (Dec 21 2022 at 23:06):

You also pointed out last time we discussed this that the previous implementation of use was the same as exists:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/use/near/306772863

Moritz Doll (Dec 21 2022 at 23:08):

three tactics for two tasks is one tactic too many

Heather Macbeth (Dec 21 2022 at 23:09):

What do you think we should do then? Maybe my second suggestion?

Heather Macbeth said:

  • use only equality up to reducible, the way we had in mathlib3 by having it invoke the trivial' tactic rather than the trivial tactic

Heather Macbeth (Dec 21 2022 at 23:10):

Then it will be three tactics for three tasks, and the nicest name (use) will go to, in my opinion, the best general-purpose choice among those three.

Heather Macbeth (Dec 21 2022 at 23:13):

So then we need trivial' (i.e. trivial at the level of reducible); does anyone know whether its skipping so far was deliberate or accidental? It doesn't show up even on a very early version of the tactic syntax file.
https://github.com/leanprover-community/mathlib4/blob/b0c3952f590d4b2e301d2ffe13bb815856fff1e5/Mathlib/Mathport/Syntax.lean

Heather Macbeth (Dec 22 2022 at 20:16):

@Mario Carneiro told me about with_reducible, which should avoid the need for the variant trivial'. But I don't understand how it works. Is this supposed to be reducibly, definitionally true? (It is accepted by Lean.)

example : 3 * 5 = 5 * 3 := by with_reducible rfl

Last updated: Dec 20 2023 at 11:08 UTC