------------------------------------------------------------------------
-- Some assumptions used to define the logical relation for erasure
------------------------------------------------------------------------

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

module Graded.Erasure.LogicalRelation.Assumptions
  {a} {M : Set a}
  {𝕄 : Modality M}
  (R : Type-restrictions 𝕄)
  where

open Type-restrictions R

open import Definition.Typed R
open import Definition.Typed.EqualityRelation R
open import Definition.Typed.Consequences.Canonicity R
open import Definition.Typed.Inversion R
open import Definition.Typed.Properties R
open import Definition.Typed.Well-formed R
open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Properties M

open import Graded.Erasure.Target using (Strictness)

open import Tools.Fin
open import Tools.Function
open import Tools.Level
open import Tools.Nat
open import Tools.Product
open import Tools.Sum

private variable
  n                             : Nat
  Ξ“                             : Con Term _
  A B C t t₁ tβ‚‚ u v v₁ vβ‚‚ w₁ wβ‚‚ : Term _
  p q qβ€² r                      : M

------------------------------------------------------------------------
-- Is-reduction-relation

-- An axiomatisation of "reduction" relations that can be used in the
-- logical relation. The context is fixed.

record Is-reduction-relation
         (Ξ“ : Con Term n) (_⇛_∷_ : Term n β†’ Term n β†’ Term n β†’ Set a) :
         Set (lsuc a) where
  field
    -- Conversion.

    conv-⇛ : t ⇛ u ∷ A β†’ Ξ“ ⊒ A ≑ B β†’ t ⇛ u ∷ B

    -- Reduction is contained in the relation.

    β‡’*→⇛ : Ξ“ ⊒ t β‡’* u ∷ A β†’ t ⇛ u ∷ A

    -- The relation is contained in definitional equality.

    β‡›β†’βŠ’β‰‘ : t ⇛ u ∷ A β†’ Ξ“ ⊒ t ≑ u ∷ A

    -- Transitivity.

    trans-⇛ : t ⇛ u ∷ A β†’ u ⇛ v ∷ A β†’ t ⇛ v ∷ A

    -- If t "reduces" to both u andΒ v, and u is a WHNF, then v
    -- "reduces" toΒ u.

    whnf-⇛ : t ⇛ u ∷ A β†’ Whnf u β†’ t ⇛ v ∷ A β†’ v ⇛ u ∷ A

    -- Some congruence properties.

    app-⇛ :
      t₁ ⇛ tβ‚‚ ∷ Ξ  p , q β–· A β–Ή B β†’
      Ξ“ ⊒ u ∷ A β†’
      t₁ ∘⟨ p ⟩ u ⇛ tβ‚‚ ∘⟨ p ⟩ u ∷ B [ u ]β‚€

    fst-⇛ :
      t₁ ⇛ tβ‚‚ ∷ Ξ£Λ’ p , q β–· A β–Ή B β†’
      fst p t₁ ⇛ fst p tβ‚‚ ∷ A

    snd-⇛ :
      t₁ ⇛ tβ‚‚ ∷ Ξ£Λ’ p , q β–· A β–Ή B β†’
      snd p t₁ ⇛ snd p tβ‚‚ ∷ B [ fst p t₁ ]β‚€

    prodrec-⇛ :
      Ξ“ βˆ™ Ξ£Κ· p , qβ€² β–· A β–Ή B ⊒ C β†’
      t₁ ⇛ tβ‚‚ ∷ Ξ£Κ· p , qβ€² β–· A β–Ή B β†’
      Ξ“ βˆ™ A βˆ™ B ⊒ u ∷ C [ prodΚ· p (var x1) (var x0) ]↑² β†’
      prodrec r p q C t₁ u ⇛ prodrec r p q C tβ‚‚ u ∷ C [ t₁ ]β‚€

    natrec-⇛ :
      Ξ“ ⊒ t ∷ A [ zero ]β‚€ β†’
      Ξ“ βˆ™ β„• βˆ™ A ⊒ u ∷ A [ suc (var x1) ]↑² β†’
      v₁ ⇛ vβ‚‚ ∷ β„• β†’
      natrec p q r A t u v₁ ⇛ natrec p q r A t u vβ‚‚ ∷ A [ v₁ ]β‚€

    J-⇛ :
      Ξ“ βˆ™ A βˆ™ Id (wk1 A) (wk1 t) (var x0) ⊒ B β†’
      Ξ“ ⊒ u ∷ B [ t , rfl ]₁₀ β†’
      w₁ ⇛ wβ‚‚ ∷ Id A t v β†’
      J p q A t B u v w₁ ⇛ J p q A t B u v wβ‚‚ ∷ B [ v , w₁ ]₁₀

    K-⇛ :
      Ξ“ βˆ™ Id A t t ⊒ B β†’
      Ξ“ ⊒ u ∷ B [ rfl ]β‚€ β†’
      v₁ ⇛ vβ‚‚ ∷ Id A t t β†’
      K-allowed β†’
      K p A t B u v₁ ⇛ K p A t B u vβ‚‚ ∷ B [ v₁ ]β‚€

  opaque

    -- If t reduces toΒ u, then t and u are well-typed.

    wf-⇛ : t ⇛ u ∷ A β†’ Ξ“ ⊒ t ∷ A Γ— Ξ“ ⊒ u ∷ A
    wf-⇛ = projβ‚‚ βˆ˜β†’ wf-βŠ’β‰‘βˆ· βˆ˜β†’ β‡›β†’βŠ’β‰‘

