Lumenary.ActionsAndUndoing

Formal library

• ActiondefDefinitionNo axioms

  /-- An action on a world of things of type `α`: for each thing, what it becomes. -/
  abbrev Action (α : Type) : Type := α → α

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

• doNothingdefDefinitionNo axioms

  /-- The action of **doing nothing**: every thing stays exactly as it was. -/
  def doNothing {α : Type} : Action α := fun x => x

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

• andThendefDefinitionNo axioms

  /-- Do `a`, and then do `b`. -/
  def andThen {α : Type} (a b : Action α) : Action α := fun x => b (a x)

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

• UndoesdefDefinitionNo axioms

  /-- `u` **undoes** `a` when doing `a` and then `u` puts every thing back as it was. -/
  def Undoes {α : Type} (u a : Action α) : Prop := ∀ x, u (a x) = x

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

• doNothing_andThentheoremProved here from basic factsNo axioms

  /-- Doing nothing and then doing `a` has the same effect as just doing `a`. -/
  theorem doNothing_andThen {α : Type} (a : Action α) : andThen doNothing a = a := rfl

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

• andThen_doNothingtheoremProved here from basic factsNo axioms

  /-- Doing `a` and then doing nothing also has the same effect as just doing `a`. -/
  theorem andThen_doNothing {α : Type} (a : Action α) : andThen a doNothing = a := rfl

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

• andThen_undotheoremProved here from basic factsQuot.sound

  /-- If `u` undoes `a`, then "do `a`, then `u`" is the same action as doing nothing. -/
  theorem andThen_undo {α : Type} {a u : Action α} (h : Undoes u a) : andThen a u = doNothing :=
    funext h

  Axioms used: Quot.soundformal/Lumenary/ActionsAndUndoing.leanTry it in the Lean web editor

• doNothing_undoes_doNothingtheoremProved here from basic factsNo axioms

  /-- Doing nothing is undone by doing nothing. -/
  theorem doNothing_undoes_doNothing {α : Type} : Undoes (doNothing : Action α) doNothing :=
    fun _ => rfl

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

• CardstructureDefinitionNo axioms

  /-- A card lies face up or face down. -/
  inductive Card where
    | faceUp | faceDown
    deriving DecidableEq, Repr

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

• flipdefDefinitionNo axioms

  /-- Flip the card over. -/
  def flip : Action Card
    | .faceUp => .faceDown
    | .faceDown => .faceUp

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

• flip_undoes_fliptheoremProved here from basic factsNo axioms

  /-- Flipping a card is undone by flipping it again. Check both cases. -/
  theorem flip_undoes_flip : Undoes flip flip := by
    intro c
    cases c <;> rfl

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

• ArrowstructureDefinitionNo axioms

  /-- An arrow on a card can point up, right, down or left. -/
  inductive Arrow where
    | up | right | down | left
    deriving DecidableEq, Repr

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

• quarterTurndefDefinitionNo axioms

  /-- Turn the arrow a quarter turn clockwise (the way clock hands go). -/
  def quarterTurn : Action Arrow
    | .up => .right
    | .right => .down
    | .down => .left
    | .left => .up

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

• quarterBackdefDefinitionNo axioms

  /-- Turn the arrow a quarter turn back (anticlockwise). -/
  def quarterBack : Action Arrow
    | .up => .left
    | .left => .down
    | .down => .right
    | .right => .up

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

• quarterBack_undoes_quarterTurntheoremProved here from basic factsNo axioms

  /-- A quarter turn is undone by a quarter turn back. -/
  theorem quarterBack_undoes_quarterTurn : Undoes quarterBack quarterTurn := by
    intro a
    cases a <;> rfl

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

• three_more_turns_undotheoremProved here from basic factsNo axioms

  /-- A quarter turn is *also* undone by three more quarter turns the same way. -/
  theorem three_more_turns_undo :
      Undoes (fun a => quarterTurn (quarterTurn (quarterTurn a))) quarterTurn := by
    intro a
    cases a <;> rfl

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

• quarterTurn_not_undone_by_itselftheoremProved here from basic factsNo axioms

  /-- A quarter turn is **not** undone by doing it again: an arrow pointing up ends up pointing
  down. One counterexample is enough. -/
  theorem quarterTurn_not_undone_by_itself : ¬ Undoes quarterTurn quarterTurn := by
    intro h
    have hup : quarterTurn (quarterTurn Arrow.up) = Arrow.up := h Arrow.up
    -- But two quarter turns take `up` to `down`, and `down ≠ up`.
    exact absurd hup (by decide)

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

• forwarddefDefinitionNo axioms

  /-- Walk `n` steps forward along a path (positions are integers). -/
  def forward (n : Int) : Action Int := fun x => x + n

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

