Zulip Chat Archive

Stream: new members

Topic: Decomposing hypotheses


view this post on Zulip Ken Roe (Jul 25 2018 at 16:46):

theorem test_split { P : Prop } { Q : Prop } { R : Prop } { S : Prop } :
    (P  (Q  R))  (Q  S)  (R  S)  (P  S) :=
begin
    intros, sorry
end

Is there a nice way to decompose the hypotheses to prove the above theorem? What should "sorry" be replaced with?

view this post on Zulip Reid Barton (Jul 25 2018 at 16:51):

tauto gets the job done in this case

view this post on Zulip Reid Barton (Jul 25 2018 at 16:52):

Manually, you could use cases, for example

    cases pqr with p qr,
    refine p, _⟩,
    cases qr with q r,
    { exact qs q },
    { exact rs r }

view this post on Zulip Ken Roe (Jul 25 2018 at 16:58):

Where can I find tauto? It is not in the standard libraries.

view this post on Zulip Reid Barton (Jul 25 2018 at 16:59):

It's in mathlib

view this post on Zulip Ken Roe (Jul 25 2018 at 18:10):

Now for a more complex example,

theorem test_split { P :   Prop } { Q :   Prop } { R :   Prop } { S :   Prop } :
    ( x, P x  (Q x  R x))  ( x, Q x  S x)  ( x, R x  S x)  ( x, P x  S x) :=
begin
    intros, sorry
end

After the intros, is there a nice way to decompose these hypotheses?

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:14):

I'm not sure what you are looking for, but here is a short proof using tauto:

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:14):

theorem test_split { P :   Prop } { Q :   Prop } { R :   Prop } { S :   Prop } :
    ( x, P x  (Q x  R x))  ( x, Q x  S x)  ( x, R x  S x)  ( x, P x  S x) :=
begin
    intros h h' h'' x,
    specialize h x,
    specialize h' x,
    specialize h'' x,
    tauto
end

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:16):

I'm not sure we currently have any tactic that can guess the specialize steps.

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:16):

If you really really want one, then the standard procedure is to hope Simon will pity you.

view this post on Zulip Simon Hudon (Jul 25 2018 at 18:36):

Haha! I'm pretty merciful though

view this post on Zulip Simon Hudon (Jul 25 2018 at 18:37):

Have you tried solve_by_elim?

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:38):

It doesn't work

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:42):

Btw Simon, how was your tauto lecture?

view this post on Zulip Simon Hudon (Jul 25 2018 at 18:45):

You can shrink the proof down to:

theorem test_split { P :   Prop } { Q :   Prop } { R :   Prop } { S :   Prop } :
    ( x, P x  (Q x  R x))  ( x, Q x  S x)  ( x, R x  S x)  ( x, P x  S x) :=
begin
    intros h h' h'' x,
    specialize h x,
    split; tauto,
end

view this post on Zulip Simon Hudon (Jul 25 2018 at 18:46):

I'm giving it tonight and I decided to talk about pi_instances after all. 5 minutes is so incredibly short :D

view this post on Zulip Patrick Massot (Jul 25 2018 at 18:47):

Did you prepare a heavily commented version of the source?

view this post on Zulip Simon Hudon (Jul 25 2018 at 18:53):

What I decided to do is write an instance for group and show how automation shrinks it. And then I mention that refine_struct is written in Lean

view this post on Zulip Mario Carneiro (Jul 26 2018 at 01:19):

rintro is a really nice way of doing all that

theorem test_split {P Q R S : Prop} :
  P ∧ (Q ∨ R) → (Q → S) → (R → S) → P ∧ S :=
begin
  rintro ⟨hp, hq | hr⟩ qs rs,
  { exact ⟨hp, qs hq⟩ },
  { exact ⟨hp, rs hr⟩ }
end

Last updated: May 14 2021 at 04:22 UTC