ex7-1-1.agda

module ex7-1-1 where

data Bool : Set where
  t : Bool
  f : Bool

not : Bool → Bool
not t = f
not f = t

_and_ : Bool → Bool → Bool
t and q = q
f and _ = f

_or_ : Bool → Bool → Bool
t or _ = t
f or q = q

infix  10 ¬_
infixr 9  _∧_
infixr 8  _∨_

open import Data.Nat
prop = ℕ

data form : Set where
  var : prop → form
  ¬_ : form → form
  _∨_ : form → form → form
  _∧_ : form → form → form

assign = prop → Bool

_⟦_⟧ : assign → form → Bool
v ⟦ var p ⟧ = v p
v ⟦ ¬ A ⟧ = not (v ⟦ A ⟧)
v ⟦ A ∨ B ⟧ = (v ⟦ A ⟧) or (v ⟦ B ⟧)
v ⟦ A ∧ B ⟧ = (v ⟦ A ⟧) and (v ⟦ B ⟧)

open import Relation.Binary.PropositionalEquality 
  renaming (_≡_ to _≈_) hiding ([_]) 
open import Relation.Binary.Core using (_≡_; _≢_; refl)

open import Data.Vec

-- x : Vec Bool 4
-- x = f ∷ (f ∷ (f ∷ (t ∷ [])))

data _≲v_ : {n : ℕ} → (Vec Bool n) → (Vec Bool n) → Set where
  leqv-zero  : [] ≲v []
  leqv-base0 : {b : Bool} → (b ∷ []) ≲v (b ∷ [])
  leqv-base1 : (f ∷ []) ≲v (t ∷ [])
  leqv-rec0  : {b : Bool} → {n : ℕ} {x y : Vec Bool n} → x ≲v y → (b ∷ x) ≲v (b ∷ y)
  leqv-rec1  : {n : ℕ} {x y : Vec Bool n} → x ≲v y → (f ∷ x) ≲v (t ∷ y)

x1-≲v-y1 : (f ∷ f ∷ t ∷ f ∷ []) ≲v (f ∷ t ∷ t ∷ f ∷ [])
x1-≲v-y1 = leqv-rec0 (leqv-rec1 (leqv-rec0 leqv-base0))

x2-≲v-y2 : (t ∷ f ∷ t ∷ f ∷ []) ≲v (f ∷ t ∷ t ∷ f ∷ [])
x2-≲v-y2 = {!!}

data _≲f_ : {n : ℕ} → (Vec Bool n → Bool) → (Vec Bool n → Bool) → Set where

-- bVec = 
-- bFunc = (n : ℕ) → (Vec Bool n → Bool)

-- isMonotone : bVec → bVec → bFunc → Set
-- isMonotone x y = λ f → {!!}