Stream: Is there code for X?

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

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?

Eric Wieser (Dec 11 2020 at 19:29):

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

Reid Barton (Dec 11 2020 at 19:30):

probably using or (and more parentheses)

Reid Barton (Dec 11 2020 at 19:30):

and a lemma on or

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'

Adam Topaz (Dec 11 2020 at 19:33):

cases f x doesn't work?

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

Eric Wieser (Dec 11 2020 at 19:34):

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

Eric Wieser (Dec 11 2020 at 19:35):

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

Reid Barton (Dec 11 2020 at 19:36):

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

Adam Topaz (Dec 11 2020 at 19:37):

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

Reid Barton (Dec 11 2020 at 19:37):

this also might not be ideally stated

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

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

Eric Wieser (Dec 11 2020 at 19:39):

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

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?

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?

Reid Barton (Dec 11 2020 at 20:39):

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

Reid Barton (Dec 11 2020 at 20:39):

These right-hand sides look pretty unpleasant

Eric Wieser (Dec 11 2020 at 20:40):

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

Reid Barton (Dec 11 2020 at 20:41):

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

Reid Barton (Dec 11 2020 at 20:41):

Because it's not making progress overall

Reid Barton (Dec 11 2020 at 20:41):

I think you want the variation of sum_sum_elim I suggested earlier

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

Oh I missed that

Reid Barton (Dec 11 2020 at 20:56):

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

Reid Barton (Dec 11 2020 at 20:57):

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

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

Reid Barton (Dec 11 2020 at 20:59):

and that reason will determine what kind of lemma you need

Reid Barton (Dec 11 2020 at 20:59):

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

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

Eric Wieser (Dec 12 2020 at 12:08):

You were right, I didn't need this

Mario Carneiro (Dec 12 2020 at 12:09):

This looks like cases e : f x

Eric Wieser (Dec 12 2020 at 12:10):

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

Mario Carneiro (Dec 12 2020 at 12:11):

so like list.partition then?

Eric Wieser (Dec 12 2020 at 12:12):

Well, except on a finset

Mario Carneiro (Dec 12 2020 at 12:13):

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

Mario Carneiro (Dec 12 2020 at 12:14):

I think the problem needs some more un-#xy

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