import MyNat.Definition
namespace MyNat
open MyNat

Advanced proposition world.

Level 10: the law of the excluded middle.

We proved earlier that (P → Q) → (¬ Q → ¬ P). The converse, that (¬ Q → ¬ P) → (P → Q) is certainly true, but trying to prove it using what we've learnt so far is impossible (because it is not provable in constructive logic). For example, after

intro h
intro p
repeat rw [not_iff_imp_false] at h

in the below, you are left with

P Q : Prop,
h : (Q → false) → P → false
p : P
⊢ Q

The tools you have are not sufficient to continue. But you can just prove this, and any other basic lemmas of this form like ¬ ¬ P → P, using the by_cases tactic. Here we start with the usual intros to turn the implication into hypotheses h : ¬ Q → ¬ P and p : P which leaves with the goal of ⊢ Q. But how can you prove Q using these hypotheses? You can use this tactic:

by_cases q : Q

This creates two sub-goals pos and neg with the first one assuming Q is true - which can easily satisfy the goal! and the second one assuming Q is false. But how can h: ¬Q → ¬P, p: P, q: ¬Q prove the goal ⊢ Q ? Well if you apply q to the hypothesis h you end up with the conclusion ¬ P, but then you have a contradiction in your hypotheses saying P and ¬ P which the contradiction tactic can take care of.

The contradiction tactic closes the main goal if its hypotheses are "trivially contradictory".

Lemma

If P and Q are true/false statements, then (¬ Q ⟹ ¬ P) ⟹ (P ⟹ Q).

lemma 
contrapositive2: ∀ (P Q : Prop), (¬Q → ¬P) → P → Q
contrapositive2 (
P: Prop
P 
Q: Prop
Q : 
Prop: Type
Prop) : (¬ 
Q: Prop
Q → ¬ 
P: Prop
P) → (
P: Prop
P → 
Q: Prop
Q) := by
P, Q: Prop
(¬Q → ¬P) → P → Q
  intro 
h: ¬Q → ¬P
h
P, Q: Prop
h: ¬Q → ¬P
P → Q
  intro 
p: P
p
P, Q: Prop
h: ¬Q → ¬P
p: P
Q
  by_cases 
q: Q
q : 
Q: Prop
Q
P, Q: Prop
h: ¬Q → ¬P
p: P
q: Q
pos
Q
P, Q: Prop
h: ¬Q → ¬P
p: P
q: ¬Q
neg
Q
  exact 
q: Q
q
P, Q: Prop
h: ¬Q → ¬P
p: P
q: ¬Q
neg
Q
  have 
np: ¬P
np := 
h: ¬Q → ¬P
h 
q: ¬Q
q
P, Q: Prop
h: ¬Q → ¬P
p: P
q: ¬Q
np: ¬P
neg
Q
  contradiction
Goals accomplished! 🐙

OK that's enough logic -- now perhaps it's time to go on to Advanced Addition World!

Pro tip

In fact the tactic tauto! just kills this goal (and many other logic goals) immediately.

Each of these can now be proved using intro, apply, exact and exfalso. Remember though that in these simple logic cases, high-powered logic tactics like tauto! will just prove everything.