Disjunctive normal form

Disjunctive.agda

module Disjunctive where

open import Data.Product
import Data.Bool as 𝔹
open import Data.Bool.Properties
open import Data.Nat
open import Data.Fin
open import Data.Vec hiding ([_])

open import Algebra.Structures

module CSR = IsCommutativeSemiring isCommutativeSemiring-∨-∧
module BA = IsBooleanAlgebra isBooleanAlgebra

open import Relation.Binary.PropositionalEquality as Eq
open ≡-Reasoning

data formula (n : ℕ) : Set where
  [_] : (k : Fin n) → formula n
  _∧_ _∨_ : (p₁ p₂ : formula n) → formula n

data conj (n : ℕ) : Set where
  [_] : (k : Fin n) → conj n
  _∧_ : (p₁ p₂ : conj n) → conj n

data dnf (n : ℕ) : Set where
  _∨_ : (p₁ p₂ : dnf n) → dnf n
  ↑_  : (p : conj n) → dnf n

↓′ : ∀ {n} (p : conj n) → formula n
↓′ [ k ]     = [ k ]
↓′ (p₁ ∧ p₂) = ↓′ p₁ ∧ ↓′ p₂

↓ : ∀ {n} (p : dnf n) → formula n
↓ (p₁ ∨ p₂) = ↓ p₁ ∨ ↓ p₂
↓ (↑ p)     = ↓′ p

_⟦∧⟧_ : ∀ {n} (p₁ p₂ : dnf n) → dnf n
(p₁ ∨ p₂) ⟦∧⟧ p₃        = (p₁ ⟦∧⟧ p₃) ∨ (p₂ ⟦∧⟧ p₃)
p₁        ⟦∧⟧ (p₂ ∨ p₃) = (p₁ ⟦∧⟧ p₂) ∨ (p₁ ⟦∧⟧ p₃)
(↑ p₁)    ⟦∧⟧ (↑ p₂)    = ↑ (p₁ ∧ p₂)

⟦dnf⟧ : ∀ {n} (p : formula n) → dnf n
⟦dnf⟧ [ k ]    = ↑ [ k ]
⟦dnf⟧ (p₁ ∧ p₂) = ⟦dnf⟧ p₁ ⟦∧⟧ ⟦dnf⟧ p₂
⟦dnf⟧ (p₁ ∨ p₂) = ⟦dnf⟧ p₁ ∨ ⟦dnf⟧ p₂

⟦_⟧_ : ∀ {n} (p : formula n) (ρ : Vec 𝔹.Bool n) → 𝔹.Bool
⟦ [ k ]   ⟧ ρ = lookup k ρ
⟦ p₁ ∧ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ 𝔹.∧ ⟦ p₂ ⟧ ρ
⟦ p₁ ∨ p₂ ⟧ ρ = ⟦ p₁ ⟧ ρ 𝔹.∨ ⟦ p₂ ⟧ ρ

⟦_⟧′_ : ∀ {n} (p : dnf n) (ρ : Vec 𝔹.Bool n) → 𝔹.Bool
⟦ p ⟧′ ρ = ⟦ ↓ p ⟧ ρ

lemma-⟦∧⟧ : ∀ {n} (p₁ p₂ : dnf n) (ρ : Vec 𝔹.Bool n) →
    ⟦ p₁ ⟧′ ρ 𝔹.∧ ⟦ p₂ ⟧′ ρ ≡ ⟦ p₁ ⟦∧⟧ p₂ ⟧′ ρ
lemma-⟦∧⟧ (↑ p₁)   (↑ p₂)    ρ = Eq.refl
lemma-⟦∧⟧ (p₁ ∨ p₂) p₃       ρ =
  let val₁ = ⟦ p₁ ⟧′ ρ
      val₂ = ⟦ p₂ ⟧′ ρ
      val₃ = ⟦ p₃ ⟧′ ρ
      ih₁₃ = lemma-⟦∧⟧ p₁ p₃ ρ
      ih₂₃ = lemma-⟦∧⟧ p₂ p₃ ρ
  in
  begin
    (val₁ 𝔹.∨ val₂) 𝔹.∧ val₃             ≡⟨ CSR.distribʳ val₃ val₁ val₂ ⟩
    (val₁ 𝔹.∧ val₃) 𝔹.∨ (val₂ 𝔹.∧ val₃) ≡⟨ cong₂ 𝔹._∨_ ih₁₃ ih₂₃ ⟩
    ⟦ p₁ ⟦∧⟧ p₃ ⟧′ ρ 𝔹.∨ ⟦ p₂ ⟦∧⟧ p₃ ⟧′ ρ
  ∎
lemma-⟦∧⟧ (↑ p₁)   (p₂ ∨ p₃) ρ =
  let val₁  = ⟦ ↑ p₁ ⟧′ ρ
      val₂  = ⟦ p₂ ⟧′ ρ
      val₃  = ⟦ p₃ ⟧′ ρ
      res₁₂ = ⟦ (↑ p₁) ⟦∧⟧ p₂ ⟧′ ρ
      res₁₃ = ⟦ (↑ p₁) ⟦∧⟧ p₃ ⟧′ ρ
      ih₁₂  = lemma-⟦∧⟧ (↑ p₁) p₂ ρ
      ih₁₃  = lemma-⟦∧⟧ (↑ p₁) p₃ ρ
  in
  begin
    val₁ 𝔹.∧ (val₂ 𝔹.∨ val₃)             ≡⟨ proj₁ CSR.distrib val₁ val₂ val₃ ⟩
    (val₁ 𝔹.∧ val₂) 𝔹.∨ (val₁ 𝔹.∧ val₃) ≡⟨ cong₂ 𝔹._∨_ ih₁₂ ih₁₃ ⟩
    res₁₂ 𝔹.∨ res₁₃
  ∎

lemma : ∀ {n} (p : formula n) (ρ : Vec 𝔹.Bool n) →
        ⟦ p ⟧ ρ ≡ ⟦ ⟦dnf⟧ p ⟧′ ρ
lemma [ k ]     ρ = Eq.refl
lemma (p₁ ∨ p₂) ρ = cong₂ 𝔹._∨_ (lemma p₁ ρ) (lemma p₂ ρ)
lemma (p₁ ∧ p₂) ρ =
  let ih₁  = lemma p₁ ρ
      ih₂  = lemma p₂ ρ
      rec₁ = ⟦dnf⟧ p₁
      rec₂ = ⟦dnf⟧ p₂
  in
  begin
    ⟦ p₁ ⟧ ρ 𝔹.∧ ⟦ p₂ ⟧ ρ       ≡⟨ cong₂ 𝔹._∧_ ih₁ ih₂ ⟩
    ⟦ rec₁ ⟧′ ρ 𝔹.∧ ⟦ rec₂ ⟧′ ρ ≡⟨ lemma-⟦∧⟧ rec₁ rec₂ ρ ⟩
    ⟦ rec₁ ⟦∧⟧ rec₂ ⟧′ ρ
  ∎