```------------------------------------------------------------------------
-- The semantics is deterministic
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

open import Atom

module Deterministic (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)
open import Tactic.By

open import Chi atoms

open χ-atoms atoms

Lookup-deterministic :
∀ {c₁ c₂ bs xs₁ xs₂ e₁ e₂} →
Lookup c₁ bs xs₁ e₁ → Lookup c₂ bs xs₂ e₂ →
c₁ ≡ c₂ → xs₁ ≡ xs₂ × e₁ ≡ e₂
Lookup-deterministic here          here          _    = refl , refl
Lookup-deterministic here          (there q _)   refl = ⊥-elim (q refl)
Lookup-deterministic (there p _)   here          refl = ⊥-elim (p refl)
Lookup-deterministic (there p₁ p₂) (there q₁ q₂) refl =
Lookup-deterministic p₂ q₂ refl

↦-deterministic :
∀ {e xs es e₁ e₂} →
e [ xs ← es ]↦ e₁ → e [ xs ← es ]↦ e₂ → e₁ ≡ e₂
↦-deterministic []    []    = refl
↦-deterministic (∷ p) (∷ q) = by (↦-deterministic p q)

mutual

⇓-deterministic : ∀ {e v₁ v₂} → e ⇓ v₁ → e ⇓ v₂ → v₁ ≡ v₂
⇓-deterministic (apply p₁ p₂ p₃) (apply q₁ q₂ q₃)
with ⇓-deterministic p₁ q₁ | ⇓-deterministic p₂ q₂
... | refl | refl = ⇓-deterministic p₃ q₃

⇓-deterministic (case p₁ p₂ p₃ p₄) (case q₁ q₂ q₃ q₄)
with ⇓-deterministic p₁ q₁
... | refl with Lookup-deterministic p₂ q₂ refl
...   | refl , refl rewrite ↦-deterministic p₃ q₃ =
⇓-deterministic p₄ q₄

⇓-deterministic (rec p)    (rec q)    = ⇓-deterministic p q
⇓-deterministic lambda     lambda     = refl
⇓-deterministic (const ps) (const qs) = by (⇓⋆-deterministic ps qs)

⇓⋆-deterministic : ∀ {es vs₁ vs₂} → es ⇓⋆ vs₁ → es ⇓⋆ vs₂ → vs₁ ≡ vs₂
⇓⋆-deterministic []       []       = refl
⇓⋆-deterministic (p ∷ ps) (q ∷ qs) =
cong₂ _∷_ (⇓-deterministic p q) (⇓⋆-deterministic ps qs)
```