non dependent chooser

Stream: general

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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]

@Simon Hudon proposed another feature for choose in #3699, if he does that then maybe this could happen at the same time.

[Reid Barton]

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]

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]

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]

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]

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]

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]

@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]

how would you present the negative case if f had several propositional arguments (which I assume are all getting deleted)?

[Mario Carneiro]

also, y could be a function

[Anatole Dedecker]

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]

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]

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]

@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]

Sure, I will look into it

[Anatole Dedecker]

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

[Patrick Massot]

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

[Mario Carneiro]

@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]

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]

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

[Sebastien Gouezel]

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]

coming right up

[Mario Carneiro]

#3842