open import Definition.Typed.Restrictions
open import Graded.Modality
module Definition.Typed.Reasoning.Reduction.Primitive
{β} {M : Set β}
{π : Modality M}
(R : Type-restrictions π)
where
open import Definition.Typed R
open import Definition.Typed.RedSteps R
open import Definition.Untyped M
open import Tools.Function
import Tools.PropositionalEquality as PE
private variable
A B t u v : Term _
Ξ : Con Term _
infix -1 finally-β* finally-β
infixr -2 step-β step-β* finally-β*β‘ finally-ββ‘
step-β : β t β Ξ β’ u β* v β· A β Ξ β’ t β u β· A β Ξ β’ t β* v β· A
step-β _ = flip _β¨_
syntax step-β t uβv tβu = t ββ¨ tβu β© uβv
{-# INLINE step-β #-}
step-β* : β t β Ξ β’ u β* v β· A β Ξ β’ t β* u β· A β Ξ β’ t β* v β· A
step-β* _ = flip _β¨β·*_
syntax step-β* t uβv tβu = t β*β¨ tβu β© uβv
{-# INLINE step-β* #-}
finally-β* : β t u β Ξ β’ t β* u β· A β Ξ β’ t β* u β· A
finally-β* _ _ tβu = tβu
syntax finally-β* t u tβu = t β*β¨ tβu β©β u β
{-# INLINE finally-β* #-}
finally-β : β t u β Ξ β’ t β u β· A β Ξ β’ u β· A β Ξ β’ t β* u β· A
finally-β _ _ tβu β’u = tβu β¨ id β’u
syntax finally-β t u tβu β’u = t ββ¨ tβu , β’u β©β u β
{-# INLINE finally-β #-}
finally-β*β‘ : β t β u PE.β‘ v β Ξ β’ t β* u β· A β Ξ β’ t β* v β· A
finally-β*β‘ _ PE.refl tβu = tβu
syntax finally-β*β‘ t uβ‘v tβu = t β*β¨ tβu β©ββ‘ uβ‘v
finally-ββ‘ : β t β u PE.β‘ v β Ξ β’ t β u β· A β Ξ β’ u β· A β Ξ β’ t β* v β· A
finally-ββ‘ _ PE.refl = finally-β _ _
syntax finally-ββ‘ t uβ‘v tβu = t ββ¨ tβu β©ββ‘ uβ‘v
infix -1 finally-β* finally-β
infixr -2 step-β step-β* finally-β*β‘ finally-ββ‘
opaque
step-β :
β v β Ξ β’ t β* u β· A β Ξ β’ u β v β· A β Ξ β’ v β· A β Ξ β’ t β* v β· A
step-β _ tβu uβv β’v = tβu β¨β·* (uβv β¨ id β’v)
syntax step-β v tβu uβv β’v = v ββ¨ uβv , β’v β© tβu
step-β* : β v β Ξ β’ t β* u β· A β Ξ β’ u β* v β· A β Ξ β’ t β* v β· A
step-β* _ = _β¨β·*_
syntax step-β* v tβu uβv = v β*β¨ uβv β© tβu
{-# INLINE step-β* #-}
finally-β* : β u t β Ξ β’ t β* u β· A β Ξ β’ t β* u β· A
finally-β* _ _ tβu = tβu
syntax finally-β* u t tβu = u β*β¨ tβu β©β t β
{-# INLINE finally-β* #-}
finally-β : β u t β Ξ β’ t β u β· A β Ξ β’ u β· A β Ξ β’ t β* u β· A
finally-β _ _ tβu β’u = tβu β¨ id β’u
syntax finally-β u t tβu β’u = u ββ¨ tβu , β’u β©β t β
{-# INLINE finally-β #-}
finally-β*β‘ : β v β u PE.β‘ t β Ξ β’ v β* u β· A β Ξ β’ v β* t β· A
finally-β*β‘ _ PE.refl vβu = vβu
syntax finally-β*β‘ v uβ‘t vβu = v β*β¨ vβu β©ββ‘ uβ‘t
finally-ββ‘ : β v β u PE.β‘ t β Ξ β’ v β u β· A β Ξ β’ u β· A β Ξ β’ v β* t β· A
finally-ββ‘ _ PE.refl = finally-β _ _
syntax finally-ββ‘ v uβ‘t vβu β’u = v ββ¨ vβu , β’u β©ββ‘ uβ‘t
infix -1 _ββ¨_β©β
infixr -2 step-β‘ step-β‘Λ _β‘β¨β©β_
step-β‘ : β t β Ξ β’ u β* v β· A β t PE.β‘ u β Ξ β’ t β* v β· A
step-β‘ _ uβv PE.refl = uβv
syntax step-β‘ t uβv tβ‘u = t β‘β¨ tβ‘u β©β uβv
step-β‘Λ : β t β Ξ β’ u β* v β· A β u PE.β‘ t β Ξ β’ t β* v β· A
step-β‘Λ _ uβv PE.refl = uβv
syntax step-β‘Λ t uβv uβ‘t = t β‘Λβ¨ uβ‘t β©β uβv
_β‘β¨β©β_ : β t β Ξ β’ t β* u β· A β Ξ β’ t β* u β· A
_ β‘β¨β©β tβu = tβu
{-# INLINE _β‘β¨β©β_ #-}
_ββ¨_β©β : β t β Ξ β’ t β· A β Ξ β’ t β* t β· A
_ ββ¨ β’t β©β = id β’t
{-# INLINE _ββ¨_β©β #-}
infix -1
finally-β*β· finally-ββ·
infixr -2
step-ββ· step-β*β· step-β*β·β‘ step-β*β·β‘Λ _β·_β‘β¨β©ββ·_ finally-β*β·β‘
finally-ββ·β‘
step-ββ· : β t A β Ξ β’ u β* v β· A β Ξ β’ t β u β· A β Ξ β’ t β* v β· A
step-ββ· _ _ = flip _β¨_
syntax step-ββ· t A uβv tβu = t β· A ββ¨ tβu β©β· uβv
{-# INLINE step-ββ· #-}
step-β*β· : β t A β Ξ β’ u β* v β· A β Ξ β’ t β* u β· A β Ξ β’ t β* v β· A
step-β*β· _ _ = flip _β¨β·*_
syntax step-β*β· t A uβv tβu = t β· A β*β¨ tβu β©β· uβv
{-# INLINE step-β*β· #-}
step-β*β·β‘ : β t A β Ξ β’ u β* v β· A β t PE.β‘ u β Ξ β’ t β* v β· A
step-β*β·β‘ _ _ uβv PE.refl = uβv
syntax step-β*β·β‘ t A uβv tβ‘u = t β· A β‘β¨ tβ‘u β©ββ· uβv
step-β*β·β‘Λ : β t A β Ξ β’ u β* v β· A β u PE.β‘ t β Ξ β’ t β* v β· A
step-β*β·β‘Λ _ _ uβv PE.refl = uβv
syntax step-β*β·β‘Λ t A uβv uβ‘t = t β· A β‘Λβ¨ uβ‘t β©ββ· uβv
_β·_β‘β¨β©ββ·_ : β t A β Ξ β’ t β* u β· A β Ξ β’ t β* u β· A
_ β· _ β‘β¨β©ββ· tβu = tβu
{-# INLINE _β·_β‘β¨β©ββ·_ #-}
finally-β*β· : β t A u β Ξ β’ t β* u β· A β Ξ β’ t β* u β· A
finally-β*β· _ _ _ tβu = tβu
syntax finally-β*β· t A u tβu = t β· A β*β¨ tβu β©ββ· u β
{-# INLINE finally-β*β· #-}
finally-ββ· : β t A u β Ξ β’ t β u β· A β Ξ β’ u β· A β Ξ β’ t β* u β· A
finally-ββ· _ _ _ tβu β’u = tβu β¨ id β’u
syntax finally-ββ· t A u tβu β’u = t β· A ββ¨ tβu , β’u β©ββ· u β
{-# INLINE finally-ββ· #-}
finally-β*β·β‘ : β t A β u PE.β‘ v β Ξ β’ t β* u β· A β Ξ β’ t β* v β· A
finally-β*β·β‘ _ _ PE.refl tβu = tβu
syntax finally-β*β·β‘ t A uβ‘v tβu = t β· A β*β¨ tβu β©ββ·β‘ uβ‘v
finally-ββ·β‘ :
β t A β u PE.β‘ v β Ξ β’ t β u β· A β Ξ β’ u β· A β Ξ β’ t β* v β· A
finally-ββ·β‘ _ _ PE.refl = finally-β _ _
syntax finally-ββ·β‘ t A uβ‘v tβu = t β· A ββ¨ tβu β©ββ·β‘ uβ‘v
infix -1
finally-β*β· finally-ββ·
infixr -2
step-ββ· step-β*β· step-β*β·β‘ step-β*β·β‘Λ _β·_β‘β¨β©ββ·_ finally-β*β·β‘
finally-ββ·β‘
opaque
step-ββ· :
β v A β Ξ β’ t β* u β· A β Ξ β’ u β v β· A β Ξ β’ v β· A β Ξ β’ t β* v β· A
step-ββ· _ _ tβu uβv β’v = tβu β¨β·* (uβv β¨ id β’v)
syntax step-ββ· v A tβu uβv β’v = v β· A ββ¨ uβv , β’v β©β· tβu
step-β*β· : β v A β Ξ β’ t β* u β· A β Ξ β’ u β* v β· A β Ξ β’ t β* v β· A
step-β*β· _ _ = _β¨β·*_
syntax step-β*β· v A tβu uβv = v β· A β*β¨ uβv β©β· tβu
{-# INLINE step-β*β· #-}
step-β*β·β‘ : β v A β Ξ β’ t β* u β· A β v PE.β‘ u β Ξ β’ t β* v β· A
step-β*β·β‘ _ _ tβu PE.refl = tβu
syntax step-β*β·β‘ v A tβu vβ‘u = v β· A β‘β¨ vβ‘u β©ββ· tβu
step-β*β·β‘Λ : β v A β Ξ β’ t β* u β· A β u PE.β‘ v β Ξ β’ t β* v β· A
step-β*β·β‘Λ _ _ tβu PE.refl = tβu
syntax step-β*β·β‘Λ v A tβu uβ‘v = v β· A β‘Λβ¨ uβ‘v β©ββ· tβu
_β·_β‘β¨β©ββ·_ : β u A β Ξ β’ t β* u β· A β Ξ β’ t β* u β· A
_ β· _ β‘β¨β©ββ· tβu = tβu
{-# INLINE _β·_β‘β¨β©ββ·_ #-}
finally-β*β· : β u A t β Ξ β’ t β* u β· A β Ξ β’ t β* u β· A
finally-β*β· _ _ _ tβu = tβu
syntax finally-β*β· u A t tβu = u β· A β*β¨ tβu β©ββ· t β
{-# INLINE finally-β*β· #-}
finally-ββ· : β u A t β Ξ β’ t β u β· A β Ξ β’ u β· A β Ξ β’ t β* u β· A
finally-ββ· _ _ _ tβu β’u = tβu β¨ id β’u
syntax finally-ββ· u A t tβu β’u = u β· A ββ¨ tβu , β’u β©ββ· t β
{-# INLINE finally-ββ· #-}
finally-β*β·β‘ : β v A β u PE.β‘ t β Ξ β’ v β* u β· A β Ξ β’ v β* t β· A
finally-β*β·β‘ _ _ PE.refl vβu = vβu
syntax finally-β*β·β‘ v A uβ‘t vβu = v β· A β*β¨ vβu β©ββ·β‘ uβ‘t
finally-ββ·β‘ :
β v A β u PE.β‘ t β Ξ β’ v β u β· A β Ξ β’ u β· A β Ξ β’ v β* t β· A
finally-ββ·β‘ _ _ PE.refl = finally-β _ _
syntax finally-ββ·β‘ v A uβ‘t vβu β’u = v β· A ββ¨ vβu , β’u β©ββ·β‘ uβ‘t
infix -1 _β·_ββ¨_β©β
_β·_ββ¨_β©β : β t A β Ξ β’ t β· A β Ξ β’ t β* t β· A
_ β· _ ββ¨ β’t β©β = id β’t
{-# INLINE _β·_ββ¨_β©β #-}
infix -2 step-β*-conv step-β*-convΛ step-β*-conv-β‘ step-β*-conv-β‘Λ
opaque
step-β*-conv : Ξ β’ t β* u β· B β Ξ β’ A β‘ B β Ξ β’ t β* u β· A
step-β*-conv tβu Aβ‘B = conv* tβu (sym Aβ‘B)
syntax step-β*-conv tβu Aβ‘B = β¨ Aβ‘B β©β tβu
opaque
step-β*-convΛ : Ξ β’ t β* u β· B β Ξ β’ B β‘ A β Ξ β’ t β* u β· A
step-β*-convΛ tβu Bβ‘A = conv* tβu Bβ‘A
syntax step-β*-convΛ tβu Bβ‘A = Λβ¨ Bβ‘A β©β tβu
step-β*-conv-β‘ : Ξ β’ t β* u β· B β A PE.β‘ B β Ξ β’ t β* u β· A
step-β*-conv-β‘ tβu PE.refl = tβu
syntax step-β*-conv-β‘ tβu Aβ‘B = β¨ Aβ‘B β©ββ‘ tβu
step-β*-conv-β‘Λ : Ξ β’ t β* u β· B β B PE.β‘ A β Ξ β’ t β* u β· A
step-β*-conv-β‘Λ tβu PE.refl = tβu
syntax step-β*-conv-β‘Λ tβu Bβ‘A = Λβ¨ Bβ‘A β©ββ‘ tβu
infix -2 step-β·β*-conv step-β·β*-convΛ step-β·β*-conv-β‘ step-β·β*-conv-β‘Λ
step-β·β*-conv : β A β Ξ β’ t β* u β· B β Ξ β’ A β‘ B β Ξ β’ t β* u β· A
step-β·β*-conv _ = step-β*-conv
syntax step-β·β*-conv A tβu Aβ‘B = β· A β¨ Aβ‘B β©β tβu
{-# INLINE step-β·β*-conv #-}
step-β·β*-convΛ : β A β Ξ β’ t β* u β· B β Ξ β’ B β‘ A β Ξ β’ t β* u β· A
step-β·β*-convΛ _ = step-β*-convΛ
syntax step-β·β*-convΛ A tβu Bβ‘A = β· A Λβ¨ Bβ‘A β©β tβu
{-# INLINE step-β·β*-convΛ #-}
step-β·β*-conv-β‘ : β A β Ξ β’ t β* u β· B β A PE.β‘ B β Ξ β’ t β* u β· A
step-β·β*-conv-β‘ _ tβu PE.refl = tβu
syntax step-β·β*-conv-β‘ A tβu Aβ‘B = β· A β¨ Aβ‘B β©ββ‘ tβu
step-β·β*-conv-β‘Λ : β A β Ξ β’ t β* u β· B β B PE.β‘ A β Ξ β’ t β* u β· A
step-β·β*-conv-β‘Λ _ tβu PE.refl = tβu
syntax step-β·β*-conv-β‘Λ A tβu Bβ‘A = β· A Λβ¨ Bβ‘A β©ββ‘ tβu
infix -2 step-β·β*-conv step-β·β*-convΛ step-β·β*-conv-β‘ step-β·β*-conv-β‘Λ
step-β·β*-conv : β A β Ξ β’ t β* u β· B β Ξ β’ A β‘ B β Ξ β’ t β* u β· A
step-β·β*-conv _ = step-β*-conv
syntax step-β·β*-conv A tβu Aβ‘B = β· A β¨ Aβ‘B β©β tβu
{-# INLINE step-β·β*-conv #-}
step-β·β*-convΛ : β A β Ξ β’ t β* u β· B β Ξ β’ B β‘ A β Ξ β’ t β* u β· A
step-β·β*-convΛ _ = step-β*-convΛ
syntax step-β·β*-convΛ A tβu Bβ‘A = β· A Λβ¨ Bβ‘A β©β tβu
{-# INLINE step-β·β*-convΛ #-}
step-β·β*-conv-β‘ : β A β Ξ β’ t β* u β· B β A PE.β‘ B β Ξ β’ t β* u β· A
step-β·β*-conv-β‘ _ tβu PE.refl = tβu
syntax step-β·β*-conv-β‘ A tβu Aβ‘B = β· A β¨ Aβ‘B β©ββ‘ tβu
step-β·β*-conv-β‘Λ : β A β Ξ β’ t β* u β· B β B PE.β‘ A β Ξ β’ t β* u β· A
step-β·β*-conv-β‘Λ _ tβu PE.refl = tβu
syntax step-β·β*-conv-β‘Λ A tβu Bβ‘A = β· A Λβ¨ Bβ‘A β©ββ‘ tβu