{-# OPTIONS --without-K #-}
module IK.Norm.Properties.Soundness where

open import Relation.Binary.PropositionalEquality
  using (_≡_ ; cong ; cong₂ ; trans)

open import IK.Norm.Base

open import IK.Norm.NbE.Model
open import IK.Norm.NbE.Reification

open import IK.Norm.Properties.Soundness.Trace

open import IK.Term

-- This module proves the completeness of evaluation (eval-complete),
-- from which the soundness of normalization (norm-sound) follows.

eval-complete : {t t' : Tm Γ a}
   ({Δ : Ctx} {γ : Sub' Δ Γ}  eval t γ  eval t' γ)
   t  t'
eval-complete {t = t} {t'} f with f {_} {idₛ'}
... | p = ≈-trans
    (⟶*-to-≈ (trace t))
    (≈-reflexive (cong embNf (cong reify p))))
  (≈-sym (⟶*-to-≈ (trace t')))

norm-sound : norm t  norm u  t  u
norm-sound {t = t} {u} t'≡u' = ≈-trans
  (⟶*-to-≈ (trace t))
    (≈-reflexive (cong embNf t'≡u'))
    (≈-sym (⟶*-to-≈ (trace u))))

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.