Converting a proposition to epsilon calculus

Stream: general

[Daniel Weber]

I have a predicate, and I want to do some kind of skolemization on it using docs#Classical.epsilon. As a concrete example:

import Mathlib.Tactic

example {p : Nat → Nat → Nat → Nat → Prop} : False := by
  let f1 (a b) := ∃ c d, p a b c d
  -- here I want to run some procedure on the above f1, to get a result like this:
  let c (a b) := Classical.epsilon (fun c ↦ ∃ d, p a b c d)
  let d (a b) := Classical.epsilon (fun d ↦ p a b (c a b) d)
  clear f1
  let f1 (a b) := p a b (c a b) (d a b)
  have hf : ∀ a b c' d', p a b c' d' → f1 a b := by
    intro a b c' d' h
    simp [f1, c, d]
    have := Classical.epsilon_spec (⟨c', ⟨d', h⟩⟩ : ∃ c, ∃ d, p a b c d)
    apply Classical.epsilon_spec this
  clear_value c d
  /-
p : ℕ → ℕ → ℕ → ℕ → Prop
d c : ℕ → ℕ → ℕ
f1 : ℕ → ℕ → Prop := fun a b => p a b (c a b) (d a b)
hf : ∀ (a b c' d' : ℕ), p a b c' d' → f1 a b
⊢ False
  -/

I assume there's no such tactic currently, although this does look similar to choose. Is there any easy way to do this (it should also be able to handle more quantifiers)? If not, does anybody have any suggestions for how to tweak choose to be able to do this?

[Yaël Dillies]

I am not sure I understand. Shouldn't the first let f1 (a b) := ∃ c d, p a b c d be have f1 (a b) : ∃ c d, p a b c d := sorry?

[Yaël Dillies]

Can you tell us what are the before and after contexts you want to see?

[Daniel Weber]

The before isn't truly important — I have a predicate p and I want to introduce some functions b_i b_{i+1} .. b_n (using docs#Classical.epsilon) such that p a_1 a_2 a_3 .. a_n -> p a_1 ... a_{i-1} (b_i a_1 ... a_{i-1}) (b_{i+1} a_1 ... a_{i-1}) .. (b_n a_1 ... a_{i-1})

[Kevin Buzzard]

Yaël Dillies said:

Can you tell us what are the before and after contexts you want to see?

I'm assuming that the before is the state of the example before the code, and the after is the state in the comment at the end! My instinct was that choose would do this but I can't get it to work. Ironically I always think that the docstring for choose is poor because it only has one example which is quite complicated, but actually the example is very close to what seems to be wanted here.

[Kevin Buzzard]

Oh I see, Yael's comment is precisely that if one changes f1 to the thing that choose wants, then choose will work.

[Daniel Weber]

choose takes a proof, while I want to skolemize the proposition directly, even if it's not true for all values

[Eric Wieser]

It would be pretty silly, but you could create a meta variable of your type, call choose on it, revert all the introduced hypotheses, then inferType

[Kevin Buzzard]

This might not work because choose ... using f seems to want f to be a proof

[Yury G. Kudryashov]

You can use choose! on fun a b (h : ∃ c d, ...) => h

[Yury G. Kudryashov]

Provided that the types of c and d are nonempty.

[Yury G. Kudryashov]

Then you'll get c d : Nat -> Nat -> Nat and H : ∀ a b, (∃ c d, p a b c d) → p a b (c a b) (c a d).

[Yury G. Kudryashov]

Possibly, we should add this trick to the docstring of choose!.

[Daniel Weber]

Yury G. Kudryashov said:

You can use choose! on fun a b (h : ∃ c d, ...) => h

Thanks!