Skip to content

Instantly share code, notes, and snippets.

@jozefg
Created April 14, 2018 18:44
Show Gist options
  • Save jozefg/e3cc5d517a5834f25dd24a33b5ff7c68 to your computer and use it in GitHub Desktop.
Save jozefg/e3cc5d517a5834f25dd24a33b5ff7c68 to your computer and use it in GitHub Desktop.
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₂
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment