------------------------------------------------------------------------
-- Some properties related to usage and the weak variant of Erased
------------------------------------------------------------------------

open import Graded.Modality
open import Graded.Usage.Restrictions

module Graded.Derived.Erased.NoEta.Usage
  {a} {M : Set a}
  (𝕄 : Modality M)
  (R : Usage-restrictions 𝕄)
  where

open Modality 𝕄
open Usage-restrictions R

open import Graded.Context 𝕄
open import Graded.Context.Properties 𝕄
open import Graded.Usage 𝕄 R
open import Graded.Usage.Inversion 𝕄 R
open import Graded.Usage.Properties 𝕄 R
open import Graded.Modality.Properties 𝕄
open import Graded.Mode 𝕄

open import Definition.Untyped M
open import Graded.Derived.Erased.NoEta.Untyped 𝕄

open import Graded.Derived.Sigma 𝕄 R

open import Tools.Bool using (T)
open import Tools.Empty
open import Tools.Function
open import Tools.Product
open import Tools.Sum
open import Tools.PropositionalEquality as PE using (_≑_)
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Relation

private variable
  A t : Term _
  Ξ³ Ξ΄ : Conβ‚˜ _
  m   : Mode
  ok  : T _

------------------------------------------------------------------------
-- Usage rules

opaque

  -- A usage rule for erased.

  β–Έerasedβ€² :
    (Β¬ T 𝟘ᡐ-allowed β†’ Trivial) β†’
    Ξ³ β–Έ[ 𝟘ᡐ? ] t β†’
    Ξ΄ β–Έ[ 𝟘ᡐ? ] A β†’
    Prodrec-allowed 𝟘ᡐ? (𝟘 ∧ πŸ™) 𝟘 𝟘 β†’
    𝟘ᢜ β–Έ[ 𝟘ᡐ? ] erased A t
  β–Έerasedβ€² {Ξ³} {t} {Ξ΄} {A} hyp = 𝟘ᡐ?-elim
    (Ξ» m β†’
       Ξ³ β–Έ[ m ] t β†’ Ξ΄ β–Έ[ m ] A β†’ Prodrec-allowed m (𝟘 ∧ πŸ™) 𝟘 𝟘 β†’
       𝟘ᢜ β–Έ[ m ] erased A t)
    (Ξ» β–Έt β–ΈA ok β†’ β–Έ-𝟘 (fstΚ·β‚˜-𝟘ᡐ ok β–Έt β–ΈA))
    (Ξ» not-ok β–Έt β–ΈA ok β†’
       case hyp not-ok of Ξ»
         trivial β†’ sub
       (fstΚ·β‚˜-πŸ™α΅ (injβ‚‚ trivial) (≑-trivial trivial) ok β–Έt
          (β–Έ-cong (Mode-propositional-without-𝟘ᡐ not-ok) β–ΈA))
       (β‰€αΆœ-reflexive (β‰ˆαΆœ-trivial trivial)))

-- Another usage rule for erased.

β–Έerased : Ξ³ β–Έ[ 𝟘ᡐ[ ok ] ] t β†’
          Ξ΄ β–Έ[ 𝟘ᡐ[ ok ] ] A β†’
          Prodrec-allowed 𝟘ᡐ[ ok ] (𝟘 ∧ πŸ™) 𝟘 𝟘 β†’
          𝟘ᢜ β–Έ[ 𝟘ᡐ[ ok ] ] erased A t
β–Έerased {ok} β–Έt β–ΈA P-ok =
  β–Έ-cong 𝟘ᡐ?β‰‘πŸ˜α΅ $
  β–Έerasedβ€²
    (βŠ₯-elim βˆ˜β†’ (_$ ok))
    (β–Έ-cong (PE.sym 𝟘ᡐ?β‰‘πŸ˜α΅) β–Έt)
    (β–Έ-cong (PE.sym 𝟘ᡐ?β‰‘πŸ˜α΅) β–ΈA)
    (PE.subst (Ξ» m β†’ Prodrec-allowed m (_ ∧ _) _ _) (PE.sym 𝟘ᡐ?β‰‘πŸ˜α΅)
       P-ok)

------------------------------------------------------------------------
-- Inversion lemmas for usage

-- An inversion lemma for erased.

inv-usage-erased :
  Ξ³ β–Έ[ m ] erased A t β†’
  𝟘ᢜ β–Έ[ 𝟘ᡐ[ ok ] ] t Γ—
  𝟘ᢜ β–Έ[ 𝟘ᡐ[ ok ] ] A Γ—
  Ξ³ β‰€αΆœ 𝟘ᢜ Γ—
  m ≑ 𝟘ᡐ[ ok ] Γ—
  Prodrec-allowed m (𝟘 ∧ πŸ™) 𝟘 𝟘
inv-usage-erased {Ξ³} {m} {ok} β–Έerased =
  case inv-usage-fstΚ· (inj₁ $ 𝟘ᡐ.πŸ˜β‰°πŸ™ ok) β–Έerased of Ξ»
    (Ξ· , _ , γ≀ , β–Έt , β–ΈA , 𝟘∧⌜mβŒπŸ˜β‰€βŒœm⌝ , P-ok) β†’
  case
    (let open Tools.Reasoning.PartialOrder ≀-poset in begin
       𝟘              β‰‘Λ˜βŸ¨ ∧-idem _ ⟩
       𝟘 ∧ 𝟘          β‰‘Λ˜βŸ¨ ∧-congΛ‘ $ Β·-zeroΚ³ _ ⟩
       𝟘 ∧ ⌜ m ⌝ Β· 𝟘  β‰€βŸ¨ 𝟘∧⌜mβŒπŸ˜β‰€βŒœm⌝ ⟩
       ⌜ m ⌝          ∎)
  of Ξ»
    πŸ˜β‰€βŒœm⌝ β†’
  case PE.singleton m of Ξ» where
    (πŸ™α΅ , PE.refl) β†’
      βŠ₯-elim $ 𝟘ᡐ.πŸ˜β‰°πŸ™ ok πŸ˜β‰€βŒœm⌝
    (𝟘ᡐ , PE.refl) β†’
        β–Έ-𝟘 β–Έt
      , β–Έ-𝟘 β–ΈA
      , (let open Tools.Reasoning.PartialOrder β‰€αΆœ-poset in begin
           Ξ³        β‰€βŸ¨ γ≀ ⟩
           𝟘ᢜ ∧ᢜ Ξ·  β‰€βŸ¨ ∧ᢜ-decreasingΛ‘ _ _ ⟩
           𝟘ᢜ       ∎)
      , 𝟘ᡐ-cong
      , P-ok