I would like to create simple bank application in idris.
I have prepared Bank type:
data Bank : Type where
Init : Bank
Deposit : Bank -> Address -> Nat -> Bank
Withdraw : (s : Bank) -> (a : Address) -> (x : Nat) -> (p : LTE x (userDeposit s a)) -> Bank
It is possible to init such Bank, deposit or withdraw some Nats to/from specific Address.
Withdraw is only possible if amount to withdraw is less than user deposit for previous state.
Function userDeposit is self describing:
total userDeposit : (s : Bank) -> (a : Address) -> Nat
userDeposit Init a = 0
userDeposit (Deposit s a x) b = case addrEq a b of
Yes Refl => add x (userDeposit s a)
No _ => userDeposit s b
userDeposit (Withdraw s a x p) b = case addrEq a b of
Yes Refl => sub (userDeposit s a) x p
No _ => userDeposit s b
It is using two arithmetic functions add and sub:
total sub : (x, y : Nat) -> LTE y x -> Nat
sub x 0 p = x
sub (S x) (S y) (LTESucc p) = sub x y p
total add : (x, y : Nat) -> Nat
add x 0 = x
add x (S y) = S (add x y)
I also wanted to have totalDeposit function, but it is a bit problematic:
total totalDeposit : (s : Bank) -> Nat
totalDeposit Init = 0
totalDeposit (Deposit s a x) = add x (totalDeposit s)
totalDeposit (Withdraw s a x p) = sub (totalDeposit s) x (transitive p (lteUserTotal s a))
I can't just subtract x from previous totalDeposit, because I don't have required proof. I could store such redundant proof, but I don't want to do it, because LTE x (userDeposit s a)) should be enough if I prove LTE (userDeposit s a) (totalDeposit s).
I thought it is easy, but I can't prove one case:
total lteUserTotal : (s : Bank) -> (a : Address) -> LTE (userDeposit s a) (totalDeposit s)
lteUserTotal Init a = LTEZero
lteUserTotal (Deposit s b x) a with (addrEq b a)
lteUserTotal (Deposit s a x) a | Yes Refl = ?op_rhs_0 (lteUserTotal s a) --easy
lteUserTotal (Deposit s b x) a | No _ = ?op_rhs_1 (lteUserTotal s a) --easy
lteUserTotal (Withdraw s b x p) a with (addrEq b a)
lteUserTotal (Withdraw s a x p) a | Yes Refl = ?op_rhs_2 (lteUserTotal s a) --easy
lteUserTotal (Withdraw s b x p) a | No _ = ?op_rhs_3 (lteUserTotal s a) --IMPOSSIBLE for me
This is the case, when b withdraws, so a deposit remains the same.
I have no idea how to solve it:
op_rhs_3 : LTE (userDeposit s a) (totalDeposit s) ->
LTE (userDeposit s a) (sub (totalDeposit s) x (transitive p (lteUserTotal s b)))
Anyone knows how to solve my problem without storing proof, that withdraw amount is less than total deposit?
Full code here: https://gist.github.com/SecuFather/6c54f8f757ec0b64070e351906eb6b31
After many attempts I have finally proved, that total balance is at least as big as user balance.
Firstly, I have modified Bank data structure. I have added new constructor Open and address is now Fin. Bank also stores number of accounts in its type.
data Bank : (n : Nat) -> Type where
Init : Bank 0
Open : Bank n -> Bank (S n)
Deposit : Bank n -> (addr : Fin n) -> (amount : Nat) -> Bank n
Withdraw : (b : Bank n) -> (addr : Fin n) -> (amount : Nat) -> (p : LTE amount (userBalance b addr)) -> Bank n
userBalance function now returns 0 on the last possible Open constructor. The rest remains similar:
total userBalance : Bank n -> (addr : Fin n) -> Nat
userBalance (Open b) FZ = 0
userBalance (Open b) (FS addr) = userBalance b addr
userBalance (Deposit b a amount) addr = case decEq addr a of
Yes Refl => add (userBalance b addr) amount
No _ => userBalance b addr
userBalance (Withdraw b a amount p) addr = case decEq addr a of
Yes Refl => sub (userBalance b addr) amount p
No _ => userBalance b addr
Now, the most important part, totalBalance function. I don't make pattern matching on Bank anymore. Instead I'm adding last userBalance to recursive totalBalance. At the end of recursion - for Bank having no accounts I return 0. I had to find the way, how to make Bank structurally smaller without looking at the Bank content. I just needed pop function, which would remove all the actions on last account. It is not so trivial, because I had to preserve actions for all but last addresses.
total totalBalance : {n : Nat} -> Bank n -> Nat
totalBalance b {n = 0} = 0
totalBalance b {n = (S n)} = add (totalBalance (pop b)) (userBalance b FZ)
While implementing pop function, I have noticed that I need to prove, that userBalance remains the same after pop to construct Withdraw for all but last addresses:
total pop : Bank (S n) -> Bank n
pop (Open b) = b
pop (Deposit b FZ amount) = pop b
pop (Deposit b (FS addr) amount) = Deposit (pop b) addr amount
pop (Withdraw b FZ amount p) = pop b
pop (Withdraw b (FS addr) amount p) = Withdraw (pop b) addr amount $ rewrite sym $ userBalanceSameAfterPop b addr in p
userBalanceSameAfterPop turned out to be the longest function, but only withdraw case requires more work, than simple recursion.
total userBalanceSameAfterPop : (b : Bank (S n)) -> (addr : Fin n) -> userBalance b (FS addr) = userBalance (pop b) addr
userBalanceSameAfterPop (Open b) addr = Refl
userBalanceSameAfterPop (Deposit b FZ amount) addr = userBalanceSameAfterPop b addr
userBalanceSameAfterPop (Deposit b (FS a) amount) addr with (decEq addr a)
userBalanceSameAfterPop (Deposit b (FS addr) amount) addr | Yes Refl = rewrite userBalanceSameAfterPop b addr in Refl
userBalanceSameAfterPop (Deposit b (FS a) amount) addr | No c = userBalanceSameAfterPop b addr
userBalanceSameAfterPop (Withdraw b FZ amount p) addr = userBalanceSameAfterPop b addr
userBalanceSameAfterPop (Withdraw b (FS a) amount p) addr with (decEq addr a)
userBalanceSameAfterPop (Withdraw b (FS addr) amount p) addr | Yes Refl = rewrite userBalanceSameAfterPop b addr in
prf where
total prf : {x, y : Nat} -> {p1, p2 : LTE y x} -> sub x y p1 = sub x y p2
prf {y = 0} = Refl
prf {p1 = (LTESucc p1)} {p2 = (LTESucc p2)} = prf
userBalanceSameAfterPop (Withdraw b (FS a) amount p) addr | No c = userBalanceSameAfterPop b addr
After this, I was ready for final proof. Having pop and userBalanceSameAfterPop makes it piece of cake:
total lteUserTotal : {n : Nat} -> (b : Bank n) -> (addr : Fin n) -> LTE (userBalance b addr) (totalBalance b)
lteUserTotal b FZ {n = (S n)} = lteAddLeft
lteUserTotal b (FS addr) {n = (S n)} = rewrite userBalanceSameAfterPop b addr in
transitive (lteUserTotal (pop b) addr) lteAddRight
Full code here: https://gist.github.com/SecuFather/6c54f8f757ec0b64070e351906eb6b31
Maybe someone will find it useful.
Thank you @NaïmFavier for showing me a good direction.