use of by_cases

Stream: new members

[Lu-Ming Zhang]

a b : nat
Why does by_cases a ≤ b gives me the message "by_cases tactic failed, type of given expression is not decidable"?

[Yakov Pechersky]

can you share #mwe? this works for me

import tactic

example (a b : nat) : true :=
begin
  by_cases a ≤ b,
  { trivial },
  { trivial }
end

[Lu-Ming Zhang]

Sorry. Here is a clarification. I am at Level 9 of the inequality world of the natural number game. Hence, a b: mynat.
Then inputting by_cases a ≤ b gives me the above error message,

[Kevin Buzzard]

Oh hard luck :-) It looks like I did not prove decidability of <= on the NNG version of the natural numbers! I am slightly surprised that everything is not running in classical mode though (where every statement would be decidable) because Freek Wiedijk already complained about this months ago and I thought I fixed it!

[Kevin Buzzard]

Oh -- the good news is that the version of mathlib we're using has the classical tactic, so you can do

classical,
by_cases a ≤ b,

[Eric Wieser]

I thought tactic#by_cases automatically tried classical anyway?

[Eric Wieser]

(it does: https://github.com/leanprover-community/lean/blob/65ad4ffdb3abac75be748554e3cbe990fb1c6500/library/init/meta/tactic.lean#L1567)

[Eric Wieser]

Ah, only since leanprover-community/lean#409. I guess NNG is on lean < 3.18.0?

[Kevin Buzzard]

It's definitely on 3.4.2.

[Kevin Buzzard]

It's officially MS-sanctioned Lean :-)

[Kevin Buzzard]

(apart from the fact that many of the tactics I teach got slightly modified)

[Kevin Buzzard]

hack.png

[Lu-Ming Zhang]

@Kevin Buzzard Thanks for your explanation! What does "decidability" mean in Lean?

[Eric Wieser]

h : decidable p is a proof that "p : Prop is decidable" (docs#decidable)

[Anne Baanen]

≤ is decidable for natural numbers because there's a computer algorithm that can tell you for any two a b : ℕ whether a is less than b. There is no such algorithm for e.g. real numbers (basically because the decimals go on forever) so ≤ is not decidable for real numbers.

[Kevin Buzzard]

<= is decidable for the natural number game type mynat, however I did not prove this in the repo and this is why you got the error.