Lumenary.FollowingInstructions

Formal library

• PosstructureDefinitionNo axioms

  /-- A square on a grid map: `x` squares to the right and `y` squares up from the start. -/
  structure Pos where
    x : Int
    y : Int
    deriving DecidableEq, Repr

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• ArrowstructureDefinitionNo axioms

  /-- The four arrow cards. -/
  inductive Arrow where
    | up | down | left | right
    deriving DecidableEq, Repr

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• stepdefDefinitionNo axioms

  /-- What one arrow card does: move one square in its direction. -/
  def step : Arrow → Pos → Pos
    | .up, p => ⟨p.x, p.y + 1⟩
    | .down, p => ⟨p.x, p.y - 1⟩
    | .left, p => ⟨p.x - 1, p.y⟩
    | .right, p => ⟨p.x + 1, p.y⟩

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• rundefDefinitionNo axioms

  /-- Follow a program of arrow cards from the square `p`: do the first card, then follow the
  rest of the program from where you are. -/
  def run : List Arrow → Pos → Pos
    | [], p => p
    | a :: prog, p => run prog (step a p)

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• startdefDefinitionNo axioms

  /-- The start square. -/
  def start : Pos := ⟨0, 0⟩

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• run_appendtheoremProved here from basic factsNo axioms

  /-- Following program `p` and then program `q` is the same as following the joined program
  `p ++ q`. Proof by induction on `p`. -/
  theorem run_append (p q : List Arrow) (s : Pos) : run (p ++ q) s = run q (run p s) := by
    induction p generalizing s with
    | nil => rfl
    | cons a p ih => exact ih (step a s)

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• to_the_treetheoremProved here from basic factsNo axioms

  /-- The program `→ → ↑` takes you from the start to the square 2 across and 1 up. -/
  theorem to_the_tree : run [.right, .right, .up] start = ⟨2, 1⟩ := rfl

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• two_programstheoremProved here from basic factsNo axioms

  /-- There is more than one correct program: `↑ → →` and `→ ↑ →` are different programs that
  end on the same square as `→ → ↑`. -/
  theorem two_programs :
      run [.up, .right, .right] start = ⟨2, 1⟩ ∧ run [.right, .up, .right] start = ⟨2, 1⟩ ∧
      [Arrow.up, .right, .right] ≠ [.right, .up, .right] := by
    decide

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• taxidefDefinitionNo axioms

  /-- The "across plus up" distance between two squares: how many squares across, plus how many
  squares up or down. (Grown-ups call it the taxicab distance.) -/
  def taxi (p q : Pos) : Nat := (q.x - p.x).natAbs + (q.y - p.y).natAbs

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• taxi_steptheoremProved here from basic factspropext, Quot.sound

  /-- One arrow card changes the "across plus up" distance from a fixed square by at most 1. -/
  theorem taxi_step (s p : Pos) (a : Arrow) : taxi s (step a p) ≤ taxi s p + 1 := by
    cases a <;> simp only [taxi, step] <;> omega

  Axioms used: propext, Quot.soundformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• taxi_le_lengththeoremProved here from basic factspropext, Quot.sound

  /-- **No program is shorter than the distance.** Every arrow program that goes from `s` to a
  square uses at least as many cards as the "across plus up" distance to that square: each card
  moves you at most one square closer. Proof by induction on the program. -/
  theorem taxi_le_length (prog : List Arrow) (s : Pos) : taxi s (run prog s) ≤ prog.length := by
    -- Strengthen: start the program at any square `p`, measuring from `s`.
    suffices h : ∀ p : Pos, taxi s (run prog p) ≤ taxi s p + prog.length by
      have := h s
      simpa [taxi] using this
    induction prog with
    | nil => intro p; simp [run]
    | cons a prog ih =>
      intro p
      have h1 := ih (step a p)
      have h2 := taxi_step s p a
      simp only [run, List.length_cons]
      omega

  Axioms used: propext, Quot.soundformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• straight_routetheoremProved here from basic factspropext, Quot.sound

  /-- **A shortest program always exists**: to reach the square `a` across and `b` up, use `a`
  right arrows and then `b` up arrows — exactly `a + b` cards, the distance. -/
  theorem straight_route (a b : Nat) :
      run (List.replicate a .right ++ List.replicate b .up) start = ⟨a, b⟩ := by
    rw [run_append]
    -- Each block of identical arrows moves you that many squares.
    have hr : ∀ (n : Nat) (p : Pos), run (List.replicate n .right) p = ⟨p.x + n, p.y⟩ := by
      intro n
      induction n with
      | zero => intro p; simp [run]
      | succ n ih =>
        intro p
        simp only [List.replicate, run, step, ih]
        congr 1
        omega
    have hu : ∀ (n : Nat) (p : Pos), run (List.replicate n .up) p = ⟨p.x, p.y + n⟩ := by
      intro n
      induction n with
      | zero => intro p; simp [run]
      | succ n ih =>
        intro p
        simp only [List.replicate, run, step, ih]
        congr 1
        omega
    rw [hr, hu]
    simp [start]

  Axioms used: propext, Quot.soundformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• HeadingstructureDefinitionNo axioms

  /-- Which way the robot is facing. -/
  inductive Heading where
    | north | east | south | west
    deriving DecidableEq, Repr

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• RobotstructureDefinitionNo axioms

  /-- A floor robot: where it is, and which way it faces. -/
  structure Robot where
    pos : Pos
    facing : Heading
    deriving DecidableEq, Repr

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• CmdstructureDefinitionNo axioms

  /-- The robot's three buttons. Turning happens on the spot: the robot stays on its square. -/
  inductive Cmd where
    | forward | turnLeft | turnRight
    deriving DecidableEq, Repr

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• execdefDefinitionNo axioms

  /-- What one button does to the robot. -/
  def exec : Cmd → Robot → Robot
    | .forward, ⟨p, .north⟩ => ⟨⟨p.x, p.y + 1⟩, .north⟩
    | .forward, ⟨p, .east⟩ => ⟨⟨p.x + 1, p.y⟩, .east⟩
    | .forward, ⟨p, .south⟩ => ⟨⟨p.x, p.y - 1⟩, .south⟩
    | .forward, ⟨p, .west⟩ => ⟨⟨p.x - 1, p.y⟩, .west⟩
    | .turnLeft, ⟨p, .north⟩ => ⟨p, .west⟩
    | .turnLeft, ⟨p, .west⟩ => ⟨p, .south⟩
    | .turnLeft, ⟨p, .south⟩ => ⟨p, .east⟩
    | .turnLeft, ⟨p, .east⟩ => ⟨p, .north⟩
    | .turnRight, ⟨p, .north⟩ => ⟨p, .east⟩
    | .turnRight, ⟨p, .east⟩ => ⟨p, .south⟩
    | .turnRight, ⟨p, .south⟩ => ⟨p, .west⟩
    | .turnRight, ⟨p, .west⟩ => ⟨p, .north⟩

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• runRobotdefDefinitionNo axioms

  /-- Press the buttons of a robot program one after another. -/
  def runRobot : List Cmd → Robot → Robot
    | [], r => r
    | c :: prog, r => runRobot prog (exec c r)

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• homedefDefinitionNo axioms

  /-- The robot starts at the start square, facing north (up the page). -/
  def home : Robot := ⟨start, .north⟩

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• order_matterstheoremProved here from basic factsNo axioms

  /-- **The order of the steps matters.** "Forward, then turn right" leaves the robot one square
  up, facing east; "turn right, then forward" leaves it one square to the right. -/
  theorem order_matters :
      runRobot [.forward, .turnRight] home = ⟨⟨0, 1⟩, .east⟩ ∧
      runRobot [.turnRight, .forward] home = ⟨⟨1, 0⟩, .east⟩ := by
    decide

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• left_then_righttheoremProved here from basic factsNo axioms

  /-- "Turn left, then turn right" does nothing at all, wherever the robot is and whichever way
  it faces. (Check all four headings.) -/
  theorem left_then_right (r : Robot) : exec .turnRight (exec .turnLeft r) = r := by
    obtain ⟨p, h⟩ := r
    cases h <;> rfl

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• four_leftstheoremProved here from basic factsNo axioms

  /-- Four left turns bring the robot back to facing the way it started. -/
  theorem four_lefts (r : Robot) : runRobot [.turnLeft, .turnLeft, .turnLeft, .turnLeft] r = r := by
    obtain ⟨p, h⟩ := r
    cases h <;> rfl

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor

• debugtheoremProved here from basic factsNo axioms

  /-- **Finding and fixing a bug.** The target is 2 squares up and 1 square to the right. The
  program "forward, forward, turn left, forward" goes the wrong way (left instead of right);
  changing the one wrong instruction to "turn right" fixes it. -/
  theorem debug :
      (runRobot [.forward, .forward, .turnLeft, .forward] home).pos = ⟨-1, 2⟩ ∧
      (runRobot [.forward, .forward, .turnRight, .forward] home).pos = ⟨1, 2⟩ := by
    decide

  Axioms used: No axiomsformal/Lumenary/FollowingInstructions.leanTry it in the Lean web editor