CoverExamples.lean

import FrontierDerivative.PrincipalCover

namespace FrontierDerivative.CoverExamples

inductive VisibleSymbol where
  | bottom
  | mark
  deriving DecidableEq, Repr

inductive VisibleLetter where
  | call
  | ret
  | stay
  deriving DecidableEq, Repr

inductive VisibleBasisIndex where
  | bottom
  | epsilon
  | empty
  deriving DecidableEq, Repr

open VisibleSymbol VisibleLetter

@[simp] theorem exists_eq_pair {A B : Type} (a : A) (b : B)
    (R : A → B → Prop) :
    (∃ x y, (x = a ∧ y = b) ∧ R x y) ↔ R a b := by
  constructor
  · rintro ⟨x, y, ⟨hx, hy⟩, hR⟩
    subst x
    subst y
    exact hR
  · intro hR
    exact ⟨a, b, ⟨rfl, rfl⟩, hR⟩

@[simp] theorem active_keep_decomposition (active : Prop)
    (s z : List VisibleSymbol) :
    (∃ X tail,
      (active ∧ X :: tail = s ++ [bottom]) ∧
      (bottom = X ∧ z = bottom :: tail ∨
        mark = X ∧ z = mark :: tail)) ↔
      active ∧ z = s ++ [bottom] := by
  constructor
  · rintro ⟨X, tail, ⟨ha, hstack⟩, hmove⟩
    refine ⟨ha, ?_⟩
    rcases hmove with ⟨hX, hz⟩ | ⟨hX, hz⟩
    · subst X
      subst z
      exact hstack
    · subst X
      subst z
      exact hstack
  · rintro ⟨ha, hz⟩
    subst z
    cases s with
    | nil =>
        exact ⟨bottom, [], ⟨ha, rfl⟩, Or.inl ⟨rfl, rfl⟩⟩
    | cons X tail =>
        cases X
        · exact ⟨bottom, tail ++ [bottom], ⟨ha, rfl⟩,
            Or.inl ⟨rfl, rfl⟩⟩
        · exact ⟨mark, tail ++ [bottom], ⟨ha, rfl⟩,
            Or.inr ⟨rfl, rfl⟩⟩

def visibleBasisLang (j : VisibleBasisIndex) : StackLang VisibleSymbol :=
  fun z =>
    match j with
    | .bottom => z = [bottom]
    | .epsilon => z = []
    | .empty => False

def visibleBasisDeriv (j : VisibleBasisIndex) (X : VisibleSymbol) :
    VisibleBasisIndex :=
  match j, X with
  | .bottom, .bottom => .epsilon
  | _, _ => .empty

def visibleBasis : DerivativeBasis VisibleBasisIndex VisibleSymbol where
  lang := visibleBasisLang
  deriv := visibleBasisDeriv
  deriv_exact := by
    intro j X tail
    cases j <;> cases X <;> cases tail <;>
      simp [visibleBasisLang, visibleBasisDeriv]

def visibleFrontier : Machine Unit VisibleLetter VisibleSymbol where
  transitions :=
    [ ⟨(), call, bottom, (), [mark, bottom]⟩
    , ⟨(), call, mark, (), [mark, mark]⟩
    , ⟨(), ret, mark, (), []⟩
    , ⟨(), stay, bottom, (), [bottom]⟩
    , ⟨(), stay, mark, (), [mark]⟩
    ]
  initial := ⟨(), [bottom]⟩
  final := fun _ => true

def visibleStep (active : Bool) (a : VisibleLetter)
    (tops : Fin 1 → Option VisibleSymbol) :
    Bool × (Fin 1 → FPRD.StackOp VisibleSymbol) :=
  if active then
    match a with
    | call => (true, fun _ => .push mark)
    | stay => (true, fun _ => .keep)
    | ret =>
        match tops 0 with
        | some mark => (true, fun _ => .pop)
        | _ => (false, fun _ => .keep)
  else
    (false, fun _ => .keep)

