confusion in the "use" tactic

Stream: new members

[Shanghe Chen]

Hi reading MIL Chapter 04
I see lots of proofs using the tactic use. I am quite confused in the deference between use and exists

[Shanghe Chen]

for example all these work:

variable {α β : Type*}
#check α
#check β
variable (f : α -> β)
variable (s t : Set α)
variable (u v : Set β)

open Function
open Set

example : s ⊆ f ⁻¹' (f '' s) := by
  intro x xs
  show f x ∈ f '' s
  use x
  -- exists x -- this works
  -- use x, xs -- this works too
  -- refine ⟨x, xs, rfl⟩ -- this also works

[Shanghe Chen]

The doc Mathlib.Tactic.Use says it's equivalent to refine with placeholders automatically inserted. But I cannot find the document for refine

[Kyle Miller]

If you hover over refine you get some documentation:

refine e behaves like exact e, except that named (?x) or unnamed (?_)
holes in e that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.

[Kyle Miller]

If there are no holes you can (and probably should) use exact instead, for example exact ⟨x, xs, rfl⟩ in the above.

[Kyle Miller]

The exists a,b,c tactic is equivalent to doing refine ⟨a,b,c,?_⟩; try trivial

[Kyle Miller]

It should be the case that exists a,b,c can always be replaced by use a,b,c (though you may have to follow it up with trivial since use uses slightly different tactics than try trivial afterwards).

Note that use x works in your above example, you don't need use x, xs.

[Shanghe Chen]

Ah I see the doc for refine now. I pressed F12 to goto doc in vscode before which shows something like

@[builtin_tactic «refine»] def evalRefine : Tactic := fun stx =>

[Kyle Miller]

"go to definition" goes to the implementation, but "go to declaration" goes to the syntax definition, which is where docstrings generally are placed.

[Shanghe Chen]

Yeah I didn't notice the difference before :tada: Thank you very much Kyle

[Kyle Miller]

The difference between exists and use is that use is smarter about handling nested inductive types. use a,b,c essentially detects whether it should do refine ⟨a,b,c,?_⟩ or exact ⟨a,b,c⟩. (Keep in mind that anonymous constructor notation is right associative, so ⟨a,b,c⟩ could stand for ⟨a,⟨b,c⟩⟩, for example in a nested Exists.

[Kyle Miller]

There's also use!, which is smarter still.

[Shanghe Chen]

Yeah I am kind of getting it now

[Kyle Miller]

In the following, use! x is the same as refine ⟨⟨x, ?property⟩, ?h⟩

example (s : Set α) (x : α) (p : α → Prop) : ∃ y : s, p y := by
  use! x
  -- case property
  -- ...
  -- ⊢ x ∈ s
  --
  -- case h
  -- ...
  -- ⊢ p ↑{ val := x, property := ?property }

[Kyle Miller]

It is willing to put more effort into applying constructors until it can use something.

[Shanghe Chen]

I am not getting the example for use!, from the document it seems similar to simp at * that manuplates both the goal and the existing varaibles. Changing it to

import Mathlib.tactic

variable (α : Type)
example (s : Set α) (x : α) (h : x ∈ s) (p : α → Prop) : ∃ y : s, p y := by
  use! x

I get a new goal:

unsolved goals
case h
α : Type
s : Set α
x : α
h : x ∈ s
p : α → Prop
⊢ p ↑{ val := x, property := h }

[Shanghe Chen]

what is { val := x, property := h } here?

[Shanghe Chen]

Oh hovering on the goal I understand the meaning of { val := x, property := h }. It's a term of the subtype { α // p}

[Shanghe Chen]

This works :tada: very smart indeed

import Mathlib.tactic

variable (α : Type)
example (s : Set α) (x : α) (h : x ∈ s) (p : α → Prop) (g : p x) : ∃ y : s, p y := by
  use! x
  -- case property
  -- ...
  -- ⊢ x ∈ s
  --
  -- case h
  -- ...
  -- ⊢ p ↑{ val := x, property := ?property }

[Shanghe Chen]

I found that if I were in the halfway of the tatic use, the goal does not show what I shoud supply to use furthur more, as in the following example:

import Mathlib.Tactic
open Set
open Function

variable {α β : Type*}
variable (f : α → β)
variable (s t : Set α)

example : f '' s ∪ f '' t ⊆ f '' (s ∪ t):= by
  rintro x (⟨x, xs, rfl⟩|⟨x, xt, rfl⟩)
  use x, Or.inl xs -- Here after comma, the goal does not hint the rest goal
  use x -- should add `, Or.inr xt`

[Shanghe Chen]

Oh it does change the goal, perfect :tada:

example : f '' s ∪ f '' t ⊆ f '' (s ∪ t):= by
  rintro x (⟨x, xs, rfl⟩|⟨x, xt, rfl⟩)
  use x, Or.inl xs -- Here after comma, the goal does not hint the rest goal
  -- before this the goal is:
  --    α : Type u_1
  --    β : Type u_2
  --    f : α → β
  --    s t : Set α
  --    x : α
  --    xt : x ∈ t
  --    ⊢ f x ∈ f '' (s ∪ t)
  use x
  -- now it's x ∈ s ∪ t ∧ f x = f x
  -- it hints the usage of `, Or.inr xt`

[Kyle Miller]

With tauto, you can discharge each goal after use x. The <;> causes the same tactic script to be used for each goal produced by rintro.

example : f '' s ∪ f '' t ⊆ f '' (s ∪ t):= by
  rintro _ (⟨x, xs, rfl⟩|⟨x, xt, rfl⟩)
    <;> · use x; tauto

[Kyle Miller]

There's also use x (discharger := tauto), which does basically the same thing