# Zulip Chat Archive

## Stream: general

### Topic: member of set used as member of corresponding type

#### Kris Brown (Jul 31 2020 at 08:59):

I'm a bit unclear about working with sets which are coerced to types. For instance, I have a `finset`

which can be coerced to a `set`

which can be coerced to a `Type`

:

```
@[simp] def finset_to_type {α: Type} (b: finset α): Type := (↑ b : set α)
```

I'm interested in this because I have an inductive type which would ideally look like this :

```
with Struct: string → Type
| mk (name: string) (fields: finset (string × PrimitiveType)): Struct name
```

This won't compile, since the `PrimitiveType`

is being mutually inductively defined and therefore cannot be inside a non-inductive-type like `finset`

. So instead I could just have some finite type of string keys and a map from those to values.

```
with Struct: string → Type
| mk (name: string) (fields: finset string)
(vals: (finset_to_type fields) → PrimitiveType): Struct name
```

In order for me to actually use this, I need a function like the following:

```
def finset_str_map: Π{s: finset string} {α: Type},
(finset_to_type s → α) → string → option α
| s α f key := if h: key ∈ s
then some (f (by {simp, rw finset.has_lift,
have h': key ∈ ↑s, by {sorry},
-- I don't actually know what to do here
-- rw set.mem_def at h',
--rw set.has_coe_to_sort.coe ↑s at h',
--exact h'
sorry}))
else none
```

Is there a simple way to express that, if I have an element of a finite set, that I can treat it as a member of the corresponding type?

#### Kris Brown (Jul 31 2020 at 09:10):

MWE

```
import data.finset.basic
@[simp] def finset_to_type {α: Type} (b: finset α): Type := (↑ b : set α)
mutual inductive PrimType, Struct
with PrimType: Type
| pBool: bool → PrimType
| pInt: ℤ → PrimType
| pStruct {s: string}: Struct s → PrimType
with Struct: string → Type
| mk (name: string) (fields: finset string)
(vals: (finset_to_type fields) → PrimType): Struct name
def finset_str_map: Π{s: finset string} {α: Type},
(finset_to_type s → α) → string → option α
| s α f key := if h: key ∈ s
then some (f (by {sorry}))
else none
```

#### Mario Carneiro (Jul 31 2020 at 09:36):

To slightly #xy your problem, I suggest using two foralls instead of a function over the subtype in the mutual inductive. You can do something like this:

```
mutual inductive PrimType, Struct
with PrimType : Type
| pBool : bool → PrimType
| pInt : ℤ → PrimType
| pStruct {s : string} : Struct s → PrimType
with Struct : string → Type
| mk (name : string) (fields : finset string)
(vals : ∀ s ∈ fields, PrimType) : Struct name
def Struct.fields : ∀ {s}, Struct s → finset string
| _ (Struct.mk _ f _) := f
def Struct.vals : ∀ {s} (c : Struct s) (s ∈ c.fields), PrimType
| _ (Struct.mk _ _ v) := v
def Struct.get {s} (c : Struct s) (key : string) : option PrimType :=
if h : key ∈ c.fields then some (c.vals _ h) else none
```

#### Mario Carneiro (Jul 31 2020 at 09:38):

in the original question though you can replace the `by {sorry}`

with `⟨key, h⟩`

#### Kris Brown (Jul 31 2020 at 10:11):

Thanks!

#### Kris Brown (Aug 01 2020 at 00:14):

Does this strategy make it impossible to show that two `Struct`

s are decidably equal? The amount of data in the mapping is finite, but it looks like I have to prove equality for a function ranging over a (seemingly) infinite domain.

```
mutual def primtype_eq, struct_eq
with primtype_eq: ...
with struct_eq: Π(s: string), decidable_eq (Struct s)
| _ ( Struct.mk a b c) (Struct.mk d e f) := by {
simp,
have p: decidable (a=d), by exact string.has_decidable_eq a d,
have q: decidable (b=e), by exact finset.has_decidable_eq b e,
cases p with pf pt,
{simp [pf], exact decidable.false}, -- different names
{rw pt, simp, cases q with qf qt,
{simp [qf], exact decidable.false}, -- different fields
subst qt,
have r: decidable (c=f), by sorry, -- TODO prove maps are equal (will need primtype_eq)
cases r with rf rt,
{simp [rf], exact decidable.false}, -- different values
subst rt, simp, exact decidable.true}} --
```

Right now the strategy seems like I should prove some lemmas saying that functions from a finite domain into a codomain (w/ decidable equality) have decidable equality, and then convince Lean that (due to the constraint imposed by the argument) that `Struct.vals`

is effectively a function from a type with a finite domain. I didn't see anything directly related to these two goals in mathlib, but it seems in principle do-able.

#### Reid Barton (Aug 01 2020 at 00:20):

May I introduce you to `classical.prop_decidable`

? :upside_down:

#### Reid Barton (Aug 01 2020 at 00:29):

This definitely should be possible though

#### Mario Carneiro (Aug 01 2020 at 00:39):

I think I should probably mention my usual advice at this point, which is that if you want to do nontrivial proofs with the type you should avoid `mutual inductive`

and roll your own

#### Kris Brown (Aug 01 2020 at 00:53):

I'm interested but don't know what rolling my own would entail. Is there an example of what you mean by this?

#### Mario Carneiro (Aug 01 2020 at 01:05):

I managed this:

```
import data.finset.basic
inductive PrimType : Type
| pBool : bool → PrimType
| pInt : ℤ → PrimType
| pStruct' (name : string) (fields : finset string)
(vals : ∀ s ∈ fields, PrimType) : PrimType
instance : decidable_eq PrimType :=
begin
intros a b, induction a generalizing b; cases b;
try {{ apply decidable.is_false, rintro ⟨⟩ }},
{ exact decidable_of_iff (a = b) (by simp) },
{ exact decidable_of_iff (a = b) (by simp) },
{ refine if h : a_name = b_name then _ else decidable.is_false (by simp [h]),
refine if h2 : a_fields = b_fields then _ else decidable.is_false (by simp [h2]),
resetI, refine decidable_of_iff (∀ x hx, a_vals x hx = b_vals x (by rwa ← h2)) _,
subst h, subst h2, simp [function.funext_iff] },
end
@[derive decidable_eq]
structure Struct (name : string) :=
(fields : finset string) (vals : ∀ s ∈ fields, PrimType)
def PrimType.pStruct : ∀ {s}, Struct s → PrimType
| s ⟨f, v⟩ := PrimType.pStruct' s f v
def Struct.get {s} (c : Struct s) (key : string) : option PrimType :=
if h : key ∈ c.fields then some (c.vals _ h) else none
```

#### Mario Carneiro (Aug 01 2020 at 01:06):

In this case it's pretty easy to avoid a mutual inductive because `Struct`

is just a package around the arguments of `pStruct`

Last updated: May 16 2021 at 21:11 UTC