## Stream: Is there code for X?

### Topic: swapping exists and or

#### Kevin Lacker (Oct 07 2020 at 22:48):

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 (Oct 07 2020 at 23:07):

I think you want some additional parentheses.

#### Kevin Lacker (Oct 07 2020 at 23:08):

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

#### Kevin Lacker (Oct 07 2020 at 23:10):

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 (Oct 07 2020 at 23:10):

Your leftmost existential contains the iff in the original

gotcha

#### Kevin Lacker (Oct 07 2020 at 23:11):

all right, now library_search finds it. thanks

#### Scott Morrison (Oct 07 2020 at 23:11):

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 (Oct 07 2020 at 23:11):

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 (Oct 07 2020 at 23:11):

yay finish!

#### Floris van Doorn (Oct 07 2020 at 23:12):

docs#exists_or_distrib

#### Yakov Pechersky (Oct 07 2020 at 23:12):

I was surprised finish can't do the split itself

#### Eric Wieser (Oct 07 2020 at 23:12):

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

#### Yakov Pechersky (Oct 07 2020 at 23:13):

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

#### Scott Morrison (Oct 07 2020 at 23:13):

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

#### Eric Wieser (Oct 07 2020 at 23:13):

What spelling didn't work @Yakov Pechersky ?

#### Kevin Lacker (Oct 07 2020 at 23:13):

once I fixed the syntax, library_search found exists_or_distrib

#### Kevin Lacker (Oct 07 2020 at 23:14):

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

#### Scott Morrison (Oct 07 2020 at 23:14):

X; Y runs Y on every goal produced by X

#### Kevin Lacker (Oct 07 2020 at 23:15):

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

almost!

#### Yakov Pechersky (Oct 07 2020 at 23:15):

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 (Oct 07 2020 at 23:15):

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

#### Kevin Lacker (Oct 07 2020 at 23:16):

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

math is hard :-)

#### Kevin Lacker (Oct 07 2020 at 23:21):

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 (Oct 07 2020 at 23:23):

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 (Oct 07 2020 at 23:29):

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

#### Eric Wieser (Oct 07 2020 at 23:29):

To fix that rintro

#### Yakov Pechersky (Oct 07 2020 at 23:29):

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

#### Eric Wieser (Oct 07 2020 at 23:30):

Does it work in parentheses?

#### Yakov Pechersky (Oct 07 2020 at 23:31):

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

#### Scott Morrison (Oct 08 2020 at 00:38):

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

Last updated: May 07 2021 at 21:10 UTC