[Agda] record with proof

[Serge D. Mechveliani]

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 Foreign.Haskell
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'  
Please, how to fix this?

Thanks,

------
Sergei