opaque instance

  -- Reduction is a "reduction" relation.

  β‡’*-is-reduction-relation : Is-reduction-relation Ξ“ (Ξ“ ⊒_β‡’*_∷_)
  β‡’*-is-reduction-relation = record
    { conv-⇛    = conv*
    ; β‡’*→⇛      = idαΆ 
    ; β‡›β†’βŠ’β‰‘      = subset*Term
    ; trans-⇛   = _β‡¨βˆ·*_
    ; whnf-⇛    = Ξ» tβ‡’*u u-whnf β†’ whrDetβ†˜Term (tβ‡’*u , u-whnf)
    ; app-⇛     = app-subst*
    ; fst-⇛     = fst-subst*
    ; snd-⇛     = snd-subst*
    ; prodrec-⇛ = prodrec-subst*
    ; natrec-⇛  = natrec-subst*
    ; J-⇛       = J-subst*
    ; K-⇛       = K-subst*
    }

opaque instance

  -- Definitional equality is a "reduction" relation.

  ≑-is-reduction-relation : Is-reduction-relation Ξ“ (Ξ“ ⊒_≑_∷_)
  ≑-is-reduction-relation = record
    { conv-⇛    = conv
    ; β‡’*→⇛      = subset*Term
    ; β‡›β†’βŠ’β‰‘      = idαΆ 
    ; trans-⇛   = trans
    ; whnf-⇛    = Ξ» t≑u _ t≑v β†’ trans (symβ€² t≑v) t≑u
    ; app-⇛     = Ξ» t₁≑tβ‚‚ ⊒u β†’ app-cong t₁≑tβ‚‚ (refl ⊒u)
    ; fst-⇛     = fst-congβ€²
    ; snd-⇛     = snd-congβ€²
    ; prodrec-⇛ = Ξ» ⊒C t₁≑tβ‚‚ ⊒u β†’
                    prodrec-congβ€² (refl ⊒C) t₁≑tβ‚‚ (refl ⊒u)
    ; natrec-⇛  = Ξ» ⊒t ⊒u v₁≑vβ‚‚ β†’
                    natrec-cong (refl (βŠ’βˆ™β†’βŠ’ (wfTerm ⊒u))) (refl ⊒t)
                      (refl ⊒u) v₁≑vβ‚‚
    ; J-⇛       = Ξ» ⊒B ⊒u w₁≑wβ‚‚ β†’
                    let ⊒A , ⊒t , ⊒v =
                          inversion-Id (wf-βŠ’β‰‘βˆ· w₁≑wβ‚‚ .proj₁)
                    in
                    J-congβ€² (refl ⊒A) (refl ⊒t) (refl ⊒B) (refl ⊒u)
                      (refl ⊒v) w₁≑wβ‚‚
    ; K-⇛       = Ξ» ⊒B ⊒u v₁≑vβ‚‚ ok β†’
                    let ⊒A , ⊒t , _ =
                          inversion-Id (wf-βŠ’β‰‘βˆ· v₁≑vβ‚‚ .proj₁)
                    in
                    K-cong (refl ⊒A) (refl ⊒t) (refl ⊒B) (refl ⊒u) v₁≑vβ‚‚
                      ok
    }

