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 _
opaque
βΈ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)))
βΈ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)
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