Product.agda

module Product where

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

{-# BUILTIN NATURAL Nat #-}

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

infixr 50 _+_

_*_ : Nat -> Nat -> Nat
zero * m = zero
suc n * m = m + n * m

infixr 60 _*_

data _==_ {X : Set} (x : X) : X -> Set where
  refl : x == x

{-# BUILTIN EQUALITY _==_ #-}

data _><_ (X : Set) (P : X -> Set) : Set where
  _,_ : (x : X) -> P x -> X >< P

infixr 40 _,_

record Product : Set where
  field
    price : Nat
    amount : Nat
    value : Nat >< \ n -> price * amount == n

data Maybe (X : Set) : Set where
  just : X -> Maybe X
  nothing : Maybe X

decideNat : (n m : Nat) -> Maybe (n == m)
decideNat zero zero = just refl
decideNat zero (suc m) = nothing
decideNat (suc n) zero = nothing
decideNat (suc n) (suc m) with decideNat n m
decideNat (suc n) (suc .n) | just refl = just refl
decideNat (suc n) (suc m) | nothing = nothing

mkProduct : Nat -> Nat -> Nat -> Maybe Product
mkProduct price amount value with decideNat (price * amount) value
mkProduct price amount value | just proof = just
  record
    { price = price
    ; amount = amount
    ; value = value , proof
    }
mkProduct price amount value | nothing = nothing