Decidable Predicates in Agda

Question

I am new to Agda and I need help to understand the Decidable function and Dec type.

I am trying to define a first-order-logic predicate, and I want to encode with the proof some sort of boolean value. I found the way to do this is using the Dec type..

Now, as far as I get it, to be able to do this, I have to re-define all logic operators to be of type decidable rather than of type set. to do so, I sort of embedded it into new type, this is how I did it for the and operator:

data _∧_ (A B : Set) : Set where 
   _&_ : A → B → A ∧ B 

Dec∧ : {A B : Set} → A ∧ B → Dec (A ∧ B) 
Dec∧ A∧B = yes (A∧B) 

Is it the way to do it, or is there another way?

Then, I want to use this operator to define a relation on Nat values, so I did something like this:

_◆_ : ℕ → ℕ → Dec∧ (Rel ℕ lzero) (ℕ → Set) 
x ◆ y = (0 < x) ∧ (x ² ≡ 2 * y ²) 

but this gives a type error..

I am not sure how to work with Dec and I would appreciate if anyone can guide me to tutorials or examples using it for proving logical statements..

Answer 1

Basically decidable predicate is a predicate for which we have an algorithm which terminates in finite time and returns either a yes together with a proof that it's true, or no together with a proof of it's negation. For example, for each two natural numbers we can either prove that they are equal or that they aren't equal.

What you wrote doesn't type check. Your function should return Dec (Rel ℕ lzero) (ℕ → Set), the first argument is correct, the second however, isn't. It should be a function, for example, \x -> 2 * x.

P.S. To me the function makes no sense. What do you want to accomplish with it?