Pattern matching behavior with variables?

Stream: new members

[Josh Chen]

I'm a little stumped by Lean's pattern-matching behavior here: dsimp[monus] fails to simplify. casesing on n beforehand works as expected, but why isn't my second argument pattern-match definitional?

open nat

def monus : nat → nat → nat
| m        0        := m
| 0        (succ n) := 0
| (succ m) (succ n) := monus m n

example (n : ℕ) : monus n 0 = n :=
begin
  dsimp[monus],
  sorry
end

[Scott Morrison]

The generated definitions don't always agree with the patterns you write! The equation compiler is making some internal decisions about how to turn your patterns into nested applications of recursors. Try #print prefix monus, and then following up with #print ... for the various subsidiary definitions that appear, to see what was actually produced.

[Scott Morrison]

There is also somewhere a useful tactic for this, that automatically does whatever case bashing is required to unfold a given definition. I can never remember its name. :-(

[Josh Chen]

Thanks! I expected something like that was happening, is there a reference for more detail on what the equation compiler is doing?

[Josh Chen]

The Lean3 reference on the equation compiler has this sentence: "If some of the patterns overlap, the equation compiler interprets the definition so that the first matching pattern applies in each case" which I interpreted to mean what I thought it meant at first.

[Scott Morrison]

tactic#unfold_cases