Zulip Chat Archive

Stream: new members

Topic: problems with equation compiler & subsets


Nicolas Rouquette (Nov 08 2020 at 05:38):

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 (Nov 08 2020 at 06:38):

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 (Nov 08 2020 at 06:39):

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 (Nov 08 2020 at 17:56):

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!


Last updated: Dec 20 2023 at 11:08 UTC