------------------------------------------------------------------------
-- Properties for the reduction relation of the target language.
------------------------------------------------------------------------

module Graded.Erasure.Target.Properties.Reduction where

open import Graded.Erasure.Target

open import Tools.Empty
open import Tools.Function
open import Tools.Nat
import Tools.PropositionalEquality as PE
open import Tools.Relation
open import Tools.Sum

private
  variable
    k n : Nat
    t t′ u u′ : Term n
    s : Strictness

-- Reduction properties

-- Concatenation of reduction closure

red*concat : t ⇒* t′ → t′ ⇒* u → t ⇒* u
red*concat refl t′⇒*u = t′⇒*u
red*concat (trans x t⇒*t′) t′⇒*u = trans x (red*concat t⇒*t′ t′⇒*u)

-- Closure of substitution reductions

app-subst* : t ⇒* t′ → t ∘⟨ s ⟩ u ⇒* t′ ∘⟨ s ⟩ u
app-subst* refl = refl
app-subst* (trans x t⇒*t′) = trans (app-subst x) (app-subst* t⇒*t′)

app-subst*-arg : Value t → u ⇒* u′ → t ∘⟨ strict ⟩ u ⇒* t ∘⟨ strict ⟩ u′
app-subst*-arg _   refl                = refl
app-subst*-arg val (trans u⇒u′ u′⇒*u″) =
  trans (app-subst-arg val u⇒u′) (app-subst*-arg val u′⇒*u″)

fst-subst* : t ⇒* t′ → fst t ⇒* fst t′
fst-subst* refl = refl
fst-subst* (trans x t⇒*t′) = trans (fst-subst x) (fst-subst* t⇒*t′)

snd-subst* : t ⇒* t′ → snd t ⇒* snd t′
snd-subst* refl = refl
snd-subst* (trans x t⇒*t′) = trans (snd-subst x) (snd-subst* t⇒*t′)

natrec-subst* : ∀ {z s} → t ⇒* t′ → natrec z s t ⇒* natrec z s t′
natrec-subst* refl = refl
natrec-subst* (trans x t⇒t′) = trans (natrec-subst x) (natrec-subst* t⇒t′)

prodrec-subst* : t ⇒* t′ → prodrec t u ⇒* prodrec t′ u
prodrec-subst* refl = refl
prodrec-subst* (trans x t⇒t′) = trans (prodrec-subst x) (prodrec-subst* t⇒t′)

unitrec-subst* : t ⇒* t′ → unitrec t u ⇒* unitrec t′ u
unitrec-subst* refl = refl
unitrec-subst* (trans x d) = trans (unitrec-subst x) (unitrec-subst* d)

-- Values do not reduce.

opaque

  Value→¬⇒ : Value t → ¬ t ⇒ u
  Value→¬⇒ lam  ()
  Value→¬⇒ prod ()
  Value→¬⇒ zero ()
  Value→¬⇒ suc  ()
  Value→¬⇒ star ()
  Value→¬⇒ ↯    ()

