Zulip Chat Archive

Stream: general

Topic: quotient.hrec_on₂


view this post on Zulip Sean Leather (Aug 06 2018 at 11:09):

I've got a definition:

def kunion : m₁.nodup_keys  m₂.nodup_keys  multiset (sigma β) :=
@quotient.hrec_on₂ _ _ _ _
  (λ (m₁ m₂ : multiset (sigma β)), m₁.nodup_keys  m₂.nodup_keys  multiset (sigma β))
  m₁ m₂
  (λ l₁ l₂ (d₁ : l₁.nodup_keys) (d₂ : l₂.nodup_keys), l₁.kunion l₂) $
    λ l₁ l₂ l₃ l₄ p₁₃ p₂₄,
    hfunext (by rw perm_nodup_keys p₁₃) $
      λ (d₁ : l₁.nodup_keys) (d₃ : l₃.nodup_keys) _,
      hfunext (by rw perm_nodup_keys p₂₄) $
        λ (d₂ : l₂.nodup_keys) (d₄ : l₄.nodup_keys) _,
        heq_of_eq $ quotient.sound $ perm_kunion d₂ d₄ p₁₃ p₂₄

local infixr ` k `:67 := kunion

and I want to prove the left and right units:

@[simp] theorem zero_kunion {m : multiset (sigma β)} :  (d : m.nodup_keys), nodup_keys_zero k d = m
@[simp] theorem kunion_zero {m : multiset (sigma β)} :  (d : m.nodup_keys), d k nodup_keys_zero = m

I'm stuck on how to proceed. If I use quotient.induction_on m, I just unfold until I get down to quot.rec_on ↑(hd :: tl) or quot.rec_on ↑nil, but I don't know how to go further. (At one point, I believe I even made the simplifier loop infinitely.)

Any suggestions on how to prove these?

view this post on Zulip Mario Carneiro (Aug 06 2018 at 11:12):

Wow, that's a weird notation

view this post on Zulip Mario Carneiro (Aug 06 2018 at 11:12):

does it have to be a partial function?

view this post on Zulip Sean Leather (Aug 06 2018 at 11:15):

does it have to be a partial function?

I don't follow you.

view this post on Zulip Mario Carneiro (Aug 06 2018 at 11:16):

you could make it return empty when the inputs don't have nodup_keys

view this post on Zulip Mario Carneiro (Aug 06 2018 at 11:17):

or it could be a roption if you are worried about the performance cost of checking nodup_keys

view this post on Zulip Sean Leather (Aug 06 2018 at 11:21):

Sorry, Mario, your use of “it” in multiple places is a bit too vague for me. Are you suggesting I use a different definition for kunion? If so, what is the type signature you're referring to?

view this post on Zulip Sean Leather (Aug 06 2018 at 11:28):

Btw, I'm not asking for a completed solution. You're welcome to give me only hints or suggestions. :smile:

view this post on Zulip Reid Barton (Aug 06 2018 at 11:29):

I think def kunion : multiset (sigma β) → multiset (sigma β) → roption (multiset (sigma β)) and then prove that kunion is defined exactly when each multiset is nodup_keys

view this post on Zulip Sean Leather (Aug 06 2018 at 11:31):

Reid: Hmm, okay, thanks.

view this post on Zulip Sean Leather (Aug 06 2018 at 11:32):

And what's the advantage to this approach? Is it simplicity of the definition and related theorems or performance or both?

view this post on Zulip Reid Barton (Aug 06 2018 at 11:32):

Then you can avoid all this dependent eliminator stuff... although it's not clear to me whether your problem is related to this

view this post on Zulip Sean Leather (Aug 06 2018 at 11:33):

Okay, well, I'll give it a shot.

view this post on Zulip Chris Hughes (Aug 06 2018 at 11:33):

Just proving at quotient.hrec_on_beta lemma might help.

view this post on Zulip Reid Barton (Aug 06 2018 at 11:34):

Yes. Is that just quotient.mk?

view this post on Zulip Sean Leather (Aug 06 2018 at 11:34):

