{-# OPTIONS --safe #-}

module Problem9 where

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Relation.Nullary
open import Data.List
open import Data.Nat.Properties using (suc-injective)
open import Data.List.Properties using (++-identityʳ;length-++; ++-assoc;unfold-reverse; length-reverse)

open ≡-Reasoning

variable A : Set

record Queue A : Set where
  constructor Q
  field
    size-front  : ℕ
    size-back   : ℕ
    front : List A
    back  : List A

    invariant : size-back ≤ size-front
    size-inv₁ : length front ≡ size-front
    size-inv₂ : length back ≡ size-back
open Queue

record CorrectQueue (Q : Set → Set) : Set₁ where
  field
    abstraction : Q A → List A
    enqueue     : A → Q A → Q A
    dequeue     : Q A → Maybe (Q A)
    first       : Q A → Maybe A
    size        : Q A → ℕ
    empty       : Q A

    emptyᵣ      : abstraction (empty {A}) ≡ []
    sizeᵣ       : ∀ (q : Q A) → size q ≡ length (abstraction q)
    firstᵣ      : ∀ (q : Q A) → first q ≡ head (abstraction q)
    dequeueᵣ    : ∀ (q : Q A) → Maybe.map abstraction (dequeue q) ≡ tail (abstraction q)
    enqueueᵣ    : ∀ (q : Q A) x → abstraction (enqueue x q) ≡ abstraction q ∷ʳ x

enqueueQ  : A → Queue A → Queue A
enqueueQ x q with suc (size-back q) ≤? size-front  q
... | yes p = Q (size-front q) (suc (size-back q)) (front q) (x ∷ back q) p (size-inv₁ q) (cong suc (size-inv₂ q))
... | no  p = Q (size-front q + suc (size-back q)) 0 (front q ++ reverse (x ∷ back q)) [] z≤n (trans (length-++ (front q)) (cong₂ _+_ (size-inv₁ q) (trans (length-reverse (x ∷ back q) ) (cong suc (size-inv₂ q))))) refl

dequeueQ : Queue A → Maybe (Queue A)
dequeueQ (Q _ _ [] [] z≤n refl refl) = nothing
dequeueQ (Q (suc size-front₁) size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄) with size-back₁ ≤? size-front₁
... | yes p  = just (Q size-front₁ size-back₁ front₁ back₁ p (suc-injective size-inv₃) size-inv₄)
... | no p   = just (Q (size-front₁ + size-back₁) 0 (front₁ ++ reverse back₁) [] z≤n (trans (length-++ front₁) (cong₂ _+_ (suc-injective size-inv₃) (trans (length-reverse back₁) size-inv₄))) refl)

firstQ : Queue A → Maybe A
firstQ (Q size-front₁ size-back₁ [] back₁ invariant₁ size-inv₃ size-inv₄) = nothing
firstQ (Q size-front₁ size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄) = just x

sizeQ : Queue A → ℕ
sizeQ q = size-front q + size-back q

emptyQ : Queue A
emptyQ = Q 0 0 [] [] z≤n refl refl

open CorrectQueue

goal : CorrectQueue Queue

-- Data portion of goal
goal .abstraction q = front q ++ reverse (back q)
goal .enqueue x q = enqueueQ x q
goal .dequeue q = dequeueQ q
goal .first q = firstQ q
goal .size q = sizeQ q
goal .empty = emptyQ

-- Correctness portion of goal
goal .emptyᵣ = refl
goal .sizeᵣ q = begin
  sizeQ q                                      ≡⟨⟩
  size-front q + size-back q                   ≡˘⟨ cong₂ _+_ (size-inv₁ q) (size-inv₂ q) ⟩
  length (front q) + length (back q)           ≡˘⟨ cong (length (front q) +_) (length-reverse (back q)) ⟩
  length (front q) + length (reverse (back q)) ≡˘⟨ length-++ (front q) ⟩
  length (front q ++ reverse (back q))         ∎
goal .firstᵣ (Q .0 .0 [] [] z≤n refl refl) = refl
goal .firstᵣ (Q _ _ (x ∷ front₁) back₁ _ _ _) = refl
goal .dequeueᵣ (Q .0 .0 [] [] z≤n refl refl) = refl
goal .dequeueᵣ (Q (suc size-front₁) size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄)
  with size-back₁ ≤? size-front₁
... | yes p = refl
... | no p = cong just (++-identityʳ (front₁ ++ reverse back₁))
goal .enqueueᵣ q x with suc (size-back q) ≤? size-front q
... | yes p = begin
  front q ++ reverse (x ∷ back q)         ≡⟨ cong (front q ++_) (unfold-reverse x (back q)) ⟩
  front q ++ reverse (back q) ++ x ∷ []   ≡˘⟨ ++-assoc (front q) (reverse (back q)) (x ∷ []) ⟩
  (front q ++ reverse (back q)) ++ x ∷ [] ∎
... | no p = begin
  (front q ++ reverse (x ∷ back q)) ++ [] ≡⟨ ++-identityʳ (front q ++ reverse (x ∷ back q)) ⟩
  front q ++ reverse (x ∷ back q)         ≡⟨ cong (front q ++_) (unfold-reverse x (back q)) ⟩
  front q ++ reverse (back q) ++ x ∷ []   ≡˘⟨ ++-assoc (front q) (reverse (back q)) (x ∷ []) ⟩
  (front q ++ reverse (back q)) ++ x ∷ [] ∎