import MyNat.Definition
namespace MyNat
open MyNat

Function World

Level 4: the apply tactic.

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

We are given p ∈ P and our goal is to find an element 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 construct an element of the set U . But l:T → U is a function, so it would suffice to construct an element of 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 functions 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 an element of P ).

Definition

Given an element of P we can define an element of U .

example: (P Q R S T U : Type) → P → (P → Q) → (Q → R) → (Q → T) → (S → T) → (T → U) → U
example (
P: Type
P 
Q: Type
Q 
R: Type
R 
S: Type
S 
T: Type
T 
U: Type
U: 
Type: Type 1
Type)
(
p: P
p : 
P: Type
P)
(
h: P → Q
h : 
P: Type
P → 
Q: Type
Q)
(
i: Q → R
i
Warning: unused variable `i` [linter.unusedVariables] : 
Q: Type
Q → 
R: Type
R)
(
j: Q → T
j : 
Q: Type
Q → 
T: Type
T)
(
k: S → T
k
Warning: unused variable `k` [linter.unusedVariables] : 
S: Type
S → 
T: Type
T)
(
l: T → U
l : 
T: Type
T → 
U: Type
U)
: 
U: Type
U := by
P, Q, R, S, T, U: Type
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: Type
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: Type
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: Type
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