choose crashes Lean

Stream: general

[Kenny Lau]

The following code crashes Lean:

import tactic.interactive

example (h : true ∧ ∀ i : ℕ, ∃ j : ℕ, i ≠ j) : true :=
by choose f using h.2

"Server has stopped with error code 3221225477."
(the error code is consistent)

[Keeley Hoek]

3221225477 = 0xC0000005, the access violation error code on Windows. Probably the stack is running out?

[Reid Barton]

It crashes for me on Linux too. I think this is the top of the stack trace of the thread that crashed:

#0  0x0000000000431241 in lean::name::imp::display_core(std::ostream&, lean::name::imp*, bool, char const*) ()
#1  0x0000000000431257 in lean::name::imp::display_core(std::ostream&, lean::name::imp*, bool, char const*) ()
#2  0x0000000000432295 in lean::operator<<(std::ostream&, lean::name const&) ()
#3  0x0000000000939bf8 in lean::revert(lean::list<lean::expr> const&, lean::tactic_state const&, bool) ()
#4  0x000000000093a0d9 in lean::tactic_revert_lst(lean::vm_obj const&, lean::vm_obj const&) ()

[Reid Barton]

Looks like maybe choose is invoking tactic.revert with h.2, and that crashes for some reason while trying to print an error?

[Simon Hudon]

revert has some issues when you misuse it. I fixed that in Lean 3.5.0

[Simon Hudon]

It's probably being called with something that isn't a local_const

[Bryan Gin-ge Chen]

In Lean 3.5.0c it doesn't crash and instead returns this:

revert tactic failed, expecting local variable, found 'and.right true (Pi (i : nat), (Exists.{1} nat (fun (j : nat), (ne.{1} nat i j)))) h'
state:
h : true ∧ ∀ (i : ℕ), ∃ (j : ℕ), i ≠ j
⊢ true

web-editor link

[Simon Hudon]

The error message could be better but it's at least clearer than a crash

[Kevin Buzzard]

Is this an issue with choose that can be fixed in mathlib so my users can use choose in 3.4.2?

[Patrick Massot]

You can still use choose in normal situations. Do you have a real use case where there is a problem?

[Kevin Buzzard]

@Amelia Livingston said it crashed her Lean.

[Amelia Livingston]

It's happened to me a couple of times; the example obviously not a real use case but the definition essentially is. I can't remember if choose is supposed to work in definitions though (hence the example too). Both of these crash Lean on their own with the same error code as above.

import tactic.basic
universe u

example {α : Type u} [comm_semiring α] (a b : α) (h : a ∣ b) : ∃ c, b = c * a :=
by choose c using exists_eq_mul_right_of_dvd h

def blah {α : Type u} [comm_semiring α] (a b : α) (h : a ∣ b) : α :=
by choose c using exists_eq_mul_right_of_dvd h

[Patrick Massot]

It's bad that Lean crashes, but exists_eq_mul_right_of_dvd h is not at all the kind of statement that choose is meant to consume.

[Amelia Livingston]

Ah - I'm pretty new to this; what sort of statement is better suited to choose?

[Patrick Massot]

"choose" is meant in the strong sense of "instantly make infinitely many choice", aka "use the axiom of choice".

[Kevin Buzzard]

import tactic.basic
universe u

noncomputable def blah {α : Type u} [comm_semiring α] (a b : α) (h : a ∣ b) : α :=
begin
  choose c h2 using (exists_eq_mul_right_of_dvd h),
  exact c
end

works for me

[Kevin Buzzard]

noncomputable def blah {α : Type u} [comm_semiring α] (a b : α) (h : a ∣ b) : α :=
  classical.some (exists_eq_mul_right_of_dvd h)

avoids the tactic completely.

[Patrick Massot]

Oh, right, Amelia also forgot to name the property

[Kevin Buzzard]

But this stops the crash :D

[Patrick Massot]

Anyway, the idiomatic mathlib way is rcases exists_eq_mul_right_of_dvd h with ⟨c, h2⟩, or, since last week, the gorgeous

obtain ⟨c, h2⟩ : ∃ c, b = a*c, from exists_eq_mul_right_of_dvd h,

[Amelia Livingston]

Aha... that works for me too. Thank you. It's not so easy to notice user error when user error is crashing Lean.
Surely you can't use rcases in a definition though?

[Patrick Massot]

What do you mean?

[Amelia Livingston]

Because of the induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop error

[Patrick Massot]

oh I see. Then you could use choose or, more traditionally, classical.some and its friends

[Patrick Massot]

We should really have a documentation file about these issues. Just like what Chris wrote about finite sets or well-founded recursion.

[Patrick Massot]

It would probably a very good exercise for you to write it.

[Patrick Massot]

It would be in mathlib's greatest documentation writing tradition. You prepare a list of examples that you can't do, or at least not without suffering. Then you ask here until you have nice and elegant solutions for all (or you people write a new helper tactic) and then you proudly put all the explanations in the docs folder.

[Amelia Livingston]

Thanks for the help. I would love to give that a go, yeah!

[Patrick Massot]

All files in https://github.com/leanprover-community/mathlib/tree/master/docs/extras were written using this strategy.