use proof in function

Stream: new members

[Joscha Mennicken]

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]

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]

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]

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

[Joscha Mennicken]

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]

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]

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]

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]

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

[Joscha Mennicken]

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.