[Agda] Help with proofs

[Ulf Norell]

Many of your problems come from the clunky proof objects you're passing
around
everywhere. It's often a better idea to represent these kind of constraints
using indexing. Here's how I would do it:

module Octet where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}
{-# BUILTIN NATPLUS _+_ #-}

-- The first thing we want to keep track of is 'zeroness'. We could use a
-- boolean here, but I find that things get clearer if you give them
-- appopriate names.

data IsZero : Set where
  nonZero : IsZero
  isZero  : IsZero

-- This function will be used to compute the zeroness of an 'or'.
bothZero : IsZero -> IsZero -> IsZero
bothZero nonZero _ = nonZero
bothZero isZero  z = z

-- We also want to know whether the least significant bit is set or not.
-- This can be represented by the parity of the number.

data Parity : Set where
  even : Parity
  odd  : Parity

-- The parity of an 'or'.
bothEven : Parity -> Parity -> Parity
bothEven odd  _ = odd
bothEven even p = p

-- The final thing we need to track is the width (or an upper bound on the
-- width) of a bit vector. We can model that as a natural number.

Width = Nat

-- Now a bit vector is datatype indexed by its width, whether it's zero, and
-- its parity. Note that this type encodes bit vectors of arbitrary length.
-- We'll get to octets later.
data Bits : Width -> IsZero -> Parity -> Set where
  zero   : forall {n} -> Bits n isZero even
  setLow : forall {n z} -> Bits (suc n) z even -> Bits (suc n) nonZero odd
  shift  : forall {n p} -> Bits n nonZero p -> Bits (suc n) nonZero even

-- Turning a bit vector to a natural number looks the same as before.
toNat : forall {n z p} -> Bits n z p -> Nat
toNat zero       = 0
toNat (setLow a) = suc (toNat a)
toNat (shift a)  = toNat a + toNat a

-- The difference is that 'or' is defined just as you would like to define
-- it, without any annoying proof objects obscuring the definition, an there
-- are no lemmas to prove.
_or_ : forall {n z₁ z₂ p₁ p₂} -> Bits n z₁ p₁ -> Bits n z₂ p₂ ->
       Bits n (bothZero z₁ z₂) (bothEven p₁ p₂)
zero     or b        = b
setLow a or zero     = setLow a
setLow a or setLow b = setLow (a or b)
setLow a or shift b  = setLow (a or shift b)
shift a  or zero     = shift a
shift a  or setLow b = setLow (shift a or b)
shift a  or shift b  = shift (a or b)

-- Finally an Octet is a bit vector of width 8 with arbitrary zeroness and
-- parity.
data Octet : Set where
  octet : forall {z p} -> Bits 8 z p -> Octet

-- 'or' on octets is defined using 'or' on the underlying bit vector.
_or₈_ : Octet -> Octet -> Octet
octet a or₈ octet b = octet (a or b)

I hope this helps.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080429/623a19ef/attachment.html