How to use choice tactic?

Stream: new members

[Li Yao'an]

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]

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]

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]

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]

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

[Kevin Buzzard]

I thought the whole point of choose was so that the user didn't have to know about classical.some_spec?

[Kevin Buzzard]

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]

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]

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]

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

[Li Yao'an]

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]

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]

so it's not about "elaborating the tactic state", it's about showing more information (hence the pp for pretty printer)