jozefg · April 14, 2018 18:44 · Apr 14, 2018
diff --git a/howe.agda b/howe.agda
@@ -0,0 +1,259 @@
+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
+  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
+
+close-flip : {L : LCS}{n : ℕ}{t₁ t₂ t₁' t₂' : Term L}
+  → Close n t₁ t₂ t₁' t₂' → Close n t₂ t₁ t₂' t₁'
+close-flip (zero t₁ t₁') = zero t₁ t₁'
+close-flip (suc t₁ t₂ t₃ t₁' t₂' closed) =
+  suc t₂ t₁ t₃ t₂' t₁' (close-flip closed)
+
+close-split : {L : LCS}{n : ℕ}{t₁ t₃ t₁' t₃' : Term L}(t₂ : Term L)
+  → Close n t₁ t₃ t₁' t₃'
+  → Σ (Term L) λ {
+    t₂' → Close n t₁ t₂ t₁' t₂' × Close n t₂ t₃ t₂' t₃'
+   }
+close-split t₂ (zero t t') = (t₂ , ( {!zero t t₂!} , {!!} ))
+close-split t₂ (suc t₁ t₁' t₄ t₃ t₃' prf) = {!!}
+
+
+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
+      coterm₁ : {o : O}(args : _) → t₁ ⇓ op o args → Σ _ λ t₄ → t₂ ⇓ op o t₄
+      coterm₂ : {o : O}(args : _) → t₂ ⇓ op o args → Σ _ λ t₄ → t₁ ⇓ op o t₄
+      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 _≈*_·_
+
+  oper-injective : {o : O}{args args' : Vec (Term L) _}
+                 → Term.op o args ≡ Term.op o args'
+                 → args ≡ args'
+  oper-injective refl = refl
+  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 oper-injective (deterministic run₁ run₂) =
+        reflexivity-many args'
+    reflexivity t .coterm₁ t₃ run₁ = (t₃ , run₁)
+    reflexivity t .coterm₂ t₃ run₁ = (t₃ , run₁)
+  mutual
+    symmetry-many : {m k : ℕ}(v v' : Vec (Term L) m)
+                  → v ≈* v' · k → v' ≈* v · k
+    symmetry-many .[] .[] (nil n) = nil _
+    symmetry-many .(h ∷ rest) .(h' ∷ rest') (cons n h h' rest rest' x prf) =
+      cons n h' h rest' rest matching (symmetry-many rest rest' prf)
+      where matching : (c c' : Term L) → Close n h' h c c' → c ≈ c'
+            matching c c' close = symmetry _ _ (x c' c (close-flip close))
+
+    symmetry : (t t' : Term L) → t ≈ t' → t' ≈ t
+    symmetry t t' eq .run args args' run₁ run₂ =
+      symmetry-many args' args (eq .run args' args run₂ run₁)
+    symmetry t t' eq .coterm₁ t₃ run₁ = eq .coterm₂ t₃ run₁
+    symmetry t t' eq .coterm₂ t₃ run₁ = eq .coterm₁ t₃ run₁
+
+  mutual
+    transitivity-many : {m k : ℕ}(v v' v'' : Vec (Term L) m)
+                      → v ≈* v' · k → v' ≈* v'' · k
+                      → v ≈* v'' · k
+    transitivity-many .[] .[] v'' (nil n) eq₂ = eq₂
+    transitivity-many .(h ∷ rest) .(h' ∷ rest') .(h'' ∷ rest'') (cons n h h' rest rest' x eq₁) (cons .n .h' h'' .rest' rest'' x₁ eq₂) =
+      cons n h h'' rest rest'' matching (transitivity-many _ _ _ eq₁ eq₂)
+      where matching : (c c' : Term L) → Close n h h'' c c' → c ≈ c'
+            matching c c' closed = {!!}
+
+    transitivity : (t t' t'' : Term L) → t ≈ t' → t' ≈ t'' → t ≈ t''
+    transitivity t t' t'' eq₁ eq₂ .run args args'' run₁ run₃
+      with eq₁ .coterm₁ args run₁
+    ... | t₂' , run₂ with eval-to-canon run₂
+    ... | op args' x =
+      transitivity-many args args' args''
+        (eq₁ .run args args' run₁ run₂)
+        (eq₂ .run args' args'' run₂ run₃)
+    transitivity t t' t'' eq₁ eq₂ .coterm₁ t₃ run₁ =
+      let (t₄ , run₂) = eq₁ .coterm₁ t₃ run₁
+      in eq₂ .coterm₁ t₄ run₂
+    transitivity t t' t'' eq₁ eq₂ .coterm₂ t₃ run₁ =
+      let (t₄ , run₂) = eq₂ .coterm₂ t₃ run₁
+      in eq₁ .coterm₂ t₄ run₂