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