## Stream: new members

### Topic: use proof in function

#### Joscha Mennicken (Nov 10 2021 at 13:35):

I'm wondering if it is possible to define a function like

myPrev (n : Nat) : n != 0 → Nat


or

myPrev : {n : Nat // n != 0} → Nat


When I tried, I expected there to be some way to get a n = 0 in the | Nat.zero => ... case of a match n with, but couldn't find any.

#### Floris van Doorn (Nov 10 2021 at 13:47):

This works:

def myPrev : (n : Nat) → n != 0 → Nat
| n+1, _ => n

def myPrev' : {n : Nat // n != 0} → Nat
| ⟨n+1, _⟩ => n


Lean will automatically figure out that you don't need to provide the 0 case.

#### Floris van Doorn (Nov 10 2021 at 13:51):

If you want to use the word match, you can do this:

def myPrev (n : Nat) (h : n != 0) : Nat :=
match n, h with
| 0, _ => by contradiction -- this line is optional, and can be removed
| n+1, _ => n


#### Floris van Doorn (Nov 10 2021 at 13:52):

In particular, you have to put h in the match, so that it changes when you consider different cases on n.

#### Joscha Mennicken (Nov 10 2021 at 13:54):

Thanks, that second example was what I was looking for. It's cool that the first version works, but it's a bit too much magic to understand what's going on.

#### Joscha Mennicken (Nov 10 2021 at 13:58):

I'm still wondering if there's a way to end up with a hypothesis n = 0 in the first match case and n != 0 (or n = x + 1 or similar) in the second and to then use the n = 0 as contradiction to n != 0 instead of using 0 != 0 as contradiction.

#### Joscha Mennicken (Nov 10 2021 at 14:01):

Something like

def myPrev (n : Nat) (h : n != 0) : Nat :=
have hn : n = n := Eq.refl n
match n, hn with
| 0, _ => sorry
| x+1, _ => x


but where lean doesn't rewrite all occurrences of n in hn

#### Floris van Doorn (Nov 10 2021 at 19:00):

Oh, I see what you mean.

Yes, you can write

def myPrev (n : Nat) (h : n != 0) : Nat :=
match n_eq_0:n with
| 0 => by subst n_eq_0; contradiction
| n+1 => n


#### Eric Wieser (Nov 10 2021 at 19:12):

Note you could also just send 0 => 0, and your function would be equal

#### Joscha Mennicken (Nov 12 2021 at 14:20):

That makes sense. Thanks for those answers, although I'm slightly surprised you can't put a space before the colon, only after: match n_eq_0: n with.

Last updated: Dec 20 2023 at 11:08 UTC