use

Stream: mathlib4

[Heather Macbeth]

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]

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]

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]

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]

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]

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]

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]

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

[Heather Macbeth]

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]

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]

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]

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

[Damiano Testa]

(either the Lean3 or Lean4 version)

[Damiano Testa]

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

[Damiano Testa]

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]

This works in Lean 3:

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

[Gabriel Ebner]

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

[Adam Topaz]

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]

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

[Adam Topaz]

I think it does?

[Gabriel Ebner]

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

[Damiano Testa]

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

[Adam Topaz]

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]

I would rather not use refine in this case

[Gabriel Ebner]

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]

right it only works for the first field.

[Adam Topaz]

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

[Adam Topaz]

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]

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]

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]

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]

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

[Moritz Doll]

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

[Moritz Doll]

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

[Moritz Doll]

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

and

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

[Kevin Buzzard]

Can you prove that two tactics are equal with rfl?

[Mario Carneiro]

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]

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

[Adam Topaz]

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

[Kyle Miller]

@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]

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]

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]

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]

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]

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

[Heather Macbeth]

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]

three tactics for two tasks is one tactic too many

[Heather Macbeth]

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]

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]

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]

@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