import MyNat.Definition
namespace MyNat
open MyNat

Advanced proposition world.

Level 5: iff_trans easter eggs.

Let's try iff_trans again. Try proving it in other ways.

A trick.

Instead of using cases on h : P ↔ Q you can just access the proofs of P → Q and Q → P directly with h.mp and h.mpr.

Lemma

If P, Q and R are true/false statements, then P ↔ Q and Q ↔ R together imply P ↔ R.

lemma 
iff_trans₂: ∀ (P Q R : Prop), (P ↔ Q) → (Q ↔ R) → (P ↔ R)
iff_trans₂ (
P: Prop
P 
Q: Prop
Q 
R: Prop
R : 
Prop: Type
Prop) : (
P: Prop
P ↔ 
Q: Prop
Q) → (
Q: Prop
Q ↔ 
R: Prop
R) → (
P: Prop
P ↔ 
R: Prop
R) := by
P, Q, R: Prop
(P ↔ Q) → (Q ↔ R) → (P ↔ R)
  intros 
hpq: P ↔ Q
hpq 
hqr: Q ↔ R
hqr
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
P ↔ R
  constructor
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mp
P → R
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mpr
R → P
  intro 
p: P
p
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
p: P
mp
R
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mpr
R → P
  apply 
hqr: Q ↔ R
hqr.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
p: P
mp
Q
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mpr
R → P
  apply 
hpq: P ↔ Q
hpq.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
p: P
mp
P
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mpr
R → P
  assumption
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
mpr
R → P
  intro 
r: R
r
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
r: R
mpr
P
  apply 
hpq: P ↔ Q
hpq.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
r: R
mpr
Q
  apply 
hqr: Q ↔ R
hqr.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
r: R
mpr
R
  assumption
Goals accomplished! 🐙

Another trick

Instead of using cases on h : P ↔ Q, you can just rw [h], and this will change all Ps to Qs in the goal. You can use this to create a much shorter proof. Note that this is an argument for not running the cases tactic on an iff statement; you cannot rewrite one-way implications, but you can rewrite two-way implications.

lemma 
iff_trans₃: ∀ (P Q R : Prop), (P ↔ Q) → (Q ↔ R) → (P ↔ R)
iff_trans₃ (
P: Prop
P 
Q: Prop
Q 
R: Prop
R : 
Prop: Type
Prop) : (
P: Prop
P ↔ 
Q: Prop
Q) → (
Q: Prop
Q ↔ 
R: Prop
R) → (
P: Prop
P ↔ 
R: Prop
R) := by
P, Q, R: Prop
(P ↔ Q) → (Q ↔ R) → (P ↔ R)
  intros 
hpq: P ↔ Q
hpq 
hqr: Q ↔ R
hqr
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
P ↔ R
  rw [
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
P ↔ R
hpq: P ↔ Q
hpq
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
Q ↔ R]
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
Q ↔ R
  rw [
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
Q ↔ R
hqr: Q ↔ R
hqr
P, Q, R: Prop
hpq: P ↔ Q
hqr: Q ↔ R
R ↔ R]
Goals accomplished! 🐙

Next up Level 6