提交 #11

import Mathlib.Tactic

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



def Pot {α : Type} (f : Tick α) (pre_pot : Nat) (post_pot : α → Nat) : Prop :=
  let (r, c) := f (); pre_pot ≥ c + post_pot r

def list_pot_lin {α : Type} (p : Nat) (l : List α) : Nat :=
  match l with
  | [] => 0
  | _ :: t => p + list_pot_lin p t

theorem list_pot_share {α : Type} (p1 p2 : Nat) (l : List α) :
  list_pot_lin (p1 + p2) l = list_pot_lin p1 l + list_pot_lin p2 l
:=
  match l with
  | [] => by
    simp [list_pot_lin]
  | _ :: t => by
    have ih := list_pot_share p1 p2 t
    simp [list_pot_lin]
    linarith

lemma list_pot_lin_length {α : Type} (p : Nat) (l : List α) :
  list_pot_lin p l = p * l.length
:=
  match l with
  | [] => by
    simp [list_pot_lin]
  | _ :: t => by
    simp [list_pot_lin]
    have ih := list_pot_lin_length p t
    linarith

theorem empty_pot (α : Type) :
  Pot (Queue.empty α) 0 (fun q => list_pot_lin 1 q.inq)
:= by
  simp [Pot, Queue.empty, pure, list_pot_lin]


theorem in_to_out_pot {α : Type} (q : Queue α) :
  Pot (Queue.in_to_out q) (list_pot_lin 1 q.inq) (fun q => list_pot_lin 1 q.inq)
:= by
  simp [Pot, Queue.in_to_out, bind, list_pot_lin]
  generalize q.outq = a
  induction q.inq generalizing a with
  | nil =>
    simp [Queue.in_to_out.aux, pure]
  | cons h t ih =>
    simp [Queue.in_to_out.aux, bind, tick, list_pot_lin]
    specialize ih (h :: a)
    exact ih

theorem enq_pot {α : Type} (q : Queue α) (x : α) :
  Pot (Queue.enq q x) (list_pot_lin 1 q.inq + 2) (fun q => list_pot_lin 1 q.inq)
:= by
  simp [Pot, Queue.enq, bind, tick, list_pot_lin]
  linarith

theorem deq_pot {α : Type} (q : Queue α) :
  Pot (Queue.deq q) (list_pot_lin 1 q.inq + 1) (fun (_, q) => list_pot_lin 1 q.inq)
:= by
  simp [Pot, Queue.deq, bind, tick]
  cases q.outq
  . simp
    have tmp := in_to_out_pot q
    simp [Pot] at tmp
    cases (q.in_to_out ()).1.outq
    . simp [pure]
      linarith
    . simp [pure]
      linarith
  . simp [pure]
    linarith

theorem seq_op_queue_pot {α : Type} (q : Queue α) (ops : List (Option α)) :
  Pot (seq_op_queue q ops) (list_pot_lin 1 q.inq + list_pot_lin 2 ops)
  (fun q => list_pot_lin 1 q.inq)
:= by
  simp [Pot]
  induction ops generalizing q with
  | nil =>
    simp [seq_op_queue, pure]
  | cons op ops' ih =>
    simp [seq_op_queue]
    cases op with
    | some x =>
      simp [bind]
      have tmp := enq_pot q x
      simp [Pot] at tmp
      specialize ih (q.enq x ()).1
      simp [list_pot_lin]
      linarith
    | none =>
      simp [bind, list_pot_lin]
      have tmp := deq_pot q
      simp [Pot] at tmp
      specialize ih (q.deq ()).1.2
      linarith

theorem seq_op_queue_from_empty_pot {α : Type} (ops : List (Option α)) :
  Pot (seq_op_queue_from_empty ops) (list_pot_lin 2 ops) (fun q => list_pot_lin 1 q.inq)
:= by
  simp [Pot, seq_op_queue_from_empty, bind]
  have h1 := empty_pot α
  simp [Pot] at h1
  have h2 := seq_op_queue_pot (Queue.empty α ()).1 ops
  simp [Pot] at h2
  linarith

theorem seq_op_queue_from_empty_cost {α : Type} (ops : List (Option α)) :
  (seq_op_queue_from_empty ops ()).2 ≤ 2 * ops.length
:= by
  have pot := seq_op_queue_from_empty_pot ops
  simp [Pot] at pot
  have len := list_pot_lin_length 2 ops
  linarith