------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of decision procedures and how to use them
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module README.Design.Decidability where

open import Data.Bool
open import Data.List.Base using (List; []; _∷_)
open import Data.List.Properties using (∷-injective)
open import Data.Nat
open import Data.Nat.Properties using (suc-injective)
open import Data.Product.Base using (uncurry)
open import Data.Unit
open import Function.Base using (id;  _∘_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nary

------------------------------------------------------------------------
-- Reflects

open import Relation.Nullary.Reflects

infix  _≡?₀_ _≡?₁_ _≡?₂_

-- A proof of `Reflects P b` shows that a proposition `P` has the truth value of
-- the boolean `b`. A proof of `Reflects P true` amounts to a proof of `P`, and
-- a proof of `Reflects P false` amounts to a refutation of `P`.

ex₀ : (n : ℕ) → Reflects (n ≡ n) true
ex₀ n = of refl

ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false
ex₁ n = of λ()

ex₂ : (b : Bool) → Reflects (T b) b
ex₂ false = of id
ex₂ true  = of tt

------------------------------------------------------------------------
-- Dec

open import Relation.Nullary.Decidable

-- A proof of `Dec P` is a proof of `Reflects P b` for some `b`.
-- `Dec P` is declared as a record, with fields:
--   does : Bool
--   proof : Reflects P does

ex₃ : (b : Bool) → Dec (T b)
does  (ex₃ b) = b
proof (ex₃ b) = ex₂ b

-- We also have pattern synonyms `yes` and `no`, allowing both fields to be
-- given at once.

ex₄ : (n : ℕ) → Dec (zero ≡ suc n)
ex₄ n = no λ ()

-- It is possible, but not ideal, to define recursive decision procedures using
-- only the `yes` and `no` patterns. The following procedure decides whether two
-- given natural numbers are equal.

_≡?₀_ : (m n : ℕ) → Dec (m ≡ n)
zero  ≡?₀ zero  = yes refl
zero  ≡?₀ suc n = no λ()
suc m ≡?₀ zero  = no λ()
suc m ≡?₀ suc n with m ≡?₀ n
... | yes p = yes (cong suc p)
... | no ¬p = no (¬p ∘ suc-injective)

-- In this case, we can see that `does (suc m ≡? suc n)` should be equal to
-- `does (m ≡? n)`, because a `yes` from `m ≡? n` gives rise to a `yes` from the
-- result, and similarly for `no`. However, in the above definition, this
-- equality does not hold definitionally, because we always do a case split
-- before returning a result. To avoid this, we can return the `does` part
-- separately, before any pattern matching.

_≡?₁_ : (m n : ℕ) → Dec (m ≡ n)
zero  ≡?₁ zero  = yes refl
zero  ≡?₁ suc n = no λ()
suc m ≡?₁ zero  = no λ()
does  (suc m ≡?₁ suc n) = does (m ≡?₁ n)
proof (suc m ≡?₁ suc n) with m ≡?₁ n
... | yes p = of (cong suc p)
... | no ¬p = of (¬p ∘ suc-injective)

-- We now get definitional equalities such as the following.

_ : (m n : ℕ) → does ( + m ≡?₁  + n) ≡ does ( + m ≡?₁ n)
_ = λ m n → refl

-- Even better, from a maintainability point of view, is to use `map` or `map′`,
-- both of which capture the pattern of the `does` field remaining the same, but
-- the `proof` field being updated.

_≡?₂_ : (m n : ℕ) → Dec (m ≡ n)
zero  ≡?₂ zero  = yes refl
zero  ≡?₂ suc n = no λ()
suc m ≡?₂ zero  = no λ()
suc m ≡?₂ suc n = map′ (cong suc) suc-injective (m ≡?₂ n)

_ : (m n : ℕ) → does ( + m ≡?₂  + n) ≡ does ( + m ≡?₂ n)
_ = λ m n → refl

-- `map′` can be used in conjunction with combinators such as `_⊎?_` and
-- `_×?_` to build complex (simply typed) decision procedures.

module ListDecEq₀ {a} {A : Set a} (_≡?ᴬ_ : (x y : A) → Dec (x ≡ y)) where

  _≡?ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
  []       ≡?ᴸᴬ []       = yes refl
  []       ≡?ᴸᴬ (y ∷ ys) = no λ()
  (x ∷ xs) ≡?ᴸᴬ []       = no λ()
  (x ∷ xs) ≡?ᴸᴬ (y ∷ ys) =
    map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≡?ᴬ y ×? xs ≡?ᴸᴬ ys)

-- The final case says that `x ∷ xs ≡ y ∷ ys` exactly when `x ≡ y` *and*
-- `xs ≡ ys`. The proofs are updated by the first two arguments to `map′`.

-- In the case of ≡-equality tests, the pattern
-- `map′ (congₙ c) c-injective (x₀ ≡? y₀ ×? ... ×? xₙ₋₁ ≡? yₙ₋₁)`
-- is captured by `≡?-mapₙ n c c-injective (x₀ ≡? y₀) ... (xₙ₋₁ ≡? yₙ₋₁)`.

module ListDecEq₁ {a} {A : Set a} (_≡?ᴬ_ : (x y : A) → Dec (x ≡ y)) where

  _≡?ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
  []       ≡?ᴸᴬ []       = yes refl
  []       ≡?ᴸᴬ (y ∷ ys) = no λ()
  (x ∷ xs) ≡?ᴸᴬ []       = no λ()
  (x ∷ xs) ≡?ᴸᴬ (y ∷ ys) = ≡?-mapₙ  _∷_ ∷-injective (x ≡?ᴬ y) (xs ≡?ᴸᴬ ys)