howe.agda

module howe where
open import Data.Nat
open import Data.Vec
open import Data.List
open import Data.Product
import Data.Fin  as F
import Relation.Binary as B
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Relation.Nullary

module Utils where
  plus0 : (n : ℕ) → n + 0 ≡ n
  plus0 zero = refl
  plus0 (suc n) rewrite plus0 n = refl

  suc-on-right : (n m : ℕ) → n + suc m ≡ suc (n + m)
  suc-on-right zero m = refl
  suc-on-right (suc n) m rewrite suc-on-right n m = refl

  plus-commute : (n m : ℕ) → n + m ≡ m + n
  plus-commute zero m rewrite plus0 m = refl
  plus-commute (suc n) m rewrite suc-on-right m n | plus-commute n m = refl

  bracket-≤ : {n m : ℕ}(x : ℕ) → n ≤ m → n + x ≤ m + x
  bracket-≤ {n} {m} zero prf rewrite plus0 n | plus0 m = prf
  bracket-≤ {n} {m} (suc x) prf rewrite suc-on-right n x | suc-on-right m x =
    s≤s (bracket-≤ x prf)

  remove-suc-right : {n m : ℕ} → n ≤ m → n ≤ suc m
  remove-suc-right z≤n = z≤n
  remove-suc-right (s≤s prf) = s≤s (remove-suc-right prf)

  remove-suc-left : {n m : ℕ} → suc n ≤ m → n ≤ m
  remove-suc-left (s≤s prf) = remove-suc-right prf

  remove-+-left : {n m x : ℕ} → x + n ≤ m → n ≤ m
  remove-+-left {n} {m} {zero} prf = prf
  remove-+-left {n} {m} {suc x} prf =
    remove-+-left {n}{m}{x} (remove-suc-left {x + n} {m} prf)

  remove-+-right : {n m x : ℕ} → n + x ≤ m → n ≤ m
  remove-+-right {n}{m}{x} rewrite plus-commute n x = remove-+-left {n}{m}{x}


record LCS : Set₁ where
  constructor lcs
  field
    O : Set
    Canon : O → Set
    arity : O → List ℕ

data Term (L : LCS) : Set where
  var : ℕ → Term L
  op  : (o : LCS.O L) → Vec (Term L) (length (LCS.arity L o)) → Term L

data WellBound {L : LCS} : ℕ → Term L → Set
data WellBoundMany {L : LCS} : {m : ℕ} →  ℕ → ℕ → Vec (Term L) m → Set

data WellBound {L : LCS} where
  var : {n m : ℕ} → n < m → WellBound m (var n)
  op  : (o : LCS.O L){m : ℕ}(args : Vec (Term L) (length (LCS.arity L o)))
      → WellBoundMany 0 m args → WellBound m (op o args)
data WellBoundMany {L : LCS} where
  nil  : {k n : ℕ} → WellBoundMany k n []
  cons : {k n m : ℕ}(h : Term L)(rest : Vec (Term L) m)
       → WellBound (n + k) h
       → WellBoundMany (suc k) n rest
       → WellBoundMany k n (h ∷ rest)

Closed : {L : LCS} → Term L → Set
Closed = WellBound 0

mutual
  well-bound-weaken : {L : LCS}{n m : ℕ}{t : Term L} → n ≤ m → WellBound n t
                    → WellBound m t
  well-bound-weaken prf (var x) =
    var (B.IsPartialOrder.trans
          (B.IsTotalOrder.isPartialOrder
            (B.IsDecTotalOrder.isTotalOrder
              (B.DecTotalOrder.isDecTotalOrder decTotalOrder))) x prf)
  well-bound-weaken prf (op o args x) =
    op o args (well-bound-many-weaken prf x)

  well-bound-many-weaken : {L : LCS}{n m k len : ℕ}{v : Vec (Term L) len}
                         → n ≤ m → WellBoundMany k n v → WellBoundMany k m v
  well-bound-many-weaken prf nil = nil
  well-bound-many-weaken {k = k} prf (cons _ _ x wbm) =
    cons _ _
      (well-bound-weaken (Utils.bracket-≤ k prf) x)
      (well-bound-many-weaken prf wbm)


data IsCanon {L : LCS} : Term L → Set where
  var : {n : ℕ} → IsCanon (var n)
  op  : {o : LCS.O L}{args : _} → LCS.Canon L o → IsCanon (op o args)


