Lean4: Proving succ a ≤ zero is obviously false

Stream: new members

[Brandon Brown]

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]

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]

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]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Brandon Brown]

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]

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

[Brandon Brown]

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]

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]

Oh I have to do

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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]

Thank you!