## 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