module Graded.Usage.Erased-matches where
open import Tools.Empty
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Unit
data Some-erased-matches : Set where
all′ some′ : Some-erased-matches
data Erased-matches : Set where
none : Erased-matches
not-none : Some-erased-matches → Erased-matches
pattern all = not-none all′
pattern some = not-none some′
private variable
em em₁ em₂ em₃ : Erased-matches
infix 4 _≤ᵉᵐ_
_≤ᵉᵐ_ : Erased-matches → Erased-matches → Set
none ≤ᵉᵐ _ = ⊤
some ≤ᵉᵐ some = ⊤
_ ≤ᵉᵐ all = ⊤
_ ≤ᵉᵐ _ = ⊥
opaque
≤ᵉᵐ-reflexive : em ≤ᵉᵐ em
≤ᵉᵐ-reflexive {em = all} = _
≤ᵉᵐ-reflexive {em = some} = _
≤ᵉᵐ-reflexive {em = none} = _
opaque
≤ᵉᵐ-transitive : em₁ ≤ᵉᵐ em₂ → em₂ ≤ᵉᵐ em₃ → em₁ ≤ᵉᵐ em₃
≤ᵉᵐ-transitive {em₁ = none} = _
≤ᵉᵐ-transitive {em₁ = some} {em₂ = some} {em₃ = some} = _
≤ᵉᵐ-transitive {em₁ = some} {em₃ = all} = _
≤ᵉᵐ-transitive {em₁ = all} {em₂ = all} {em₃ = all} = _
opaque
none-≤ᵉᵐ : none ≤ᵉᵐ em
none-≤ᵉᵐ {em = all} = _
none-≤ᵉᵐ {em = some} = _
none-≤ᵉᵐ {em = none} = _
opaque
≤ᵉᵐ-all : em ≤ᵉᵐ all
≤ᵉᵐ-all {em = all} = _
≤ᵉᵐ-all {em = some} = _
≤ᵉᵐ-all {em = none} = _
opaque
≤ᵉᵐ→≡none→≡none : em₁ ≤ᵉᵐ em₂ → em₂ ≡ none → em₁ ≡ none
≤ᵉᵐ→≡none→≡none {em₁ = none} {em₂ = none} _ _ = refl
≤ᵉᵐ→≡none→≡none {em₁ = all} {em₂ = none} ()
opaque
≤ᵉᵐ→≡some→≡not-none :
em₁ ≤ᵉᵐ em₂ → em₁ ≡ some → ∃ λ sem → em₂ ≡ not-none sem
≤ᵉᵐ→≡some→≡not-none {em₁ = some} {em₂ = not-none _} _ _ = _ , refl
opaque
≤ᵉᵐ→≡all→≡all : em₁ ≤ᵉᵐ em₂ → em₁ ≡ all → em₂ ≡ all
≤ᵉᵐ→≡all→≡all {em₁ = all} {em₂ = all} _ _ = refl