Proof inspired by a discussion with Komi in the Programming Language Development Discord

Komi20250302.agda

module Komi20250302 where

data _≡_ {A : Set} (base : A) : A → Set where
  refl : base ≡ base

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl p = p

ap : {A B : Set} {x1 x2 : A} (f : A → B) → x1 ≡ x2 → f x1 ≡ f x2
ap f refl = refl

ap2 : {A B C : Set} {x1 x2 : A} {y1 y2 : B} (f : A → B → C) → x1 ≡ x2 → y1 ≡ y2 → f x1 y1 ≡ f x2 y2
ap2 f refl refl = refl

≡⟨⟩-syntax : {A : Set} (u : A) {v w : A} → u ≡ w → w ≡ v → u ≡ v
≡⟨⟩-syntax w = trans
infixr 2 ≡⟨⟩-syntax
syntax ≡⟨⟩-syntax u p q = u ≡⟨ p ⟩ q

_∎ : {A : Set} (u : A) → u ≡ u
_∎ u = refl
infix 3 _∎

record Σ (base : Set) (fam : base → Set) : Set where
  constructor [_,_]
  field
    fst : base
    snd : fam fst
open Σ

syntax Σ base (λ x → fam) = [ x ∈ base ]× fam

data Nat : Set where
  zero : Nat
  succ : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

succ-inj : (m n : Nat) → succ m ≡ succ n → m ≡ n
succ-inj m n refl = refl

_+N_ : Nat → Nat → Nat
zero +N n = n
succ m +N n = succ (m +N n)

+N-zero : (n : Nat) → (n +N 0) ≡ n
+N-zero zero =
  0 ∎
+N-zero (succ n) =
  succ (n +N 0) ≡⟨ ap succ (+N-zero n) ⟩
  succ  n       ∎

+N-succ : (m n : Nat) → (m +N succ n) ≡ succ (m +N n)
+N-succ zero n =
  succ n ∎
+N-succ (succ m) n =
  succ (m +N succ n)   ≡⟨ ap succ (+N-succ m n) ⟩
  succ (succ (m +N n)) ∎

+N-comm : (m n : Nat) → (m +N n) ≡ (n +N m)
+N-comm zero n =
  n      ≡⟨ sym (+N-zero n) ⟩
  n +N 0 ∎
+N-comm (succ m) n =
  succ (m +N n) ≡⟨ ap succ (+N-comm m n) ⟩
  succ (n +N m) ≡⟨ sym (+N-succ n m) ⟩
  n +N succ m   ∎

+N-assoc : (m n o : Nat) → (m +N (n +N o)) ≡ ((m +N n) +N o)
+N-assoc zero n o =
  n +N o ∎
+N-assoc (succ m) n o =
  succ (m +N (n +N o)) ≡⟨ ap succ (+N-assoc m n o) ⟩
  succ ((m +N n) +N o) ∎

+N-inj : (m n o : Nat) → (m +N o) ≡ (n +N o) → m ≡ n
+N-inj m n zero p =
  m ≡⟨ sym (+N-zero m) ⟩
  m +N 0 ≡⟨ p ⟩
  n +N 0 ≡⟨ +N-zero n ⟩
  n ∎
+N-inj m n (succ o) p = +N-inj m n o (succ-inj (m +N o) (n +N o) (
    succ (m +N o) ≡⟨ sym (+N-succ m o) ⟩
    m +N succ o   ≡⟨ p ⟩
    n +N succ o   ≡⟨ +N-succ n o ⟩
    succ (n +N o) ∎
  ))

data Fin : Nat → Set where
  zero : (n : Nat) → Fin (succ n)
  succ : {n : Nat} → Fin n → Fin (succ n)

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : {n : Nat} → A → Vec A n → Vec A (succ n)

replicate : {A : Set} (x : A) (n : Nat) → Vec A n
replicate x zero = []
replicate x (succ n) = x ∷ replicate x n

∷-inj-head : {A : Set} {n : Nat} {h1 h2 : A} {t1 t2 : Vec A n} → (h1 ∷ t1) ≡ (h2 ∷ t2) → h1 ≡ h2
∷-inj-head refl = refl

∷-inj-tail : {A : Set} {n : Nat} {h1 h2 : A} {t1 t2 : Vec A n} → (h1 ∷ t1) ≡ (h2 ∷ t2) → t1 ≡ t2
∷-inj-tail refl = refl

