Zulip Chat Archive

Stream: general

Topic: Equal question mark


view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 18 2021 at 09:56):

Do you mean a bool valued equality operator?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 18 2021 at 09:56):

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

view this post on Zulip Scott Morrison (Mar 18 2021 at 09:56):

and then as Kevin says :-)

view this post on Zulip 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)

view this post on Zulip Phiroc (Mar 18 2021 at 09:58):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Phiroc (Mar 18 2021 at 10:13):

What is « constructivism »?

view this post on Zulip Johan Commelin (Mar 18 2021 at 10:16):

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


Last updated: May 14 2021 at 03:27 UTC