# Zulip Chat Archive

## Stream: maths

### Topic: has_mem instance for factor_set

#### Paul van Wamelen (Sep 14 2020 at 01:58):

I'm trying to add a `has_mem`

instance for `factor_set`

:

```
import ring_theory.unique_factorization_domain
variables {α : Type*}
variables [integral_domain α] [unique_factorization_domain α]
namespace associates
open unique_factorization_domain associated
def factor_set_mem : {a : associates α // irreducible a} → (factor_set α) → Prop
| _ ⊤ := true
| p (some l) := p ∈ l
instance : has_mem {a : associates α // irreducible a} (factor_set α) := ⟨factor_set_mem⟩
lemma mem_factor_set_some' {p : associates α} {hp : irreducible p}
{l : multiset {a : associates α // irreducible a }} {ll : factor_set α} (h : ll = some l):
subtype.mk p hp ∈ ll ↔ subtype.mk p hp ∈ l :=
begin
rw h, refl
end
lemma mem_factor_set_some'' {p : associates α} {hp : irreducible p}
{l : multiset {a : associates α // irreducible a }} :
factor_set_mem (subtype.mk p hp) ((some l) : factor_set α) ↔ subtype.mk p hp ∈ l := by refl
lemma mem_factor_set_some {p : associates α} {hp : irreducible p}
{l : multiset {a : associates α // irreducible a }}:
subtype.mk p hp ∈ ((some l) : factor_set α) ↔ subtype.mk p hp ∈ l :=
begin
refl
end
end associates
```

In my `mem_factor_set_some`

lemma the first `∈`

gives me a `failed to synthesize type class instance for`

`has_mem {p // irreducible p} (option (multiset {a // irreducible a}))`

error. The single primed and double primed versions of `mem_factor_set_some`

works, so I don't think I'm messing something up, but of course they are not what we would want. Is there some way of helping lean understand what we want the `∈`

to mean?

Thanks in advance for any help!

#### Johan Commelin (Sep 14 2020 at 06:06):

Isn't there a coercion that's supposed to be used? (I don't know this part of the library too well.)

Or is `some l`

the intended way of moving between the multiset and the factor_set?

#### Anne Baanen (Sep 14 2020 at 10:01):

I think what's going on here is the elaborator checks `((some l) : factor_set α)`

, sees it doesn't make sense, and does unfolding to get `((some l) : roption (multiset _))`

. Satisfied that this makes sense, it processes `subtype.mk p hp ∈ ((some l) : roption (multiset _))`

, the typeclass inference system doesn't know anything about `roption`

and it fails.

I can't find an instance for `has_coe α (roption α)`

, only for `has_coe (option α) (roption α)`

. Coercing would solve the issue because the elaborator doesn't have to unfold `factor_set`

.

#### Paul van Wamelen (Sep 14 2020 at 11:56):

Why does `((some l) : factor_set α)`

not make sense? `factor_set`

is `with_top`

and `with_top`

is `option`

and `option`

is by definition `none`

or `some`

, so I thought `some l`

is by definition a `factor_set`

. How does `roption`

come into the picture? Very confused!

Here are the definitions:

```
@[reducible] def {u} factor_set (α : Type u) [integral_domain α] :
Type u :=
with_top (multiset { a : associates α // irreducible a })
```

and

```
def with_top (α : Type*) := option α
```

and

```
inductive option (α : Type u)
| none : option
| some (val : α) : option
```

#### Paul van Wamelen (Sep 14 2020 at 11:57):

I don't understand why but

```
lemma mem_factor_set_some {p : associates α} {hp : irreducible p}
{l : multiset {a : associates α // irreducible a }}:
subtype.mk p hp ∈ (↑l : factor_set α) ↔ subtype.mk p hp ∈ l := by refl
```

works...

#### Kevin Buzzard (Sep 14 2020 at 13:18):

I think this is unituitive but expected behaviour in Lean. My understanding (which might be wrong) is this: when the kernel sees `a : B`

it checks that `a`

could be thought of as having type definitionally equal to `B`

, but this does not guarantee that `a`

will be thought of as having type *syntactically* equal to `B`

in any further calculations.

#### Kevin Buzzard (Sep 14 2020 at 14:06):

```
def to_with_top {β : Sort*} : option β → with_top β := id
lemma mem_factor_set_some {p : associates α} {hp : irreducible p}
{l : multiset {a : associates α // irreducible a }}:
subtype.mk p hp ∈ (to_with_top (some l) : factor_set α) ↔ subtype.mk p hp ∈ l :=
begin
refl
end
```

#### Aaron Anderson (Sep 14 2020 at 16:18):

As I’m refactoring `unique_factorization_domain`

, I have to ask, what really is the point of `factor_set`

?

#### Aaron Anderson (Sep 14 2020 at 16:18):

The only place it’s used by something else is for putting a `gcd_monoid`

instance on ufds.

#### Aaron Anderson (Sep 14 2020 at 16:21):

It’s useful for that construction because `factors’`

is actually order-preserving, but the exact implementation could change easily

Last updated: May 11 2021 at 17:39 UTC