data Expr (Γ : Nat) : Set where
  var : Fin Γ → Expr Γ
  inj : Nat → Expr Γ
  _+e_ : Expr Γ → Expr Γ → Expr Γ

_⋅e_ : {Γ : Nat} → Nat → Expr Γ → Expr Γ
zero ⋅e u = inj 0
succ n ⋅e u = u +e (n ⋅e u)

data _⊢_≡_ (Γ : Nat) : Expr Γ → Expr Γ → Set where
  ⊢refl : ∀{e} → Γ ⊢ e ≡ e
  ⊢sym : ∀{u v} → Γ ⊢ u ≡ v → Γ ⊢ v ≡ u
  ⊢trans : ∀{u v w} → Γ ⊢ u ≡ w → Γ ⊢ w ≡ v → Γ ⊢ u ≡ v
  ⊢+-comm : ∀{u v} → Γ ⊢ (u +e v) ≡ (v +e u)
  ⊢+-assoc : ∀{u v w} → Γ ⊢ (u +e (v +e w)) ≡ ((u +e v) +e w)
  ⊢inj-+ : ∀{m n} → Γ ⊢ (inj m +e inj n) ≡ inj (m +N n)
  ⊢+-zero : ∀{u} → Γ ⊢ (u +e inj 0) ≡ u
  ⊢ap-+ : ∀{ul ur vl vr} → Γ ⊢ ul ≡ vl → Γ ⊢ ur ≡ vr → Γ ⊢ (ul +e ur) ≡ (vl +e vr)

⊢≡⟨⟩-syntax : {Γ : Nat} (u : Expr Γ) {v w : Expr Γ} → Γ ⊢ u ≡ w → Γ ⊢ w ≡ v → Γ ⊢ u ≡ v
⊢≡⟨⟩-syntax w = ⊢trans
infixr 2 ⊢≡⟨⟩-syntax
syntax ⊢≡⟨⟩-syntax u p q = u ⊢≡⟨ p ⟩ q

_⊢∎ : {Γ : Nat} (u : Expr Γ) → Γ ⊢ u ≡ u
_⊢∎ u = ⊢refl
infix 3 _⊢∎

⊢≡ : {Γ : Nat} {u v : Expr Γ} → u ≡ v → Γ ⊢ u ≡ v
⊢≡ refl = ⊢refl

⊢zero-+ : {Γ : Nat} {u : Expr Γ} → Γ ⊢ (inj 0 +e u) ≡ u
⊢zero-+ {Γ} {u} =
  inj 0 +e u ⊢≡⟨ ⊢+-comm ⟩
  u +e inj 0 ⊢≡⟨ ⊢+-zero ⟩
  u ⊢∎

⊢+⋅e : {Γ : Nat} (m n : Nat) (u : Expr Γ) → Γ ⊢ ((m +N n) ⋅e u) ≡ ((m ⋅e u) +e (n ⋅e u))
⊢+⋅e zero n u =
  n ⋅e u            ⊢≡⟨ ⊢sym ⊢zero-+ ⟩
  inj 0 +e (n ⋅e u) ⊢∎
⊢+⋅e (succ m) n u =
  u +e ((m +N n) ⋅e u)        ⊢≡⟨ ⊢ap-+ ⊢refl (⊢+⋅e m n u) ⟩
  u +e ((m ⋅e u) +e (n ⋅e u)) ⊢≡⟨ ⊢+-assoc ⟩
  (u +e (m ⋅e u)) +e (n ⋅e u) ⊢∎

zeroes : (Γ : Nat) → Vec Nat Γ
zeroes Γ = replicate 0 Γ

record NF (Γ : Nat) : Set where
  constructor mk-NF
  field constant : Nat
  field coefs : Vec Nat Γ

NF-inj : {Γ : Nat} → Nat → NF Γ
NF-inj n .NF.constant = n
NF-inj n .NF.coefs = zeroes _

single-coef : {Γ : Nat} → Fin Γ → Vec Nat Γ
single-coef (zero Γ) = 1 ∷ zeroes Γ
single-coef (succ v) = 0 ∷ single-coef v

NF-var : {Γ : Nat} → Fin Γ → NF Γ
NF-var v .NF.constant = 0
NF-var v .NF.coefs = single-coef v

_+coefs_ : {Γ : Nat} → Vec Nat Γ → Vec Nat Γ → Vec Nat Γ
[] +coefs [] = []
(u ∷ us) +coefs (v ∷ vs) = (u +N v) ∷ (us +coefs vs)

