Zulip Chat Archive

Stream: Is there code for X?

Topic: swapping exists and or


view this post on Zulip 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

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:07):

I think you want some additional parentheses.

view this post on Zulip Kevin Lacker (Oct 07 2020 at 23:08):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 07 2020 at 23:10):

Your leftmost existential contains the iff in the original

view this post on Zulip Kevin Lacker (Oct 07 2020 at 23:10):

gotcha

view this post on Zulip Kevin Lacker (Oct 07 2020 at 23:11):

all right, now library_search finds it. thanks

view this post on Zulip 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.

view this post on Zulip 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 }

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:11):

yay finish!

view this post on Zulip Floris van Doorn (Oct 07 2020 at 23:12):

docs#exists_or_distrib

view this post on Zulip Yakov Pechersky (Oct 07 2020 at 23:12):

I was surprised finish can't do the split itself

view this post on Zulip Eric Wieser (Oct 07 2020 at 23:12):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:13):

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

view this post on Zulip Eric Wieser (Oct 07 2020 at 23:13):

What spelling didn't work @Yakov Pechersky ?

view this post on Zulip Kevin Lacker (Oct 07 2020 at 23:13):

once I fixed the syntax, library_search found exists_or_distrib

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:14):

X; Y runs Y on every goal produced by X

view this post on Zulip Kevin Lacker (Oct 07 2020 at 23:15):

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

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:15):

almost!

view this post on Zulip 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

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:15):

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

view this post on Zulip Kevin Lacker (Oct 07 2020 at 23:16):

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

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:20):

math is hard :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 07 2020 at 23:29):

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

view this post on Zulip Eric Wieser (Oct 07 2020 at 23:29):

To fix that rintro

view this post on Zulip Yakov Pechersky (Oct 07 2020 at 23:29):

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

view this post on Zulip Eric Wieser (Oct 07 2020 at 23:30):

Does it work in parentheses?

view this post on Zulip Yakov Pechersky (Oct 07 2020 at 23:31):

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

view this post on Zulip 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