Skip to content

Instantly share code, notes, and snippets.

@gallais
Created April 17, 2014 11:46
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save gallais/10976846 to your computer and use it in GitHub Desktop.
Disjunctive normal form
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₂ ⟧′ ρ
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment