swapping exists and or

Stream: Is there code for X?

[Kevin Lacker]

Is there a way to prove this swap of order of operations simply, or do I have to spell it out:

example (f g : ℕ → Prop) : ∃ k : ℕ, f k ∨ ∃ k : ℕ, g k ↔ ∃ k : ℕ, f k ∨ g k :=
sorry

[Scott Morrison]

I think you want some additional parentheses.

[Kevin Lacker]

because it's unreadable or because it's wrong?

[Kevin Lacker]

well at any rate what i mean is:

example (f g : ℕ → Prop) : (∃ k : ℕ, f k) ∨ (∃ k : ℕ, g k) ↔ ∃ k : ℕ, f k ∨ g k :=
sorry

[Eric Wieser]

Your leftmost existential contains the iff in the original

[Kevin Lacker]

gotcha

[Kevin Lacker]

all right, now library_search finds it. thanks

[Scott Morrison]

I'd hoped that by { tidy, solve_by_elim* [or.inl, or.inr] { max_depth := 20 }, } was going to solve it, but instead I seem to have found a bug in solve_by_elim.

[Yakov Pechersky]

example (f g : ℕ → Prop) : ((∃ k : ℕ, f k) ∨ ∃ k : ℕ, g k) ↔ ∃ k : ℕ, f k ∨ g k :=
begin
  split,
  { intro h,
    rcases h with ⟨kf, hf⟩|⟨kg, hg⟩,
    { exact ⟨kf, or.inl hf⟩ },
    { exact ⟨kg, or.inr hg⟩ } },
  { rintro ⟨k, hf | hg⟩,
    { exact or.inl ⟨k, hf⟩ },
    { exact or.inr ⟨k, hg⟩ } },
end

example (f g : ℕ → Prop) : ((∃ k : ℕ, f k) ∨ ∃ k : ℕ, g k) ↔ ∃ k : ℕ, f k ∨ g k :=
by { split; finish }

[Scott Morrison]

yay finish!

[Floris van Doorn]

docs#exists_or_distrib

[Yakov Pechersky]

I was surprised finish can't do the split itself

[Eric Wieser]

May as well use rintro in place of intro, rcases in that long proof

[Yakov Pechersky]

I couldn't get the right rintro invocation for the mp case, it was unfolding the nat instead for me

[Scott Morrison]

In fact, you can also prove this by two successive calls to hint. :-)

[Eric Wieser]

What spelling didn't work @Yakov Pechersky ?

[Kevin Lacker]

once I fixed the syntax, library_search found exists_or_distrib

[Kevin Lacker]

so { split; finish } works but {split, finish} doesn't - what does the semicolon do that's different from the comma?

[Scott Morrison]

X; Y runs Y on every goal produced by X

[Kevin Lacker]

oh i see. so x; y is the same as saying x, all_goals { y} ?

[Scott Morrison]

almost!

[Yakov Pechersky]

example (f g : ℕ → Prop) : ((∃ k : ℕ, f k) ∨ ∃ k : ℕ, g k) ↔ ∃ k : ℕ, f k ∨ g k :=
begin
  split,
  rintro ⟨⟨kf, hf⟩|⟨kg, hg⟩⟩,
  sorry
end

does not do what I expected

[Scott Morrison]

If there were already multiple goals then they will behave differently.

[Kevin Lacker]

why does there have to be a dozen different ways to do everything

[Scott Morrison]

math is hard :-)

[Kevin Lacker]

well, thanks. on this particular instance where f and g are actually big formulas, running split; finish is taking like 4-5 seconds to compile. but refine exists_or_distrib is a lot faster so i'll go with that one

[Yakov Pechersky]

finish can be slow because it's doing basically what my explicit proof is, breaks down everything to as far as it can go, then reconstructs by the "obvious" type matching expressions

[Eric Wieser]

@Yakov Pechersky, I think you can remove the outer angle brackets

[Eric Wieser]

To fix that rintro

[Yakov Pechersky]

Then the pipe doesn't work, | has to be inside angle brackets in rintro

[Eric Wieser]

Does it work in parentheses?

[Yakov Pechersky]

OK, yeah, rintro (⟨kf, hf⟩|⟨kg, hg⟩), works

[Scott Morrison]

Scott Morrison said:

I'd hoped that by { tidy, solve_by_elim* [or.inl, or.inr] { max_depth := 20 }, } was going to solve it, but instead I seem to have found a bug in solve_by_elim.

#4519