def visibleExecutor : FPRD.StackMachine VisibleLetter Bool VisibleSymbol 1 where
  step := visibleStep
  init := true
  accept := fun active => active

def visibleCoordinates :
    CoverCoordinates Bool Unit VisibleBasisIndex VisibleSymbol 1 where
  basis := visibleBasis
  owner := fun _ => ()
  slotBasis := fun active _ => if active then some .bottom else none

theorem visible_rep_iff (c : FPRD.Config Bool VisibleSymbol 1)
    (z : List VisibleSymbol) :
    visibleCoordinates.Rep c () z ↔
      c.ctrl = true ∧ z = c.stacks 0 ++ [bottom] := by
  cases hctrl : c.ctrl <;>
    simp [CoverCoordinates.Rep, visibleCoordinates, hctrl, visibleBasis,
      visibleBasisLang, Fin.exists_fin_one]

@[simp] theorem visible_rep_iff_any (c : FPRD.Config Bool VisibleSymbol 1)
    (q : Unit) (z : List VisibleSymbol) :
    visibleCoordinates.Rep c q z ↔
      c.ctrl = true ∧ z = c.stacks 0 ++ [bottom] := by
  cases q
  exact visible_rep_iff c z

def visibleCover :
    PrincipalCover visibleFrontier visibleExecutor VisibleBasisIndex where
  coordinates := visibleCoordinates
  valid := fun _ => True
  init_valid := trivial
  step_valid := by
    intro c a h
    trivial
  init_exact := by
    intro q z
    cases q
    rw [visible_rep_iff]
    simp [visibleExecutor, visibleFrontier, FPRD.StackMachine.initConfig,
      Machine.Frontier, Machine.run, Machine.runFrom]
  step_exact := by
    intro c a hvalid q z
    cases q
    cases hctrl : c.ctrl <;> cases a <;> cases hstack : c.stacks 0 <;>
      simp [visible_rep_iff_any, frontierDerivative, visibleExecutor, visibleStep,
        visibleFrontier, FPRD.StackMachine.stepConfig, exists_eq_pair, hctrl,
        hstack]
    all_goals
      rename_i head tail
      cases head <;>
        simp
  readout_exact := by
    intro c hvalid
    simp [visibleExecutor, visibleFrontier, visible_rep_iff_any]

/-! ## A finite parallel cover

The first `tick` keeps the left run and also activates a right run.  The second
slot is maintained in sync before activation; `valid` records that reachable
invariant.  This is the small case that motivates making exactness conditional
on a preserved invariant rather than arbitrary junk configurations.
-/

inductive BranchLetter where
  | tick
  deriving DecidableEq, Repr

structure BranchCtrl where
  left : Bool
  right : Bool
  deriving DecidableEq, Repr

def branchFrontier : Machine Bool BranchLetter VisibleSymbol where
  transitions :=
    [ ⟨false, .tick, bottom, false, [bottom]⟩
    , ⟨false, .tick, bottom, true, [bottom]⟩
    , ⟨false, .tick, mark, false, [mark]⟩
    , ⟨false, .tick, mark, true, [mark]⟩
    , ⟨true, .tick, bottom, true, [bottom]⟩
    , ⟨true, .tick, mark, true, [mark]⟩
    ]
  initial := ⟨false, [bottom]⟩
  final := fun q => q

def branchStep (ctrl : BranchCtrl) (_ : BranchLetter)
    (_ : Fin 2 → Option VisibleSymbol) :
    BranchCtrl × (Fin 2 → FPRD.StackOp VisibleSymbol) :=
  (⟨ctrl.left, ctrl.left || ctrl.right⟩, fun _ => .keep)

def branchExecutor :
    FPRD.StackMachine BranchLetter BranchCtrl VisibleSymbol 2 where
  step := branchStep
  init := ⟨true, false⟩
  accept := fun ctrl => ctrl.right

