Multiplication in Pattern Matching

Stream: new members

[ROCKY KAMEN-RUBIO]

I'm getting errors when I try to pattern match on whether a nat is even or odd, but keep getting errors. I thought this was fair game for pattern matching. Is that not the case?

def test : ℕ → ℕ
| (2*n) := 0
| (2*n + 1) := 1

[Kevin Buzzard]

That's definitely not fair game

[Kevin Buzzard]

You can't expect the equation compiler to prove that every natural number is of the form 2n or 2n+1 -- this proof has a small amount of content.

[Kevin Buzzard]

But test (n : nat) := n % 2 is the function you're defining -- it's already there.

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

But test (n : nat) := n % 2 is the function you're defining -- it's already there.

Gotcha. It seems like it didn't like the pattern match on the multiplication, rather than the lack of exhaustive cases. Is there a way to add an "otherwise" case like in Haskell? That feels a little silly though.

For context, I wanted to prove this lemma, but Lean didn't like that (-1) wasn't a nat, so I thought I'd do a case split on whether m is even or odd.

import data.nat.basic
import data.list.basic
import tactic
@[reducible]
def fib : ℕ → ℕ
| 0 := 0
| 1 := 1
| (n+2) := fib n + fib (n+1)
@[reducible]
def luc : ℕ → ℕ
| 0 := 2
| 1 := 1
| (n+2) := fib n + fib (n+1)

lemma l3 {m : ℕ} : luc (2*m) = (luc m)^2 + (-1)^(m-1)*2 := sorry

[Bryan Gin-ge Chen]

Your definition of luc should probably use luc rather than fib, right? For your lemma, I'd just cast everything to int and try to prove it there. Tactics like norm_cast and push_cast should hopefully make the casts easy to deal with.

[ROCKY KAMEN-RUBIO]

Bryan Gin-ge Chen said:

Your definition of luc should probably use luc rather than fib, right? For your lemma, I'd just cast everything to int and try to prove it there. Tactics like norm_cast and push_cast should hopefully make the casts easy to deal with.

Yes! Thanks for catching that. Here is the updated code. I realized I also didn't need to include fib for this example.

import data.nat.basic
import data.list.basic
import tactic

@[reducible]
def luc : ℕ → ℕ
| 0 := 2
| 1 := 1
| (n+2) := luc n + luc (n+1)

lemma l3 {m : ℕ} : luc (2*m) = (luc m)^2 + (-1)^(m-1)*2 := sorry

[Kevin Buzzard]

Why don't you just make luc integer-valued? What you have there doesn't make any sense, because -1 isn't a natural.

[Kevin Buzzard]

ROCKY KAMEN-RUBIO said:

Gotcha. It seems like it didn't like the pattern match on the multiplication, rather than the lack of exhaustive cases. Is there a way to add an "otherwise" case like in Haskell? That feels a little silly though.

Sure -- you can just put _. But that won't change the fact that you cannot pattern match on 2 * n at all, it's not a valid pattern and that's the end of it.

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

Why don't you just make luc integer-valued? What you have there doesn't make any sense, because -1 isn't a natural.

I was thinking about that. Since they're all positive it seemed like I should be able to use nat, and this expression could be rewritten using nat subtraction instead of -1, but maybe that's not really practical.

[Kevin Buzzard]

Feel free to rewrite it using nat subtraction, but you can't use -1 because it's not a natural -- you'll have to do the rewriting yourself.

[Kevin Buzzard]

The assertion that "they're all positive" might be obvious to you, but it's not obvious to Lean -- it needs a proof.

[Kevin Buzzard]

It's much easier just to make everything integer-valued if you want to do subtraction. Natural number subtraction is really badly behaved, it is not a function you should use at all if you're doing mathematics.

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

ROCKY KAMEN-RUBIO said:

Gotcha. It seems like it didn't like the pattern match on the multiplication, rather than the lack of exhaustive cases. Is there a way to add an "otherwise" case like in Haskell? That feels a little silly though.

Sure -- you can just put _. But that won't change the fact that you cannot pattern match on 2 * n at all, it's not a valid pattern and that's the end of it.

Right, forgot you could just put a general wildcard with no structure on it. From your earlier post it sounded like the problem was that 2*n and 2*n+1 didn't register as exhaustive cases for a nat to the compiler, but it sounds like that's not the extent of why this isn't allowed? Should I just take it as an axiom that you can't pattern match on multiplication then, or is there a deeper reason this doesn't work?

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

It's much easier just to make everything integer-valued if you want to do subtraction. Natural number subtraction is really badly behaved, it is not a function you should use at all if you're doing mathematics.

Ok, I'll try doing everything with integers.

[Kevin Buzzard]

If you are pattern matching on a natural, you can only pattern match on the constructors for that natural, which are zero and succ, or combinations of these constructors (at least as far as I know -- I am no expert in the equation compiler). Note that in the lucas definition, n+2 is by definition succ (succ n) so that's OK. But 2*n and n*2 are definitely not OK.

[Bryan Gin-ge Chen]

I was just typing out something like what Kevin said. See also 8.1 and 8.2 of TPiL.

[ROCKY KAMEN-RUBIO]

Kevin Buzzard said:

If you are pattern matching on a natural, you can only pattern match on the constructors for that natural, which are zero and succ, or combinations of these constructors (at least as far as I know -- I am no expert in the equation compiler). Note that in the lucas definition, n+2 is by definition succ (succ n) so that's OK. But 2*n and n*2 are definitely not OK.

Right, that makes sense. For some reason I thought we could pattern match on patterns other than the type constructors.

[Kenny Lau]

nat.binary_rec_on