------------------------------------------------------------------------
-- "Equational" reasoning combinators for _⇛_∷_
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
import Definition.Untyped
import Graded.Erasure.LogicalRelation.Assumptions
open import Graded.Modality

module Graded.Erasure.LogicalRelation.Assumptions.Reasoning
  {a} {M : Set a}
  (open Definition.Untyped M)
  {𝕄 : Modality M}
  {R : Type-restrictions 𝕄}
  (open Graded.Erasure.LogicalRelation.Assumptions R)
  {k} {Ξ” : Con Term k}
  {_⇛_∷_ : Term k β†’ Term k β†’ Term k β†’ Set a}
  (is-reduction-relation : Is-reduction-relation Ξ” _⇛_∷_)
  where

open Is-reduction-relation is-reduction-relation

open import Definition.Typed R
open import Definition.Typed.Properties.Reduction R

open import Tools.Function
import Tools.PropositionalEquality as PE

private variable
  A B t u v : Term _

------------------------------------------------------------------------
-- Combinators for left-to-right reductions

infix  -1 finally-⇛ finally-β‡’* finally-β‡’
infixr -2 step-⇛ step-β‡’* step-β‡’ finally-⇛≑ finally-β‡’*≑ finally-⇒≑

opaque

  -- A form of transitivity.

  step-⇛ : βˆ€ t β†’ u ⇛ v ∷ A β†’ t ⇛ u ∷ A β†’ t ⇛ v ∷ A
  step-⇛ _ = flip trans-⇛

  syntax step-⇛ t u⇛v t⇛u = t β‡›βŸ¨ t⇛u ⟩ u⇛v

opaque

  -- Multiple reduction steps.

  step-β‡’* : βˆ€ t β†’ u ⇛ v ∷ A β†’ Ξ” ⊒ t β‡’* u ∷ A β†’ t ⇛ v ∷ A
  step-β‡’* _ u⇛v tβ‡’*u = trans-⇛ (β‡’*→⇛ tβ‡’*u) u⇛v

  syntax step-β‡’* t uβ‡’v tβ‡’u = t β‡’*⟨ tβ‡’u βŸ©β‡› uβ‡’v

opaque

  -- A single reduction step.

  step-β‡’ : βˆ€ t β†’ u ⇛ v ∷ A β†’ Ξ” ⊒ t β‡’ u ∷ A β†’ t ⇛ v ∷ A
  step-β‡’ _ u⇛v tβ‡’u = step-β‡’* _ u⇛v (redMany tβ‡’u)

  syntax step-β‡’ t uβ‡’v tβ‡’u = t β‡’βŸ¨ tβ‡’u βŸ©β‡› uβ‡’v

-- A combinator that can be used as the last one in a chain of
-- reasoning steps.

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-⇛ #-}

opaque

  -- A variant of finally-⇛.

  finally-β‡’ : βˆ€ t u β†’ Ξ” ⊒ t β‡’ u ∷ A β†’ t ⇛ u ∷ A
  finally-β‡’ _ _ tβ‡’u = β‡’*→⇛ (redMany tβ‡’u)

  syntax finally-β‡’ t u tβ‡’u = t β‡’βŸ¨ tβ‡’u βŸ©βˆŽβ‡› u ∎

opaque

  -- A variant of finally-⇛.

  finally-β‡’* : βˆ€ t u β†’ Ξ” ⊒ t β‡’* u ∷ A β†’ t ⇛ u ∷ A
  finally-β‡’* _ _ tβ‡’u = β‡’*→⇛ tβ‡’u

  syntax finally-β‡’* t u tβ‡’u = t β‡’*⟨ tβ‡’u βŸ©βˆŽβ‡› u ∎

-- A variant of finally-⇛ that makes it possible to end the chain of
-- reasoning steps with a propositional equality, without the use of
-- _∎⟨_βŸ©β‡›.

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

opaque

  -- A variant of finally-⇛≑.

  finally-β‡’*≑ : βˆ€ t β†’ u PE.≑ v β†’ Ξ” ⊒ t β‡’* u ∷ A β†’ t ⇛ v ∷ A
  finally-β‡’*≑ _ PE.refl = finally-β‡’* _ _

  syntax finally-β‡’*≑ t u≑v tβ‡’u = t β‡’*⟨ tβ‡’u βŸ©βˆŽβ‰‘β‡› u≑v