def branchCoordinates :
    CoverCoordinates BranchCtrl Bool VisibleBasisIndex VisibleSymbol 2 where
  basis := visibleBasis
  owner := fun i => if i = 0 then false else true
  slotBasis := fun ctrl i =>
    if i = 0 then
      if ctrl.left then some .bottom else none
    else
      if ctrl.right then some .bottom else none

@[simp] theorem branch_rep_false_iff
    (c : FPRD.Config BranchCtrl VisibleSymbol 2) (z : List VisibleSymbol) :
    branchCoordinates.Rep c false z ↔
      c.ctrl.left = true ∧ z = c.stacks 0 ++ [bottom] := by
  rcases hc : c.ctrl with ⟨left, right⟩
  cases left <;> cases right <;>
    simp [CoverCoordinates.Rep, branchCoordinates, visibleBasis,
      visibleBasisLang, hc]

@[simp] theorem branch_rep_true_iff
    (c : FPRD.Config BranchCtrl VisibleSymbol 2) (z : List VisibleSymbol) :
    branchCoordinates.Rep c true z ↔
      c.ctrl.right = true ∧ z = c.stacks 1 ++ [bottom] := by
  rcases hc : c.ctrl with ⟨left, right⟩
  cases left <;> cases right <;>
    simp [CoverCoordinates.Rep, branchCoordinates, visibleBasis,
      visibleBasisLang, hc]

theorem branch_rep_not_nil (c : FPRD.Config BranchCtrl VisibleSymbol 2)
    (q : Bool) : ¬branchCoordinates.Rep c q [] := by
  cases q <;> simp

theorem branch_derivative_false_iff
    (R : FrontierRel Bool VisibleSymbol)
    (hne : ∀ q, ¬R q []) (z : List VisibleSymbol) :
    frontierDerivative branchFrontier R .tick false z ↔ R false z := by
  constructor
  · rintro ⟨q, X, tail, t, hR, ht, hsource, hinput, htop, htarget, hz⟩
    simp only [branchFrontier, List.mem_cons, List.not_mem_nil, or_false] at ht
    rcases ht with rfl | rfl | rfl | rfl | rfl | rfl
    · change false = q at hsource
      change bottom = X at htop
      change z = bottom :: tail at hz
      subst q
      subst X
      subst z
      exact hR
    · change false = true at htarget
      contradiction
    · change false = q at hsource
      change mark = X at htop
      change z = mark :: tail at hz
      subst q
      subst X
      subst z
      exact hR
    · change false = true at htarget
      contradiction
    · change false = true at htarget
      contradiction
    · change false = true at htarget
      contradiction
  · intro hR
    cases z with
    | nil => exact (hne false hR).elim
    | cons X tail =>
        cases X
        · exact ⟨false, bottom, tail,
            ⟨false, .tick, bottom, false, [bottom]⟩,
            hR, by simp [branchFrontier], rfl, rfl, rfl, rfl, rfl⟩
        · exact ⟨false, mark, tail,
            ⟨false, .tick, mark, false, [mark]⟩,
            hR, by simp [branchFrontier], rfl, rfl, rfl, rfl, rfl⟩

