# [Agda] record with proof

Serge D. Mechveliani mechvel at botik.ru
Sun Aug 26 23:07:24 CEST 2012

```On Fri, Aug 24, 2012 at 11:29:45PM +0400, Serge D. Mechveliani wrote:
> [..]
> 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?
>
> [..]

It looks like I have fixed it. See below  remBySuc.

--------------------------------------------------------------------
module IntResidue where
open import Data.Nat as Nat renaming ( _Б┴╓_ to _NБ┴╓_; _Б┴╓?_ to _NБ┴╓?_ )

-- Remainder of division of  n  by  (suc m)

record Rem (m : Б└∙) : Set where
field  r          : Б└∙     -- remainer by  suc m
boundProof : r NБ┴╓ m

remBySuc : Б└∙ -> (m : Б└∙) -> Rem m
remBySuc n m =  rem n n
where                           -- below  m'  is a constant subtrahend
m' = suc m
rem : Б└∙ -> Б└∙ -> Rem m                -- н╩ n counter -> remainder by m'
rem 0 _         = record{ r = 0;  boundProof = zБ┴╓n }
rem _ 0         = record{ r = 0;  boundProof = zБ┴╓n }
-- accessible only for  m = 0
rem n (suc cnt)  with  n NБ┴╓? m
...            | yes p =  record{ r = n;  boundProof = p }
...            | _     =  rem (n Б┬╦ m') cnt
--------------------------------------------------------------------

Is it all right?
Trying to use it:

--------------------------------------------------------------
module Foo where
open import IO.Primitive
open import Data.String as String
open import Data.Nat as Nat
open import Data.Nat.Show
open import Prelude using (toCostring)  -- by F. Kettelhoit
open import IntResidue                  -- my lib

remRes : Rem 3
remRes = remBySuc 14 3  -- remainder by 4

rm : Б└∙
rm = remRes.r

main : IO Unit
main = putStrLn (toCostring (show rm))
------------------------------------------------------

The compiler compiles  IntResidue,
and for  Foo,  it reports
Not in scope:
remRes.r

I wonder: how to take the  r  field in  remRes ?
I tried
(Rem 3).r

-- because the Guide says that if  r  is a field in a record  RR,  then
RR.r  is a function (value)  r  in a module  RR  related to the record
RR.

But the compiler rejects this `(Rem 3).r'