-- Typed βη equality for the simply typed lambda calculus.
--
-- β would be the same for the untyped lambda calculus,
-- but for η it is convenient that we have the type information.

module Term.Equality where

open import Prelude
open import Term
open import Term.Weakening
open import Term.Substitution

open import Term.Weakening.Properties using (wk1-wk)
open import Term.Substitution.Properties using (wk-sg; sub-sg; wk1-sub)

private
  variable
    Γ Δ : Context
    a b : Ty
    t t' t'' t₁ t₂ t₃ u u' : Term Γ a
    σ σ' : Sub Γ Δ
    ρ ρ' : Wk Γ Δ

infix  _≅_

-- t ≅ t' is the congruence generated by axioms from β and η,
-- congruence meaning that it is an equivalence relation (refl, trans, sym)
-- and closed under all term constructors (abs, app).
--
-- Closure under weakening and substitution is proven subsequently.

data _≅_ : (t t' : Term Γ a) → Set where
  β      : app (abs t) u ≅ t [ u ]₀
  η      : {t : Term Γ (a ⇒ b)} → t ≅ abs (app (wk1 t) (var zero))
  abs    : (et : t ≅ t') → abs t ≅ abs t'
  app    : (et : t ≅ t') (eu : u ≅ u') → app t u ≅ app t' u'
  refl   : t ≅ t
  ≅trans : (e₁ : t₁ ≅ t₂) (e₂ : t₂ ≅ t₃) → t₁ ≅ t₃
  ≅sym   : (e : t ≅ t') → t' ≅ t

-- Closure of t ≅ t' under weakening.
--
-- Proof by induction on t ≅ t'.
-- Only the base cases (β and η) are interesting, they need properties
-- about weakening and substitution.

wk-≅ : t ≅ t' → wk ρ t ≅ wk ρ t'

-- Case β-contraction: Show wk ρ (app (abs t) u) ≅  wk ρ (t [ u ]₀).
-- By definition of wk:     wk ρ (app (abs t) u) = app (abs (wk (keep ρ) t)) (wk ρ u)
-- Thus, β gives:           wk ρ (app (abs t) u) ≅ (wk (keep ρ) t) [ wk ρ u ]₀
-- We need the fact that wk over the single substitution,
--    wk-sg : (wk (keep ρ) t) [ wk ρ u ]₀ ≡ wk ρ (t [ u ]₀)
-- to conclude the proof by a cast ("subst").
wk-≅ {ρ = ρ} (β {t = t} {u = u}) =
  subst
    (app (abs (wk (keep ρ) t)) (wk ρ u) ≅_)
    (wk-sg {t = t})  -- wk (keep ρ) t) [ wk ρ u ]₀  ≡ wk ρ (t [ u ]₀)
    β

-- Case η-expansion: Show wk ρ t ≅ wk ρ (abs (app (wk1 t) (var zero)))
--                               = abs (wk (keep ρ) (app (wk1 t) (var zero)))
--                               = abs (app (wk (keep ρ) (wk1 t)) (wk (keep ρ) (var zero)))
--                               = abs (app (wk (keep ρ) (wk1 t)) (var (lookup (keep ρ) zero)))
--                               = abs (app (wk (keep ρ) (wk1 t)) (var zero))
-- η gives  wk ρ t ≅ abs (app (wk1 (wk ρ t)) (var zero)
-- So we need to cast with  wk1-wk : wk1 (wk ρ t) ≡ wk (keep ρ) (wk1 t).
wk-≅ {ρ = ρ} (η {t = t}) =
  subst
    (λ u → wk ρ t ≅ abs (app u (var zero)))
    wk1-wk
    (η {t = wk ρ t})

-- Other cases by induction hypothesis:
wk-≅ (abs e)             = abs (wk-≅ e)
wk-≅ (app e e₁)          = app (wk-≅ e) (wk-≅ e₁)
wk-≅ refl                = refl
wk-≅ (≅trans e e₁)       = ≅trans (wk-≅ e) (wk-≅ e₁)
wk-≅ (≅sym e)            = ≅sym (wk-≅ e)

-- Closure of t ≅ t' under substitution.
--
-- Proof by induction on t ≅ t'.
-- Only the base cases (β and η) are interesting, they need the substitution laws.

sub-≡ : t ≅ t' → sub σ t ≅ sub σ t'

-- Case β-contraction: sub σ (app (abs t) u) ≅ sub σ (t [ u ]₀)
sub-≡ {σ = σ} (β {t = t} {u = u}) =
  subst
    (app (abs (sub (lift σ) t)) (sub σ u) ≅_)
    (sym (sub-sg {σ = σ} {t = t} {u = u}))
    β

-- Case η-expansion: sub σ t ≅ sub σ (abs (app (wk1 t) (var zero)))
sub-≡ {σ = σ} (η {t = t}) =
  subst
    (λ u → sub σ t ≅ abs (app u (var zero)))
    (wk1-sub {σ = σ} {t = t})
    (η {t = sub σ t})

-- Other cases by induction hypothesis:
sub-≡ {σ = σ} (abs e)       = abs (sub-≡ e)
sub-≡ {σ = σ} (app e e₁)    = app (sub-≡ e) (sub-≡ e₁)
sub-≡ {σ = σ} refl          = refl
sub-≡ {σ = σ} (≅trans e e₁) = ≅trans (sub-≡ e) (sub-≡ e₁)
sub-≡ {σ = σ} (≅sym e)      = ≅sym (sub-≡ e)