theorem branch_derivative_true_iff
    (R : FrontierRel Bool VisibleSymbol)
    (hne : ∀ q, ¬R q []) (z : List VisibleSymbol) :
    frontierDerivative branchFrontier R .tick true z ↔
      R false z ∨ R true z := by
  constructor
  · rintro ⟨q, X, tail, t, hR, ht, hsource, hinput, htop, htarget, hz⟩
    simp only [branchFrontier, List.mem_cons, List.not_mem_nil, or_false] at ht
    rcases ht with rfl | rfl | rfl | rfl | rfl | rfl
    · change true = false at htarget
      contradiction
    · change false = q at hsource
      change bottom = X at htop
      change z = bottom :: tail at hz
      subst q
      subst X
      subst z
      exact Or.inl hR
    · change true = false at htarget
      contradiction
    · change false = q at hsource
      change mark = X at htop
      change z = mark :: tail at hz
      subst q
      subst X
      subst z
      exact Or.inl hR
    · change true = q at hsource
      change bottom = X at htop
      change z = bottom :: tail at hz
      subst q
      subst X
      subst z
      exact Or.inr hR
    · change true = q at hsource
      change mark = X at htop
      change z = mark :: tail at hz
      subst q
      subst X
      subst z
      exact Or.inr hR
  · intro hR
    rcases hR with hR | hR
    · cases z with
      | nil => exact (hne false hR).elim
      | cons X tail =>
          cases X
          · exact ⟨false, bottom, tail,
              ⟨false, .tick, bottom, true, [bottom]⟩,
              hR, by simp [branchFrontier], rfl, rfl, rfl, rfl, rfl⟩
          · exact ⟨false, mark, tail,
              ⟨false, .tick, mark, true, [mark]⟩,
              hR, by simp [branchFrontier], rfl, rfl, rfl, rfl, rfl⟩
    · cases z with
      | nil => exact (hne true hR).elim
      | cons X tail =>
          cases X
          · exact ⟨true, bottom, tail,
              ⟨true, .tick, bottom, true, [bottom]⟩,
              hR, by simp [branchFrontier], rfl, rfl, rfl, rfl, rfl⟩
          · exact ⟨true, mark, tail,
              ⟨true, .tick, mark, true, [mark]⟩,
              hR, by simp [branchFrontier], rfl, rfl, rfl, rfl, rfl⟩

def branchCover :
    PrincipalCover branchFrontier branchExecutor VisibleBasisIndex where
  coordinates := branchCoordinates
  valid := fun c => c.stacks 0 = c.stacks 1
  init_valid := rfl
  step_valid := by
    intro c a hvalid
    simpa [branchExecutor, branchStep, FPRD.StackMachine.stepConfig] using hvalid
  init_exact := by
    intro q z
    cases q <;>
      simp [branchExecutor, branchFrontier, FPRD.StackMachine.initConfig,
        Machine.Frontier, Machine.run, Machine.runFrom]
  step_exact := by
    intro c a hvalid q z
    cases a
    cases q
    · rw [branch_derivative_false_iff (branchCoordinates.Rep c)
          (branch_rep_not_nil c)]
      simp [branchExecutor, branchStep, FPRD.StackMachine.stepConfig]
    · rw [branch_derivative_true_iff (branchCoordinates.Rep c)
          (branch_rep_not_nil c)]
      simp [branchExecutor, branchStep, FPRD.StackMachine.stepConfig,
        or_and_right, hvalid]
  readout_exact := by
    intro c hvalid
    simp [branchExecutor, branchFrontier]

#check principalDerivative_nil
#check principalDerivative_cons_eq
#check principalDerivative_cons_ne
#check PrincipalCover.cover_run_exact
#check PrincipalCover.cover_decides_iff
#check PrincipalCover.compiled_cover_decides_iff

example : (visibleExecutor.run [call, call, ret, stay]).stacks 0 = [mark] := by
  decide

example : visibleExecutor.decides [ret] = false := by
  decide

example : visibleExecutor.decides [call, ret, stay] = true := by
  decide

example : visibleFrontier.Accepts [call, ret, stay] := by
  exact (visibleCover.cover_decides_iff [call, ret, stay]).1 (by decide)

example :
    (FPRD.compile visibleExecutor).decides [call, ret, stay] = true ↔
      visibleFrontier.Accepts [call, ret, stay] :=
  visibleCover.compiled_cover_decides_iff [call, ret, stay]

example : branchExecutor.decides [] = false := by
  decide

example : branchExecutor.decides [.tick] = true := by
  decide

example : branchFrontier.Accepts [.tick] := by
  exact (branchCover.cover_decides_iff [.tick]).1 (by decide)

example :
    (FPRD.compile branchExecutor).decides [.tick, .tick] = true ↔
      branchFrontier.Accepts [.tick, .tick] :=
  branchCover.compiled_cover_decides_iff [.tick, .tick]

end FrontierDerivative.CoverExamples