# [Agda] record with proof

Serge D. Mechveliani mechvel at botik.ru
Fri Aug 24 21:29:45 CEST 2012

```People,
I am trying to understand usage of Agda by programming the  division
remainder  for natural numbers (of Nat -- Б└∙).
(This is under  Agda-2.3.0.1 + Standard library lib-0.6).
So far, I ignore  Data.Nat.DivMod,  because it is rather difficult to
understand, and I try to begin with a simpler, home-made approach.

remainder n m,  m > 0,   is found by repeated subtraction of m from the
current remainder.
1. remNat  finds the remainder all right.
It uses an auxiliary function  rem  which processes an additional
argument for the  counter  - the number of subtractions applied.
The counter is used in order to make a termination proof trivial.

2. remNatP  is a variant of  remNat  with producing a proof for
"remainder < m".
Its idea is to provide a recursive proof together with a recursive
evaluation of the remainder. As there are the two result values, I
introduce the  record  Rem m  with the two fields. The second field is
for a proof, its type depends on  m  and on the value of the remainder
field  r.
And  remNatP  is not compiled. I wonder, what is wrong there?

-------------------------------------------------------------------
module MyLib where
open import IO.Primitive
open import Relation.Nullary.Core
open import Data.Bool as Bool
open import Data.String as String
open import Data.Nat as Nat
open import Data.Nat.Show
open import Prelude using (toCostring)

lessNat? : Б└∙ -> Б└∙ -> Bool
lessNat? 0       0       = false
lessNat? 0       (suc _) = true
lessNat? (suc _) 0       = false
lessNat? (suc n) (suc m) = lessNat? n m

LessNat? : Б└∙ -> Б└∙ -> Set
LessNat? n m = T (lessNat? n m)

PositiveNat? : Б└∙ -> Set
PositiveNat? 0 = T false
PositiveNat? _ = T true

remNat : Б└∙ -> (m : Б└∙) -> PositiveNat? m -> Б└∙
remNat _ 0 ()   -- unaccessible
remNat n m _ =  rem n n            -- below  m  is a constant subtrahend
where
rem : Б└∙ -> Б└∙ -> Б└∙                -- н╩ n counter -> r,  counter  is the
-- number of subtractions applied
rem 0 _         = 0
rem n 0         = 0                -- accessible only for  m = 1
rem n (suc cnt) = if lessNat? n m then  n
else                  rem (n Б┬╦ m) cnt

record Rem (m : Б└∙) : Set where
field
r          : Б└∙
boundProof : LessNat? r m

remNatP : Б└∙ -> (m : Б└∙) -> PositiveNat? m -> Rem m
remNatP _ 0       ()    -- unaccessible
remNatP n (suc k) _  =  rem n n
where                           -- below  m'  is a constant subtrahend
m' = suc k
rem : Б└∙ -> Б└∙ -> Rem m'               -- н╩ n counter -> remainder by m'
rem 0 _         = record{ r = 0;  boundProof = _ }
rem _ 0         = record{ r = 0;  boundProof = _ }
-- accessible only for  m' = 1
rem n (suc cnt) =
-- (1)
if lessNat? n m' then  record{ r = n;  boundProof = _ }
else                   rem (n Б┬╦ m') cnt

{- (3)
if not (lessNat? n m') then  rem (n Б┬╦ m') cnt
else
record{ r = n;  boundProof = p }
where
p : LessNat? n m'
p = _
-- Unsolved metas at the following locations:  `p = _'
-}

{- (4)
if lessNat? n m' then ( record{ r = n;  boundProof = p }
where
p : LessNat? n m'
p = _
)
else  rem (n Б┬╦ m') cnt
-- Parse error   where<ERROR> ...
-}

main : IO Unit
main = putStrLn (toCostring "done")
-------------------------------------------------------------------

record Rem (m : Б└∙) : Set where
field
r          : Б└∙
boundProof : LessNat? r m
:
I thought that a function cannot return a value of this type other than
providing a proof for  LessNat? r m
(?)
I do not know, may be, I am missing something about dependent records.

4. The variant (1) in  rem  yields
"Unsolved metas at the following locations:"
for the line of  `record ...'.
Why?
In the branch of   lessNat? n m',  the condition for  boundProof  is
trivially satisfied, so, I put  record{ r = n;  boundProof = _ }
-- ?

5. Setting here  `r = 0'  instead of  `r = n'  makes it compiled.
But this function expresses the constant of  0,  not the remainder.

6. The variant (3) uses the construct of
record{ r = n;  boundProof = p }
where
p : LessNat? n m'
p = _
It yields, again,
"Unsolved metas at the following locations:"  for  `p = _'.

7. The variant (4) only transposes the branches of (3) in  if-then-else
into a more natural order.
But the report is different:
"Parse error   where<ERROR> ..."

Can you comment, please? How to fix the program?
Thank you in advance for explanation,

------
Sergei
```