open import 1Lab.Prelude

open import Data.Partial.Total
open import Data.Partial.Base
open import Data.Vec.Base

open import Realisability.PCA

import Realisability.PCA.Sugar as S

module Realisability.Data.Bool {ℓ} (𝔸 : PCA ℓ) where

open S 𝔸
private variable
  ℓ' : Level
  V A B C : Type ℓ'
  a b : ↯ ⌞ 𝔸 ⌟

Booleans in a PCA🔗

We construct booleans in a partial combinatory algebra by defining boolean values to be functions which select one of their two arguments. In effect, we are defining booleans so that the program $if b then x else y$ is simply $b x y .$ Therefore, we have:

`true : ↯⁺ 𝔸
`true = val ⟨ x ⟩ ⟨ y ⟩ x

`false : ↯⁺ 𝔸
`false = val ⟨ x ⟩ ⟨ y ⟩ y

We define an overloaded notation for constructing terms which case on a boolean.

`if_then_else_
  : ⦃ _ : To-term V A ⦄ ⦃ _ : To-term V B ⦄ ⦃ _ : To-term V C ⦄
  → A → B → C → Termʰ V
`if x then y else z = x `· y `· z

We can prove the following properties: applying `true and `false to a single argument results in a defined value; `true selects its first argument; and `false selects its second argument.

abstract
  `true↓₁ : ⌞ a ⌟ → ⌞ `true ⋆ a ⌟
  `true↓₁ x = subst ⌞_⌟ (sym (abs-βₙ [] ((_ , x) ∷ []))) (abs↓ _ _)

  `false↓₁ : ⌞ a ⌟ → ⌞ `false ⋆ a ⌟
  `false↓₁ ah = subst ⌞_⌟ (sym (abs-βₙ [] ((_ , ah) ∷ []))) (abs↓ _ _)

  `true-β : ⌞ a ⌟ → ⌞ b ⌟ → `true ⋆ a ⋆ b ≡ a
  `true-β {a} {b} ah bh = abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ [])

  `false-β : ⌞ a ⌟ → ⌞ b ⌟ → `false ⋆ a ⋆ b ≡ b
  `false-β {a} {b} ah bh = abs-βₙ [] ((b , bh) ∷ (a , ah) ∷ [])

We can define negation using `if_then_else_, and show that it computes as expected.

`not : ↯⁺ 𝔸
`not = val ⟨ x ⟩ `if x then `false else `true

abstract
  `not-βt : `not ⋆ `true ≡ `false .fst
  `not-βt = abs-β _ [] `true ∙ abs-βₙ [] (`true ∷ `false ∷ [])

  `not-βf : `not ⋆ `false ≡ `true .fst
  `not-βf = abs-β _ [] `false ∙ abs-βₙ [] (`true ∷ `false ∷ [])