Type mismatch expected to have type Type ? : Type (?+1)

Stream: new members

[Johannes Tantow]

Hi,

I am newly working with Lean and try different formalizations of finite sets. (I know that there is a definition for finite sets in mathlib already). I get the type mismatch error and can't make any sense of why this is. My example is below.

universe u

inductive Kuratowski (A:Type u)
| empty: Kuratowski
| singleton : A -> Kuratowski
| union : Kuratowski  -> Kuratowski  -> Kuratowski

variable A: Type u

notation (name :=emptyset) ∅ := Kuratowski.empty
notation {a} := Kuratowski.singleton a
notation (name := union) x ∪ y := Kuratowski.union x y

def kuratowski_member [decidable_eq A] : A -> Kuratowski A -> bool
| x ∅ := false
| x {y} := x=y
| x (y ∪ z) := (kuratowski_member x z) ∨ (kuratowski_member x y)

notation (name := kuratowski_member) x ∈ y := kuratowski_member x y

def comprehension: (A -> bool) -> Kuratowski A -> Kuratowski A
| ϕ ∅ := ∅
| ϕ {a} := if ϕ a then {a} else ∅
| ϕ (x ∪ y) := comprehension ϕ x ∪ comprehension ϕ y

def intersection [decidable_eq A] (x y:Kuratowski A) : Kuratowski A:= comprehension (λ (a:A), a ∈ y) x

I receive the following error (line 26 is the definition of the intersection.

none of the overloads are applicable
error for kuratowski_member
type mismatch at application
  kuratowski_member a
term
  a
has type
  A : Type u
but is expected to have type
  Type ? : Type (?+1)

error for has_mem.mem
failed to synthesize type class instance for
A : Type u,
_inst_1 : decidable_eq A,
x y : Kuratowski A,
a : A
⊢ has_mem A (Kuratowski A)
Additional information:
/home/johannes/finSets/Test.lean:26:96: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available

This only partially makes sense for me. I can understand the second part, because I use my own membership function and not the one from a standard library, so it doesn't know what to use, but I don't understand why my member function is refusing my definition and requires some obscure type. (λ (a:A), a ∈ y) takes an element from A and returns a boolean and y is a constant and then comprehension also gets a correct function and a fitting Kuratowski set object. I don't see why a should be a Type object.

If I remove the type definition from the lambda, it then asks for a proof of decidable_eq a, but I don't see how to give this in for some general a.
How to interprete this error and solve it ?

[Ruben Van de Velde]

Probably the first argument should be A and then a can be the second?

[Johannes Tantow]

Ruben Van de Velde schrieb:

Probably the first argument should be A and then a can be the second?

Hi, thanks for answering
Can you state that a bit more precise for what statement as the first argument ? As the first argument for\in ? I don't see how this works with the custom notation. If I write instead kuratowski_member A a yI get another type mismatch as it then tries to find A \in a

type mismatch at application
  comprehension (λ (a : A), (A∈a) y)
term
  λ (a : A), (A∈a) y
has type
  A → bool : Type u
but is expected to have type
  Type ? : Type (?+1)
Additional information:
/home/johannes/finSets/Kuratowski.lean:95:72: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    comprehension ?m_1 ?m_2
  has type
    Kuratowski ?m_1 → Kuratowski ?m_1 : Type ?
  but is expected to have type
    Kuratowski A : Type u

[Ruben Van de Velde]

Oh, I misread partially. You need A as the first argument to comprehension, but the lambda then still goes wrong

[Ruben Van de Velde]

Trying to override the core ∈ is only making your life harder here

[Ruben Van de Velde]

So you can replace that by kuratowski_member A a y inside the lambda

[Johannes Tantow]

Thank you this works. I assumed that the type is read off from the other inputs. Is it possible to hide "normal set" languages so I can use $\in$ ?

[Yakov Pechersky]

The type is read off from the other inputs if you specify that. You declared "variables A : Type u". That makes A an explicit argument. I think you might want "variables {A : Type u}" instead.

[Jireh Loreaux]

Note that this formalization of finite sets doesn't work. You would need to take a quotient in order to say that some of the ways to build a set actually give you the same thing. For example, if you take a b : A, put them into singletons and then union, you get different elements of kuratowski based on which order you put them in the union.

[Johannes Tantow]

Jireh Loreaux schrieb:

Note that this formalization of finite sets doesn't work. You would need to take a quotient in order to say that some of the ways to build a set actually give you the same thing. For example, if you take a b : A, put them into singletons and then union, you get different elements of kuratowski based on which order you put them in the union.

Thank you for your help, but I think I dealt with this. I have added axioms like these

axiom union_comm {A:Type u} (x y : Kuratowski A): x ∪ y = y ∪ x
axiom union_singleton_idem {A:Type u} (x : A): {x} ∪ {x} = {x}

to my code, but they didn't seem to be relevant here and I didn't want to clutter the example more.

[Eric Wieser]

I'm pretty sure that will allow you to prove false

[Eric Wieser]

example : false := by cases union_singleton_idem ()

[Eric Wieser]

The general rule is "don't add axioms unless you really know what you're doing"! Mathlib contains no axioms.

[Eric Wieser]

As Jireh Loreaux says, if you want to make these things equal you need to take the quotient

[Johannes Tantow]

I'll take a look at this