import MyNat.Definition
namespace MyNat
open MyNat

Proposition world.

Level 4: apply.

Let's do the same level again a different way:

We are given a proof p of P and our goal is to find a proof of U, or in other words to find a path through the maze that links P to U. In level 3 we solved this by using haves to move forward, from P to Q to T to U. Using the apply tactic we can instead construct the path backwards, moving from U to T to Q to P.

Our goal is to prove U. But l:T ⟹ U is an implication which we are assuming, so it would suffice to prove T. Tell Lean this by starting the proof below with

apply l,

and notice that our assumptions don't change but the goal changes from ⊢ U to ⊢ T.

Keep applying implications until your goal is P, and try not to get lost! Now solve this goal with exact p. Note: you will need to learn the difference between exact p (which works) and exact P (which doesn't, because P is not a proof of P).

Lemma : maze₂

We can solve a maze.

lemma 
maze₂: ∀ (P Q R S T U : Prop), P → (P → Q) → (Q → R) → (Q → T) → (S → T) → (T → U) → U
maze₂ (
P: Prop
P 
Q: Prop
Q 
R: Prop
R 
S: Prop
S 
T: Prop
T 
U: Prop
U: 
Prop: Type
Prop)
(
p: P
p : 
P: Prop
P)
(
h: P → Q
h : 
P: Prop
P → 
Q: Prop
Q)
(
i: Q → R
i
Warning: unused variable `i` [linter.unusedVariables] : 
Q: Prop
Q → 
R: Prop
R)
(
j: Q → T
j : 
Q: Prop
Q → 
T: Prop
T)
(
k: S → T
k
Warning: unused variable `k` [linter.unusedVariables] : 
S: Prop
S → 
T: Prop
T)
(
l: T → U
l : 
T: Prop
T → 
U: Prop
U)
: 
U: Prop
U := by
P, Q, R, S, T, U: Prop
p: P
h: P → Q
i: Q → R
j: Q → T
k: S → T
l: T → U
U
  apply 
l: T → U
l
P, Q, R, S, T, U: Prop
p: P
h: P → Q
i: Q → R
j: Q → T
k: S → T
l: T → U
T
  apply 
j: Q → T
j
P, Q, R, S, T, U: Prop
p: P
h: P → Q
i: Q → R
j: Q → T
k: S → T
l: T → U
Q
  apply 
h: P → Q
h
P, Q, R, S, T, U: Prop
p: P
h: P → Q
i: Q → R
j: Q → T
k: S → T
l: T → U
P
  exact 
p: P
p
Goals accomplished! 🐙

Next up Level 5