Correct-by-construction solutions to the Wolf-Goat-Cabbage game

adts.lean

namespace ADTs

/-
  In the game we have two banks of a river: left and right,
  and four characters: a wolf, a goat, a cabbage, and a farmer.
  The farmer prevents abybody from eathing anything, otherweise
  the wolf eats the goat, or the goat eats the cabbage.
  The game starts with all the characters on the left bank and
  the goal is to move everyone to the right bank safe and sound.
  The farmer can carry a single other character at a time
  to the opposite bank in a boat.
-/

/-
  We will encode legit states of both banks as distinct
  (Algebraic) Data Types, and moves from one state to another
  as _constructors_ of said Data Types.

  In this way we implement the idea of "making invalid states
  unrepresentable" — we won't be able even _name_ invalid states
  (no types encoding invalid states), much less construct them.
-/

mutual

  -- Left bank: Wolf, Goat, Cabbage, Farmer
  -- Right bank: empty
  -- This is the initial state of the game
  -- (and we can always reset the game to this state
  -- according to our encoding)
  inductive WGCF_empty
    | initial
    | take_goat_back : WC_GF -> WGCF_empty

  inductive WC_GF
    | take_goat_forward : WGCF_empty -> WC_GF
    | go_forward : WCF_G -> WC_GF -- travelling across the river empty
                                  -- makes little sense, but for the sake
                                  -- of completeness :)

  inductive WCF_G
    | go_back           : WC_GF -> WCF_G
    | take_cabbage_back : W_GCF -> WCF_G
    | take_wolf_back    : C_WGF -> WCF_G

  inductive W_GCF
    | take_cabbage_forward : WCF_G -> W_GCF

  inductive C_WGF
    | take_wolf_forward : WCF_G -> C_WGF

  inductive WGF_C
    | take_goat_back : W_GCF -> WGF_C

  inductive GCF_W
    | take_goat_back : C_WGF -> GCF_W

  inductive G_WCF
    | take_wolf_forward    : WGF_C -> G_WCF
    | take_cabbage_forward : GCF_W -> G_WCF

  inductive GF_WC
    | go_back : G_WCF -> GF_WC

  inductive empty_WGCF
    | take_goat_forward : GF_WC -> empty_WGCF

end

def solution1 := empty_WGCF.take_goat_forward $
                 GF_WC.go_back $
                 G_WCF.take_wolf_forward $
                 WGF_C.take_goat_back $
                 W_GCF.take_cabbage_forward $
                 WCF_G.go_back $
                 WC_GF.take_goat_forward $
                 WGCF_empty.initial

-- the same solution constructed with `apply` tactic
example : empty_WGCF := by
  apply empty_WGCF.take_goat_forward
  apply GF_WC.go_back
  apply G_WCF.take_wolf_forward
  apply WGF_C.take_goat_back
  apply W_GCF.take_cabbage_forward
  apply WCF_G.go_back
  apply WC_GF.take_goat_forward
  apply WGCF_empty.initial