+coefs-zero : {Γ : Nat} (u : Vec Nat Γ) → (u +coefs zeroes Γ) ≡ u
+coefs-zero [] = refl
+coefs-zero (u ∷ us) = ap2 _∷_ (+N-zero u) (+coefs-zero us)

+coefs-comm : {Γ : Nat} (u v : Vec Nat Γ) → (u +coefs v) ≡ (v +coefs u)
+coefs-comm [] [] = refl
+coefs-comm (u ∷ us) (v ∷ vs) = ap2 _∷_ (+N-comm u v) (+coefs-comm us vs)

+coefs-assoc : {Γ : Nat} (u v w : Vec Nat Γ) → (u +coefs (v +coefs w)) ≡ ((u +coefs v) +coefs w)
+coefs-assoc [] [] [] = refl
+coefs-assoc (u ∷ us) (v ∷ vs) (w ∷ ws) = ap2 _∷_ (+N-assoc u v w) (+coefs-assoc us vs ws)

+coefs-inj : {Γ : Nat} (u v w : Vec Nat Γ) → (u +coefs w) ≡ (v +coefs w) → u ≡ v
+coefs-inj [] [] [] p = p
+coefs-inj (u ∷ us) (v ∷ vs) (w ∷ ws) p = ap2 _∷_
  (+N-inj u v w (∷-inj-head p))
  (+coefs-inj us vs ws (∷-inj-tail p))

_+NF_ : {Γ : Nat} → NF Γ → NF Γ → NF Γ
(u +NF v) .NF.constant = (u .NF.constant) +N (v .NF.constant)
(u +NF v) .NF.coefs = (u .NF.coefs) +coefs (v .NF.coefs)

+NF-comm : {Γ : Nat} (u v : NF Γ) → (u +NF v) ≡ (v +NF u)
+NF-comm u v = ap2 mk-NF
  (+N-comm (u .NF.constant) (v .NF.constant))
  (+coefs-comm (u .NF.coefs) (v .NF.coefs))

+NF-assoc : {Γ : Nat} (u v w : NF Γ) → (u +NF (v +NF w)) ≡ ((u +NF v) +NF w)
+NF-assoc u v w = ap2 mk-NF
  (+N-assoc (u .NF.constant) (v .NF.constant) (w .NF.constant))
  (+coefs-assoc (u .NF.coefs) (v .NF.coefs) (w .NF.coefs))

+NF-inj : {Γ : Nat} (u v w : NF Γ) → (u +NF w) ≡ (v +NF w) → u ≡ v
+NF-inj u v w p = ap2 mk-NF
  (+N-inj (u .NF.constant) (v .NF.constant) (w .NF.constant) (ap NF.constant p))
  (+coefs-inj (u .NF.coefs) (v .NF.coefs) (w .NF.coefs) (ap NF.coefs p))

eval : {Γ : Nat} → (e : Expr Γ) → NF Γ
eval {Γ} (var v) = NF-var v
eval (inj n) = NF-inj n
eval (u +e v) = eval u +NF eval v

quot-coefs : {Γ Δ : Nat} → Vec Nat Δ → (Fin Δ → Fin Γ) → Expr Γ
quot-coefs [] lift-var = inj 0
quot-coefs (coef ∷ coefs) lift-var = (coef ⋅e var (lift-var (zero _))) +e (quot-coefs coefs λ v → lift-var (succ v))

quot : {Γ : Nat} → NF Γ → Expr Γ
quot {Γ} nf = inj constant +e quot-coefs coefs (λ v → v)
  where open NF nf

quot-coefs-zero : (Γ Δ : Nat) (lift-var : Fin Δ → Fin Γ) → Γ ⊢ quot-coefs (zeroes Δ) lift-var ≡ inj 0
quot-coefs-zero Γ zero lift-var =
  inj 0 ⊢∎
quot-coefs-zero Γ (succ Δ) lift-var =
  ((0 ⋅e var (lift-var (zero Δ))) +e quot-coefs (zeroes Δ) (λ v → lift-var (succ v))) ⊢≡⟨ ⊢zero-+ ⟩
                                     quot-coefs (zeroes Δ) (λ v → lift-var (succ v))  ⊢≡⟨ quot-coefs-zero Γ Δ (λ v → lift-var (succ v)) ⟩
  inj 0                                                                               ⊢∎

