------------------------------------------------------------------------
-- "Equational" reasoning combinators for _⊢_:⇒*:_∷_
------------------------------------------------------------------------

open import Definition.Typed.Restrictions
open import Graded.Modality

module Definition.Typed.Reasoning.Reduction.Well-typed
  {ℓ} {M : Set ℓ}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  where

open import Definition.Typed R
open import Definition.Typed.Properties 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 _

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

infix  -1 finally-:⇒*:
infixr -2 step-:⇒*: finally-:⇒*:≡

opaque

  -- 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

-- The reflexivity proof requires one to prove that the term is
-- well-typed. In a non-empty chain of reasoning steps one can instead
-- end with the following combinator.

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-:⇒*: #-}

-- 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

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

infix  -1 finally-:⇐*:
infixr -2 step-:⇐*: finally-:⇐*:≡

opaque

  -- Transitivity.

  step-:⇐*: :
    ∀ v → Γ ⊢ t :⇒*: u ∷ A → Γ ⊢ u :⇒*: v ∷ A → Γ ⊢ t :⇒*: v ∷ A
  step-:⇐*: _ = trans-:⇒*:

  syntax step-:⇐*: v t⇒u u⇒v = v :⇐*:⟨ u⇒v ⟩ t⇒u

-- The reflexivity proof requires one to prove that the term is
-- well-typed. In a non-empty chain of reasoning steps one can instead
-- end with the following combinator.

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-:⇐*: #-}

-- 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 → Γ ⊢ 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

------------------------------------------------------------------------
-- 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 _≡⟨⟩:⇒:_ #-}

opaque

  -- Reflexivity.

  _∎⟨_⟩:⇒: : ∀ t → Γ ⊢ t ∷ A → Γ ⊢ t :⇒*: t ∷ A
  _ ∎⟨ ⊢t ⟩:⇒: = idRedTerm:*: ⊢t

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

infix  -1 finally-:⇒*:∷
infixr -2 step-:⇒*:∷ step-:⇒*:∷≡ step-:⇒*:∷≡˘ _∷_≡⟨⟩:⇒:∷_ finally-:⇒*:∷≡

opaque

  -- Transitivity.

  step-:⇒*:∷ :
    ∀ t A → Γ ⊢ u :⇒*: v ∷ A → Γ ⊢ t :⇒*: u ∷ A → Γ ⊢ t :⇒*: v ∷ A
  step-:⇒*:∷ _ _ = flip trans-:⇒*:

  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 _∷_≡⟨⟩:⇒:∷_ #-}

-- The reflexivity proof requires one to prove that the term is
-- well-typed. In a non-empty chain of reasoning steps one can instead
-- end with the following combinator.

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-:⇒*:∷ #-}

-- 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

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

infix  -1 finally-:⇐*:∷
infixr -2 step-:⇐*:∷ step-:⇐*:∷≡ step-:⇐*:∷≡˘ _∷_≡⟨⟩:⇐:∷_ finally-:⇐*:∷≡

opaque

  -- Transitivity.

  step-:⇐*:∷ :
    ∀ v A → Γ ⊢ t :⇒*: u ∷ A → Γ ⊢ u :⇒*: v ∷ A → Γ ⊢ t :⇒*: v ∷ A
  step-:⇐*:∷ _ _ = trans-:⇒*:

  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 _∷_≡⟨⟩:⇐:∷_ #-}

-- The reflexivity proof requires one to prove that the term is
-- well-typed. In a non-empty chain of reasoning steps one can instead
-- end with the following combinator.

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-:⇐*:∷ #-}

-- 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 → Γ ⊢ 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

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

opaque

  infix -1 _∷_∎⟨_⟩:⇒:

  -- Reflexivity.

  _∷_∎⟨_⟩:⇒: : ∀ t A → Γ ⊢ t ∷ A → Γ ⊢ t :⇒*: t ∷ A
  _ ∷ _ ∎⟨ ⊢t ⟩:⇒: = idRedTerm:*: ⊢t

------------------------------------------------------------------------
-- 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 = convRed:*: 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 = convRed:*: 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-≡˘

-- 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

{-# INLINE step-∷:⇒*:-conv #-}

-- 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

{-# INLINE step-∷:⇒*:-conv˘ #-}

-- 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-≡˘

-- 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

{-# INLINE step-∷:⇐*:-conv #-}

-- 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

{-# INLINE step-∷:⇐*:-conv˘ #-}

-- 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