TPL, Ex 4.6.2 b

Stream: new members

[Claus-Peter Becke]

I stick at the following point:

example : (∀ x, p x ∨ s) ↔ (∀ x, p x) ∨ s :=
begin
    split,
    intro h1,
    left,
    intro x,
    have h2 := h1 x,
    cases h2 with h3 h4,
    exact h3,
end

The result which had been generated using the tactics above is the following one:

case or.inr
α: Type u_1
p: α → Prop
s: Prop
h1: ∀ (x : α), p x ∨ s
x: α
h4: s
⊢ p x
α: Type u_1
p: α → Prop
s: Prop
⊢ (∀ (x : α), p x) ∨ s → ∀ (x : α), p x ∨ s

I don't see any way to prove p x. Maybe it had been the completely wrong path I chose? Maybe there are any further tactics which could help to prove the goal?

[Mario Carneiro]

The theorem requires classical logic. If you choose either left or right on line 3 the goal becomes unprovable

[Mario Carneiro]

try case analysis on s

[Ruben Van de Velde]

Fortunately it isn't false - proof in https://gist.github.com/Ruben-VandeVelde/89dd1e210dd3ff14056062eb35da86ec if you don't figure it out :)

[Claus-Peter Becke]

@ Mario Carneiro
Unfortunately I didn't find a hint in chapter 3.5. about classical logic which I could apply to solve this problem. There was an example I proved using the push_neg and by_cases-tactics among others which worked without any problems. And I don't know which additional possibilities I achieve using classical logic.

[Mario Carneiro]

The basic hint on using classical logic is to use it once you run out of obvious steps and you aren't done yet

[Claus-Peter Becke]

@Ruben Van de Velde
Thank you for this link. I will study carefully. As far as I see now is that I should have used the by_cases-tqactic to get a further assumption.

[Kevin Buzzard]

@Claus-Peter Becke I think that before you start on a Lean proof of this, you should make sure you have a clear understanding of a paper proof. You can't just blindly go forward with steps like left, you need to know what proof you are formalising.

[Claus-Peter Becke]

To choose 'left' wasn't done blindly, I suppose. It was a necessary step
in my opinion because I had to remove the quantifier from the hypothesis
after having introduced x as an arbitrary object. On the other hand I'm
very thankful for this advice and I will keep in my mind and apply it in
further attempts. But please have in mind that I'm a very beginner in
Leanprover and also in mathematics although I tried a few times to
become familiar with mathematical proof-techniques. Unfortunately I
almost failed. Because I'm as interested in mathematical issues as I am
I try it yet and hope to be more successful than in the past. Leanprover
is a fantastic tool. It's the first time for me to experience the
pleasure of writing mathematical proofs after having been introduced
with Daniel Velleman's Proof Designer. Parallel I'm studying his book
"How to prove it" to get a better idea of what it is to think
mathematically.
Claus-Peter