# Zulip Chat Archive

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