Contrived user history example to show off dependent types

users.idr

module main

{-
I assume you're coming here from
http://chromaticleaves.com/posts/idris-and-dependent-types.html

If not, please take a moment to read it. It's a very important white paper.
Completely serious, too.

Now that we have that out of the way, this gist is a contrived example that
shows how you might enforce a relationship in Idris at compile time instead
of having to enforce it with runtime checks and error handling.

The goal is to make a user history type that tracks user actions and ensures
that users cannot redeem more tokens than they've earned. At any given time,
you can't construct an instance of the History type without supplying a proof
that the number of redeemed tokens is <= the number of earned tokens, so this
particular case doesn't need to be tested.
-}

-- identify users by name only (YOLO)
data User = MkUser String

-- a data type representing the redemption of a token
data Redeem = MkRedeem Int

-- users can earn a token by recommending the app to a user
data Earn = Recommend User

-- user actions are either redeeming tokens or earning them
Action : Type
Action = Either Redeem Earn


-- a history type to keep track of user actions
-- the offset will be explained later, but notice how we use
-- `LTE (redeemed + offset) earned` in the type signature to show you can't
-- make an instance of History unless you can show there are fewer token
-- redemptions than recommendations to frineds
data History : Type where
  MkHist :  (user     : User)               ->
            (redeemed : Nat)                ->
            (offset   : Nat)                ->
            (earned   : Nat)                ->
            LTE (redeemed + offset) earned  ->
            Vect (redeemed + earned) Action ->
            History


-- we can make an empty history using lteZero, a relationship that says
-- 0 is less than or equal to any other natural number
emptyHistory : User -> History
emptyHistory user = MkHist user 0 0 0 lteZero []


-- when the user recommends the app to a friend, we add it to their history.
-- thanks to @esmooov for the rewrite tip!
recommendApp : History -> User -> History
recommendApp (MkHist u r o e p v) friend =
  MkHist u r (S o) (S e) ?recommendPrf v'
    where a  : Action
          a = Right $ Recommend friend
          v' : Vect (r + (S e)) Action
          v' = rewrite (sym $ plusSuccRightSucc r e) in a :: v


-- if our offset is 0 then we can't redeem a token because all we can say for
-- sure is the number of redeemed tokens is <= the number of earned tokens, and
-- there's no way to increase the number of redeemed tokens while still proving
-- that relationship holds. If the offset is greater than 0, we can show that
-- redeemed + (1 + offset) can be rewritten as (redeemed + 1) + offset, without
-- changing the value of the lefthand side of redeemed + offset <= earned.
redeemToken : History -> Redeem -> Maybe History
redeemToken (MkHist _ _ Z     _ _ _) _     = Nothing
redeemToken (MkHist u r (S o) e p v) token =
  Just $ MkHist u (S r) o e ?redeemPrf (Left token :: v)


-- now we need a way to show that if the left hand side of the relation contains
-- the sum of two variables, we can increment one as long as we increment the
-- right side
total
ltePlusK : (k : Nat) -> LTE (n + k) m -> LTE (n + (S k)) (S m)
ltePlusK k p = ?plusK


-- next we'll have to show that we can rewrite the left side of the relation
-- n + (S k) as (S n) + k
total
lteShift : LTE (plus n (S k)) m -> LTE (plus (S n) k) m
lteShift p = ?lteShiftL





---------- Proofs ----------

main.recommendPrf = proof
  intros
  rewrite (plusSuccRightSucc r o)
  mrefine lteSucc
  trivial


main.redeemPrf = proof
  compute
  intro
  intro
  intro
  intro
  rewrite plusSuccRightSucc r o
  intros
  trivial


main.lteShiftL = proof
  intros
  rewrite sym (plusSuccRightSucc n k)
  trivial


main.plusK = proof
  compute
  intros
  rewrite (plusSuccRightSucc n k)
  mrefine lteSucc
  trivial

Can anyone help me out with how exactly the lteShiftL and plusK proofs come into play? They're not explicitly referenced anywhere. My guess would be that these were propositions that were needed during the course of proving redeemPrf and were therefore proved separately in order to be used in redeemPrf. But I'm really kind of baffled by these proofs as source code - how is one supposed to approach reading that? Is it not intended to be read like normal source code but only in the interactive context with the proof assistant?

That's my oversight that lteShiftL and plusK are still there. I added them initially to show what needed to be proved as part of redeemPrf, but I ran into an issue where if I actually used them in redeemPrf it'd work interactively and not typecheck.

I'll leave them there only because they prove the relationships we want to prove, but since I ended up proving redeemPrf without them, you could remove them and everything would still work.