Proving `(n: Nat) -> n < 0 -> False` in term mode

Stream: new members

[Sky]

I'm trying to learn Lean and some type theory, but I haven't been able to figure this out. In AGDA I could case split on a proof of n < 0 and it'd detect it as an absurd pattern, but I wanted to understand what was going on on a deeper level (and without using tactics). I feel like I'll need a noConfusion or something like it, but I'm not sure exactly how

[Kevin Buzzard]

Whether or not this trick would work in Lean will depend on the exact definition of < on nat. Let's take a look...

[Kevin Buzzard]

OK so < is nat.lt which is defined by a < b := a.succ <= b and <= is defined recursively:

inductive less_than_or_equal (a : ℕ) : ℕ → Prop
| refl : less_than_or_equal a
| step : Π {b}, less_than_or_equal b → less_than_or_equal (succ b)

[Kevin Buzzard]

So it should work. And it does!

example (n : ℕ) (hn : n < 0) : false :=
begin
  cases hn,
end

[Sky]

Thanks! I did want it in term mode, but the #print output doesn't look too bad. I'll take a closer look

[Yaël Dillies]

And this works too!

example (n : ℕ) : ¬ n < 0 .

[Sky]

I've read about that dot here on Zulip before. Does it have an equivalent in lean4?

[Chris B]

@Sky

If you really want to expose the gears, you need something like this; the second one is maybe a bit easier since it uses a concrete value and <=:

example (a b : Nat) (h : a < b) : b = 0 -> False :=
Nat.le.recOn (motive := fun (x : Nat) (h : a < x) => x = 0 -> False)
h
(fun one_eq_zero => Nat.noConfusion one_eq_zero)
(fun h1 h2 succ_eq_zero => Nat.noConfusion succ_eq_zero)

example (b : Nat) (h : 1 <= b) : b = 0 -> False :=
Nat.le.recOn (motive := fun (x : Nat) (h : 1 <= x) => x = 0 -> False)
h
(fun one_eq_zero => Nat.noConfusion one_eq_zero)
(fun h1 h2 succ_eq_zero => Nat.noConfusion succ_eq_zero)

[Kyle Miller]

@Sky There's now a nomatch keyword:

example (n : Nat) (h : n < 0) : false := nomatch h

The syntax seems to be just like match, but it has no alternatives.

[Kyle Miller]

The Lean 3 equivalent is

example (n : ℕ) (h : n < 0) : false := match h with end

but since Lean 4 does not use the end keyword, it has a new syntactic construct.