record Eval (L : LCS) : Set₁ where
  constructor eval
  field
    _⇓_ : Term L → Term L → Set
    steps : ℕ → Term L → Term L → Set
    -- Expected properties of a stepping relation
    eval-to-canon : {t t' : Term L} → t ⇓ t' → IsCanon t'
    canon-to-canon : {t : Term L} → IsCanon t → t ⇓ t
    deterministic : {t t₁ t₂ : Term L} → t ⇓ t₁ → t ⇓ t₂ → t₁ ≡ t₂
    -- Indexed steps
    steps-eventually : {t t' : Term L} → t ⇓ t' → Σ ℕ λ n → steps n t t'
    steps-agrees : {t t' : Term L}{n : ℕ} → steps n t t' → t ⇓ t'

mutual
  -- This relies on the fact that we only ever substitute closed terms
  subst : {L : LCS} → Term L → ℕ → Term L → Term L
  subst new n (var x) with compare x n
  ... | less .x k = var x
  ... | equal .n = new
  ... | greater .n k = var (n + k)
  subst {L} new n (op o args) = op o (subst-many 0 new n args)

  subst-many : {L : LCS}{n : ℕ} → ℕ → Term L → ℕ → Vec (Term L) n → Vec (Term L) n
  subst-many m new n [] = []
  subst-many m new n (x ∷ v) = subst new (n + m) x ∷ subst-many (suc m) new n v

mutual
  subst-closes : {L : LCS}{n x : ℕ}(t t' : Term L)
               → x < n
               → WellBound (suc n) t → Closed t'
               → WellBound n (subst t' x t)
  subst-closes {x = x} .(var n) t' x<n (var {n} prf) closed with compare n x
  subst-closes {_} {_} {.(suc (m + k))} .(var m) t' x<n (var {.m} prf) closed
    | less m k = var (Utils.remove-+-right (Utils.remove-suc-left x<n))
  subst-closes {_} {_} {.m} .(var m) t' x<n (var {.m} prf) closed
    | equal m = well-bound-weaken z≤n closed
  subst-closes {_} {_} {.m} .(var (suc (m + k))) t' x<n (var {.(suc (m + k))} (s≤s prf)) closed
    | greater m k = var prf
  subst-closes .(op o args) t' x<n (op o args x) closed =
    op o _ (subst-closes-many args t' x<n x closed)

  subst-closes-many : {L : LCS}{len n k x : ℕ}(v : Vec (Term L) len)(t : Term L)
                    → x < n
                    → WellBoundMany k (suc n) v → Closed t
                    → WellBoundMany k n (subst-many k t x v)
  subst-closes-many .[] t x<n nil closed = nil
  subst-closes-many {k = k} .(h ∷ rest) t x<n (cons h rest x wb) closed
    rewrite Utils.plus0 k =
      cons _ _ (subst-closes h t (Utils.bracket-≤ _ x<n) x closed)
        (subst-closes-many rest t x<n wb closed)

data Close {L : LCS} : ℕ → Term L → Term L → Term L → Term L → Set where
  zero : (t t' : Term L) → Close 0 t t t' t'
  suc  : {n : ℕ}(t₁ t₁' t₂ t₃ t₃' : Term L)
       → Close n (subst t₂ 0 t₁) (subst t₂ 0 t₁') t₃ t₃'
       → Close (suc n) t₁ t₁' t₃ t₃'

close-equals : {L : LCS}{n : ℕ}(t t₁ t₂ : Term L) → Close n t t t₁ t₂
             → t₁ ≡ t₂
close-equals t t₁ .t₁ (zero .t .t₁) = refl
close-equals t t₁ t₂ (suc .t .t t₃ .t₁ .t₂ closing)
  rewrite close-equals _ _ _ closing = refl

module Equivalence (L : LCS)(E : Eval L) where
  open LCS L
  open Eval E

  data _≈*_·_ : {m : ℕ} → Vec (Term L) m → Vec (Term L) m → ℕ → Set
  record _≈_ (t₁ t₂ : Term L) : Set

  record _≈_ (t₁ t₂ : Term L) where
    coinductive
    constructor equiv
    field
      run :
        {o : O}{args args' : _}
        → t₁ ⇓ op o args → t₂ ⇓ op o args'
        → args ≈* args · 0

  data _≈*_·_ where
    nil  : (n : ℕ) → [] ≈* [] · n
    cons : {m : ℕ}(n : ℕ)(h h' : Term L)(rest rest' : Vec (Term L) m)
         → ((c c' : Term L) → Close n h h' c c' → c ≈ c')
         → rest ≈* rest' · suc n
         → (h ∷ rest) ≈* (h ∷ rest') · n
  open _≈_
  open _≈*_·_

  mutual
    reflexivity-many : {m k : ℕ}(v : Vec (Term L) m) → v ≈* v · k
    reflexivity-many {k} [] = nil _
    reflexivity-many {k} (x ∷ v) =
      cons _ x x v v matching (reflexivity-many v)
      where matching : (c c' : Term L) → Close _ x x c c' → c ≈ c'
            matching c c' closing rewrite close-equals x c c' closing =
              reflexivity c'

    reflexivity : (t : Term L) → t ≈ t
    reflexivity t .run {args = args} run₁ run₂ rewrite deterministic run₁ run₂ =
      reflexivity-many args