opaque

  -- A variant of finally-⇛≑.

  finally-⇒≑ : βˆ€ t β†’ u PE.≑ v β†’ Ξ” ⊒ t β‡’ u ∷ A β†’ t ⇛ v ∷ A
  finally-⇒≑ _ PE.refl = finally-β‡’ _ _

  syntax finally-⇒≑ t u≑v tβ‡’u = t β‡’βŸ¨ tβ‡’u βŸ©βˆŽβ‰‘β‡› u≑v

------------------------------------------------------------------------
-- Combinators for right-to-left reductions

infix  -1 finally-β‡š finally-⇐* finally-⇐
infixr -2 step-β‡š step-⇐* step-⇐ finally-β‡šβ‰‘ finally-⇐*≑ finally-⇐≑

opaque

  -- A form of transitivity.

  step-β‡š : βˆ€ t β†’ t ⇛ u ∷ A β†’ u ⇛ v ∷ A β†’ t ⇛ v ∷ A
  step-β‡š _ = trans-⇛

  syntax step-β‡š v t⇛u u⇛v = v β‡šβŸ¨ u⇛v ⟩ t⇛u

opaque

  -- Multiple steps.

  step-⇐* : βˆ€ v β†’ t ⇛ u ∷ A β†’ Ξ” ⊒ u β‡’* v ∷ A β†’ t ⇛ v ∷ A
  step-⇐* _ t⇛u uβ‡’v = trans-⇛ t⇛u (β‡’*→⇛ uβ‡’v)

  syntax step-⇐* v t⇛u uβ‡’v = v ⇐*⟨ uβ‡’v βŸ©β‡š t⇛u

opaque

  -- A single step.

  step-⇐ : βˆ€ v β†’ t ⇛ u ∷ A β†’ Ξ” ⊒ u β‡’ v ∷ A β†’ t ⇛ v ∷ A
  step-⇐ _ t⇛u uβ‡’v = step-⇐* _ t⇛u (redMany uβ‡’v)

  syntax step-⇐ v t⇛u uβ‡’v = v β‡βŸ¨ uβ‡’v βŸ©β‡š t⇛u

-- A combinator that can be used as the last one in a chain of
-- reasoning steps.

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-β‡š #-}

