problems with equation compiler & subsets

Stream: new members

[Nicolas Rouquette]

I am trying to define a function where the domain is a subset of elements and I'm really surprised at Lean's behavior.
Can someone please explain how to define a function using the equation compiler for a subset type ?

import data.fintype.basic

def ns := {n: ℕ | n ≤ 3}

def n0 : ns := ⟨ 0, begin refine set.mem_Iic.mpr _, exact sup_eq_left.mp rfl, end ⟩
def n1 : ns := ⟨ 1, begin refine set.mem_Iic.mpr _, exact sup_eq_left.mp rfl, end ⟩
def n2 : ns := ⟨ 2, begin refine set.mem_Iic.mpr _, exact sup_eq_left.mp rfl, end ⟩
def n3 : ns := ⟨ 3, begin refine set.mem_Iic.mpr _, exact sup_eq_left.mp rfl, end ⟩

def n2s_incomplete : ns → string
| n0 := "zero"

#eval n2s_incomplete n1
-- result: "zero"  -- why is this the case?

#eval n2s_incomplete n0
-- result: "zero" -- this function seems to be equivalent to a constant; that is, the argument seems to be completely ignored.

def n2s : ns → string
| n0 := "0" -- no error
| n1 := "1" -- equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
| n2 := "2" -- equation compiler error, equation #3 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
| n3 := "3" -- equation compiler error, equation #4 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable

[Alex J. Best]

lean is treating n0 on the left as just a new identifier. Doing

def n2s_incomplete : ns → string
| ⟨0, h⟩ := "zero"
| ⟨1, h⟩ := "one"
| ⟨2, h⟩ := "two"
| ⟨3, h⟩ := "three"
| ⟨n + 4, h⟩ := ""

seems to work. There is an attribute @[pattern] you can add to defs, but lean doesn't like it in this case.

[Alex J. Best]

But if you really just want a type with four terms you can just make a simple inductive

inductive ns
| n0
| n1
| n2
| n3

open ns
def n2s : ns → string
| n0 := "0"
| n1 := "1"
| n2 := "2"
| n3 := "3"

[Nicolas Rouquette]

Alex J. Best said:

lean is treating n0 on the left as just a new identifier. Doing

def n2s_incomplete : ns → string
| ⟨0, h⟩ := "zero"
| ⟨1, h⟩ := "one"
| ⟨2, h⟩ := "two"
| ⟨3, h⟩ := "three"
| ⟨n + 4, h⟩ := ""

seems to work. There is an attribute @[pattern] you can add to defs, but lean doesn't like it in this case.

Thanks Alex!