DecidableOPE.agda

module DecidableOPE where

open import Agda.Primitive using (_⊔_)

data ⊥ : Set where

elim⊥ : ∀ {ℓ} {X : Set ℓ} → ⊥ → X
elim⊥ ()

infix 3 ¬_
¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ X = X → ⊥

_↯_ : ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′} → X → ¬ X → Y
p ↯ ¬p = elim⊥ (¬p p)

infix 4 _≡_
data _≡_ {ℓ} {X : Set ℓ} (A : X) : X → Set ℓ where
  refl : A ≡ A
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

data Dec {ℓ} (X : Set ℓ) : Set ℓ where
  yes : X → Dec X
  no  : ¬ X → Dec X

Decidable : ∀ {ℓ ℓ′ ℓ″} {X : Set ℓ} {Y : Set ℓ′} → (X → Y → Set ℓ″) → Set (ℓ ⊔ ℓ′ ⊔ ℓ″)
Decidable _R_ = ∀ x y → Dec (x R y)

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

data List {ℓ} (X : Set ℓ) : Set ℓ where
  ∅   : List X
  _,_ : List X → X → List X

module ListOPE where
  infix 3 _⊆_
  data _⊆_ {ℓ} {X : Set ℓ} : List X → List X → Set ℓ where
    done : ∅ ⊆ ∅
    skip : ∀ {L L′ x} → L ⊆ L′ → L ⊆ L′ , x
    keep : ∀ {L L′ x} → L ⊆ L′ → L , x ⊆ L′ , x

  inf⊆ : ∀ {ℓ} {X : Set ℓ} {L : List X} → ∅ ⊆ L
  inf⊆ {L = ∅}     = done
  inf⊆ {L = L , x} = skip inf⊆

  module _ {ℓ} {X : Set ℓ} {{_≡?_ : Decidable {X = X} _≡_}} where
    _⊆?_ : Decidable {X = List X} _⊆_
    ∅       ⊆? ∅         = yes done
    ∅       ⊆? (L′ , x′) = yes inf⊆
    (L , x) ⊆? ∅         = no λ ()
    (L , x) ⊆? (L′ , x′) with (L , x) ⊆? L′
    (L , x) ⊆? (L′ , x′) | yes Lx⊆L′ = yes (skip Lx⊆L′)
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  with L ⊆? L′
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  | no L⊈L′  = no λ { (skip η) → η ↯ Lx⊈L′
                                                       ; (keep η) → η ↯ L⊈L′
                                                       }
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  | yes L⊆L′ with x ≡? x′
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  | yes L⊆L′ | yes refl = yes (keep L⊆L′)
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  | yes L⊆L′ | no x≢x′  = no λ { (skip η) → η ↯ Lx⊈L′
                                                                  ; (keep η) → refl ↯ x≢x′
                                                                  }

data Vec {ℓ} (X : Set ℓ) : Nat → Set ℓ where
  ∅   : Vec X zero
  _,_ : ∀ {n} → Vec X n → X → Vec X (suc n)

module VecOPE where
  infix 3 _⊆_
  data _⊆_ {ℓ} {X : Set ℓ} : ∀ {n n′} → Vec X n → Vec X n′ → Set ℓ where
    done : ∅ ⊆ ∅
    skip : ∀ {n n′} {L : Vec X n} {L′ : Vec X n′} {x} → L ⊆ L′ → L ⊆ L′ , x
    keep : ∀ {n n′} {L : Vec X n} {L′ : Vec X n′} {x} → L ⊆ L′ → L , x ⊆ L′ , x

  inf⊆ : ∀ {ℓ} {X : Set ℓ} {n} {L : Vec X n} → ∅ ⊆ L
  inf⊆ {L = ∅}     = done
  inf⊆ {L = L , x} = skip inf⊆

  module _ {ℓ} {X : Set ℓ} {{_≡?_ : Decidable {X = X} _≡_}} where
    _⊆?_ : ∀ {n n′} → Decidable {X = Vec X n} {Vec X n′} _⊆_
    ∅       ⊆? ∅         = yes done
    ∅       ⊆? (L′ , x′) = yes inf⊆
    (L , x) ⊆? ∅         = no λ ()
    (L , x) ⊆? (L′ , x′) with (L , x) ⊆? L′
    (L , x) ⊆? (L′ , x′) | yes Lx⊆L′ = yes (skip Lx⊆L′)
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  with L ⊆? L′
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  | no L⊈L′  = no λ { (skip η) → η ↯ Lx⊈L′
                                                       ; (keep η) → η ↯ L⊈L′
                                                       }
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  | yes L⊆L′ with x ≡? x′
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  | yes L⊆L′ | yes refl = yes (keep L⊆L′)
    (L , x) ⊆? (L′ , x′) | no Lx⊈L′  | yes L⊆L′ | no x≢x′  = no λ { (skip η) → η ↯ Lx⊈L′
                                                                  ; (keep η) → refl ↯ x≢x′
                                                                  }