opaque

  -- A variant of finally-β‡š.

  finally-⇐* : βˆ€ u t β†’ Ξ” ⊒ t β‡’* u ∷ A β†’ t ⇛ u ∷ A
  finally-⇐* _ _ = finally-β‡’* _ _

  syntax finally-⇐* u t tβ‡’u = u ⇐*⟨ tβ‡’u βŸ©βˆŽβ‡š t ∎

  {-# INLINE finally-⇐* #-}

opaque

  -- A variant of finally-⇐*.

  finally-⇐ : βˆ€ u t β†’ Ξ” ⊒ t β‡’ u ∷ A β†’ t ⇛ u ∷ A
  finally-⇐ _ _ = finally-β‡’ _ _

  syntax finally-⇐ u t tβ‡’u = u β‡βŸ¨ tβ‡’u βŸ©βˆŽβ‡š t ∎

  {-# INLINE finally-⇐ #-}

-- A variant of finally-⇐* that makes it possible to end the chain of
-- reasoning steps with a propositional equality, without the use of
-- _∎⟨_βŸ©β‡›.

finally-β‡šβ‰‘ : βˆ€ v β†’ u PE.≑ t β†’ u ⇛ v ∷ A β†’ t ⇛ v ∷ A
finally-β‡šβ‰‘ _ PE.refl u⇛v = u⇛v

syntax finally-β‡šβ‰‘ v u≑t u⇛v = v β‡šβŸ¨ u⇛v βŸ©βˆŽβ‰‘ u≑t

opaque

  -- A variant of finally-β‡šβ‰‘.

  finally-⇐*≑ : βˆ€ v β†’ u PE.≑ t β†’ Ξ” ⊒ u β‡’* v ∷ A β†’ t ⇛ v ∷ A
  finally-⇐*≑ _ PE.refl = finally-⇐* _ _

  syntax finally-⇐*≑ v u≑t uβ‡’v = v ⇐*⟨ uβ‡’v βŸ©βˆŽβ‰‘β‡š u≑t

opaque

  -- A variant of finally-β‡šβ‰‘.

  finally-⇐≑ : βˆ€ v β†’ u PE.≑ t β†’ Ξ” ⊒ u β‡’ v ∷ A β†’ t ⇛ v ∷ A
  finally-⇐≑ _ PE.refl = finally-⇐ _ _

  syntax finally-⇐≑ v u≑t uβ‡’v = v β‡βŸ¨ uβ‡’v βŸ©βˆŽβ‰‘β‡š u≑t

------------------------------------------------------------------------
-- Combinators for left-to-right or right-to-left reductions

infix  -1 _∎⟨_βŸ©β‡›
infixr -2 step-≑ step-β‰‘Λ˜ _β‰‘βŸ¨βŸ©β‡›_

-- A reasoning step that uses propositional equality.

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

-- A reasoning step that uses propositional equality, combined with
-- symmetry.

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

-- A reasoning step that uses (Agda's) definitional equality.

_β‰‘βŸ¨βŸ©β‡›_ : βˆ€ t β†’ t ⇛ u ∷ A β†’ t ⇛ u ∷ A
_ β‰‘βŸ¨βŸ©β‡› t⇛u = t⇛u

{-# INLINE _β‰‘βŸ¨βŸ©β‡›_ #-}

-- Reflexivity.

_∎⟨_βŸ©β‡› : βˆ€ t β†’ Ξ” ⊒ t ∷ A β†’ t ⇛ t ∷ A
_ ∎⟨ ⊒t βŸ©β‡› = β‡’*→⇛ (id ⊒t)

{-# INLINE _∎⟨_βŸ©β‡› #-}

------------------------------------------------------------------------
-- Combinators for left-to-right reductions with explicit types

infix  -1 finally-β‡›βˆ· finally-β‡’*∷ finally-β‡’βˆ·
infixr -2 step-β‡›βˆ· step-β‡’*∷ step-β‡’βˆ· step-β‡›βˆ·β‰‘ step-β‡›βˆ·β‰‘Λ˜ _∷_β‰‘βŸ¨βŸ©β‡›βˆ·_
          finally-β‡›β‰‘βˆ· finally-β‡’*β‰‘βˆ· finally-β‡’β‰‘βˆ·

opaque

  -- A form of transitivity.

  step-β‡›βˆ· : βˆ€ t A β†’ u ⇛ v ∷ A β†’ t ⇛ u ∷ A β†’ t ⇛ v ∷ A
  step-β‡›βˆ· _ _ = step-⇛ _

  syntax step-β‡›βˆ· t A u⇛v t⇛u = t ∷ A β‡›βŸ¨ t⇛u ⟩∷ u⇛v

opaque

  -- Multiple reduction steps.

  step-β‡’*∷ : βˆ€ t A β†’ u ⇛ v ∷ A β†’ Ξ” ⊒ t β‡’* u ∷ A β†’ t ⇛ v ∷ A
  step-β‡’*∷ _ _ = step-β‡’* _

  syntax step-β‡’*∷ t A uβ‡’v tβ‡’u = t ∷ A β‡’*⟨ tβ‡’u βŸ©β‡›βˆ· uβ‡’v

opaque

  -- A single reduction step.

  step-β‡’βˆ· : βˆ€ t A β†’ u ⇛ v ∷ A β†’ Ξ” ⊒ t β‡’ u ∷ A β†’ t ⇛ v ∷ A
  step-β‡’βˆ· _ _ = step-β‡’ _

  syntax step-β‡’βˆ· t A uβ‡’v tβ‡’u = t ∷ A β‡’βŸ¨ tβ‡’u βŸ©β‡›βˆ· uβ‡’v

-- A reasoning step that uses propositional equality.

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

-- A reasoning step that uses propositional equality, combined with
-- symmetry.

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

-- A reasoning step that uses (Agda's) definitional equality.

_∷_β‰‘βŸ¨βŸ©β‡›βˆ·_ : βˆ€ t A β†’ t ⇛ u ∷ A β†’ t ⇛ u ∷ A
_ ∷ _ β‰‘βŸ¨βŸ©β‡›βˆ· t⇛u = t⇛u

{-# INLINE _∷_β‰‘βŸ¨βŸ©β‡›βˆ·_ #-}

-- A combinator that can be used as the last one in a chain of
-- reasoning steps.

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-β‡›βˆ· #-}

opaque

  -- A variant of finally-β‡›βˆ·.

  finally-β‡’βˆ· : βˆ€ t A u β†’ Ξ” ⊒ t β‡’ u ∷ A β†’ t ⇛ u ∷ A
  finally-β‡’βˆ· _ _ _ = finally-β‡’ _ _

  syntax finally-β‡’βˆ· t A u tβ‡’u = t ∷ A β‡’βŸ¨ tβ‡’u βŸ©βˆŽβ‡›βˆ· u ∎

opaque

  -- A variant of finally-β‡›βˆ·.

  finally-β‡’*∷ : βˆ€ t A u β†’ Ξ” ⊒ t β‡’* u ∷ A β†’ t ⇛ u ∷ A
  finally-β‡’*∷ _ _ = finally-β‡’* _

  syntax finally-β‡’*∷ t A u tβ‡’u = t ∷ A β‡’*⟨ tβ‡’u βŸ©βˆŽβ‡›βˆ· u ∎

-- A variant of finally-⇛ that makes it possible to end the chain of
-- reasoning steps with a propositional equality, without the use of
-- _∷_∎⟨_βŸ©β‡›.

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

opaque

  -- A variant of finally-β‡›β‰‘βˆ·.

  finally-β‡’*β‰‘βˆ· : βˆ€ t A β†’ u PE.≑ v β†’ Ξ” ⊒ t β‡’* u ∷ A β†’ t ⇛ v ∷ A
  finally-β‡’*β‰‘βˆ· _ _ = finally-β‡’*≑ _

  syntax finally-β‡’*β‰‘βˆ· t A u≑v tβ‡’u = t ∷ A β‡’*⟨ tβ‡’u βŸ©βˆŽβ‡›βˆ·β‰‘ u≑v

opaque

  -- A variant of finally-β‡›β‰‘βˆ·.

  finally-β‡’β‰‘βˆ· : βˆ€ t A β†’ u PE.≑ v β†’ Ξ” ⊒ t β‡’ u ∷ A β†’ t ⇛ v ∷ A
  finally-β‡’β‰‘βˆ· _ _ = finally-⇒≑ _

  syntax finally-β‡’β‰‘βˆ· t A u≑v tβ‡’u = t ∷ A β‡’βŸ¨ tβ‡’u βŸ©βˆŽβ‡›βˆ·β‰‘ u≑v

------------------------------------------------------------------------
-- Combinators for right-to-left reductions with explicit types

infix  -1 finally-β‡šβˆ· finally-⇐*∷ finally-β‡βˆ·
infixr -2 step-β‡šβˆ· step-⇐*∷ step-β‡βˆ· step-β‡šβˆ·β‰‘ step-β‡šβˆ·β‰‘Λ˜ _∷_β‰‘βŸ¨βŸ©β‡šβˆ·_
          finally-β‡šβ‰‘βˆ· finally-⇐*β‰‘βˆ· finally-β‡β‰‘βˆ·

opaque

  -- A form of transitivity.

  step-β‡šβˆ· : βˆ€ t A β†’ t ⇛ u ∷ A β†’ u ⇛ v ∷ A β†’ t ⇛ v ∷ A
  step-β‡šβˆ· _ _ = step-β‡š _

  syntax step-β‡šβˆ· v A t⇛u u⇛v = v ∷ A β‡šβŸ¨ u⇛v ⟩∷ t⇛u

opaque

  -- Multiple steps.

  step-⇐*∷ : βˆ€ v A β†’ t ⇛ u ∷ A β†’ Ξ” ⊒ u β‡’* v ∷ A β†’ t ⇛ v ∷ A
  step-⇐*∷ _ _ = step-⇐* _

  syntax step-⇐*∷ v A t⇛u uβ‡’v = v ∷ A ⇐*⟨ uβ‡’v βŸ©β‡šβˆ· t⇛u

opaque

  -- A single step.

  step-β‡βˆ· : βˆ€ v A β†’ t ⇛ u ∷ A β†’ Ξ” ⊒ u β‡’ v ∷ A β†’ t ⇛ v ∷ A
  step-β‡βˆ· _ _ = step-⇐ _

  syntax step-β‡βˆ· v A t⇛u uβ‡’v = v ∷ A β‡βŸ¨ uβ‡’v βŸ©β‡šβˆ· t⇛u

-- A reasoning step that uses propositional equality.

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

-- A reasoning step that uses propositional equality, combined with
-- symmetry.

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

-- A reasoning step that uses (Agda's) definitional equality.

_∷_β‰‘βŸ¨βŸ©β‡šβˆ·_ : βˆ€ u A β†’ t ⇛ u ∷ A β†’ t ⇛ u ∷ A
_ ∷ _ β‰‘βŸ¨βŸ©β‡šβˆ· t⇛u = t⇛u

{-# INLINE _∷_β‰‘βŸ¨βŸ©β‡šβˆ·_ #-}

-- A combinator that can be used as the last one in a chain of
-- reasoning steps.

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-β‡šβˆ· #-}

opaque

  -- A variant of finally-β‡šβˆ·.

  finally-⇐*∷ : βˆ€ u A t β†’ Ξ” ⊒ t β‡’* u ∷ A β†’ t ⇛ u ∷ A
  finally-⇐*∷ _ _ _ = finally-⇐* _ _

  syntax finally-⇐*∷ u A t tβ‡’u = u ∷ A ⇐*⟨ tβ‡’u βŸ©βˆŽβ‡šβˆ· t ∎

  {-# INLINE finally-⇐*∷ #-}

opaque

  -- A variant of finally-⇐*∷.

  finally-β‡βˆ· : βˆ€ u A t β†’ Ξ” ⊒ t β‡’ u ∷ A β†’ t ⇛ u ∷ A
  finally-β‡βˆ· _ _ _ = finally-⇐ _ _

  syntax finally-β‡βˆ· u A t tβ‡’u = u ∷ A β‡βŸ¨ tβ‡’u βŸ©βˆŽβ‡šβˆ· t ∎

  {-# INLINE finally-β‡βˆ· #-}

-- A variant of finally-⇐* that makes it possible to end the chain of
-- reasoning steps with a propositional equality, without the use of
-- _∷_∎⟨_βŸ©β‡›.

finally-β‡šβ‰‘βˆ· : βˆ€ v A β†’ u PE.≑ t β†’ u ⇛ v ∷ A β†’ t ⇛ v ∷ A
finally-β‡šβ‰‘βˆ· _ _ PE.refl u⇛v = u⇛v

syntax finally-β‡šβ‰‘βˆ· v A u≑t u⇛v = v ∷ A β‡šβŸ¨ u⇛v βŸ©βˆŽβˆ·β‰‘ u≑t

opaque

  -- A variant of finally-β‡šβ‰‘βˆ·.

  finally-⇐*β‰‘βˆ· : βˆ€ v A β†’ u PE.≑ t β†’ Ξ” ⊒ u β‡’* v ∷ A β†’ t ⇛ v ∷ A
  finally-⇐*β‰‘βˆ· _ _ = finally-⇐*≑ _

  syntax finally-⇐*β‰‘βˆ· v A u≑t uβ‡’v = v ∷ A ⇐*⟨ uβ‡’v βŸ©βˆŽβ‡šβˆ·β‰‘ u≑t

opaque

  -- A variant of finally-β‡šβ‰‘βˆ·.

  finally-β‡β‰‘βˆ· : βˆ€ v A β†’ u PE.≑ t β†’ Ξ” ⊒ u β‡’ v ∷ A β†’ t ⇛ v ∷ A
  finally-β‡β‰‘βˆ· _ _ = finally-⇐≑ _

  syntax finally-β‡β‰‘βˆ· v A u≑t uβ‡’v = v ∷ A β‡βŸ¨ uβ‡’v βŸ©βˆŽβ‡šβˆ·β‰‘ u≑t

------------------------------------------------------------------------
-- A combinator for left-to-right or right-to-left reductions with
-- explicit types

infix -1 _∷_∎⟨_βŸ©β‡›

-- Reflexivity.

_∷_∎⟨_βŸ©β‡› : βˆ€ t A β†’ Ξ” ⊒ t ∷ A β†’ t ⇛ t ∷ A
_ ∷ _ ∎⟨ ⊒t βŸ©β‡› = β‡’*→⇛ (id ⊒t)

{-# INLINE _∷_∎⟨_βŸ©β‡› #-}

------------------------------------------------------------------------
-- Conversion combinators

infix -2 step-⇛-conv step-⇛-conv˘ step-⇛-conv-≑ step-⇛-conv-β‰‘Λ˜

opaque

  -- Conversion.

  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

  -- Conversion.

  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

-- Conversion using propositional equality.

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

-- Conversion using propositional equality.

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

------------------------------------------------------------------------
-- Conversion combinators for left-to-right reductions with explicit
-- types

infix -2 step-βˆ·β‡›-conv step-βˆ·β‡›-conv˘ step-βˆ·β‡›-conv-≑ step-βˆ·β‡›-conv-β‰‘Λ˜

opaque

  -- Conversion.

  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

opaque

  -- Conversion.

  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

-- Conversion using propositional equality.

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

-- Conversion using propositional equality.

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

------------------------------------------------------------------------
-- Conversion combinators for right-to-left reductions with explicit
-- types

infix -2 step-βˆ·β‡š-conv step-βˆ·β‡š-conv˘ step-βˆ·β‡š-conv-≑ step-βˆ·β‡š-conv-β‰‘Λ˜

opaque

  -- Conversion.

  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

opaque

  -- Conversion.

  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

-- Conversion using propositional equality.

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

-- Conversion using propositional equality.

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