Stream: general

Topic: Equal question mark

Phiroc (Mar 18 2021 at 09:46):

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 (Mar 18 2021 at 09:56):

Do you mean a bool valued equality operator?

Kevin Buzzard (Mar 18 2021 at 09:56):

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 (Mar 18 2021 at 09:56):

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

Scott Morrison (Mar 18 2021 at 09:56):

and then as Kevin says :-)

Kevin Buzzard (Mar 18 2021 at 09:57):

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 (Mar 18 2021 at 09:58):

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

Phiroc (Mar 18 2021 at 09:58):

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 (Mar 18 2021 at 09:59):

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 (Mar 18 2021 at 10:02):

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 (Mar 18 2021 at 10:07):

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

Kevin Buzzard (Mar 18 2021 at 10:07):

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 (Mar 18 2021 at 10:11):

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 (Mar 18 2021 at 10:12):

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 (Mar 18 2021 at 10:13):

What is « constructivism »?

Johan Commelin (Mar 18 2021 at 10:16):

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

Last updated: May 14 2021 at 03:27 UTC