# Zulip Chat Archive

## Stream: general

### Topic: non dependent chooser

#### Patrick Massot (Aug 12 2020 at 10:57):

Dear expert tactic writers, a couple of years ago, I wrote the first version of the `choose`

tactic. It was a very simple wrapper around `classical.some`

and `classical.some_spec`

, but already very useful for mathematicians. Very quickly, Johannes made it much more general so that it's more useful but I probably lost hope to understand the code. Now I would need a new version and I don't know what to do (I could build an independent stupid version but it would probably be better to integrate it as an option to `choose`

). The situation that came up several times recently is this:

```
import tactic
noncomputable theory
variables {X Y : Type*} [nonempty Y] {P : X → Prop} {Q :Y → Prop}
def bad_chooser (h : ∀ x, P x → ∃ y, Q y) : Π x, P x → Y := λ x hx, classical.some $ h x hx
lemma choose_aux (h : ∀ x, P x → ∃ y, Q y) : ∀ x, ∃ y, P x → Q y :=
begin
intros x,
by_cases hx : P x,
{ cases h x hx with y hy,
use [y, λ _, hy] },
{ inhabit Y,
use default Y }
end
def chooser (h : ∀ x, P x → ∃ y, Q y) : X → Y :=
λ x, classical.some (choose_aux h x)
lemma chooser_spec (h : ∀ x, P x → ∃ y, Q y) : ∀ x, P x → Q (chooser h x) :=
λ x, classical.some_spec (choose_aux h x)
```

The issue with `bad_chooser`

is that the dependent function type is often less convenient to use as the version offered by the last two declarations. And `choose f hf using h`

currently gives the bad version.

#### Patrick Massot (Aug 12 2020 at 10:58):

Let me ping @Anatole Dedecker since he is the latest one to have stumbled on this.

#### Patrick Massot (Aug 12 2020 at 11:29):

Actually the above version is already not general enough, I should have written:

```
variables {X Y : Type*} [nonempty Y] {P : X → Prop} {Q :X → Y → Prop}
lemma classical.choose_aux (h : ∀ x, P x → ∃ y, Q x y) : ∀ x, ∃ y, P x → Q x y :=
begin
intros x,
by_cases hx : P x,
{ cases h x hx with y hy,
use [y, λ _, hy] },
{ inhabit Y,
use default Y }
end
noncomputable
def classical.chooser (h : ∀ x, P x → ∃ y, Q x y) : X → Y :=
λ x, classical.some (classical.choose_aux h x)
lemma classical.chooser_spec (h : ∀ x, P x → ∃ y, Q x y) : ∀ x, P x → Q x (classical.chooser h x) :=
λ x, classical.some_spec (classical.choose_aux h x)
```

#### Patrick Massot (Aug 12 2020 at 11:30):

Anatole, while waiting for a potential improved version of `choose`

, you can put those functions and lemmas somewhere and then in your proof, use:

```
have : ∀ x ∈ Ioo a b, ∃ c ∈ Ioo a x, (f x) * (g' c) = (g x) * (f' c),
{ intros x hx,
rw [← sub_zero (f x), ← sub_zero (g x)],
exact exists_ratio_has_deriv_at_eq_ratio_slope' g g' hx.1 f f'
(λ y hy, hgg' y $ sub x hx hy) (λ y hy, hff' y $ sub x hx hy) hga hfa
(tendsto_nhds_within_of_tendsto_nhds (hgg' x hx).continuous_at.tendsto)
(tendsto_nhds_within_of_tendsto_nhds (hff' x hx).continuous_at.tendsto) },
simp_rw exists_prop at this,
let c := classical.chooser this,
have hc := classical.chooser_spec this,
```

#### Rob Lewis (Aug 12 2020 at 11:33):

@Simon Hudon proposed another feature for `choose`

in #3699, if he does that then maybe this could happen at the same time.

#### Reid Barton (Aug 12 2020 at 11:39):

Maybe it would be better to treat this as two operations, `choose`

with the current behavior followed by `extend`

which extends a partial function to a total one

#### Patrick Massot (Aug 12 2020 at 12:03):

I agree with both Rob and Reid. I'll experiment with Reid's version, but I need to disappear for one day and a half.

#### Patrick Massot (Aug 12 2020 at 12:43):

Reid, did you mean some version of:

```
def extend (f : Π x, P x → Y) : X → Y :=
λ x, if hx : P x then f x hx else default Y
def chooser' (h : ∀ x, P x → ∃ y, Q y) : X → Y :=
extend (λ x hx, classical.some $ h x hx)
lemma chooser_spec' (h : ∀ x, P x → ∃ y, Q y) : ∀ x, P x → Q (chooser' h x) :=
begin
intros x hx,
simp [chooser', extend, hx],
exact classical.some_spec (h x hx)
end
```

and now I really leave (I'll read Zulip but won't have Lean for one day and a half).

#### Mario Carneiro (Aug 12 2020 at 12:47):

any ideas on syntax? I think I know how this can be implemented, but the new strategy requires `Y`

to be inhabited/has_zero/nonempty