opaque

  -- Propositional equality is a "reduction" relation for the empty
  -- context, or if equality reflection is allowed.

  Id-is-reduction-relation :
    Empty-con Ξ“ ⊎ Equality-reflection β†’
    Is-reduction-relation Ξ“ (Ξ» t u A β†’ βˆƒ Ξ» v β†’ Ξ“ ⊒ v ∷ Id A t u)
  Id-is-reduction-relation {Ξ“} ok = record
    { conv-⇛    = Ξ» (_ , ⊒v) A≑B β†’
                    let _ , ⊒t , ⊒u = inversion-Id (wf-⊒∷ ⊒v) in
                    _ , conv ⊒v (Id-cong A≑B (refl ⊒t) (refl ⊒u))
    ; β‡’*→⇛      = βŠ’β‰‘β†’β‡› βˆ˜β†’ subset*Term
    ; β‡›β†’βŠ’β‰‘      = β‡›β†’βŠ’β‰‘
    ; trans-⇛   = Ξ» (_ , ⊒v₁) (_ , ⊒vβ‚‚) β†’ _ , ⊒transitivity ⊒v₁ ⊒vβ‚‚
    ; whnf-⇛    = Ξ» (_ , ⊒v₁) _ (_ , ⊒vβ‚‚) β†’
                    _ , ⊒transitivity (⊒symmetry ⊒vβ‚‚) ⊒v₁
    ; app-⇛     = Ξ» t₁⇛tβ‚‚ ⊒u β†’ βŠ’β‰‘β†’β‡› (R.app-⇛ (β‡›β†’βŠ’β‰‘ t₁⇛tβ‚‚) ⊒u)
    ; fst-⇛     = βŠ’β‰‘β†’β‡› βˆ˜β†’ R.fst-⇛ βˆ˜β†’ β‡›β†’βŠ’β‰‘
    ; snd-⇛     = βŠ’β‰‘β†’β‡› βˆ˜β†’ R.snd-⇛ βˆ˜β†’ β‡›β†’βŠ’β‰‘
    ; prodrec-⇛ = Ξ» ⊒C t₁⇛tβ‚‚ ⊒u β†’ βŠ’β‰‘β†’β‡› (R.prodrec-⇛ ⊒C (β‡›β†’βŠ’β‰‘ t₁⇛tβ‚‚) ⊒u)
    ; natrec-⇛  = Ξ» ⊒A ⊒u v₁⇛vβ‚‚ β†’ βŠ’β‰‘β†’β‡› (R.natrec-⇛ ⊒A ⊒u (β‡›β†’βŠ’β‰‘ v₁⇛vβ‚‚))
    ; J-⇛       = Ξ» ⊒B ⊒u w₁⇛wβ‚‚ β†’ βŠ’β‰‘β†’β‡› (R.J-⇛ ⊒B ⊒u (β‡›β†’βŠ’β‰‘ w₁⇛wβ‚‚))
    ; K-⇛       = Ξ» ⊒B ⊒u v₁⇛vβ‚‚ ok β†’ βŠ’β‰‘β†’β‡› (R.K-⇛ ⊒B ⊒u (β‡›β†’βŠ’β‰‘ v₁⇛vβ‚‚) ok)
    }
    where
    module R = Is-reduction-relation (≑-is-reduction-relation {Ξ“ = Ξ“})

    β‡›β†’βŠ’β‰‘ : (βˆƒ Ξ» v β†’ Ξ“ ⊒ v ∷ Id A t u) β†’ Ξ“ ⊒ t ≑ u ∷ A
    β‡›β†’βŠ’β‰‘ (_ , ⊒v) = case ok of Ξ» where
      (inj₁ Ξ΅) β†’
        Ρ⊒∷Idβ†’Ξ΅βŠ’β‰‘βˆ· ⊒v
      (injβ‚‚ ok) β†’
        equality-reflectionβ€² ok ⊒v

    βŠ’β‰‘β†’β‡› : Ξ“ ⊒ t ≑ u ∷ A β†’ βˆƒ Ξ» v β†’ Ξ“ ⊒ v ∷ Id A t u
    βŠ’β‰‘β†’β‡› t≑u = rfl , rflβ±Όβ€² t≑u

------------------------------------------------------------------------
-- Assumptions

-- Assumptions used to define the logical relation for erasure.

record Assumptions : Set (lsuc a) where
  infix 4 _⇛_∷_

  field
    -- An "EqRelSet".
    ⦃ eqRelSet ⦄ : EqRelSet

  open EqRelSet eqRelSet public

  field
    -- The size of the context below.
    {k} : Nat

    -- A context.
    {Ξ”} : Con Term k

    -- The context is well-formed.
    βŠ’Ξ” : ⊒ Ξ”

    -- Neutrals-included holds or Ξ” is empty.
    ⦃ inc ⦄ : Neutrals-included or-empty Ξ”

    -- Should applications be extracted to strict or non-strict
    -- applications?
    str : Strictness

    -- A "reduction" relation.
    _⇛_∷_ : Term k β†’ Term k β†’ Term k β†’ Set a

    -- The "reduction" relation satisfies certain properties.
    is-reduction-relation : Is-reduction-relation Ξ” _⇛_∷_

  open Is-reduction-relation is-reduction-relation public

  instance

    -- Equality reflection is not allowed or Ξ” is empty.

    no-equality-reflection-or-empty :
      No-equality-reflection or-empty Ξ”
    no-equality-reflection-or-empty =
      or-empty-map
        (No-equality-reflection⇔ .projβ‚‚ βˆ˜β†’
         flip Equality-reflection-allowed→¬Neutrals-included)
        inc