import MyNat.Definition
namespace MyNat
open MyNat

Proposition world.

Level 9: a big maze.

Hint: Lean's "congruence closure" tactic cc is good at mazes. You might want to try it now. Perhaps I should have mentioned it earlier.

Lemma

There is a way through the following maze.

example: ∀ (A B C D E F G H I J K L : Prop),
  (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: Prop
A 
B: Prop
B 
C: Prop
C 
D: Prop
D 
E: Prop
E 
F: Prop
F 
G: Prop
G 
H: Prop
H 
I: Prop
I 
J: Prop
J 
K: Prop
K 
L: Prop
L : 
Prop: Type
Prop)
(
f1: A → B
f1 : 
A: Prop
A → 
B: Prop
B) (
f2: B → E
f2 : 
B: Prop
B → 
E: Prop
E) (
f3: E → D
f3
Warning: unused variable `f3` [linter.unusedVariables] : 
E: Prop
E → 
D: Prop
D) (
f4: D → A
f4
Warning: unused variable `f4` [linter.unusedVariables] : 
D: Prop
D → 
A: Prop
A) (
f5: E → F
f5 : 
E: Prop
E → 
F: Prop
F)
(
f6: F → C
f6
Warning: unused variable `f6` [linter.unusedVariables] : 
F: Prop
F → 
C: Prop
C) (
f7: B → C
f7
Warning: unused variable `f7` [linter.unusedVariables] : 
B: Prop
B → 
C: Prop
C) (
f8: F → G
f8 : 
F: Prop
F → 
G: Prop
G) (
f9: G → J
f9 : 
G: Prop
G → 
J: Prop
J) (
f10: I → J
f10
Warning: unused variable `f10` [linter.unusedVariables] : 
I: Prop
I → 
J: Prop
J)
(
f11: J → I
f11 : 
J: Prop
J → 
I: Prop
I) (
f12: I → H
f12
Warning: unused variable `f12` [linter.unusedVariables] : 
I: Prop
I → 
H: Prop
H) (
f13: E → H
f13
Warning: unused variable `f13` [linter.unusedVariables] : 
E: Prop
E → 
H: Prop
H) (
f14: H → K
f14
Warning: unused variable `f14` [linter.unusedVariables] : 
H: Prop
H → 
K: Prop
K) (
f15: I → L
f15 : 
I: Prop
I → 
L: Prop
L)
 : 
A: Prop
A → 
L: Prop
L := by
A, B, C, D, E, F, G, H, I, J, K, L: Prop
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: Prop
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: Prop
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: Prop
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: Prop
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: Prop
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: Prop
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: Prop
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: Prop
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! 🐙

-- BUGBUG: NNG uses cc which is missing in lean4...

Now move onto advanced proposition world, where you will see how to prove goals such as P ∧ Q (P and Q), P ∨ Q (P or Q), P ↔ Q (P ⟺ Q). You will need to learn five more tactics: split, cases, left, right, and exfalso, but they are all straightforward, and furthermore they are essentially the last tactics you need to learn in order to complete all the levels of this tutorial, including all the 17 levels of Inequality World.

Next up advanced proposition world.