rfl with underscore in equation compiler

Stream: new members

[Kenny Lau]

def is_pos : ℕ → bool
| 0 := ff
| _ := tt

#print prefix is_pos

example (n : ℕ) : is_pos n.succ = tt := rfl

[Kenny Lau]

How does this rfl work?

[Kenny Lau]

The equational lemmas are:

is_pos.equations._eqn_1 : is_pos 0 = ff
is_pos.equations._eqn_2 : ∀ (_x : ℕ), ¬_x = 0 → is_pos _x = tt

[Mario Carneiro]

that may be the equation lemmas, but the kernel reduction doesn't use equation lemmas

[Kenny Lau]

what's the right tactic to use if this occurs inside some larger term? simp and unfold cannot reduce the goal at all, and rw changes the goal into ¬n.succ = 0

[Mario Carneiro]

that looks like progress

[Kenny Lau]

or maybe one shouldn't use underscore to begin with

[Mario Carneiro]

what's actually happening is that the compilation strategy created a term like if n = 0 then ff else tt and decidable (n.succ = 0) reduces to false

[Kevin Buzzard]

Kenny Lau said:

or maybe one shouldn't use underscore to begin with

Unsurprisingly, this does produce better equation lemmas.