Closure attempt number omega

closure.agda

open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

data ⊥ : Set where

¬_ : (A : Set) → Set
¬ A = A → ⊥

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

_≢_ : {A : Set} → A → A → Set
x ≢ y = ¬(x ≡ y)

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

Decidable≡ : Set → Set
Decidable≡ A = (x y : A) → Dec (x ≡ y)

data Fin : ℕ → Set where
  fzero : ∀{n} → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

Fvec : Set → ℕ → Set
Fvec A n = Fin n → A

_∈_ : {A : Set} {n : ℕ} → A → Fvec A n → Set
x ∈ xs  = Σ _ λ k → xs k ≡ x

∅ : {A : Set} → Fvec A zero
∅ ()

All : {A : Set} {n : ℕ} → (A → Set) → Fvec A n → Set
All P xs = ∀ k → P (xs k)

module Deduction
    {A T : Set}
    (_≟_ : Decidable≡ A)
    (_⇒_ : {n : ℕ} → Fvec A n → A → T)
    where

  data _⊢_ {n} (αs : Fvec T n) (x : A) : Set where
    leaf : (∅ ⇒ x) ∈ αs → αs ⊢ x
    stem : ∀{xs} → (xs ⇒ x) ∈ αs → All (αs ⊢_) xs → αs ⊢ x

data Arrow : Set where
  _⇒_ : ∀{n} → Fvec ℕ n → ℕ → Arrow

postulate natEq : Decidable≡ ℕ

open Deduction natEq _⇒_

Fvec.agda

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma
open import Decidable

module Fvec where

data Fin : ℕ → Set where
  fzero : ∀{n} → Fin (suc n)
  fsuc  : ∀{n} → Fin n → Fin (suc n)

Fvec : Set → ℕ → Set
Fvec A n = Fin n → A

head : ∀{A n} → Fvec A (suc n) → A
head φs = φs fzero

tail : ∀{A n} → Fvec A (suc n) → Fvec A n
tail φs = λ k → φs (fsuc k)

∅ : {A : Set} → Fvec A zero
∅ ()

All : {A : Set} {n : ℕ} → (A → Set) → Fvec A n → Set
All P φs = ∀ k → P (φs k)

Any : {A : Set} {n : ℕ} → (A → Set) → Fvec A n → Set
Any P φs = Σ _ λ k → P (φs k)

_∈_ : {A : Set} {n : ℕ} → A → Fvec A n → Set
x ∈ φs  = Any (x ≡_) φs

all : ∀{n A} {P : Pred A} (p : Decidable P) → (φs : Fvec A n) → Dec (All P φs)
all {zero}  p φs = yes (λ ())
all {suc n} p φs with p (φs fzero)
all {suc n} p φs | no ¬P0 = no (λ z → ¬P0 (z fzero))
...              | yes P0 with all p (tail φs)
...                       | no ¬Ps = no (λ k → ¬Ps (λ j → k (fsuc j)))
...                       | yes Ps = yes ind
                                     where
                                       ind : _
                                       ind fzero    = P0
                                       ind (fsuc k) = Ps k

any : ∀{n A} {P : Pred A} (p : Decidable P) → (φs : Fvec A n) → Dec (Any P φs)
any {zero}  p φs = no ∅any
                   where
                    ∅any : _
                    ∅any (() , _)
any {suc n} p φs with p (φs fzero)
...              | yes P0 = yes (fzero , P0)
...              | no ¬P0 with any p (tail φs)
...                       | yes (k , Ps) = yes (fsuc k , Ps)
...                       | no ¬k,Ps     = no ind
                                           where
                                             ind : _
                                             ind (fzero , P0) = ¬P0 P0
                                             ind (fsuc k , Ps) = ¬k,Ps (k , Ps)

decide∈ : ∀{A n} → Decidable≡ A → (x : A) → (xs : Fvec A n) → Dec (x ∈ xs)
decide∈ deq x φs = any (deq x) φs