提交 #25

import Mathlib.Tactic.Linarith


def Tick (α : Type) : Type := Unit → α × Nat

instance : Monad Tick where
  pure r := fun _ => (r, 0)
  bind f g := fun _ =>
    let (r1, c1) := f ()
    let (r2, c2) := g r1 ()
    (r2, c1 + c2)

def tick (c : Nat) : Tick Unit := fun _ => ((), c)

structure Queue (α : Type) where
  inq : List α
  outq : List α

def Queue.empty (α : Type) : Tick (Queue α) := pure (mk [] [])

def Queue.in_to_out {α : Type} (q : Queue α) : Tick (Queue α) :=
  let rec aux (l1 l2 : List α) : Tick (List α) :=
    match l1 with
    | [] => pure l2
    | h :: t =>
      tick 1 >>= fun _ =>
      aux t (h :: l2)
  aux q.inq q.outq >>= fun r =>
  pure (mk [] r)

def Queue.enq {α : Type} (q : Queue α) (x : α) : Tick (Queue α) :=
  tick 1 >>= fun _ =>
  pure (mk (x :: q.inq) q.outq)

def Queue.deq {α : Type} (q : Queue α) : Tick (Option α × Queue α) :=
  tick 1 >>= fun _ =>
  match q.outq with
  | h :: t => pure (some h, mk q.inq t)
  | [] =>
    q.in_to_out >>= fun q' =>
    match q'.outq with
    | [] => pure (none, q')
    | h :: t => pure (some h, mk q'.inq t)

def seq_op_queue {α : Type} (q : Queue α) (ops : List (Option α)) : Tick (Queue α) :=
  match ops with
  | [] => pure q
  | op :: ops' =>
    match op with
    | some x =>
      q.enq x >>= fun q' =>
      seq_op_queue q' ops'
    | none =>
      q.deq >>= fun (_, q') =>
      seq_op_queue q' ops'

def seq_op_queue_from_empty {α : Type} (ops : List (Option α)) : Tick (Queue α) :=
  Queue.empty α >>= fun q =>
  seq_op_queue q ops

  
variable {α : Type}

def Potential (q : Tick (Queue α)) : Nat := (q ()).1.inq.length + (q ()).2

lemma bind_assoc {α β γ : Type} (m : Tick α) (f : α → Tick β) (g : β → Tick γ) :
  (m >>= f) >>= g = m >>= λ x ↦ (f x) >>= g := by
  unfold Bind.bind
  unfold instMonadTick
  simp
  refine funext λ () ↦ ?_
  simp [Nat.add_assoc]

lemma in_to_out_1 (q : Queue α) : (q.in_to_out ()).1.inq = [] := rfl

lemma in_to_out_2_aux (l₁ l₂ : List α) : (Queue.in_to_out.aux l₁ l₂ ()).2 = l₁.length := by
  induction l₁ generalizing l₂ with
  | nil => rfl
  | cons h t k =>
    change 1 + _ = (h :: t).length
    rw [k (h :: l₂)]
    simp only [List.length_cons, Nat.add_comm]

lemma in_to_out_2 (q : Queue α) : (q.in_to_out ()).2 = q.inq.length := in_to_out_2_aux q.inq q.outq

lemma enq_τ (q : Tick (Queue α)) (x : α) :
  Potential (q >>= λ r ↦ r.enq x) ≤ Potential q + 2 := by
  change (q ()).fst.inq.length + 1 + ((q ()).snd + 1) ≤ (q ()).fst.inq.length + (q ()).snd + 2
  linarith

lemma deq_τ (q : Tick (Queue α)) :
  Potential (q >>= λ r ↦ Prod.snd <$> r.deq) ≤ Potential q + 2 := by
  let Q := (q ()).1
  let t := (q ()).2
  change (Q.deq ()).1.2.inq.length + (t + (Q.deq ()).2) ≤ Q.inq.length + t + 2
  suffices h : (Q.deq ()).1.2.inq.length + (Q.deq ()).2 ≤ Q.inq.length + 2 by omega
  cases h₀ : Q.outq with
  | cons h t =>
    unfold Queue.deq
    simp only [h₀]
    change Q.inq.length + 1 ≤ Q.inq.length + 2
    simp
  | nil =>
    unfold Queue.deq
    simp only [h₀]
    unfold Bind.bind
    unfold instMonadTick
    simp
    set R := (Q.in_to_out ()).1.outq with R_def
    cases R with
    | nil =>
      simp
      rw [in_to_out_1, List.length_nil, zero_add, in_to_out_2]
      change 1 + _ ≤ _ + 2
      omega
    | cons h t =>
      simp
      rw [in_to_out_1, List.length_nil, zero_add, in_to_out_2]
      change 1 + _ ≤ _ + 2
      omega

lemma seq_op_queue_τ (q : Tick (Queue α)) (ops : List (Option α)) :
  Potential (q >>= λ r ↦ seq_op_queue r ops) ≤ Potential q + 2 * ops.length := by
  induction ops generalizing q with
  | nil => rfl
  | cons op₁ opᵣ h =>
    rw [List.length_cons, Nat.mul_succ, ← Nat.add_assoc _ _ 2]
    cases op₁ with
    | some x =>
      unfold seq_op_queue
      simp only
      rw [← bind_assoc]
      let q' := q >>= λ r ↦ r.enq x
      refine (h q').trans ?_
      suffices h : Potential q' ≤ Potential q + 2 by omega
      exact enq_τ q x
    | none =>
      unfold seq_op_queue
      simp only
      rw [← bind_assoc]
      let q' := q >>= λ r ↦ Prod.snd <$> r.deq
      refine (h q').trans ?_
      suffices h : Potential q' ≤ Potential q + 2 by omega
      exact deq_τ q

theorem seq_op_queue_from_empty_cost (ops : List (Option α)) : (seq_op_queue_from_empty ops ()).2 ≤ 2 * ops.length := by
  have h : Potential (seq_op_queue_from_empty ops) ≤ 0 + 2 * ops.length := seq_op_queue_τ (Queue.empty α) ops
  simp [Potential] at h
  omega