Equal question mark

Stream: general

[Phiroc]

Hello,
Does anyone know what the Lean equivalent of the Coq =? operator (https://coq.inria.fr/library/Coq.Init.Nat.html) is?
Many thanks.

[Scott Morrison]

Do you mean a bool valued equality operator?

[Kevin Buzzard]

You're asking about boolean equality on nats? In Lean we have this decidable typeclass which I think means that we can avoid this definition completely.

[Scott Morrison]

We don't do it that way: = is Prop valued.

[Scott Morrison]

and then as Kevin says :-)

[Kevin Buzzard]

def nat.beq (m n : ℕ) := if m = n then tt else ff . This compiles because equality on nats is decidable. But why would you need it in Lean? What is it used for in Coq? (I know very little about theorem provers in general, I should say)

[Phiroc]

I’ll give you an example from Sofware Foundations in a sec

[Phiroc]

Theorem plus_1_neq_0 : ∀ n : nat,
(n + 1) =? 0 = false.
Proof.
intros n. destruct n as [| n'] eqn:E.

- reflexivity.
- reflexivity. Qed.
Cf. https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html

[Horatiu Cheval]

Also, if equality is decidable, it can be implicitly converted to bool (but as said, it's not idiomatic)

def b : bool := 2 = 3
#print b -- to_bool (2 = 3)
#reduce b -- ff

[Kevin Buzzard]

The example you give just makes me more confused. Why is it not just more sensible to prove n + 1 ≠ 0?

import tactic

theorem plus_one_ne_zeto (n : ℕ) : n + 1 ≠ 0 :=
begin
  simp,
end

I'm asking "what is the point of having a boolean equality" and your response is "because then we can prove theorems that involve boolean equalities, giving us twice as many theorems". I was hoping for a better answer in some sense.

[Phiroc]

I’m a newbie. I don’t know why they use that operator in the SF book. Let me think about it.

[Kevin Buzzard]

aah, I see: is the point that after induction you can prove the result with refl? Such proofs are discouraged in Lean because we ran into situations where clever rewrites would do the job more quickly than laboriously reducing complex terms and checking for definitional equality. I think it might be a cultural issue here -- the mathlib community is not really focused on constructivism.

[Phiroc]

Although I am only at the beginning of the book, I’ve noticed that the Lean tactics to the SF theorems and exercises are often simpler than those provided by the authors.

[Kevin Buzzard]

OK if you're not an expert then I will just leave you with the following comment. There is a type called bool with two terms tt and ff in Lean. I don't think I've ever used it. There is also a Universe called Prop which has a much richer structure, but if you believe in the law of the excluded middle and propositional extensionality then Prop and bool biject with each other. This proves that they are interchangeable unless you are a constructivist who does not believe in LEM. In Coq they take constructivism very seriously so perhaps have a prop-valued equality and a bool-valued one too. In mathlib, the biggest Lean development, we do not take constructivism particularly seriously, and the constructivists have the decidable typeclass which is doing the explicit translation between Prop and bool in cases where it can be done, but it's just more convenient when doing nonconstructive stuff to work in Prop because it is a richer environment, being a universe and not just a type.

[Phiroc]

What is « constructivism »?

[Johan Commelin]

https://en.wikipedia.org/wiki/Intuitionistic_logic