# Zulip Chat Archive

## Stream: general

### Topic: quotient.hrec_on₂

#### 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?

#### Mario Carneiro (Aug 06 2018 at 11:12):

Wow, that's a weird notation

#### Mario Carneiro (Aug 06 2018 at 11:12):

does it have to be a partial function?

#### Sean Leather (Aug 06 2018 at 11:15):

does it have to be a partial function?

I don't follow you.

#### Mario Carneiro (Aug 06 2018 at 11:16):

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

#### 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`

#### 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?

#### 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:

#### 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`

#### Sean Leather (Aug 06 2018 at 11:31):

Reid: Hmm, okay, thanks.

#### 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?

#### 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

#### Sean Leather (Aug 06 2018 at 11:33):

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

#### Chris Hughes (Aug 06 2018 at 11:33):

Just proving at ` quotient.hrec_on_beta`

lemma might help.

#### Reid Barton (Aug 06 2018 at 11:34):

Yes. Is that `↑`

just `quotient.mk`

?

#### Sean Leather (Aug 06 2018 at 11:34):

Yes, I think so.

#### Sean Leather (Aug 06 2018 at 11:34):

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

#### Reid Barton (Aug 06 2018 at 11:35):

Well, `quotient.rec_on`

applied to `quotient.mk`

should reduce...

#### Chris Hughes (Aug 06 2018 at 11:35):

Or use `show`

#### 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

#### Mario Carneiro (Aug 06 2018 at 12:00):

that is trivially true, since both sides are propositions

#### 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

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

#### Reid Barton (Aug 06 2018 at 12:08):

I think someone probably copied `lift_beta`

to `ind_beta`

without realizing it was rather unnecessary.

#### 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`

.

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

#### 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)

#### Sean Leather (Aug 06 2018 at 12:20):

Right.

#### 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₂)`

#### Sean Leather (Aug 06 2018 at 12:33):

Got that, thanks. How should I coerce the 0 (`multiset.zero`

) for `kunion' 0 ↑l`

?

#### Sean Leather (Aug 06 2018 at 12:35):

If I do `simp [has_zero.zero, multiset.zero]`

, lean never ends.

#### Mario Carneiro (Aug 06 2018 at 12:37):

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

#### Mario Carneiro (Aug 06 2018 at 12:37):

or you can rewrite with `coe_nil_eq_zero`

#### 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)

#### 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?

#### 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₂`

#### Mario Carneiro (Aug 06 2018 at 14:36):

of course this hypothesis eliminates the need for d1 and d2

#### 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

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

#### 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`

.

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

#### Mario Carneiro (Aug 07 2018 at 07:51):

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

#### 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

#### 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`

?

#### Sean Leather (Aug 07 2018 at 07:53):

(Just search for `hrec_on`

.)

#### 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

#### 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?

#### 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`

#### Sean Leather (Aug 07 2018 at 07:56):

That's an interesting suggestion.

#### 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

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

#### Sean Leather (Aug 07 2018 at 08:01):

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

#### 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?

#### 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)

#### Sean Leather (Aug 07 2018 at 08:02):

Mainly, for type class instance resolution.

#### 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

#### 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

#### Sean Leather (Aug 07 2018 at 08:04):

You mean the `if h : m.nodup_keys ... then ... else ...`

pattern?

#### Mario Carneiro (Aug 07 2018 at 08:04):

no, the `roption`

or `hrec_on`

version

#### 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)

#### 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`

?

#### Sean Leather (Aug 07 2018 at 08:07):

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

#### Sean Leather (Aug 07 2018 at 08:07):

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

#### Sean Leather (Aug 07 2018 at 08:07):

Yeah, I think I see it.

#### 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`

#### Sean Leather (Aug 07 2018 at 08:08):

Right.

#### 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`

?

#### Mario Carneiro (Aug 07 2018 at 08:13):

right

#### Mario Carneiro (Aug 07 2018 at 08:13):

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

trick

#### 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

#### Sean Leather (Aug 07 2018 at 08:15):

That's true.

#### Sean Leather (Aug 07 2018 at 08:17):

Okay, I'm convinced.

#### 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`

?

#### Sean Leather (Aug 07 2018 at 08:21):

Because I use the `mem`

one in the non-`mem`

.

#### Sean Leather (Aug 07 2018 at 08:22):

I suppose I don't have to.

#### Mario Carneiro (Aug 07 2018 at 08:23):

the proof is just `map_comp`

#### Mario Carneiro (Aug 07 2018 at 08:23):

you shouldn't use `mem`

to try to characterize a multiset, it gets messy

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

#### Sean Leather (Aug 07 2018 at 08:25):

the proof is just

`map_comp`

The proof of which?

#### 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

#### Sean Leather (Aug 07 2018 at 08:31):

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

#### 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

#### Sean Leather (Aug 07 2018 at 08:33):

Btw, did you mean `map_map`

instead of `map_comp`

?

#### Mario Carneiro (Aug 07 2018 at 08:34):

yes

#### Mario Carneiro (Aug 07 2018 at 08:34):

it's written backwards for simp lemmas because `comp`

is dumb

#### Mario Carneiro (Aug 07 2018 at 08:34):

so the name becomes `map_map`

instead of `map_comp`

#### 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?

#### Mario Carneiro (Aug 08 2018 at 08:24):

What does the one arg version look like?

#### 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

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

#### 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

#### Mario Carneiro (Aug 08 2018 at 10:11):

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

#### 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: Aug 03 2023 at 10:10 UTC