Yes, I think so.

view this post on Zulip Sean Leather (Aug 06 2018 at 11:34):

Chris: I wondered the same thing. I'm not sure how to start with that.

view this post on Zulip Reid Barton (Aug 06 2018 at 11:35):

Well, quotient.rec_on applied to quotient.mk should reduce...

view this post on Zulip Chris Hughes (Aug 06 2018 at 11:35):

Or use show

view this post on Zulip Sean Leather (Aug 06 2018 at 11:37):

I suppose it would look something like:

lemma quot.ind_beta (p :  a, β (quot.mk r a)) (a : α) : (ind p (quot.mk r a) : β (quot.mk r a)) = p a

view this post on Zulip Mario Carneiro (Aug 06 2018 at 12:00):

that is trivially true, since both sides are propositions

view this post on Zulip Mario Carneiro (Aug 06 2018 at 12:01):

The advantage of using roption is avoiding all the hrec mess. I've had to define partial functions over quotients before, and I wish I'd thought of this then

view this post on Zulip Sean Leather (Aug 06 2018 at 12:03):

that is trivially true, since both sides are propositions

Are you referring to quot.ind_beta, which is in the core library, or something else?

The advantage of using roption is avoiding all the hrec mess. I've had to define partial functions over quotients before, and I wish I'd thought of this then

Great! I'm working on it now.

view this post on Zulip Reid Barton (Aug 06 2018 at 12:08):

I think someone probably copied lift_beta to ind_beta without realizing it was rather unnecessary.

view this post on Zulip Sean Leather (Aug 06 2018 at 12:10):

Ah! I see what you're saying now. I didn't look that closely at ind_beta.

view this post on Zulip Sean Leather (Aug 06 2018 at 12:14):

This is definitely a much nicer definition:

def kunion' (m₁ m₂ : multiset (sigma β)) : roption (multiset (sigma β)) :=
quotient.lift_on₂ m₁ m₂ (λ l₁ l₂, roption.mk (l₁.nodup_keys  l₂.nodup_keys) (λ _, (l₁.kunion l₂ : multiset (sigma β)))) $
  λ l₁ l₂ l₃ l₄ p₁₃ p₂₄, roption.ext'
    (and_congr (perm_nodup_keys p₁₃) (perm_nodup_keys p₂₄))
    (λ d₁, d₂ d₃, d₄, quotient.sound $ perm_kunion d₂ d₄ p₁₃ p₂₄)

view this post on Zulip Mario Carneiro (Aug 06 2018 at 12:18):

so now the theorem you want is either m k∪ 0 = some m or m ∈ m k∪ 0 (they are equivalent)

view this post on Zulip Sean Leather (Aug 06 2018 at 12:20):

Right.

view this post on Zulip Mario Carneiro (Aug 06 2018 at 12:22):

and the coercion lemma you want says l₁.nodup_keys → l₂.nodup_keys → ↑l₁ k∪ ↑l₂ = some (l₁.kunion l₂)

view this post on Zulip Sean Leather (Aug 06 2018 at 12:33):

Got that, thanks. How should I coerce the 0 (multiset.zero) for kunion' 0 ↑l?

view this post on Zulip Sean Leather (Aug 06 2018 at 12:35):

If I do simp [has_zero.zero, multiset.zero], lean never ends.

view this post on Zulip Mario Carneiro (Aug 06 2018 at 12:37):

you can just force it to unfold by applying kunion_coe.trans _

view this post on Zulip Mario Carneiro (Aug 06 2018 at 12:37):

or you can rewrite with coe_nil_eq_zero

view this post on Zulip Sean Leather (Aug 06 2018 at 14:05):

The aforementioned theorems:

@[simp] theorem zero_kunion :  (d : m.nodup_keys), kunion' 0 m = roption.some m :=
quotient.induction_on m $ λ _ d, (kunion_coe nodup_keys_zero d).trans rfl

