Idris银行应用中用户存款≤总存款的证明难题求助

问题背景 #

已定义Bank类型：

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

实现了userDeposit、add、sub等函数，在证明LTE (userDeposit s a) (totalDeposit s)时，卡在Withdraw分支中取款地址b与目标地址a不同的场景，需要推导的目标类型为：

op_rhs_3 : LTE (userDeposit s a) (totalDeposit s) -> 
           LTE (userDeposit s a) (sub (totalDeposit s) x (transitive p (lteUserTotal s b)))

核心思路 #

当a ≠ b时，userDeposit (Withdraw s b x p) a = userDeposit s a，而totalDeposit (Withdraw s b x p) = totalDeposit s - x（合法，因为x ≤ userDeposit s b ≤ totalDeposit s）。此时要证原用户a的存款仍小于等于新总存款，关键利用两个Nat的LTE性质：

1. 若x ≤ y且(a + x) ≤ y，则a ≤ y - x（对应lte_sub_iff_add系列定理）
2. 任意两个用户的存款之和小于等于总存款，即userDeposit s a + userDeposit s b ≤ totalDeposit s

具体实现 #

op_rhs_3 : LTE (userDeposit s a) (totalDeposit s) -> 
           LTE (userDeposit s a) (sub (totalDeposit s) x (transitive p (lteUserTotal s b)))
op_rhs_3 ih = lte_sub_iff_add_right (transitive (lteAddRight p) user_sum_le_total)
  where
    -- 归纳证明两个用户的存款之和小于等于总存款
    user_sum_le_total : LTE (userDeposit s a + userDeposit s b) (totalDeposit s)
    user_sum_le_total Init = lteZeroPlus
    user_sum_le_total (Deposit s addr n) =
      case addr == a, addr == b of
        (True, _) => lteAddRight user_sum_le_total
        (_, True) => lteAddLeft user_sum_le_total
        (False, False) => user_sum_le_total
    user_sum_le_total (Withdraw s addr x' p') =
      case addr == a, addr == b of
        (True, _) => lteAddRight user_sum_le_total
        (_, True) => lteAddLeft user_sum_le_total
        (False, False) => user_sum_le_total

代码说明 #

• user_sum_le_total通过归纳法完成证明：初始状态总存款为0，两个用户存款和也为0；Deposit/Withdraw操作仅影响单个用户的存款，因此两个用户的存款和与总存款的LTE关系始终成立。
• lteAddRight p推导userDeposit s a + x ≤ userDeposit s a + userDeposit s b（因为x ≤ userDeposit s b）。
• 结合user_sum_le_total得到userDeposit s a + x ≤ totalDeposit s，再通过lte_sub_iff_add_right直接推导得出userDeposit s a ≤ totalDeposit s - x，完成目标证明。

内容的提问来源于stack exchange，提问作者rejkowic