import MyNat.Definition
namespace MyNat
open MyNat

Function world.

Level 9: a big maze.

In Proposition World you will see a variant of this example which can be solved by a tactic. It would be an interesting project to make a tactic which could automatically solve this sort of level in Lean.

You can of course work both forwards and backwards, or you could crack and draw a picture.

Definition

Given a bunch of functions, we can define another one.

example: (A B C D E F G H I J K L : Type) →
  (A → B) →
    (B → E) →
      (E → D) →
        (D → A) →
          (E → F) →
            (F → C) → (B → C) → (F → G) → (G → J) → (I → J) → (J → I) → (I → H) → (E → H) → (H → K) → (I → L) → A → L
example (
A: Type
A 
B: Type
B 
C: Type
C 
D: Type
D 
E: Type
E 
F: Type
F 
G: Type
G 
H: Type
H 
I: Type
I 
J: Type
J 
K: Type
K 
L: Type
L : 
Type: Type 1
Type)
(
f1: A → B
f1 : 
A: Type
A → 
B: Type
B) (
f2: B → E
f2 : 
B: Type
B → 
E: Type
E) (
f3: E → D
f3
Warning: unused variable `f3` [linter.unusedVariables] : 
E: Type
E → 
D: Type
D) (
f4: D → A
f4
Warning: unused variable `f4` [linter.unusedVariables] : 
D: Type
D → 
A: Type
A) (
f5: E → F
f5 : 
E: Type
E → 
F: Type
F)
(
f6: F → C
f6
Warning: unused variable `f6` [linter.unusedVariables] : 
F: Type
F → 
C: Type
C) (
f7: B → C
f7
Warning: unused variable `f7` [linter.unusedVariables] : 
B: Type
B → 
C: Type
C) (
f8: F → G
f8 : 
F: Type
F → 
G: Type
G) (
f9: G → J
f9 : 
G: Type
G → 
J: Type
J) (
f10: I → J
f10
Warning: unused variable `f10` [linter.unusedVariables] : 
I: Type
I → 
J: Type
J)
(
f11: J → I
f11 : 
J: Type
J → 
I: Type
I) (
f12: I → H
f12
Warning: unused variable `f12` [linter.unusedVariables] : 
I: Type
I → 
H: Type
H) (
f13: E → H
f13
Warning: unused variable `f13` [linter.unusedVariables] : 
E: Type
E → 
H: Type
H) (
f14: H → K
f14
Warning: unused variable `f14` [linter.unusedVariables] : 
H: Type
H → 
K: Type
K) (
f15: I → L
f15 : 
I: Type
I → 
L: Type
L)
 : 
A: Type
A → 
L: Type
L := by
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
A → L
  intro 
a: A
a
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
a: A
L
  apply 
f15: I → L
f15
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
a: A
I
  apply 
f11: J → I
f11
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
a: A
J
  apply 
f9: G → J
f9
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
a: A
G
  apply 
f8: F → G
f8
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
a: A
F
  apply 
f5: E → F
f5
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
a: A
E
  apply 
f2: B → E
f2
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
a: A
B
  apply 
f1: A → B
f1
A, B, C, D, E, F, G, H, I, J, K, L: Type
f1: A → B
f2: B → E
f3: E → D
f4: D → A
f5: E → F
f6: F → C
f7: B → C
f8: F → G
f9: G → J
f10: I → J
f11: J → I
f12: I → H
f13: E → H
f14: H → K
f15: I → L
a: A
A
  assumption
Goals accomplished! 🐙

Here we finish this proof with a new tactic assumption instead of exact a. The assumption tactic tries to solve the goal using a hypothesis of compatible type. Since we have the hypothesis named a it finds it and completes the proof.

That's the end of Function World! Next it's Proposition World, and the tactics you've learnt in Function World are enough to solve all nine levels! In fact, the levels in Proposition World might look strangely familiar...