# Zulip Chat Archive

## Stream: new members

### Topic: How to use choice tactic?

#### Li Yao'an (Nov 20 2019 at 03:20):

When we have an existential statement, we can use choice to construct a witness w. However, while w retains the correct type, the fact that it is a witness to a particular proposition is sometimes (seemingly) lost. Here is an example:

import tactic open function noncomputable theory def inv {α β} (f : α → β) (h : surjective f) : β → α := begin intro b, rw [surjective] at h, choose a h using h b, exact a end theorem should_be_trivial {α β} (f : α → β) (h : surjective f) : let f' := inv f h in ∀ b : β, f (f' b) = b := begin simp, intro b, rw inv, admit end

Rewriting inv gives some scary-looking term, and simp-ing gives "f (classical.some _) = b", when it seems that the proposition that choice was made on has been lost.

What is a good way of recovering the proposition in an existential statement? How could this proof be fixed? (A proof ending with "assumption" would be extra nice, to show how the proposition can be added as a hypothesis)

#### Bryan Gin-ge Chen (Nov 20 2019 at 04:53):

The key is `classical.some_spec`

:

import tactic open function noncomputable theory def inv {α β} (f : α → β) (h : surjective f) : β → α := begin intro b, rw [surjective] at h, choose a h using h b, exact a end theorem should_be_trivial {α β} (f : α → β) (h : surjective f) : let f' := inv f h in ∀ b : β, f (f' b) = b := begin intros f' b, exact classical.some_spec (h b), end -- n.b. using tactics in defs is discouraged (because it leads to scary-looking terms) def inv' {α β} (f : α → β) (h : surjective f) : β → α := λ b, classical.some (h b)

#### Bryan Gin-ge Chen (Nov 20 2019 at 05:22):

`foo_spec`

seems to be the conventional name for the theorem that provides the defining property of `foo`

, e.g. `nat.find_greatest_spec`

(for `nat.find_greatest`

), `finset.choose_spec`

(for `finset.choose`

), etc.

#### Li Yao'an (Nov 20 2019 at 08:20):

Thanks for the reply, but I am still confused. I believe this is at least in part due to the "classical.some _" terms which appear.

It seems to me that after unfolding the definition, the witnesses appear in the interactive tactic window as classical.some _, which does not tell us what the value is a witness for (although Lean seems to know of this). For example:

theorem contrived_example {α β} (f : α → β) (h : surjective f) (a1 a2 : α) (b1 b2 : β) (h2 : a1 = inv' f h b1) (h3 : a2 = inv' f h b2) (h4 : b1 = b2): a1 = a2 := begin rw [h2, h3], dunfold inv', -- At this point the goal is to show "classical.some _ = classical.some _", refl fails simp [h4] -- something happens behind the scenes and it's probably eventually resolved by refl end

Is there a way to elaborate this "classical.some _"?

Additionally, would it be possible to have an interactive tactic to extract the propositions from the values resulting from the application of classical.some? For example, if we had "p : nat -> Prop" and "h : \exists n, p n", then we could replace instances of "classical.some h" with x and add an additional hypothesis "p x".

#### Mario Carneiro (Nov 20 2019 at 08:24):

it's a printing setting. Try setting `set_option pp.proofs true`

#### Kevin Buzzard (Nov 20 2019 at 08:32):

I thought the whole point of `choose`

was so that the user didn't have to know about `classical.some_spec`

?

#### Kevin Buzzard (Nov 20 2019 at 08:35):

Aah I see. So in the `def`

you get the proof you need, but then the def finishes and the proof is lost. I guess you shouldn't be using tactic mode for the definition of the inverse function really. If you define it using `choose`

in `should_be_trivial`

you'll be OK. I guess an alternative is to define `inv`

not just to return a function but to return a pair consisting of a function and the proof that it's an inverse.

#### Kevin Buzzard (Nov 20 2019 at 08:43):

import tactic.linarith open function noncomputable def inv' {α β} (f : α → β) (h : surjective f) : { f' : β → α // ∀ b : β, f (f' b) = b} := begin rw [surjective] at h, choose f' hh using h, exact ⟨f', hh⟩, end

#### Mario Carneiro (Nov 20 2019 at 08:56):

The recommended way to define functions using choice is to write down the property defining the function and prove it straight away with `some`

and `some_spec`

:

def inv {α β} (f : α → β) (h : surjective f) : β → α := λ b, classical.some (h b) theorem should_be_trivial {α β} (f : α → β) (h : surjective f) : let f' := inv f h in ∀ b : β, f (f' b) = b := λ b, classical.some_spec (h b)

#### Mario Carneiro (Nov 20 2019 at 08:56):

The `choose`

tactic is only appropriate if you only need the function local to a proof

#### Li Yao'an (Nov 20 2019 at 09:04):

Thanks everybody who replied. Here is my takeaway from this thread (hopefully useful to any future lost souls):

1) When using choice to extract witnesses, "set_option pp.proofs true" elaborates the tactics state so that it makes sense.

2) We can use classical.some_spec to extract the hypothesis of the witness.

Example:

theorem should_be_trivial {α β} (f : α → β) (h : surjective f) : let f' := inv' f h in ∀ b : β, f (f' b) = b := begin intros f' b, simp [f'], dunfold inv', have := classical.some_spec (h b), -- the argument of some_spec is precisely that of classical.some in the tactic state assumption end

#### Mario Carneiro (Nov 20 2019 at 09:13):

1) Lean doesn't print holes in terms as `_`

, it prints them as `?m_1`

. If you see a `_`

it's a proof that has been suppressed from printing but is present internally

#### Mario Carneiro (Nov 20 2019 at 09:14):

so it's not about "elaborating the tactic state", it's about showing more information (hence the `pp`

for pretty printer)

Last updated: May 13 2021 at 18:26 UTC