opaque

  -- Reduction is deterministic.

  redDet : (u : Term n) → u ⇒ t → u ⇒ t′ → t PE.≡ t′
  redDet _ = λ where
    (app-subst p) → λ where
      (app-subst q)       → PE.cong (_∘⟨ _ ⟩ _) $ redDet _ p q
      (app-subst-arg v _) → ⊥-elim $ Value→¬⇒ v p
      (β-red _)           → case p of λ ()
    (app-subst-arg v p) → λ where
      (app-subst q)       → ⊥-elim $ Value→¬⇒ v q
      (app-subst-arg _ q) → PE.cong (_ ∘⟨ _ ⟩_) $ redDet _ p q
      (β-red v)           → ⊥-elim $ Value→¬⇒ v p
    (β-red v) → λ where
      (app-subst ())
      (app-subst-arg _ q) → ⊥-elim $ Value→¬⇒ v q
      (β-red _)           → PE.refl
    (fst-subst p) → λ where
      (fst-subst q) → PE.cong fst $ redDet _ p q
      Σ-β₁          → case p of λ ()
    (snd-subst p) → λ where
      (snd-subst q) → PE.cong snd $ redDet _ p q
      Σ-β₂          → case p of λ ()
    Σ-β₁ → λ where
      (fst-subst ())
      Σ-β₁           → PE.refl
    Σ-β₂ → λ where
      (snd-subst ())
      Σ-β₂           → PE.refl
    (prodrec-subst p) → λ where
      (prodrec-subst q) → PE.cong (flip prodrec _) $ redDet _ p q
      prodrec-β         → case p of λ ()
    prodrec-β → λ where
      (prodrec-subst ())
      prodrec-β          → PE.refl
    (natrec-subst p) → λ where
      (natrec-subst q) → PE.cong (natrec _ _) $ redDet _ p q
      natrec-zero      → case p of λ ()
      natrec-suc       → case p of λ ()
    natrec-zero → λ where
      (natrec-subst ())
      natrec-zero       → PE.refl
    natrec-suc → λ where
      (natrec-subst ())
      natrec-suc        → PE.refl
    (unitrec-subst p) → λ where
      (unitrec-subst q) → PE.cong (flip unitrec _) $ redDet _ p q
      unitrec-β         → case p of λ ()
    unitrec-β → λ where
      (unitrec-subst ())
      unitrec-β          → PE.refl

-- Reduction closure is deterministic
-- (there is only one reduction path)
-- If a ⇒* b and a ⇒* c then b ⇒* c or c ⇒* b

red*Det : u ⇒* t → u ⇒* t′ → (t ⇒* t′) ⊎ (t′ ⇒* t)
red*Det refl refl = inj₁ refl
red*Det refl (trans x u⇒t′) = inj₁ (trans x u⇒t′)
red*Det (trans x u⇒t) refl = inj₂ (trans x u⇒t)
red*Det {u = u} (trans x u⇒t) (trans x₁ u⇒t′)
  rewrite redDet u x x₁ = red*Det u⇒t u⇒t′

-- Non-reducible terms

↯-noRed : ↯ ⇒* t → t PE.≡ ↯
↯-noRed refl         = PE.refl
↯-noRed (trans () _)

zero-noRed : zero ⇒* t → t PE.≡ zero
zero-noRed refl         = PE.refl
zero-noRed (trans () _)

suc-noRed : suc t ⇒* t′ → t′ PE.≡ suc t
suc-noRed refl         = PE.refl
suc-noRed (trans () _)

prod-noRed : prod t t′ ⇒* u → u PE.≡ prod t t′
prod-noRed refl         = PE.refl
prod-noRed (trans () _)

star-noRed : star ⇒* t → t PE.≡ star
star-noRed refl         = PE.refl
star-noRed (trans () _)

opaque

  Value→⇒*→≡ : Value t → t ⇒* u → u PE.≡ t
  Value→⇒*→≡ = λ where
    lam  refl          → PE.refl
    prod refl          → PE.refl
    zero refl          → PE.refl
    suc  refl          → PE.refl
    star refl          → PE.refl
    ↯    refl          → PE.refl
    t-v  (trans t⇒u _) → ⊥-elim $ Value→¬⇒ t-v t⇒u

opaque

  -- If t is a value, then Value⟨ s ⟩ t holds.

  Value→Value⟨⟩ : Value t → Value⟨ s ⟩ t
  Value→Value⟨⟩ {s = strict}     v = v
  Value→Value⟨⟩ {s = non-strict} _ = _

opaque

  -- Numerals are values.

  Numeral→Value : Numeral t → Value t
  Numeral→Value zero    = zero
  Numeral→Value (suc _) = suc

opaque

  -- The term sucᵏ k is a value.

  Value-sucᵏ : Value (sucᵏ {n = n} k)
  Value-sucᵏ {k = }    = zero
  Value-sucᵏ {k = 1+ _} = suc