quotient.hrec_on₂

Stream: general

[Sean Leather]

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?

[Mario Carneiro]

Wow, that's a weird notation

[Mario Carneiro]

does it have to be a partial function?

[Sean Leather]

does it have to be a partial function?

I don't follow you.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

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?

[Sean Leather]

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

[Reid Barton]

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

[Sean Leather]

Reid: Hmm, okay, thanks.

[Sean Leather]

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

[Reid Barton]

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

[Sean Leather]

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

[Chris Hughes]

Just proving at quotient.hrec_on_beta lemma might help.

[Reid Barton]

Yes. Is that ↑ just quotient.mk?

[Sean Leather]

Yes, I think so.

[Sean Leather]

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

[Reid Barton]

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

[Chris Hughes]

Or use show

[Sean Leather]

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

[Mario Carneiro]

that is trivially true, since both sides are propositions

[Mario Carneiro]

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

[Sean Leather]

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.

[Reid Barton]

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

[Sean Leather]

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

[Sean Leather]

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₂₄)

[Mario Carneiro]

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

[Sean Leather]

Right.

[Mario Carneiro]

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

[Sean Leather]

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

[Sean Leather]

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

[Mario Carneiro]

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

[Mario Carneiro]

or you can rewrite with coe_nil_eq_zero

[Sean Leather]

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)

[Sean Leather]

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?

[Mario Carneiro]

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

[Mario Carneiro]

of course this hypothesis eliminates the need for d1 and d2

[Mario Carneiro]

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

[Sean Leather]

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.

[Sean Leather]

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.

[Sean Leather]

@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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

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

[Sean Leather]

(Just search for hrec_on.)

[Mario Carneiro]

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

[Sean Leather]

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?

[Mario Carneiro]

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

[Sean Leather]

That's an interesting suggestion.

[Mario Carneiro]

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

[Sean Leather]

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

[Sean Leather]

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

[Mario Carneiro]

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

[Sean Leather]

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)

[Sean Leather]

Mainly, for type class instance resolution.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

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

[Mario Carneiro]

no, the roption or hrec_on version

[Mario Carneiro]

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

[Sean Leather]

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

[Sean Leather]

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

[Sean Leather]

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

[Sean Leather]

Yeah, I think I see it.

[Mario Carneiro]

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

[Sean Leather]

Right.

[Sean Leather]

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

[Mario Carneiro]

right

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

That's true.

[Sean Leather]

Okay, I'm convinced.

[Mario Carneiro]

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?

[Sean Leather]

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

[Sean Leather]

I suppose I don't have to.

[Mario Carneiro]

the proof is just map_comp

[Mario Carneiro]

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

[Sean Leather]

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.

[Sean Leather]

the proof is just map_comp

The proof of which?

[Mario Carneiro]

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

[Sean Leather]

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

[Mario Carneiro]

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

[Sean Leather]

Btw, did you mean map_map instead of map_comp?

[Mario Carneiro]

yes

[Mario Carneiro]

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

[Mario Carneiro]

so the name becomes map_map instead of map_comp

[Sean Leather]

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?

[Mario Carneiro]

What does the one arg version look like?

[Sean Leather]

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

[Sean Leather]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sean Leather]

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