Zulip Chat Archive

Stream: Is there code for X?

Topic: If it's not sum.inr then it's sum.inr


view this post on Zulip Eric Wieser (Dec 11 2020 at 19:28):

Is there a better way to state ∀ i, ¬∃ (i' : α), sum.inl i' = i → ∃ (i' : α), sum.inr i' = i?

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:29):

(it's obviously an iff, but I only need that direction)

view this post on Zulip Reid Barton (Dec 11 2020 at 19:30):

probably using or (and more parentheses)

view this post on Zulip Reid Barton (Dec 11 2020 at 19:30):

and a lemma on or

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:32):

To un-xy, I want to split a sum over x into the cases when f x is sum.inl x' and sum.inr x'

view this post on Zulip Adam Topaz (Dec 11 2020 at 19:33):

cases f x doesn't work?

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:33):

And right now I do it by inserting if ( ∃ (i' : α), sum.inl i' = f i) then g x else g x then using docs#finset.sum_ite

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:34):

If I used sum.elim, then I'd need a different finset lemma

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:35):

Oh, I'm looking for that "make conjunction/disjunction of inductive" command, I think?

view this post on Zulip Reid Barton (Dec 11 2020 at 19:36):

hmm is that the only lemma with a sum of two sums on the right?

view this post on Zulip Adam Topaz (Dec 11 2020 at 19:37):

(∃ b : β, f x = sum.inl b) ∨ (∃ c : γ, f x = sum.inr c) ?

view this post on Zulip Reid Barton (Dec 11 2020 at 19:37):

How about docs#finset.sum_sum_elim

view this post on Zulip Reid Barton (Dec 11 2020 at 19:37):

this also might not be ideally stated

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:38):

Oh that would be perfect. Whoops. I assumed it would be more general so I could use it on arbitrary enum-like typee

view this post on Zulip Reid Barton (Dec 11 2020 at 19:38):

It would be nice if it just had h x on the left, and h (sum.inl x) and h (sum.inr x) on the right

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:39):

Yeah, you're right that the current statement isn't enough for me

view this post on Zulip Eric Wieser (Dec 11 2020 at 19:40):

Is there a version of mk_iff_of_inductive_prop that works for data and produces existentials?

view this post on Zulip Eric Wieser (Dec 11 2020 at 20:35):

Coming back to this with lean accessible - the best statement I can come up with is:

example {α β γ δ : Type*} [fintype γ] [comm_monoid δ] (f : γ  α  β) (g : γ  δ) :
   (i : γ), g i =  (i : γ) in finset.univ.filter (λ i,  i', f i = sum.inl i'), g i *
                    (i : γ) in finset.univ.filter (λ i,  i', f i = sum.inr i'), g i := sorry

or for a more general case

example {α β γ δ : Type*} [fintype γ] [comm_monoid δ] (f : γ  α  β) (g : γ  α  δ) (h : γ  β  δ) :
   (i : γ), (f i).elim (g i) (h i) =
                    (i : {i : γ //  i', f i = sum.inl i'}), g i (classical.some i.prop) *
                    (i : {i : γ //  i', f i = sum.inr i'}), h i (classical.some i.prop) := sorry

Can you think of a better theorem statement?

view this post on Zulip Reid Barton (Dec 11 2020 at 20:39):

the first one is just a special case of product over a disjoint union right?

view this post on Zulip Reid Barton (Dec 11 2020 at 20:39):

These right-hand sides look pretty unpleasant

view this post on Zulip Eric Wieser (Dec 11 2020 at 20:40):

Yes, it is - do we have a lemma for that already?

view this post on Zulip Reid Barton (Dec 11 2020 at 20:41):

surely, but I don't think it really helps you

view this post on Zulip Reid Barton (Dec 11 2020 at 20:41):

Because it's not making progress overall

view this post on Zulip Reid Barton (Dec 11 2020 at 20:41):

I think you want the variation of sum_sum_elim I suggested earlier

view this post on Zulip Eric Wieser (Dec 11 2020 at 20:51):

The difficulty is I'm not splitting over the summand, I'm splitting over some function of it

view this post on Zulip Reid Barton (Dec 11 2020 at 20:53):

Oh I missed that

view this post on Zulip Reid Barton (Dec 11 2020 at 20:56):

I don't know, this is too abstract I think

view this post on Zulip Reid Barton (Dec 11 2020 at 20:57):

I mean a lemma only helps if the new expression is actually easier to deal with

view this post on Zulip Reid Barton (Dec 11 2020 at 20:58):

There must be some reason why knowing what side f i is in helps you evaluate the sum

view this post on Zulip Reid Barton (Dec 11 2020 at 20:59):

and that reason will determine what kind of lemma you need

view this post on Zulip Reid Barton (Dec 11 2020 at 20:59):

but in general, there's docs#finset.sum_union :shrug:

view this post on Zulip Eric Wieser (Dec 11 2020 at 21:04):

Perhaps I should just push forward with what I have, and ask again once I have a working proof

view this post on Zulip Eric Wieser (Dec 12 2020 at 12:08):

You were right, I didn't need this

view this post on Zulip Mario Carneiro (Dec 12 2020 at 12:09):

This looks like cases e : f x

view this post on Zulip Eric Wieser (Dec 12 2020 at 12:10):

Indeed - although I thought I need to split the sum before I had x available

view this post on Zulip Mario Carneiro (Dec 12 2020 at 12:11):

so like list.partition then?

view this post on Zulip Eric Wieser (Dec 12 2020 at 12:12):

Well, except on a finset

view this post on Zulip Mario Carneiro (Dec 12 2020 at 12:13):

there is a theorem about partitioning a finset using finset.filter

view this post on Zulip Mario Carneiro (Dec 12 2020 at 12:14):

I think the problem needs some more un-#xy

view this post on Zulip Eric Wieser (Dec 12 2020 at 12:16):

I got what I needed with something completely different (in #5269, alternating.lean:590, with by_cases). The PR hasn't been cleaned up yet, but once it has been I'd appreciate suggestions for shortening the proof


Last updated: May 17 2021 at 16:26 UTC