Zulip Chat Archive

Stream: maths

Topic: has_mem instance for factor_set


view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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