# Zulip Chat Archive

## 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