quot-coefs-+ : (Γ Δ : Nat) (lift-var : Fin Δ → Fin Γ) (u v : Vec Nat Δ) → Γ ⊢ quot-coefs (u +coefs v) lift-var ≡ (quot-coefs u lift-var +e quot-coefs v lift-var)
quot-coefs-+ Γ zero lift-var [] [] =
  inj 0            ⊢≡⟨ ⊢sym ⊢inj-+ ⟩
  (inj 0 +e inj 0) ⊢∎
quot-coefs-+ Γ (succ Δ) lift-var (u ∷ us) (v ∷ vs) = let
    v0 = var (lift-var (zero Δ))
    qsum = quot-coefs (us +coefs vs) (λ v' → lift-var (succ v'))
    qus = quot-coefs us (λ v' → lift-var (succ v'))
    qvs = quot-coefs vs (λ v' → lift-var (succ v'))
  in
  (((u +N v) ⋅e v0) +e qsum)                 ⊢≡⟨ ⊢ap-+ (⊢+⋅e u v (var (lift-var (zero Δ)))) ⊢refl ⟩
  (((u ⋅e v0) +e (v ⋅e v0)) +e qsum)         ⊢≡⟨ ⊢ap-+ ⊢refl (quot-coefs-+ Γ Δ (λ v' → lift-var (succ v')) us vs) ⟩
  (((u ⋅e v0) +e (v ⋅e v0)) +e (qus +e qvs)) ⊢≡⟨ ⊢sym ⊢+-assoc ⟩
  ((u ⋅e v0) +e ((v ⋅e v0) +e (qus +e qvs))) ⊢≡⟨ ⊢ap-+ ⊢refl ⊢+-assoc ⟩
  ((u ⋅e v0) +e (((v ⋅e v0) +e qus) +e qvs)) ⊢≡⟨ ⊢ap-+ ⊢refl (⊢ap-+ ⊢+-comm ⊢refl) ⟩
  ((u ⋅e v0) +e ((qus +e (v ⋅e v0)) +e qvs)) ⊢≡⟨ ⊢ap-+ ⊢refl (⊢sym ⊢+-assoc) ⟩
  ((u ⋅e v0) +e (qus +e ((v ⋅e v0) +e qvs))) ⊢≡⟨ ⊢+-assoc ⟩
  (((u ⋅e v0) +e qus) +e ((v ⋅e v0) +e qvs)) ⊢∎

quot-+ : {Γ : Nat} (u v : NF Γ) → Γ ⊢ quot (u +NF v) ≡ (quot u +e quot v)
quot-+ {Γ} u v = let
    coefs-sum = quot-coefs (NF.coefs (u +NF v)) (λ v₁ → v₁)
    coefs-u = quot-coefs (NF.coefs u) (λ v' → v')
    coefs-v = quot-coefs (NF.coefs v) (λ v' → v')

    const-sum = inj (NF.constant (u +NF v))
    const-u = inj (NF.constant u)
    const-v = inj (NF.constant v)
  in
  const-sum +e coefs-sum                       ⊢≡⟨ ⊢ap-+ (⊢sym ⊢inj-+) ⊢refl ⟩
  (const-u +e const-v) +e coefs-sum            ⊢≡⟨ ⊢ap-+ ⊢refl (quot-coefs-+ Γ Γ (λ v' → v') (u .NF.coefs) (v .NF.coefs)) ⟩
  (const-u +e const-v) +e (coefs-u +e coefs-v) ⊢≡⟨ ⊢sym ⊢+-assoc ⟩
  const-u +e (const-v +e (coefs-u +e coefs-v)) ⊢≡⟨ ⊢ap-+ ⊢refl ⊢+-assoc ⟩
  const-u +e ((const-v +e coefs-u) +e coefs-v) ⊢≡⟨ ⊢ap-+ ⊢refl (⊢ap-+ ⊢+-comm ⊢refl) ⟩
  const-u +e ((coefs-u +e const-v) +e coefs-v) ⊢≡⟨ ⊢ap-+ ⊢refl (⊢sym ⊢+-assoc) ⟩
  const-u +e (coefs-u +e (const-v +e coefs-v)) ⊢≡⟨ ⊢+-assoc ⟩
  (const-u +e coefs-u) +e (const-v +e coefs-v) ⊢∎

