## Stream: new members

### Topic: Lean4: Proving succ a ≤ zero is obviously false

#### Brandon Brown (May 19 2021 at 17:51):

Oh good to know - thank you, Daniel. Re: @Johan Commelin it does not appear you can do that, I get the error

type mismatch
this
has type
nat.ple (succ a) zero = false : Prop
but is expected to have type
false = true : Prop


The nat.ple a.succ zero does not get reduced to false. If I do

variable (a : nat)
#reduce nat.ple a.succ zero -- false


It reduces to false as expected but it does not get automatically reduced in the proof term.

#### Brandon Brown (May 19 2021 at 18:06):

If I try to force it to evaluate the function using do notation I get a weird error in VS code, squiggly red line under the do.

theorem succ_le_zero_false {a : nat} (h : nat.le a.succ zero) : false := do {
return nat.le a.succ zero
}
/-
error: invalid universe level, 0 is not greater than 0
-/


#### Kevin Buzzard (May 19 2021 at 18:50):

theorem foo (a : nat) : nat.ple a.succ zero = false := rfl -- works fine


@Brandon Brown if you want to prove theorem succ_le_zero_false {a : nat} : (nat.le a.succ zero) → false then why are you using a bool-valued <=? -> is for Props. Bools are for computing (so you should prove what Johan suggests) and Props are for reasoning.

#### Kevin Buzzard (May 19 2021 at 18:51):

theorem succ_le_zero_false {a : nat} : (nat.le a.succ zero) → false := id


#### Kevin Buzzard (May 19 2021 at 18:53):

#check false → false -- false = true → false = true : Prop


Lean is jumping through hoops trying to make your bools into Props because you're using → on them

#### Brandon Brown (May 19 2021 at 20:11):

But I get a prop using ‘nat.le’ as wrapper around ‘nat.ple’

#### Kevin Buzzard (May 19 2021 at 20:29):

oh I see, I'm a fool :-) I thought coercion was doing it itself. Anyway, id does it.

#### Kevin Buzzard (May 19 2021 at 20:31):

But you're still using false as a Prop. Why not use False?

#### Brandon Brown (May 19 2021 at 21:01):

Good question. I don't know, I didn't know there was a False : Prop I was just following the way core Lean4 defined nat.le So, good to know,
thanks!

#### Kevin Buzzard (May 19 2021 at 21:08):

false is a bool but there's a coercion from bool to Prop which sends b to b = true.

#### Brandon Brown (May 19 2021 at 21:23):

I will change everything to True and False:

protected def nat.le (a b : nat) : Prop :=
match a, b with
| zero, b => True
| succ a, zero => False
| succ a, succ b => nat.le a b


Now I don't need the wrapper function. Not sure why core lean uses Bool with a wrapper.

#### Brandon Brown (May 19 2021 at 21:35):

Well now I think I have an idea why Lean4 core uses that way. Everything is harder to prove now. I don't know how to prove this:
example : nat.le zero zero.succ.succ := sorry before I could prove with rfl

#### Brandon Brown (May 19 2021 at 21:47):

Oh I have to do

example : nat.le zero zero.succ.succ := True.intro


#### Mario Carneiro (May 19 2021 at 22:17):

by the way, in mathlib4 there is fun. which allows you to do these proofs similarly to how you would in lean 3:

import Mathlib.Tactic.Basic

theorem succ_le_zero_false {a : nat} : ¬ nat.le a.succ zero := fun.


#### Brandon Brown (May 20 2021 at 04:05):

I need some help here as well. I do not understand the last 3 lines of this proof. How am I getting a proof of h1 : a ≤ b from l : succ a ≤ succ b and what is ▸ rfl. I'm not familiar with that notation and can't find where it's defined in Lean4 src.

inductive nat : Type where
| zero : nat
| succ : nat → nat

open nat

protected def nat.le (a b : nat) : Prop :=
match a, b with
| zero, b => True
| succ a, zero => False
| succ a, succ b => nat.le a b

infixl:50 (priority := high) " ≤ " => nat.le

theorem le_asymm {a b : nat} : (a ≤ b) ∧ (b ≤ a) → a = b :=
fun h =>
match a, b, h with
| zero, zero, ⟨l,r⟩ => rfl
| succ a, succ b, ⟨l,r⟩ =>
have h1 : a ≤ b from l;
have h2 : b ≤ a from r;
le_asymm (And.intro h1 h2) ▸ rfl


#### Michael Shaw (May 20 2021 at 04:12):

I believe rfl is reflexitivity proving that x = x. I'm not entirely sure but im basing my understanding off of the natural numbers game.

#### Mario Carneiro (May 20 2021 at 04:12):

e ▸ rfl means "rewrite the goal with e, and prove the resulting goal with rfl"

#### Mario Carneiro (May 20 2021 at 04:14):

How am I getting a proof of h1 : a ≤ b from l : succ a ≤ succ b

a ≤ b is actually defeq to succ a ≤ succ b, because:

• (a ≤ b) = (nat.le a b)
• (succ a ≤ succ b) = (nat.le (succ a) (succ b))
• nat.le (succ a) (succ b) = nat.le a b

#### Brandon Brown (May 20 2021 at 12:10):

Thank you!

Last updated: Dec 20 2023 at 11:08 UTC