CODEWITHSUNDEEP
agda
usul
usul

Reputation: 804

Branch on equality test in Agda? (basic)

A very basic question, but as an Agda beginner I'm stumped.

I just want to check if two terms are equal and return different things based on the different cases. I could write my own equality tester, but how do I do this using equiv (or what is the proper way to do it)?

This is a minimal example:

import Data.Nat
import Relation.Binary
myeqtest : ℕ → ℕ → ℕ
myeqtest x y = if x Data.Nat.≟ y then true else false

Error message: .Relation.Nullary.Core.Dec (x .Relation.Binary.Core.Dummy.≡ y) !=< Bool of type Set when checking that the expression x Data.Nat.≟ y has type Bool

I actually want to do something more complicated of course (I know that the above is redundant in several ways), but the point is that x \?= y is not of type Bool, it is of type Set, and I don't know how to turn that Set into a Bool. Thanks.

Upvotes: 3

Views: 1107

Answers (1)

effectfully
effectfully

Reputation: 12715

Boring imports:

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary.Core
open import Data.Bool hiding (_≟_)
open import Data.Nat

Now let's ask Agda, what she thinks:

myeqtest : ℕ -> ℕ -> Bool
myeqtest x y = {!x ≟ y!}

C-C C-d in the hole gives Dec (x ≡ y). Dec is about decidable propositions and defined in the Relation.Nullary.Core module:

data Dec {p} (P : Set p) : Set p where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

I.e. there always exists a proof of either P or ¬ P, where ¬ means "not". This is just a handmade law of excluded middle for some proposition. In our case there always exists a proof, that one number is either equal or non-equal to another.

So Dec has two contructors: yes and no, and you can use them in pattern-matching:

myeqtest : ℕ -> ℕ -> Bool
myeqtest x y with x ≟ y
... | yes _ = true
... | no  _ = false

There is a function in the Relation.Nullary.Decidable module, that turns a Dec into a Bool:

⌊_⌋ : ∀ {p} {P : Set p} → Dec P → Bool
⌊ yes _ ⌋ = true
⌊ no  _ ⌋ = false

So you can define myeqtest as

myeqtest : ℕ -> ℕ -> Bool
myeqtest x y = if ⌊ x ≟ y ⌋ then true else false

or simply

myeqtest : ℕ -> ℕ -> Bool
myeqtest x y = ⌊ x ≟ y ⌋

Upvotes: 9

Related Questions