quot-eval-correct : {Γ : Nat} (e : Expr Γ) → Γ ⊢ quot (eval e) ≡ e
quot-eval-correct {Γ} (var v) =
  inj 0 +e quot-coefs (single-coef v) (λ v₁ → v₁) ⊢≡⟨ ⊢zero-+ ⟩
  quot-coefs (single-coef v) (λ v₁ → v₁)          ⊢≡⟨ go Γ (λ v' → v') v ⟩
  var v                                           ⊢∎
  where
    go : (Δ : Nat) (lift-var : Fin Δ → Fin Γ) (v : Fin Δ) → Γ ⊢ quot-coefs (single-coef v) lift-var ≡ var (lift-var v)
    go (succ Δ) lift-var (zero .Δ) =
      (var (lift-var (zero Δ)) +e inj 0) +e quot-coefs (zeroes Δ) (λ v₁ → lift-var (succ v₁)) ⊢≡⟨ ⊢ap-+ ⊢refl (quot-coefs-zero Γ Δ λ v' → lift-var (succ v')) ⟩
      (var (lift-var (zero Δ)) +e inj 0) +e inj 0                                             ⊢≡⟨ ⊢ap-+ ⊢+-zero ⊢refl ⟩
      var (lift-var (zero Δ)) +e inj 0                                                        ⊢≡⟨ ⊢+-zero ⟩
      var (lift-var (zero Δ))                                                                 ⊢∎
    go (succ Δ) lift-var (succ v) =
      inj 0 +e quot-coefs (single-coef v) (λ v' → lift-var (succ v')) ⊢≡⟨ ⊢zero-+ ⟩
      quot-coefs (single-coef v) (λ v' → lift-var (succ v'))          ⊢≡⟨ go Δ (λ v' → lift-var (succ v')) v ⟩
      var (lift-var (succ v))                                         ⊢∎
quot-eval-correct {Γ} (inj n) =
  inj n +e quot-coefs (NF.coefs (eval (inj n))) (λ v → v) ⊢≡⟨ ⊢ap-+ ⊢refl (quot-coefs-zero Γ Γ (λ v → v)) ⟩
  inj n +e inj 0                                          ⊢≡⟨ ⊢+-zero ⟩
  inj n                                                   ⊢∎
quot-eval-correct (u +e v) =
  inj (eval (u +e v) .NF.constant) +e quot-coefs (eval (u +e v) .NF.coefs) (λ v' → v') ⊢≡⟨ quot-+ (eval u) (eval v) ⟩
  quot (eval u) +e quot (eval v)                                                       ⊢≡⟨ ⊢ap-+ (quot-eval-correct u) ⊢refl ⟩
  u +e quot (eval v)                                                                   ⊢≡⟨ ⊢ap-+ ⊢refl (quot-eval-correct v) ⟩
  u +e v                                                                               ⊢∎

eval-preservation : {Γ : Nat} {u v : Expr Γ} → Γ ⊢ u ≡ v → eval u ≡ eval v
eval-preservation ⊢refl = refl
eval-preservation (⊢sym p) = sym (eval-preservation p)
eval-preservation (⊢trans p q) = trans (eval-preservation p) (eval-preservation q)
eval-preservation (⊢+-comm {u} {v}) = +NF-comm (eval u) (eval v)
eval-preservation (⊢+-assoc {u} {v} {w}) = +NF-assoc (eval u) (eval v) (eval w)
eval-preservation ⊢inj-+ = ap2 mk-NF refl (+coefs-zero (zeroes _))
eval-preservation ⊢+-zero = ap2 mk-NF (+N-zero _) (+coefs-zero _)
eval-preservation (⊢ap-+ p q) = ap2 _+NF_ (eval-preservation p) (eval-preservation q)

eval-reflect : {Γ : Nat} {u v : Expr Γ} → eval u ≡ eval v → Γ ⊢ u ≡ v
eval-reflect {Γ} {u} {v} p =
  u             ⊢≡⟨ ⊢sym (quot-eval-correct u) ⟩
  quot (eval u) ⊢≡⟨ ⊢≡ (ap quot p) ⟩
  quot (eval v) ⊢≡⟨ quot-eval-correct v ⟩
  v             ⊢∎

theorem : {Γ : Nat} (u v : Expr Γ) → Γ ⊢ (u +e inj 1) ≡ (v +e inj 1) → Γ ⊢ u ≡ v
theorem u v p =
  u ⊢≡⟨ eval-reflect (+NF-inj (eval u) (eval v) (NF-inj 1) (eval-preservation p)) ⟩
  v ⊢∎