choose and autoparams

Stream: general

[Chris Henson]

What is the cleanest way to use autoparams where you would normally use choose? E.g. if I have

import Mathlib

example (h : (k : ℕ) → (h : k < 0) → ∃ x, x = k) : True := by
  choose foo foo_spec using h
  -- foo : (k : ℕ) → k < 0 → ℕ
  -- foo_spec : ∀ (k : ℕ) (h : k < 0), foo k h = k
  sorry

what is the easiest way I can have (h : k < 0 := by grind) in the signature(s)?

[Jakub Nowak]

I don't understand. Could you provide an example of what you want to happen?

[Chris Henson]

Hmm, I'm not sure how to restate more clearly. I'd like to know the best way for instance in the above example to end up with foo : (k : ℕ) → (h : k < 0 := by grind) → ℕ and/or foo_spec : ∀ (k : ℕ) (h : k < 0 := by grind), foo k h = k, does that make sense?

[Jakub Nowak]

Thanks, now I understand.

[Edward van de Meent]

I haven't added autoparams inside a proof before, but presumably this would do it:

have h' : (k : ℕ) → (h' : k < 0 := by grind) → ∃ x, x = k := h
choose foo foo_spec using h'

[Jakub Nowak]

Edward van de Meent said:

I haven't added autoparams inside a proof before, but presumably this would do it:

have h' : (k : ℕ) → (h' : k < 0 := by grind) → ∃ x, x = k := h
choose foo foo_spec using h'

Nope, this doesn't work, choose evaluates autoParam too eagerly.

[Jakub Nowak]

But I suspect, it's possible to make choose handle autoParam so that this works.

[Edward van de Meent]

Wait what? What are you saying choose does here? Surely it isn't able to synthesize a proof of k < 0?

[Edward van de Meent]

(I'm typing from mobile)

[Jakub Nowak]

Yes, it fails, because it couldn't synthesize the proof of k < 0.

[Chris Henson]

Right, it can't synthesize a proof, but will eagerly fail to do so.

[Jakub Nowak]

This does what you want, but the syntax is far from perfect.

import Mathlib

structure NatWrap where
  val : ℕ
  prop : k < 0 := by grind

instance : Coe NatWrap Nat where
  coe w := w.val

example (h : (k : NatWrap) → ∃ (x : ℕ), x = k) : True := by
  choose foo foo_spec using h
  let x := foo (.mk 3)
  have hx := foo_spec (.mk 3)
  dsimp only at hx

[Chris Henson]

The above isn't working in the web editor or locally for me. Did you mean to have prop : 0 < val := by grind for this example?

[Jakub Nowak]

Oh, wait, you just need to write using @h, not using h and it works.

[Jakub Nowak]

Chris Henson said:

The above isn't working in the web editor or locally for me. Did you mean to have prop : 0 < val := by grind for this example?

It works, in the sense, that I tried to prove 3 < 0 using by grind. It failed to prove it of course.

[Jakub Nowak]

Ah, no, sorry, it should be val < 0, not k < 0. But you can also use 0 < val, if you want to see what happens whenby grind succeeds.

[Jakub Nowak]

Anyway, that is obsolete now. This does exactly what you wanted:

import Mathlib.Tactic.Choose

example (h : (k : ℕ) → (h : k < 0 := by grind) → ∃ x, x = k) : True := by
  choose foo foo_spec using @h

[Jakub Nowak]

What happens, is that it wasn't choose fault, that autoProp was eagerly expanded. The term h, when elaborated, already expands autoProp, that's why you need @h.

[Chris Henson]

This is perfect, thanks!

[Chris Henson]

(your explanation is good too!)