Is this idomatic?

Stream: lean4

[Pim Otte]

I have some questions about the code below. This is code I'm writing for use in a handson session to introduce software engineers to Lean. I'm aiming for a piece that shows the power of lean in a clear way, not necessarily the most golfed version.

• In checkValid, is there a way to do without the "have prop" lines? Messing with the structure like this feels weird.
• In checkValid, is there a way to do without the "unreachable .none"? Ideally I would just match on tx.kind and have two branches.
• Is there some way I can derive Repr for Valid?
• Any other pointers? (I guess sumWithdraws/sumDeposits could be improved, but I'm tempted to leave it as is, because then "write a sumDeposits" function is a good exercise to include)

inductive TransactionKind where
  | deposit : TransactionKind
  | withdraw : TransactionKind
deriving Repr, DecidableEq

structure Transaction where
  amount : Nat
  kind : TransactionKind
deriving Repr

abbrev TransactionHistory := List Transaction

@[simp]
def balance (hist : TransactionHistory) : Nat :=
  match hist with
  | .nil => 0
  | .cons tx txs =>
    match tx.kind with
    | .deposit => balance txs + tx.amount
    | .withdraw => balance txs - tx.amount

inductive Valid : TransactionHistory → Type where
  | empty : Valid []
  | afterDeposit   (validity : Valid txs)
                   (amount : Nat) :
                   Valid (⟨ amount, .deposit⟩ :: txs)
  | afterWithdraw  (validity : Valid txs)
                   (amount : Nat)
                   (sufficientBalance : amount <= balance txs) :
                   Valid (⟨amount, .withdraw⟩ :: txs)


@[simp]
def sumWithdraws : TransactionHistory → Nat
  | [] => 0
  | tx :: txs =>
    match tx.kind with
    | .deposit => sumWithdraws txs
    | .withdraw => tx.amount + sumWithdraws txs

@[simp]
def sumDeposits : TransactionHistory → Nat
  | [] => 0
  | tx :: txs =>
    match tx.kind with
    | .deposit => tx.amount + sumDeposits txs
    | .withdraw => sumDeposits txs

def balanceCorrect (validHistory : Valid txs) : balance txs + sumWithdraws txs = sumDeposits txs := by
  match validHistory with
  | .empty => simp
  | .afterDeposit validity amount => {
    simp_arith
    apply balanceCorrect validity
  }
  | .afterWithdraw validity amount sufficientBalance => {
    simp_arith
    erw [Nat.sub_add_cancel sufficientBalance]
    apply balanceCorrect validity
  }

def checkValid : (txs : TransactionHistory) → Option (Valid txs)
  | [] => .some .empty
  | tx :: txs =>
    if h : tx.kind = .deposit then
      do
        let prevValid ← checkValid txs
        have prop : tx = { amount := tx.amount, kind := .deposit} := by
          rw [← h]
        return (prop ▸ .afterDeposit prevValid tx.amount)
    else
      if h1 : tx.kind = .withdraw then
        if sufficientBalance : tx.amount <= balance txs then
          do
            let prevValid ← checkValid txs
            have prop : tx = { amount := tx.amount, kind := .withdraw} := by
              rw [← h1]
            return (prop ▸ .afterWithdraw prevValid tx.amount sufficientBalance)
        else
          .none
      else
        .none

[Marcus Rossel]

You can simplify things by matching on the Transactions and their kind directly.

inductive TransactionKind where
  | deposit
  | withdraw
  deriving Repr, DecidableEq

structure Transaction where
  amount : Nat
  kind : TransactionKind
  deriving Repr

abbrev TransactionHistory := List Transaction

@[simp]
def balance : TransactionHistory → Nat
  | []                         => 0
  | ⟨amount, .deposit⟩ :: txs  => balance txs + amount
  | ⟨amount, .withdraw⟩ :: txs => balance txs - amount

inductive Valid : TransactionHistory → Type where
  | empty : Valid []
  | afterDeposit   (validity : Valid txs)
                   (amount : Nat) :
                   Valid (⟨ amount, .deposit⟩ :: txs)
  | afterWithdraw  (validity : Valid txs)
                   (amount : Nat)
                   (sufficientBalance : amount <= balance txs) :
                   Valid (⟨amount, .withdraw⟩ :: txs)

@[simp]
def sumWithdraws : TransactionHistory → Nat
  | []                         => 0
  | ⟨_, .deposit⟩ :: txs       => sumWithdraws txs
  | ⟨amount, .withdraw⟩ :: txs => amount + sumWithdraws txs

@[simp]
def sumDeposits : TransactionHistory → Nat
  | []                        => 0
  | ⟨amount, .deposit⟩ :: txs => amount + sumDeposits txs
  | ⟨_, .withdraw⟩ :: txs     => sumDeposits txs

theorem balanceCorrect : Valid txs → balance txs + sumWithdraws txs = sumDeposits txs
  | .empty => rfl
  | .afterDeposit validity _ => by
    simp_arith
    apply balanceCorrect validity
  | .afterWithdraw validity _ sufficientBalance => by
    simp_arith
    erw [Nat.sub_add_cancel sufficientBalance]
    apply balanceCorrect validity

def checkValid : (txs : TransactionHistory) → Option (Valid txs)
  | [] => some .empty
  | ⟨amount, .deposit⟩ :: txs => do
      let prevValid ← checkValid txs
      return (.afterDeposit prevValid amount)
  | ⟨amount, .withdraw⟩ :: txs => do
      if sufficientBalance : amount <= balance txs then
        let prevValid ← checkValid txs
        return (.afterWithdraw prevValid amount sufficientBalance)
      else
        none

[Marcus Rossel]

Also, I wasn't aware that one could use @[simp] on non-theorem definitions, so I'm not sure if that's idiomatic.

[Pim Otte]

Ah, yes, that makes sense, thanks!

[Horațiu Cheval]

Marcus Rossel said:

Also, I wasn't aware that one could use @[simp] on non-theorem definitions, so I'm not sure if that's idiomatic.

I wouldn't say @[simp] def is unidiomatic, e.g. https://github.com/leanprover/std4/blob/main/Std/Data/Option/Basic.lean has several @[simp] defs. What it does AFAIK is it generates equational lemmas corresponding to the function definition which can then be used by simp.

[Yaël Dillies]

The equational lemmas are always generated. This is what lets you do rw [my_def]. What changes is whether the equational lemmas are tagged @[simp].

[Horațiu Cheval]

How can I see them without @[simp]? With @[simp] I can do

@[simp] def f : Nat → Nat
  | 0 => 1
  | n + 1 => f n

#check f._eq_2

but f._eq_2 is unknown otherwise

[Horațiu Cheval]

My recalling about this was based on this thread

[Kevin Buzzard]

Try whatsnew in def f : ... (needs a mathlib import) to see what declarations are generated by a definition.

[Alistair Tucker]

Is this idiomatic?

It's probably more idiomatic to have Valid : TransactionHistory → Prop and then prove Decidable (Valid txs).

instance decValid : (txs : TransactionHistory) → Decidable (Valid txs)
  | [] => isTrue .empty
  | ⟨amount, .deposit⟩ :: txs =>
    match decValid txs with
    | isTrue prevValid => isTrue (.afterDeposit prevValid amount)
    | isFalse prevValid' => isFalse (fun | .afterDeposit v a => prevValid' v)
  | ⟨amount, .withdraw⟩ :: txs =>
    match decValid txs with
    | isTrue prevValid =>
      if sufficientBalance : amount <= balance txs then
        isTrue (.afterWithdraw prevValid amount sufficientBalance)
      else
        isFalse (fun | .afterWithdraw _ a sb => sufficientBalance sb)
    | isFalse prevValid' => isFalse (fun | .afterWithdraw v a sb => prevValid' v)

[Pim Otte]

Ah, yeah, that looks very clean. Thanks!