use vs. exists

Stream: general

[Mirek Olšák]

I was usually using exists, then someone mentioned to me that use is recommended. What is the difference? I thought I could see a difference in the examples provided by the docs of use but that is not much helpful, these are the examples in the docs of use:

example : ∃ x : Nat, x = x := by use 42
-- all `use`, `exists`, `use!` succeed

example : ∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42
-- all `use`, `exists`, `use!` succeed

example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")
-- all `use`, `exists`, `use!` succeed

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42
-- Error no matter which tactic I write, bug in the docs I suppose

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! (42, 42)
-- all `use`, `exists`, `use!` succeed

[Mirek Olšák]

Oh, I see in cases like

inductive Foo : Prop
| intro (x y : Nat) (h : x < y)

example (a b : Nat) (h : a < b) : Foo := by
  use a -- here exists fails

there should be also a more natural example without a custom structure...

[Kyle Miller]

The difference between exists and use doesn't really appear until you have constructors with more than two arguments.

The use! tactic is able to flatten structures. Unlike you, I'm seeing that use! succeeds in the following example (using the latest Mathlib on live.lean-lang.org)

example : ∃ p : Nat × Nat, p.1 = p.2 := by use! 42, 42

You can do use! 42 as well.

[Kyle Miller]

Maybe the difference is that I tested it with import Mathlib.Tactic.Common. Importing all of Mathlib breaks it for some reason.

[Kyle Miller]

Ah, if you do use! 42 you can see the problem. It's using the OfNat instance for ℕ × ℕ. The use! tactic tries elaborating a value for a constructor field, and if that fails, then it tries going into that constructor field. Unfortunately for this example, elaboration succeeds for ℕ × ℕ.

[Kyle Miller]

Here's one that works with all of Mathlib imported:

example : ∃ p : Bool × Nat, p.1 = p.2 := by use! true, 1; rfl

[Mirek Olšák]

Interesting, I am usually just doing import Mathlib, sometimes import Mathlib.Tactic

[Kyle Miller]

It's a surprise, but at least it's not a bug.

For what it's worth, this example is in MathlibTest/Use.lean, to make sure the docstring is accurate. (That said, the "forty-two" example is not in the test file...)

[Mirek Olšák]

Even if if it is not a bug, wouldn't it be helpful to have more stable & demonstrative examples?

[Mirek Olšák]

Or maybe use!just cannot be stable under different import...

[Kyle Miller]

Feel free to make a PR to improve the docstring, with some more realistic examples (and make sure the test file actually includes all the docstring examples). You can't completely protect against all possible imports, but you can at least protected against obvious culprits — in this case the cartesian product has a natural algebraic structure.

[Kyle Miller]

You could also use a type ascription in the use argument to protect against it, and use the example as a gotcha of use!.

[Mirek Olšák]

Ok, will think about better examples, I am not sure if I understand it perfectly but hopefully better now.

[Mirek Olšák]

Perhaps these examples?

1. use, but not exists

example : Nonempty Nat := by use 5
example : Nonempty (ℕ+ ≃ ℕ) := by
  use PNat.natPred, Nat.succPNat
  · exact PNat.succPNat_natPred
  · intro; rfl

2. use! but not use

example : ∃ n : {n : Nat // n%2 = 0}, n.val > 10 := by use! 20; simp

[Kyle Miller]

Those seem reasonable. I'm actually surprised that the second example can be done with use; I'd have expected use! since this needs to first apply the Nonempty constructor.

[Mirek Olšák]

Kyle Miller said:

Feel free to make a PR to improve the docstring, with some more realistic examples (and make sure the test file actually includes all the docstring examples).

Like this? https://github.com/leanprover-community/mathlib4/pull/32699
I needed to import some more files to make the example with PNat working, which also caused the ℕ notation in the tests.

[Violeta Hernández]

I've not once used exists. I always assumed it was some kind of holdover, or one of those "for teaching only" tactics.

[Mirek Olšák]

Violeta Hernández said:

I've not once used exists. I always assumed it was some kind of holdover, or one of those "for teaching only" tactics.

Poor exists... On the other hand, isn't it the case that exists is good enough for 90% cases of your applications of use? I would say exists is a natural word to write when you don't know the tactic but I would approve making it a direct synonym to use. Then I am also aware of existsi which doesn't try the automatic discharging (so its output is more predictable).

[Michael Rothgang]

To me, using use to fill an existential feels more natural thanexists.

[Mirek Olšák]

Nothing against that, perhaps I just knew exists from Rocq, or an older Lean version... but what is the long-term plan with exists & existsi when they seem to be almost forgotten by the community?

[Mirek Olšák]

I am actually a little surprised that existsi is a Mathlib tactic, and smarter exists is a Core tactic.

[Kyle Miller]

Maybe one day the core exists will do what use does, and mathlib's can be a synonym. That seems like a reasonable outcome. For the short term though it seems low-priority to do anything about it.

Something that would be neat is if use could avoid splitting the goal, if it would reassemble the goal into an existential as needed.

It would also be neat if use could make use of the names of constructor fields or of the binders for existentials. For example, if your goal was exists x, exists y, ..., imagine being able to do use y := 3. Or if the goal was a structure, write use invFun := fun x => .... Havig use reassemble the goal as an existential would enable you to use use to introduce choices one at a time.