## Stream: new members

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

#### Sky (Jan 05 2022 at 19:27):

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 (Jan 05 2022 at 19:28):

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 (Jan 05 2022 at 19:30):

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 (Jan 05 2022 at 19:31):

So it should work. And it does!

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


#### Sky (Jan 05 2022 at 19:35):

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 (Jan 05 2022 at 19:38):

And this works too!

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


#### Sky (Jan 05 2022 at 19:42):

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

#### Chris B (Jan 05 2022 at 20:07):

@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 (Jan 05 2022 at 20:07):

@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 (Jan 05 2022 at 20:12):

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.

Last updated: Dec 20 2023 at 11:08 UTC