Not true by definition

Stream: lean4

[Brandon Brown]

I'm not understanding why the last example isn't true by definition (rfl):

open Nat

inductive int : Type where
| pos : Nat → int
| neg_succ : Nat → int

open int

def sub_nat (n m : Nat) : int :=
  match n,m with
  | n, zero => pos n
  | zero, succ m => neg_succ m
  | succ n, succ m => sub_nat n m

#reduce sub_nat 9 0 -- pos 9

example : sub_nat 0 k.succ = neg_succ k := rfl -- works
example : sub_nat j.succ k.succ = sub_nat j k := rfl -- works

example : sub_nat j 0 = pos j := rfl -- doesn't work

[Yakov Pechersky]

You have to case on j.

[Yakov Pechersky]

Does the match definition do the same thing as the eq compiler in lean4 now? I'm not sure. But what's going on is that in your current def, the n, zero case is being broken down into the two inductive cases.

[Brandon Brown]

Thanks, yeah I figured out I can prove it by cases, but it just seems like it should be true by definition since it exactly matches one of my definitional match cases. But oh well

[Kevin Buzzard]

In lean 3 you could not guarantee that the equation compiler wouldn't break up your definition some more and it looks like the same is going on here.

[Mario Carneiro]

Yakov Pechersky said:

Does the match definition do the same thing as the eq compiler in lean4 now? I'm not sure.

Yes, there is no longer a difference between top level match and a regular match expression with a recursive call inside

[Mario Carneiro]

the former macro expands to the latter

[Mario Carneiro]

As for the example, my guess is that it will work if you swap the arguments to sub_nat

[Mario Carneiro]

or you use two matches

[Mario Carneiro]

By trial and error, this works:

def sub_nat (n m : Nat) : int :=
  match m, n with
  | zero, n => pos n
  | succ m, zero => neg_succ m
  | succ m, succ n =>
    let ih n := sub_nat n m
    ih n