De wolf, geit en kool puzzel

wolf_geit_kool.lean

import data.list.basic

/-
Om het spel te spelen moet u helemaal naar beneden scrollen.
Daar vindt u meer uitleg.

De volgende code is een gedeeltelijke vertaling van code
die geschreven is door Mario Carneiro.
-/

namespace list

instance decidable_chain₂ {α R} [decidable_rel R] (a : α) (l : list α) : decidable (chain R a l) :=
begin
  induction l generalizing a,
  exact is_true chain.nil,
  exactI decidable_of_iff' _ chain_cons
end

instance decidable_chain'₂ {α R} [decidable_rel R] (l : list α) : decidable (chain' R l) :=
by cases l; dunfold chain'; apply_instance

end list

namespace WGC

structure state := (wolf geit kool boer : bool)

def valid (s : state) :=
¬ (s.wolf = s.geit ∧ s.boer ≠ s.wolf) ∧
¬ (s.geit = s.kool ∧ s.boer ≠ s.geit)

instance : decidable_pred valid | s := by unfold valid; apply_instance

def step (s₁ s₂ : state) :=
s₁.boer ≠ s₂.boer ∧
((s₁.wolf = s₂.wolf ∧ s₁.geit = s₂.geit ∧ s₁.kool = s₂.kool) ∨
 (s₁.wolf = s₂.wolf ∧ s₁.geit = s₂.geit ∧ s₁.kool = s₁.boer ∧ s₂.kool = s₂.boer) ∨
 (s₁.wolf = s₂.wolf ∧ s₁.geit = s₁.boer ∧ s₂.geit = s₂.boer ∧ s₁.kool = s₂.kool) ∨
 (s₁.wolf = s₁.boer ∧ s₂.wolf = s₂.boer ∧ s₁.kool = s₂.kool ∧ s₁.geit = s₂.geit))

instance : decidable_rel step | s₁ s₂ := by unfold step; apply_instance

def positie (s : state) :=
{p : list state // p.head' = some s ∧
  p.last' = some ⟨tt, tt, tt, tt⟩ ∧
  list.chain' step p ∧
  ∀ s' ∈ p, valid s'}

def finish : positie ⟨tt, tt, tt, tt⟩ :=
⟨[⟨_, _, _, _⟩], ⟨rfl, rfl, dec_trivial, dec_trivial⟩⟩

def positie.step {s₁} (s₂)
  (H₁ : valid s₁) (H₂ : step s₁ s₂)
  (p : positie s₂) : positie s₁ :=
⟨s₁ :: p.1, begin
  rcases p.2 with ⟨h₁, h₂, h₃, h₄⟩,
  cases p.1 with a l; cases h₁,
  exact ⟨rfl, h₂, list.chain.cons H₂ h₃,
    list.forall_mem_cons.2 ⟨H₁, h₄⟩⟩
end⟩

section
open tactic tactic.interactive interactive lean.parser

meta def negate : expr → tactic expr
| `(tt) := return `(ff)
| `(ff) := return `(tt)
| _ := fail "invalid goal"

meta def vervoer (n : parse ident) : tactic unit := do
  `(positie ⟨%%w, %%g, %%c, %%f⟩) ← target | fail "invalid goal",
  f' ← negate f,
  (w', g', c') ← match n with
  | `wolf := do
    when (¬ w =ₐ f) $ fail "Dat kan niet, de wolf is aan de overkant.",
    w' ← negate w,
    when (g =ₐ c ∧ ¬ g =ₐ f') $ fail "Dat kan niet, de geit zou de kool opeten.",
    return (w', g, c)
  | `geit := do
    when (¬ g =ₐ f) $ fail "Dat kan niet, de goat is aan de overkant.",
    g' ← negate g,
    return (w, g', c)
  | `kool := do
    when (¬ c =ₐ f) $ fail "Dat kan niet, de kool is aan de overkant.",
    c' ← negate c,
    when (w =ₐ g ∧ ¬ g =ₐ f') $ fail "Dat kan niet, de wolf zou de geit opeten.",
    return (w, g, c')
  | `niets := do
    when (g =ₐ c ∧ ¬ g =ₐ f') $ fail "Dat kan niet, de geit zou de kool opeten.",
    when (w =ₐ g ∧ ¬ g =ₐ f') $ fail "Dat kan niet, de wolf zou de geit opeten.",
    return (w, g, c)
  | _ := fail "ongeldige optie"
  end,
  tactic.refine ``(positie.step
    ⟨%%w', %%g', %%c', %%f'⟩ dec_trivial dec_trivial _),
  tactic.try (exact `(finish))

run_cmd add_interactive [``vervoer]

end

notation `rechteroever` := tt
notation `linkeroever`  := ff

/-
Vanaf hier begint het spel.

Plaats uw cursor tussen de woorden "begin" en "end". U ziet dan in het rechterscherm tekst verschijnen:

De boer, wolf, geit en kool staan allemaal op de linkeroever.

Er is 1 commando: vervoer.
Dit commando kent 4 opties: wolf, geit, kool en niets.

U kunt dus "vervoer niets," of "vervoer kool," schrijven.
Als u de cursor achter de "," plaats,
ziet u dat de tekst in het rechterscherm is veranderd.
De boer staat nu op de rechteroever.

Als u de puzzel hebt opgelost, dan verschijnt
de enigszins deprimerende tekst "no goals".
Dit betekent dat u alles goed hebt gedaan.

Veel plezier!
-/

theorem oplossing : positie ⟨linkeroever, linkeroever, linkeroever, linkeroever⟩ :=
begin
  -- Plaat uw cursor hier op de volgende regel.
  
end

end WGC