Zulip Chat Archive

Stream: new members

Topic: Boolean equality on nats


Donald Sebastian Leung (Feb 22 2020 at 06:04):

In the Coq standard library, there is a boolean test for equality on the natural numbers n =? m which returns true if n and m are equal and false otherwise. Is there a similar function in Lean?

On the other hand, I found nat.decidable_eq in the Lean stdlib which I presume is analogous to Coq's sumbool. In Coq, we can convert it into a boolean by placing it in an if/then/else as follows (assuming eq_dec is our sumbool instance): if eq_dec then true else false. Is there a similar mechanism in Lean?

Donald Sebastian Leung (Feb 22 2020 at 06:12):

Donald Sebastian Leung said:

In the Coq standard library, there is a boolean test for equality on the natural numbers n =? m which returns true if n and m are equal and false otherwise. Is there a similar function in Lean?

On the other hand, I found nat.decidable_eq in the Lean stdlib which I presume is analogous to Coq's sumbool. In Coq, we can convert it into a boolean by placing it in an if/then/else as follows (assuming eq_dec is our sumbool instance): if eq_dec then true else false. Is there a similar mechanism in Lean?

I skipped to Chapter 10 and found that you could pattern-match on nat.decidable_eq n m (for some n m : ℕ)

Bryan Gin-ge Chen (Feb 22 2020 at 06:46):

In Lean, you can use if ... then ... else on decidable Props like this:

def foo (m n : ) : bool := if m = n then tt else ff

#eval foo 2 3

You can also coerce decidable Props to bools:

#eval (2 = 3 : bool)

def foo' (m n : ) : bool := m = n

#print foo' -- `to_bool` is inserted

Donald Sebastian Leung (Feb 22 2020 at 06:47):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC