1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of decision procedures and how to use them
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --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 4 _≟₀_ _≟₁_ _≟₂_
-- 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 (5 + m ≟₁ 3 + n) ≡ does (2 + 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 (5 + m ≟₂ 3 + n) ≡ does (2 + m ≟₂ n)
_ = λ m n → refl
-- `map′` can be used in conjunction with combinators such as `_⊎-dec_` and
-- `_×-dec_` 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 ×-dec 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₀ ×-dec ... ×-dec 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ₙ 2 _∷_ ∷-injective (x ≟ᴬ y) (xs ≟ᴸᴬ ys)
|
