Lean code for fleet scenarios - whether the ship is stuck or not
The code is not fully complete, still working on nuances as I'm new to Lean.
import Mathlib
namespace LaestrygonianHarbor
abbrev Ship := Nat
/-- Harbor settings. -/
structure Harbor where
narrowEntrance : Bool
closedBasin : Bool
exitOpen : Bool
deriving DecidableEq, Repr
/-- Ship states. -/
inductive ShipState
| outside
| entering
| inside
| moored
| trapped
| escaped
deriving DecidableEq, Repr
open ShipState
/-- Full fleet state. -/
structure FleetState where
harbor : Harbor
ships : Ship → ShipState
/-- No ship is trapped. -/
def Safe (s : FleetState) : Prop :=
∀ sh, s.ships sh ≠ trapped
/-- Bad harbor shape. -/
def TrapConfig (h : Harbor) : Prop :=
h.narrowEntrance = true ∧ h.closedBasin = true ∧ h.exitOpen = false
/-- Policy rules out the bad shape. -/
def SafePolicy (h : Harbor) : Prop :=
¬ TrapConfig h
/-- Local ship moves. -/
inductive Step (h : Harbor) : ShipState → ShipState → Prop
| enter : h.narrowEntrance = true → h.closedBasin = false → Step outside entering
| pass : h.narrowEntrance = true → Step entering inside
| moor : h.exitOpen = true → Step inside moored
| escape : h.exitOpen = true → Step inside escaped
| trap : h.closedBasin = true → h.exitOpen = false → Step moored trapped
/-- One ship changes state. -/
inductive FleetStep : FleetState → FleetState → Prop
| move
(h : Harbor)
(f : Ship → ShipState)
(sh : Ship)
{st st' : ShipState}
(hs : Step h st st')
(hcur : f sh = st) :
FleetStep
{ harbor := h, ships := f }
{ harbor := h, ships := fun x => if x = sh then st' else f x }-- Multi-step reachability.
inductive Reach : FleetState → FleetState → Prop
| refl (s : FleetState) : Reach s s
| trans {s₁ s₂ s₃ : FleetState} : FleetStep s₁ s₂ → Reach s₂ s₃ → Reach s₁ s₃
namespace Reach
/-- One step is reachable. -/
theorem step {s₁ s₂ : FleetState} (h : FleetStep s₁ s₂) : Reach s₁ s₂ :=
Reach.trans h (Reach.refl _)
end Reach
/-- A trapped ship makes the fleet unsafe. -/
theorem trapped_not_safe
(s : FleetState) (sh : Ship) (htrap : s.ships sh = trapped) : ¬ Safe s := by
intro hs
exact (hs sh) htrap
/-- One step preserves safety. -/
theorem fleet_step_preserves_safe
(s₁ s₂ : FleetState) (hsafe : Safe s₁) (hstep : FleetStep s₁ s₂) (hpol : SafePolicy s₁.harbor) : Safe s₂ := by
rcases hstep with ⟨h, f, sh, st, st', hs, hcur⟩
dsimp at hcur
subst s₁
intro k
by_cases hk : k = sh
· subst hk
cases hs with
| enter hn hb =>
simp [FleetState.ships]
| pass hn =>
simp [FleetState.ships]
| moor hex =>
simp [FleetState.ships]
| escape hex =>
simp [FleetState.ships]
| trap hb hex =>
simp [FleetState.ships]· simp [FleetState.ships, hk]
exact hsafe k
/-- Reachable states stay safe. -/
theorem reachable_safe
(s₀ s : FleetState) (hstart : Safe s₀) (hpol : SafePolicy s₀.harbor) (hreach : Reach s₀ s) : Safe s := by
induction hreach with
| refl =>
exact hstart
| trans hstep hrest ih =>
exact fleet_step_preserves_safe _ _ ih hstep hpol
/-- Policy excludes the hazard. -/
theorem policy_excludes_hazard
(h : Harbor) (hp : SafePolicy h) : ¬ TrapConfig h := by
exact hp
/-- Main theorem. -/
theorem main
(s₀ s : FleetState) (hstart : Safe s₀) (hpol : SafePolicy s₀.harbor) (hreach : Reach s₀ s) : Safe s := by
exact reachable_safe s₀ s hstart hpol hreach
end LaestrygonianHarbor