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

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⟩


coming right up

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

#3842

Last updated: Aug 03 2023 at 10:10 UTC