confused about membership

Stream: new members

[Oscar Martin]

how do i make \mem work for lists or sets made of structures i have created?
or sets in general

i always get something along the lines of

"failed to synthesize
Decidable (p1 ∈ list_point) "

as an error message

import Init.Data.Array
import Init.Data.List
import Mathlib.Init.Set

structure Point  where
  x : Float
  y : Float
deriving Repr

def p1 : Point := {x := 1 , y := 0}
def p0 : Point := {x := 0 , y := 0}

def list_point := [p0,p1]

def set_point : Set Point := {p0,p1}

def set_float : Set Float := {1,2}

#eval p1 ∈ list_point

#eval 1 ∈ [1,2] -- this works fine for me

#eval p0 ∈ set_point

#eval 1 ∈ set_float

[Siddhartha Gadgil]

The problem is that you cannot evaluate membership in a list if you cannot evaluate equality of the underlying type. So the following variant of your code works.

import Init.Data.Array
import Init.Data.List
import Mathlib.Init.Set

structure Point  where
  x : Nat
  y : Nat
deriving Repr, DecidableEq

def p1 : Point := {x := 1 , y := 0}
def p0 : Point := {x := 0 , y := 0}

def list_point := [p0,p1]

def set_point : Set Point := {p0,p1}

def set_float : Set Float := {1,2}

#eval p1 ∈ list_point

[Siddhartha Gadgil]

If your Point has Float components, then you cannot derive DecidableEq because equality of Floats is not decidable.

[Siddhartha Gadgil]

The final part of the code will not work even with integers because membership in a set is not decidable. You could use FinSet if you wanted finite sets and the underlying type had decidable equality.

[Oscar Martin]

Siddhartha Gadgil said:

If your Point has Float components, then you cannot derive DecidableEq because equality of Floats is not decidable.

ok thanks a lot. My overall aim is to prove that a certain point is an element of a finite set or list. Right now i'm working with floats (just so i can evaluate functions and see if they work) but the end goal is to do this with reals.
I've created a function "point_in" which just takes lists and figures out if the selected point is in the list. Again the end goal is to work with sets, but i don't understand enough lean to do this yet.
this is what i have so far

structure Point  where
  x : Float
  y : Float
deriving Repr, BEq

def p1 : Point := {x := 1 , y := 0}
def p0 : Point := {x := 0 , y := 0}

def point_in (p : Point) (ps : List Point) : Bool :=
  match ps with
  | [] => False
  | x :: xs => if x == p then true else point_in p xs

theorem p_in : point_in p1 [p1,p0] = true := by
  sorry

i'm trying to prove this first theorem with Lists first and then I'll move onto sets? i guess?
any advice?
thanks :pray:

[Luigi Massacci]

I haven’t written many proofs about code, but I would imagine just by native_decide should work for that

[Luigi Massacci]

Having said that, what do you mean  “Doing this with reals”? You are going to have a hard time performing computations with Lean’s reals

[Oscar Martin]

Brilliant thanks, these have been very helpful! I can't figure out how to index my list. I now need to apply a function to each element in the list, and then union the result. Is there something like a BigOperation but for Unions?

[Luigi Massacci]

you can do indexing with docs#List.get! , or use an docs#Array , Lean has all the usual FP functions, so in particular docs#List.map and so on. Not sure what you meany by “union the result”