{-# OPTIONS --safe --without-K #-}
module IK.Term.Conversion where

open import PEUtil

open import IK.Term.Base
open import IK.Term.Reduction
  as Reduction

import Data.Sum as Sum

open import Relation.Nullary
  using (¬_)

open import Relation.Binary
  using (Setoid)

open import Relation.Binary.Construct.Closure.Equivalence
  using (setoid)
import Relation.Binary.Construct.Closure.Equivalence.Properties
  as EquivalenceProperties

open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  as ReflexiveTransitive
  using (Star)

open import Relation.Binary.PropositionalEquality
  using    (_≡_ ; cong ; cong₂)
  renaming (refl to ≡-refl ; sym to ≡-sym ; trans to ≡-trans)

open Sum public
  using (inj₁ ; inj₂)
open ReflexiveTransitive public
  using (ε ; _◅_)
open EquivalenceProperties public
  using    ()
  renaming (a—↠b⇒a↔b to ⟶*-to-≈)

-- Convertibility is defined by taking the equivalence closure of the
-- reduction relation `_⟶_`, i.e. two terms `t` and `u` are
-- convertible (written `t ≈ u`) if and only if there is a sequence of
-- terms `sᵢ` for i = 0,…,n such that 1. `s₀ = t`, 2. `sₙ = u`, and
-- 3. `sᵢ ⟶ sᵢ₊₁` or `sᵢ₊₁ ⟶ sᵢ` for all i.
--
-- Note that `_⟶_` is already a congruence, i.e. `u ⟶ v` implies `t[u]
-- ⟶ t[v]`, and being a congruence preserved by closing under
-- reflexivity, symmetry and transitivity.
Tm-setoid : (Γ : Ctx) → (a : Ty) → Setoid _ _
Tm-setoid Γ a = setoid (_⟶_ {Γ} {a})

module _ {Γ : Ctx} {a : Ty} where
  open Setoid (Tm-setoid Γ a) public
    using    (_≈_)
    renaming (refl to ≈-refl ; reflexive to ≈-reflexive ; sym to ≈-sym ; trans to ≈-trans ; isEquivalence to ≈-equiv)

≈-reflexive˘ : t' ≡ t → t ≈ t'
≈-reflexive˘ t'≡t = ≈-reflexive (≡-sym t'≡t)

⟶-to-≈ : t ⟶ t' → t ≈ t'
⟶-to-≈ p = inj₁ p ◅ ε

module _ {t : Tm Γ a → Tm Δ b} (cong-t : ∀ {u u' : Tm Γ a} → (u⟶u' : u ⟶ u') → t u ⟶ t u') where
  cong-⟶-to-cong-≈ : ∀ (u≈u' : u ≈ u') → t u ≈ t u'
  cong-⟶-to-cong-≈ ε                     = ε
  cong-⟶-to-cong-≈ (inj₁ u⟶u'' ◅ u''≈u') = inj₁ (cong-t u⟶u'') ◅ cong-⟶-to-cong-≈ u''≈u'
  cong-⟶-to-cong-≈ (inj₂ u⟵u'' ◅ u''≈u') = inj₂ (cong-t u⟵u'') ◅ cong-⟶-to-cong-≈ u''≈u'

red-fun≈ : (t : Tm (Γ `, a) b) (u : Tm Γ a) → (app (lam t) u) ≈ substTm (idₛ `, u) t
red-fun≈ t u = ⟶-to-≈ Reduction.red-fun

exp-fun≈ : (t : Tm Γ (a ⇒ b)) → t ≈ lam (app (wkTm fresh t) (var zero))
exp-fun≈ t = ⟶-to-≈ Reduction.exp-fun

red-box≈ : (t : Tm (ΓL #) a) (e : LFExt Γ (ΓL #) ΓR) → unbox (box t) e ≈ wkTm (LFExtToWk e) t
red-box≈ t e = ⟶-to-≈ Reduction.red-box

exp-box≈ : (t : Tm Γ (□ a)) → t ≈ box (unbox t new)
exp-box≈ t = ⟶-to-≈ Reduction.exp-box

cong-lam≈ : ∀ (t≈t' : t ≈ t') → lam t ≈ lam t'
cong-lam≈ = cong-⟶-to-cong-≈ Reduction.cong-lam

cong-app≈≡ : ∀ (t≈t' : t ≈ t') (u≡u' : u ≡ u') → app t u ≈ app t' u
cong-app≈≡ t≈t' ≡-refl = cong-⟶-to-cong-≈ Reduction.cong-app1 t≈t'

cong-app1≈ : ∀ (t≈t' : t ≈ t') → app t u ≈ app t' u
cong-app1≈ t≈t' = cong-app≈≡ t≈t' ≡-refl

cong-app≡≈ : ∀ (t≡t' : t ≡ t') (u≈u' : u ≈ u') → app t u ≈ app t' u'
cong-app≡≈ ≡-refl u≈u' = cong-⟶-to-cong-≈ Reduction.cong-app2 u≈u'

cong-app2≈ : ∀ (u≈u' : u ≈ u') → app t u ≈ app t u'
cong-app2≈ u≈u' = cong-app≡≈ ≡-refl u≈u'

cong-app≈ : ∀ (t≈t' : t ≈ t') (u≈u' : u ≈ u') → app t u ≈ app t' u'
cong-app≈ t≈t' u≈u' = ≈-trans (cong-app1≈ t≈t') (cong-app2≈ u≈u')

cong-box≈ : ∀ (t≈t' : t ≈ t') → box t ≈ box t'
cong-box≈ = cong-⟶-to-cong-≈ Reduction.cong-box

cong-unbox≈ : ∀ (t≈t' : t ≈ t') → unbox t e ≈ unbox t' e
cong-unbox≈ = cong-⟶-to-cong-≈ Reduction.cong-unbox

module _ {t : Tm ΓL (□ a)} {e : LFExt Γ (ΓL  #) ΓR} {e' : LFExt Γ (ΓL #) ΓR'} where
  cong-unbox2≈ : unbox t e ≈ unbox t e'
  cong-unbox2≈ = ≈-reflexive (dcong₂ (λ _ΓR → unbox t) (extRUniq e e') (ExtIsProp′ e e'))

cong-unbox≈′ : ∀ (t≈t' : t ≈ t') → unbox t e ≈ unbox t' e'
cong-unbox≈′ t≈t' = ≈-trans (cong-unbox≈ t≈t') cong-unbox2≈

cong-unbox≈′′ : ∀ (Γ≡Γ' : Γ ≡ Γ') (t≈t' : subst1 Tm Γ≡Γ' t ≈ t') → unbox t e ≈ unbox t' e'
cong-unbox≈′′ ≡-refl = cong-unbox≈′

--------------------
-- Derived equations
--------------------

Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.