@[simp] theorem kunion_zero :  (d : m.nodup_keys), kunion' m 0 = roption.some m :=
quotient.induction_on m $ λ _ d, (kunion_coe d nodup_keys_zero).trans (by simp)

view this post on Zulip Sean Leather (Aug 06 2018 at 14:21):

One last related question: Now that I have an roption-wrapped multiset, how should I specify theorems that involve the result of kunion'? For example, I had:

@[simp] theorem mem_kunion {s : sigma β} :  (d₁ : m₁.nodup_keys) (d₂ : m₂.nodup_keys),
  disjoint m₁.keys m₂.keys  (s  d₁ k d₂  s  m₁  s  m₂) :=
quotient.induction_on₂ m₁ m₂ $ λ _ _ _ _, mem_kunion_iff

Should this become...?

@[simp] theorem mem_kunion' {s : sigma β} :  (d₁ : m₁.nodup_keys) (d₂ : m₂.nodup_keys),
  disjoint m₁.keys m₂.keys   m  kunion' m₁ m₂, s  m  s  m₁  s  m₂ :=
quotient.induction_on₂ m₁ m₂ $ λ l₁ l₂ d₁ d₂ dk,
  ⟨_, roption.eq_some_iff.mp (kunion_coe d₁ d₂), mem_kunion_iff dk

Specifically, I mean: should I use a pattern like ∃ m ∈ kunion' m₁ m₂, ... for theorems like this, or is there a better way?

view this post on Zulip Mario Carneiro (Aug 06 2018 at 14:35):

I would take m ∈ kunion' m₁ m₂ as a hypothesis and prove s ∈ m ↔ s ∈ m₁ ∨ s ∈ m₂

view this post on Zulip Mario Carneiro (Aug 06 2018 at 14:36):

of course this hypothesis eliminates the need for d1 and d2

view this post on Zulip Mario Carneiro (Aug 06 2018 at 14:37):

alternatively, you can define kunion as (kunion' m1 m2).get <d1, d2> and have all your old theorems back

view this post on Zulip Sean Leather (Aug 06 2018 at 17:07):

True. I'm not sure which is a better definition to work with. If I were using the multiset interface directly, I would lean towards defining kunion as (kunion' m1 m2).get <d1, d2>. But since it's really meant to be the underlying implementation of finmap, perhaps it's not necessary.

view this post on Zulip Sean Leather (Aug 06 2018 at 17:08):

Also, do you think I should use roption + quotient.lift_on consistently instead of quotient.hrec_on? I don't have any more uses of quotient.hrec_on₂, but I do have a number of uses of quotient.hrec_on.

view this post on Zulip Sean Leather (Aug 07 2018 at 07:50):

@Mario Carneiro I'd like to get your thoughts on this :point_up:. I haven't had any problems with quotient.hrec_on up to now, but maybe things would just be nicer all around if I used roption more. I'm not sure.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 07:51):

I think if it works once, it will probably work again

view this post on Zulip Mario Carneiro (Aug 07 2018 at 07:52):

Also, another option I forgot to mention was to make kunion a nondependent function, using the fact that nodup_keys is decidable

view this post on Zulip Sean Leather (Aug 07 2018 at 07:52):

Just to be clear about what you mean, do you think I should change the defs here to use roption?

view this post on Zulip Sean Leather (Aug 07 2018 at 07:53):

(Just search for hrec_on.)

view this post on Zulip Mario Carneiro (Aug 07 2018 at 07:53):

Even if we suppose that checking this is expensive, it doesn't matter if you are just using it as an abstract version so you can prove equations about it

view this post on Zulip Sean Leather (Aug 07 2018 at 07:53):

Also, another option I forgot to mention was to make kunion a nondependent function, using the fact that nodup_keys is decidable

What do you mean by this?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 07:55):

