has_mem instance for factor_set

Stream: maths

[Paul van Wamelen]

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]

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]

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]

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]

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]

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]

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]

As I’m refactoring unique_factorization_domain, I have to ask, what really is the point of factor_set?

[Aaron Anderson]

The only place it’s used by something else is for putting a gcd_monoid instance on ufds.

[Aaron Anderson]

It’s useful for that construction because factors’ is actually order-preserving, but the exact implementation could change easily