Membership of Dependent Type in a Set of Dependent Type

Stream: new members

[Mrigank Pawagi]

I have a type for functions from "first n Natural Numbers", parameterized by the size of the domain, i.e., n. Further, I have another type for sets of such functions where the size parameter may not be homogenous. I do this by defining it in the following way:

import Mathlib

def Func (n: ℕ) : Type := Fin n → ℕ
def FuncSet : Type := Set (Σ n, Func n)

To make it easy to work with these objects, I want to define Membership of Func n in FuncSet:

instance {n: ℕ} : Membership (Func n) FuncSet := ⟨fun f S => ⟨n, f⟩ ∈ S⟩

But I get the following errors:

invalid constructor ⟨...⟩, expected type must be an inductive type
  ?m.47

failed to synthesize
  Membership ?m.47 (Func n)

instance does not provide concrete values for (semi-)out-params
  Membership (Func ?n) FuncSet

I thought that an alternative would be to define coercion from Func n to Σ n, Func n, but that gave the "instance does not provide concrete values for (semi-)out-params" error. Any guidance on whether this is a bad way of doing things, or on a way to fix this error, would be super helpful! Thanks!

Link to live code.

[Ruben Van de Velde]

It sounds like lean can't figure out the types in your code. Try adding some type annotations

[Mrigank Pawagi]

@Ruben Van de Velde I tried adding type annotations, and even tried instance {n: ℕ} : Membership (Fin n → ℕ) (Set (Σ n, Func n)) := ... but neither worked.

[Kevin Buzzard]

docs#Membership

[Kevin Buzzard]

The first input for Membership is an Outparam and there's already Membership X (Set X) so this setup will be intrinsically problematic I think.

[Kevin Buzzard]

You're the second person to try this this week.

Oh you've made FuncSet a def so this should get around the Set X issue, but there's still the issue that you have infinitely many n :-/

[Mrigank Pawagi]

Is this not the recommended way to create such sets?

[Kevin Buzzard]

This is your problem:

/--
warning: declaration uses 'sorry'
---
error: instance does not provide concrete values for (semi-)out-params
  Membership (Func ?n) FuncSet
-/
#guard_msgs in
instance {n: ℕ} : Membership (Func n) FuncSet := sorry

I think that error says "I want exactly one choice of X for Membership X FuncSet so what the heck is that variable doing there?" You also seem to have made a syntax error but this is the pertinent issue.

[Mrigank Pawagi]

I see... I understand somewhat. Does that mean I have to do something like

structure Func where
 n: ℕ
 f: Fin n → ℕ

def FuncSet : Type := Set Func

which makes things a bit clunky

[Kevin Buzzard]

It means "you can't ever have instance {n: ℕ} : Membership (Func n) FuncSet whatever your definitions, so give up on the idea of using Membership to express what you want if you want n unbundled"

[Mrigank Pawagi]

Thanks for the response. I previously had to use an existential quantifier over n to say something like "f is Func n for some n" and thought maybe I could simplify things.

[Mrigank Pawagi]

But also I really wanted to have another function, say foobar which returned a set of Funcs.

[Kevin Buzzard]

You could always experiment with just using your own notation -- perhaps you'll find out why Membership uses an outparam, or perhaps you'll find out that it shouldn't be using an outparam

[Mrigank Pawagi]

Thanks so much for your time! Your advice and help on this Zulip server is amazing!