define kunion m1 m2 = if h : m1.nodup_keys /\ m2.nodup_keys then (kunion' m1 m2).get h else 0

view this post on Zulip Sean Leather (Aug 07 2018 at 07:56):

That's an interesting suggestion.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 07:57):

in fact, even if nodup_keys wasn't decidable you could make this definition anyway noncomputably and just not use it for evaluation

view this post on Zulip Sean Leather (Aug 07 2018 at 08:00):

Hmm, yes, I think I like this definition of kunion. I don't have to pass around the m1.nodup_keys everywhere.

view this post on Zulip Sean Leather (Aug 07 2018 at 08:01):

Okay, well, I'll play around with it.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:01):

Yet more alternatively, you could define the subtype. Didn't you have finmap at one point for this?

view this post on Zulip Sean Leather (Aug 07 2018 at 08:02):

I decided to go with the structure for the same reasons finset is a structure:

structure finmap (α : Type u) (β : α  Type v) : Type (max u v) :=
(val : multiset (sigma β))
(nodup_keys : val.nodup_keys)

view this post on Zulip Sean Leather (Aug 07 2018 at 08:02):

Mainly, for type class instance resolution.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:03):

that's fine, my point was that you can define finmap.rec_on to encapsulate this definition pattern

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:03):

and this way you never have to carry around any proofs since they are embedded in the type

view this post on Zulip Sean Leather (Aug 07 2018 at 08:04):

You mean the if h : m.nodup_keys ... then ... else ... pattern?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:04):

no, the roption or hrec_on version

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:04):

(it doesn't really matter too much which one you use, since it only has to be done once)

view this post on Zulip Sean Leather (Aug 07 2018 at 08:06):

Oh.... I'm awfully dumb today. So, define a finmap.rec_on that takes an roption (multiset (sigma β)) to a finmap?

view this post on Zulip Sean Leather (Aug 07 2018 at 08:07):

Err, actually the arrow goes the other way...

view this post on Zulip Sean Leather (Aug 07 2018 at 08:07):

Anyway, it'd be a higher-order function.

view this post on Zulip Sean Leather (Aug 07 2018 at 08:07):

Yeah, I think I see it.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:08):

finmap.rec_on takes a finmap A B, a function list (sigma B) -> C, and a proof that this function is equal up to permutation when the arguments have nodup_keys

view this post on Zulip Sean Leather (Aug 07 2018 at 08:08):

Right.

view this post on Zulip Sean Leather (Aug 07 2018 at 08:10):

So, given that, I would be skipping defining all of the defs and theorems for multiset and define them for only list and finmap?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:13):

right

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:13):

You can reconstruct the multiset definitions from the finmap ones by the if ... else 0 trick

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:15):

I think multisets are a good stepping stone if you can actually define functions on them, but in your case the functions already have to assume nodup just to be well defined, so they've already jumped to finmap

view this post on Zulip Sean Leather (Aug 07 2018 at 08:15):

That's true.

view this post on Zulip Sean Leather (Aug 07 2018 at 08:17):

Okay, I'm convinced.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:20):

I notice you have theorems like s.1 ∈ (m.map_snd f).keys ↔ s.1 ∈ m.keys with several variations. Why isn't this just (m.map_snd f).keys = m.keys?

view this post on Zulip Sean Leather (Aug 07 2018 at 08:21):

Because I use the mem one in the non-mem.

view this post on Zulip Sean Leather (Aug 07 2018 at 08:22):

I suppose I don't have to.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:23):

the proof is just map_comp

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:23):

you shouldn't use mem to try to characterize a multiset, it gets messy

view this post on Zulip Sean Leather (Aug 07 2018 at 08:25):

The other problem with the map_snd/keys theorems is that I wanted to use it in finmap, but the best I could come up with was using [inhabited (∀ a, β₁ a)]. I'm not happy with that solution.

view this post on Zulip Sean Leather (Aug 07 2018 at 08:25):

the proof is just map_comp

The proof of which?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:27):

I'm really confused about your confusion. It should be provable that (m.map_snd f).keys = m.keys, this makes the last 7 theorems or so unnecessary and it doesn't require any weird assumptions

view this post on Zulip Sean Leather (Aug 07 2018 at 08:31):

Okay, I think I see what you're saying. I'll give it a shot.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:31):

