# 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: May 14 2021 at 04:22 UTC