Zulip Chat Archive

Stream: new members

Topic: Pattern matching behavior with variables?


Josh Chen (Nov 09 2021 at 23:07):

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 (Nov 09 2021 at 23:11):

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 (Nov 09 2021 at 23:12):

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 (Nov 09 2021 at 23:12):

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

Josh Chen (Nov 09 2021 at 23:14):

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 (Nov 09 2021 at 23:15):

tactic#unfold_cases


Last updated: Dec 20 2023 at 11:08 UTC