wait, just the last 4. The ones about (m.map f).keys are a bit awkward because f : sigma B1 -> sigma B2 can mingle keys and values in an unpredictable way. How about defining m.map f g where f : A1 -> A2 and g : ∀ a, B1 a -> B2 (f a); then you should be able to prove (m.map f g).keys = m.keys.map f and life is good

view this post on Zulip Sean Leather (Aug 07 2018 at 08:33):

Btw, did you mean map_map instead of map_comp?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:34):

yes

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:34):

it's written backwards for simp lemmas because comp is dumb

view this post on Zulip Mario Carneiro (Aug 07 2018 at 08:34):

so the name becomes map_map instead of map_comp

view this post on Zulip Sean Leather (Aug 08 2018 at 07:53):

I could only figure out how to do a general 2-arg finmap recursor using quotient.hrec_on₂:

protected def lrec_on₂ {γ : Sort*} (f g : finmap α β)
  (φ :  {l₁ l₂ : list (sigma β)}, l₁.nodup_keys  l₂.nodup_keys  γ)
  (c :  {l₁ l₂ l₃ l₄} (p₁₃ : l₁ ~ l₃) (p₂₄ : l₂ ~ l₄) d₁ d₂ d₃ d₄, φ d₁ d₂ = φ d₃ d₄) : γ :=
@quotient.hrec_on₂ _ _ _ _
  (λ (m₁ m₂ : multiset (sigma β)), m₁.nodup_keys  m₂.nodup_keys  γ)
  f.val g.val
  (λ l₁ l₂ (d₁ : l₁.nodup_keys) (d₂ : l₂.nodup_keys), φ d₁ d₂)
  (λ l₁ l₂ l₃ l₄ p₁₃ p₂₄, hfunext (by rw list.perm_nodup_keys p₁₃) $
    λ d₁ d₃ _, hfunext (by rw list.perm_nodup_keys p₂₄) $
      λ d₂ d₄ _, heq_of_eq $ c p₁₃ p₂₄ d₁ d₂ d₃ d₄)
  f.nodup_keys g.nodup_keys

I have a general 2-arg finmap.lift_on₂:

protected def lift_on₂ {γ : Type*}
  (f g : finmap α β)
  (φ :  {l₁ l₂ : list (sigma β)}, l₁.nodup_keys  l₂.nodup_keys  γ)
  (c :  {l₁ l₂ l₃ l₄} (p₁₃ : l₁ ~ l₃) (p₂₄ : l₂ ~ l₄) d₁ d₂ d₃ d₄, φ d₁ d₂ = φ d₃ d₄) :
  roption γ :=
quotient.lift_on₂ f.val g.val
  (λ l₁ l₂, roption.mk (l₁.nodup_keys  l₂.nodup_keys) (λ d₁, d₂, φ d₁ d₂))
  (λ l₁ l₂ l₃ l₄ p₁₃ p₂₄, roption.ext'
    (and_congr (list.perm_nodup_keys p₁₃) (list.perm_nodup_keys p₂₄))
    (λ d₁, d₂ d₃, d₄, c p₁₃ p₂₄ d₁ d₂ d₃ d₄))

But it seems like the roption.dom has a pair of lists, so this only seems useful in combination with quotient.induction_on₂. Is that right? Or can I do better?

view this post on Zulip Mario Carneiro (Aug 08 2018 at 08:24):

What does the one arg version look like?

view this post on Zulip Sean Leather (Aug 08 2018 at 08:25):

protected def lrec_on {γ : Sort*} (f : finmap α β)
  (φ :  {l : list (sigma β)}, l.nodup_keys  γ)
  (c :  {l₁ l₂} (p : l₁ ~ l₂) d₁ d₂, φ d₁ = φ d₂) : γ :=
@quotient.hrec_on _ _ (λ (m : multiset (sigma β)), m.nodup_keys  γ)
  f.val
  (λ l (d : l.nodup_keys), φ d)
  (λ l₁ l₂ p, hfunext (by rw list.perm_nodup_keys p) $ λ d₁ d₂ _, heq_of_eq $ c p d₁ d₂)
  f.nodup_keys

