## 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.

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?

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