match on pnat

Stream: general

[Etienne Laurin]

Is it possible to teach lean to match on mathlib's pnat?

import data.pnat.basic

-- invalid function application in pattern, it cannot be reduced to a constructor (possible solution
example (a : ℕ+) := match a with
| 1 := tt
| _ := ff
end

[Etienne Laurin]

Are there any advantages of defining pnat using subtype instead of something like

inductive pnat' | pnat_succ (nat_pred : ℕ)
instance : has_one pnat' := ⟨⟨0⟩⟩

-- OK
example (a : pnat') := match a with
| 1 := tt
| _ := ff
end

[Adam Topaz]

You can still pattern match, for example like this:

import data.pnat.basic

example (a : ℕ+) := match a with
| ⟨0,h⟩ := false.elim $ by simpa using h
| ⟨1,h⟩ := tt
| _ := ff
end

(there may be some other spelling for the false.elim case, but you get the point...)

[Adam Topaz]

Or you can use docs#pnat.rec_on directly:

import data.pnat.basic

example (a : ℕ+) : bool :=
pnat.rec_on a tt (λ _ _, ff)

[Kevin Buzzard]

I guess you don't even have to fill in the \<0,h\> branch