#### Mario Carneiro (Aug 12 2020 at 12:51):

For example `choose! f hf using h`

will do the same thing as `choose`

but it will remove all propositional arguments from `f`

using a default value that it magics up somehow

#### Mario Carneiro (Aug 12 2020 at 12:52):

the under the hood implementation can be as reid says, but I think it would be nicer from the user point of view to be able to do both parts in one tactic call

#### Reid Barton (Aug 12 2020 at 13:04):

@Patrick Massot I'm imagining something along the following lines--not sure how feasible this is to implement:

```
-- α β : Type
-- y : β
-- P : α → Prop
-- Q : β → Prop
-- f : Π (x : α), P x → β
-- hf : ∀ (x : α) (H : P x), Q (f x H)
extend f [using y] [with hf'],
-- f : α → β
-- hf : ∀ (x : α), P x → Q (f x)
-- hf' : ∀ (x : α), (¬ P x) → f x = y
```

#### Mario Carneiro (Aug 12 2020 at 13:06):

how would you present the negative case if `f`

had several propositional arguments (which I assume are all getting deleted)?

#### Mario Carneiro (Aug 12 2020 at 13:07):

also, `y`

could be a function

#### Anatole Dedecker (Aug 12 2020 at 13:28):

Patrick Massot said:

Anatole, while waiting for a potential improved version of

`choose`

, you can put those functions and lemmas somewhere and then in your proof, use [...]

I know Patrick can't answer now, but what would be a good place to put this into the library ?

#### Patrick Massot (Aug 13 2020 at 20:47):

Mario Carneiro said:

For example

`choose! f hf using h`

will do the same thing as`choose`

but it will remove all propositional arguments from`f`

using a default value that it magics up somehow. the under the hood implementation can be as reid says, but I think it would be nicer from the user point of view to be able to do both parts in one tactic call

This all sounds perfect to me. My initial reaction to `choose!`

was: no the exclamation mark means "try harder", but I managed to convinced myself that eliminating propositional arguments was trying harder to make a (non-dependent) function.

#### Patrick Massot (Aug 13 2020 at 20:50):

Anatole Dedecker said:

Anatole, while waiting for a potential improved version of

`choose`

, you can put those functions and lemmas somewhere and then in your proof, use [...]I know Patrick can't answer now, but what would be a good place to put this into the library ?

It could be in `logic.function.basic`

but if Mario says he can merge it into the `choose`

tactic soon then he will handle that. In any case I think we need the definition and lemma outside of the tactic, since we can want to use it in term mode definitions.

#### Patrick Massot (Aug 15 2020 at 16:20):

@Mario Carneiro could you tell whether you intend to work on this improvement to `choose`

in the near future? We need to decide whether #3740 is waiting for this.

#### Mario Carneiro (Aug 15 2020 at 16:22):

Sure, I will look into it

#### Anatole Dedecker (Aug 15 2020 at 16:22):

Oh yeah I completely forgot to make a PR for Patrick's lemmas, sorry :(

#### Patrick Massot (Aug 15 2020 at 16:24):

Mario doesn't need us to prove those lemmas, this is negligible compared to the tactic side.

#### Mario Carneiro (Aug 15 2020 at 20:28):

@Patrick Massot :tada: #3806

```
example (h : ∀n m : ℕ, n < m → ∃i j, m = n + i ∨ m + j = n) : true :=
begin
choose! i j h using h,
guard_hyp i := ℕ → ℕ → ℕ,
guard_hyp j := ℕ → ℕ → ℕ,
guard_hyp h := ∀ (n m : ℕ), n < m → m = n + i n m ∨ m + j n m = n,
trivial
end
```

#### Sebastien Gouezel (Aug 17 2020 at 10:16):

I tried to use the new choose to streamline the proof of Baire theorem, and it seems to me that this use case is not covered by the new version. The issue is that the type might be empty, but in the choosing process there is a universal quantification over this type, so if the type is empty everything becomes trivial. Here is a mwe:

```
import analysis.normed_space.basic
lemma zou {α : Type*} (p : α → Prop) (q : α → α → Prop)
(h : ∀ (x : α), p x → ∃ y, q x y) :
∃ F : α → α, ∀ x, p x → q x (F x) :=
begin
have : ∀ (x : α), ∃ y, p x → q x y,
{ assume x,
by_cases hx : p x,
{ simpa [hx] using h x hx },
{ use x } },
choose F hF using this,
exact ⟨F, hF⟩
end
```

I would like to be able to `choose! F hF using h`

, but `α`

might be empty.

#### Patrick Massot (Aug 17 2020 at 10:48):

Do you mean you want a special case where the target type appears in the variables as well?

#### Sebastien Gouezel (Aug 17 2020 at 11:59):

Yes, when a target type appears in a forall, then the forall variable could be used as a default value (or to inhabit the type). In my mwe, I would like the proof to be

```
choose! F hF using h
exact ⟨F, hF⟩
```

#### Mario Carneiro (Aug 17 2020 at 15:03):

coming right up

#### Mario Carneiro (Aug 17 2020 at 18:19):

Last updated: Aug 03 2023 at 10:10 UTC