CODEWITHSUNDEEP
agdatheorem-proving
Tan Kian-teng
Tan Kian-teng

Reputation: 81

How to make a Adga function with a premise work

I want to make a subtraction of Natural Number work. However, the argument of the function have a premise that forall a, b in N ; a >= b. so I make some related functions:

data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

data _NotLessThan_ : (n m : ℕ) → Set where
    ZERO : zero NotLessThan zero
    SUC_ZERO : ∀ n → (suc n) NotLessThan zero
    STEP : ∀ m n → m NotLessThan n → (suc m) NotLessThan (suc n)

sub : (m n : ℕ) →  (a : m NotLessThan n) → ℕ
    sub zero (suc n) () -- zero - n can't return
    sub zero zero _ = zero
    sub (suc m) zero _ = (suc m)
    sub (suc x) (suc y) a = sub x y (x NotLessThan y)

However, I get the error:

 Set !=< x NotLessThan y of type Set₁
 when checking that the expression x NotLessThan y has type
 x NotLessThan y

I find tht the type is x NotLessThan y as I excepted. Is there any type error? How to debug this kind of type error or how to declare a function to skip the type-detecting error?

Upvotes: 3

Views: 229

Answers (2)

MrO
MrO

Reputation: 1347

In short

There is a type incompatibility in your code snippet, namely that (x NotLessThan y) is a type, and not a value of type (x NotLessThan y), which you have to provide in order for your function to be type correct. The following snippets corrects the issue:

sub : (m n : ℕ) →  (a : m NotLessThan n) → ℕ
sub .zero .zero ZERO = zero
sub .(suc n) .zero SUC n ZERO = suc n
sub .(suc m) .(suc n) (STEP m n a) = sub m n a

In long

This is the main problem in your code, but there are also several inaccuracies that prevented you from writing a correct code. These are as follow:

  • Your data type name _NotLessThan_ can somewhat be improved to better match mathematical concepts (and to match what you will find in the standard library).

  • Constructors are not usually written with capital letters.

  • You provide two constructors ZERO and SUC_ZERO that have the same purpose, that is saying that any natural number is greater or equal than zero. These can be factorized.

  • Your second constructor SUC_ZERO contains an underscore, which Agda will interpret as the location where the parameter for this constructor will be placed. I feel like this was not intended, in which case you should definitely avoid underscores in constructor names.

  • In your function  sub you case-split on your two natural variables although the third argument (the proof that a is greater that b) already contains the necessary information for the computation to happens. Pattern matching on this argument instead will also avoid any empty cases.

Taking these remarks into account leads to the following definition for your data type:

data _≤_ : ℕ → ℕ → Set where
  z≤s : ∀ {a} → zero ≤ a
  s≤s : ∀ {a b} → a ≤ b → suc a ≤ suc b

From this data type, the sub function is then written very naturally:

sub' : ∀ a b → b ≤ a → ℕ
sub' a .zero z≤s = a
sub' ._ ._ (s≤s p) = sub' _ _ p

Note that in this snippet underscores (and dots on the left side of the definition) are used to mark parameters whose value can be inferred by Agda, which makes visible the fact that the proof is sufficient to compute the subtraction.

To go further

This can be interesting to let Agda compute the proof alone instead of having to provide it whenever you want to make a subtraction. In order to do so, your data type has to be proven decidable, which means that, given two natural numbers a and b, a function has to be written that either computes the proof that a ≤ b or the negation of it. This requires several steps, the first being the definition of the logical false (the empty type):

data ⊥ : Set where

From this data type, the logical negation can be defined:

¬ : Set → Set
¬ A = A → ⊥

We can now define the type of decidable types (roughly, either it can be proven true or false):

data Dec (A : Set) : Set where
  yes : A → Dec A
  no : ¬ A → Dec A

Then, we can prove that for any input, the lesser or equal data type is decidable regarding this definition:

_≤?_ : ∀ a b → Dec (a ≤ b)
zero ≤? b = yes z≤s
suc a ≤? zero = no (λ ())
suc a ≤? suc b with a ≤? b
suc a ≤? suc b | yes p = yes (s≤s p)
suc a ≤? suc b | no ¬p = no λ {(s≤s q) → ¬p q}

In order to encapsulate the error case for the subtraction, we need the maybe monad, which is either and error case, or a value:

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

Finally, we can write a subtraction that takes two natural numbers, checks whether the satisfy the requirement for the subtraction, returns an error if not, and computes it when possible:

_-M_ : (a b : ℕ) → Maybe ℕ
a -M b with b ≤? a
a -M b | yes p = just (sub' a b p)
a -M b | no _ = nothing

As an example of failure, here is an unsound subtraction:

error : Maybe ℕ
error = suc (suc (zero)) -M (suc (suc (suc (suc (suc (suc zero))))))

Here is what Agda gives when evaluating error:

nothing

As an example of success, here is a sound subtraction:

success : Maybe ℕ
success = (suc (suc (suc (suc (suc (suc zero)))))) -M suc (suc (zero))

Here is what Agda gives when evaluating success:

just (suc (suc (suc (suc zero))))

Note that all of these quantities (up until the definition of the maybe data type) can be found in the standard library, and that I deliberately omitted universe levels when presenting them.

Upvotes: 1

white_wolf
white_wolf

Reputation: 646

The expression (x NotLessThan y) is not of type (x NotLessThan y). NotLessThan is a data definition of type set (an indexed one). You construct elements of NotLessThan with its three constructors you have defined. In this case you have to pattern patch on a, to get the appropriate constructor and the element of the type you need. So the last case would be

sub (suc x) (suc y) (STEP _ _ a) = sub x y a

Upvotes: 4

Related Questions