{-# 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.