• backdefDefinitionNo axioms

  /-- Walk `n` steps back. -/
  def back (n : Int) : Action Int := fun x => x - n

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

• back_undoes_forwardtheoremApplies a library theorempropext

  /-- "Take 3 steps forward" is undone by "take 3 steps back" — for any number of steps.
  This applies core Lean's `Int.add_sub_cancel`. -/
  theorem back_undoes_forward (n : Int) : Undoes (back n) (forward n) :=
    fun x => Int.add_sub_cancel x n

  Axioms used: propextformal/Lumenary/ActionsAndUndoing.leanTry it in the Lean web editor

• forward_not_undone_by_itselftheoremProved here from basic factspropext, Quot.sound

  /-- Walking forward again does **not** undo walking forward (unless the number of steps is
  `0`): starting from `0`, two walks of `n` steps end at `n + n`, not at `0`. -/
  theorem forward_not_undone_by_itself (n : Int) (hn : n ≠ 0) :
      ¬ Undoes (forward n) (forward n) := by
    intro h
    have h0 : 0 + n + n = 0 := h 0
    omega

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

• cannot_undo_of_same_resulttheoremProved here from basic factsNo axioms

  /-- **Why some actions cannot be undone.** If an action sends two *different* things `x`
  and `y` to the *same* result, then no action can undo it: an undo would have to take that one
  result back to `x` and also back to `y`.
  `x = u (a x) = u (a y) = y`, which contradicts `x ≠ y`. -/
  theorem cannot_undo_of_same_result {α : Type} (a : Action α) {x y : α} (hxy : x ≠ y)
      (h : a x = a y) : ¬ ∃ u, Undoes u a := by
    intro ⟨u, hu⟩
    apply hxy
    calc x = u (a x) := (hu x).symm
      _ = u (a y) := by rw [h]
      _ = y := hu y

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

• BoardstructureDefinitionNo axioms

  /-- A small whiteboard that shows a picture of a cat, a picture of a dog, or nothing. -/
  inductive Board where
    | cat | dog | blank
    deriving DecidableEq, Repr

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

• wipedefDefinitionNo axioms

  /-- Wipe the board clean, whatever was on it. -/
  def wipe : Action Board := fun _ => .blank

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

• wipe_cannot_be_undonetheoremProved here from basic factsNo axioms

  /-- Wiping the board cannot be undone: the cat board and the dog board both become blank,
  so no action can know which picture to bring back. -/
  theorem wipe_cannot_be_undone : ¬ ∃ u, Undoes u wipe :=
    cannot_undo_of_same_result wipe (x := .cat) (y := .dog) (by decide) rfl

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

• EggstructureDefinitionNo axioms

  /-- An egg is whole or cracked. -/
  inductive Egg where
    | whole | cracked
    deriving DecidableEq, Repr

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

• crackdefDefinitionNo axioms

  /-- Crack the egg. (Cracking an egg that is already cracked leaves it cracked.) -/
  def crack : Action Egg := fun _ => .cracked

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

• crack_cannot_be_undonetheoremProved here from basic factsNo axioms

  /-- Cracking an egg cannot be undone, even in our tiny model: a whole egg and a cracked egg
  both end up cracked. -/
  theorem crack_cannot_be_undone : ¬ ∃ u, Undoes u crack :=
    cannot_undo_of_same_result crack (x := .whole) (y := .cracked) (by decide) rfl

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

• addBlockdefDefinitionNo axioms

  /-- Put one more block on a tower (the tower's height is a natural number). -/
  def addBlock : Action Nat := fun n => n + 1

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

• takeBlockdefDefinitionNo axioms

  /-- Take one block off the tower. Taking a block from an empty spot does nothing:
  in Lean, `0 - 1 = 0` for natural numbers. -/
  def takeBlock : Action Nat := fun n => n - 1

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

• takeBlock_undoes_addBlocktheoremApplies a library theorempropext

  /-- Adding a block is undone by taking it away again. This applies core Lean's
  `Nat.add_sub_cancel`. -/
  theorem takeBlock_undoes_addBlock : Undoes takeBlock addBlock :=
    fun n => Nat.add_sub_cancel n 1

  Axioms used: propextformal/Lumenary/ActionsAndUndoing.leanTry it in the Lean web editor

• takeBlock_cannot_be_undonetheoremProved here from basic factsNo axioms

  /-- But "take a block away" cannot be undone in general: a tower of 1 block and an empty
  spot both end up with 0 blocks, so nothing can tell whether to put a block back. -/
  theorem takeBlock_cannot_be_undone : ¬ ∃ u, Undoes u takeBlock :=
    cannot_undo_of_same_result takeBlock (x := 1) (y := 0) (by decide) rfl

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