[Agda] record with proof
Serge D. Mechveliani
mechvel at botik.ru
Fri Aug 24 21:29:45 CEST 2012
People,
can you, please, answer my questions on the following simple program?
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 Foreign.Haskell
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")
-------------------------------------------------------------------
3. About
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
More information about the Agda
mailing list