Zulip Chat Archive

Stream: new members

Topic: Decomposing hypotheses

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?

Reid Barton (Jul 25 2018 at 16:51):

tauto gets the job done in this case

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 }

Ken Roe (Jul 25 2018 at 16:58):

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

Reid Barton (Jul 25 2018 at 16:59):

It's in mathlib

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?

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:

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

Patrick Massot (Jul 25 2018 at 18:16):

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

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.

Simon Hudon (Jul 25 2018 at 18:36):

Haha! I'm pretty merciful though

Simon Hudon (Jul 25 2018 at 18:37):

Have you tried solve_by_elim?

Patrick Massot (Jul 25 2018 at 18:38):

It doesn't work

Patrick Massot (Jul 25 2018 at 18:42):

Btw Simon, how was your tauto lecture?

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

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

Patrick Massot (Jul 25 2018 at 18:47):

Did you prepare a heavily commented version of the source?

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

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: Dec 20 2023 at 11:08 UTC