view this post on Zulip Sean Leather (Aug 08 2018 at 08:30):

There are theorems where quotient.induction_on₂ needs more than just l₁.nodup_keys and l₂.nodup_keys:

@[simp] theorem mem_kunion' {s : sigma β} :  (d₁ : m₁.nodup_keys) (d₂ : m₂.nodup_keys),
  disjoint m₁.keys m₂.keys   m  kunion' m₁ m₂, s  m  s  m₁  s  m₂ :=
quotient.induction_on₂ m₁ m₂ $ λ l₁ l₂ d₁ d₂ dk,
  ⟨_, roption.eq_some_iff.mp (kunion_coe d₁ d₂), mem_kunion_iff dk

So, I think the above finmap.lift_on₂ definition makes sense.

view this post on Zulip Mario Carneiro (Aug 08 2018 at 10:10):

I would suggest you state lrec_on like this:

protected def lrec_on {γ : Sort*} (f : finmap α β)
  (φ : list (sigma β) → γ)
  (c : ∀ {l₁ l₂} (p : l₁ ~ l₂), l₁.nodup_keys → l₂.nodup_keys → φ l₁ = φ l₂) : γ :=

Recall that we are trying to avoid partial functions. The function φ is defined on lists, so there presumably won't be any trouble making arbitrary choices that depend on the order

view this post on Zulip Mario Carneiro (Aug 08 2018 at 10:11):

Given this it should not be hard to just iterate it twice to get lrec_on₂

view this post on Zulip Sean Leather (Aug 08 2018 at 12:04):

Okay, so I have the following.

My initial version:

protected def lrec_on {γ : Sort*} (f : finmap α β)
  (φ :  {l : list (sigma β)}, l.nodup_keys  γ)
  (c :  {l₁ l₂} (p : l₁ ~ l₂) d₁ d₂, φ d₁ = φ d₂) : γ :=
@quotient.hrec_on _ _ (λ (m : multiset (sigma β)), m.nodup_keys  γ)
  f.val
  (λ l (d : l.nodup_keys), φ d)
  (λ l₁ l₂ p, hfunext (by rw list.perm_nodup_keys p) $ λ d₁ d₂ _, heq_of_eq $ c p d₁ d₂)
  f.nodup_keys

def erase (f : finmap α β) (a : α) : finmap α β :=
finmap.lrec_on f
  (λ l d, l.kerase a, list.nodup_keys_kerase a d)
  (λ l₁ l₂ p d₁ d₂, eq_of_veq $ quotient.sound $ list.perm_kerase a d₁ d₂ p)

Your suggestion:

protected def lrec_on' {γ : Sort*} (f : finmap α β)
  (φ : list (sigma β)  γ)
  (c :  {l₁ l₂} (p : l₁ ~ l₂), l₁.nodup_keys  l₂.nodup_keys  φ l₁ = φ l₂) : γ :=
@quotient.hrec_on _ _ (λ (m : multiset (sigma β)), m.nodup_keys  γ)
  f.val
  (λ l _, φ l)
  (λ l₁ l₂ p, hfunext (by simp [list.perm_nodup_keys p]) $ λ d₁ d₂ _, heq_of_eq $ c p d₁ d₂)
  f.nodup_keys

def erase' (f : finmap α β) (a : α) : finmap α β :=
finmap.lrec_on' f
  (λ l, l.kerase a, list.nodup_keys_kerase a _⟩)
  (λ l₁ l₂ p d₁ d₂, eq_of_veq $ quotient.sound $ list.perm_kerase a d₁ d₂ p)

I can define erase with lrec_on, but how do I define erase' with lrec_on'?

error: don't know how to synthesize placeholder
context:
α : Type u,
_inst_1 : decidable_eq α,
β : α  Type v,
f : finmap α β,
a : α,
l : list (sigma β)
 list.nodup_keys l

Last updated: May 08 2021 at 04:14 UTC