Why Lean

The problemTwo promos landed on the same item and sold it below what we paid. Each was approved and reviewed on its own. Nobody checked what they do together.

It has already happened

Amazon Prime Day, July 2019: everything at $94.48
Items sold by Amazon itself, a $13,000 Canon lens among them, went out at $94.48. One shopper worked out that the system was meant to charge 94.48% of the discounted price and instead put $94.48 down as the final amount. A percentage confused with an absolute value — exactly what types and a proof catch. Amazon shipped many of those orders anyway.
techspot.com
Amazon UK and RepricerExpress, December 2014: everything at a penny
Automatic repricing software was supposed to keep prices just under the competition. Instead, between 7pm and 8pm on a Friday, a bug sent hundreds of items out for nothing. One seller shipped 675 items normally priced at £5–100 for a penny each and lost £20,000. The worse part: Amazon could not cancel orders already on their way — FBA warehouses shipped without ever looking at the price. The invariant "price never below the floor" belongs at the boundary of the system, not in an external repricer you trust.
iol.co.za

A test is a sentence about one case. “This pair of promos is fine” gets checked and passes. More promos keep arriving and the pairs between them grow quadratically. Nobody writes that many tests.

Nothing crashes. The order goes through the normal path and shows up in monitoring as a successful sale. Somebody finds it at month end, looking at margin per SKU. Or earlier, if an employee stumbles onto the combination by accident.

Lean lets you write a different sentence: “no set of promos takes the price below cost”. That one covers every case at once, and it has no green-tests state — it is either proved or refuted by a specific pair.

The compiler catches one more thing. If we ever want to add a new kind of discount — cashback, say — the file stops compiling. The function that computes the size of a discount matches on the promo type case by case, the new case has no branch, and Lean names the missing one out loud. Until that branch is written, until somebody decides what cashback takes off the price, there is no build. The rule itself is never at risk: the proof never looks inside a mechanic, and it bounds the receipt total from below. Later cashback payments are outside that guarantee.

Where else rules add up

Shipping rules, tariff plans, loyalty tiers, marketplace commission schedules. Anywhere rules compose and nobody owns the sum.

Where the line is

You can ship pricing without a proof assistant. The question is what kind of sentence you need. “This pair is fine” is a test, and there will never be enough of them. “No set of promos takes the price below cost” is what the business asked for in the first place.

The proof only bounds the receipt total. Later cashback payments, shipping, and other expenses are outside the model, so the theorem does not establish profitability. If the list price starts below cost, this model raises the total to cost even without promos — a chosen policy, not a property of Lean.

The Pricing.lean file from this write-up compiles as a whole: Lean 4.34, no errors. The numbers in the output are what the compiler printed.

cost floor · 32.00Item.cost · what we paid

price50.00Item.price · list

price37.50after −25%

1An item has two prices. The engine sees one.

React Flow

Step 1 of 16
An item has two prices
One is what we sell it for. The other is what we paid, and it lives elsewhere: in procurement, in the ERP, in a supplier feed. The pricing engine never sees it. The code stores cents: 5000 means 50.00, and 3200 means 32.00.
Pricing.lean
```
-- what we sell it for, and what we paid
structure Item where
  price : Nat
  cost  : Nat

def sneakers : Item := { price := 5000, cost := 3200 }
```
Step 2 of 16
Marketing sets up the mechanics
A percentage and a flat amount. Marketing configures both in an admin panel, bypassing the deploy and the code review: no developer ever hears about it.
Pricing.lean
```
-- two mechanics: a percentage and a flat amount
inductive Promo where
  | percent (p : Nat)
  | fixed   (cents : Nat)
```
Step 3 of 16
The size of one discount
cut takes a price and one promo and returns the discount amount. Percentages use the price passed in. Money is stored in cents, so division rounds the discount down to a whole cent. A flat amount does not look at the price at all.
Pricing.lean
```
-- discount in cents: −25% of 50.00 is 12.50, a flat 5.00 is always 5.00
def cut (price : Nat) : Promo → Nat
  | .percent p => price * p / 100
  | .fixed c   => c
```
Step 4 of 16
How they stack
stack walks the list and hands cut the already reduced price each time. After the first 25% discount, 37.50 remains; the next promo uses that amount. Nothing here mentions cost.
Pricing.lean
```
-- one at a time: each percentage uses the already reduced price
def stack (price : Nat) : List Promo → Nat
  | []      => price
  | p :: ps => stack (price - cut price p) ps
```

Step 5 of 16

One promo

The category sale and the coupon each offer 25% off. On its own, each reduces 50.00 to 37.50, above the cost of 32.00. These are the very same two promos we will combine next: both individual tests pass.

Pricing.lean

def categorySale : Promo := .percent 25
def coupon : Promo := .percent 25

-- each of these two promos alone leaves the price above cost
example : stack sneakers.price [categorySale] = 3750 := by decide
example : stack sneakers.price [coupon] = 3750 := by decide

Output

Pricing.lean: no errors

Step 6 of 16
What if two land together?
One marketer set up the category sale in May. Another set up the coupon in June. Each is safe on its own. And together? There are 30 promos and 435 pairs, and nobody tested this pair. After the first promo, 37.50 remains against a cost of 32.00. Do you think the coupon will keep the price above cost?
The result is 28.13, which is 3.87 below cost. The second 25% applies to 37.50: the discount of 9.375 rounds down to 9.37. Combining two individually safe promos breaks the rule.
−25% coupon
Pricing.lean
```
def promos : List Promo := [categorySale, coupon]

#eval stack sneakers.price promos
```
Output
```
2813
```

Step 7 of 16

Clamp it at cost

The customer now pays 32.00. But the report still calculates its discount through the old engine, bypassing the receipt: 3200 paid, 2187 reported as discounted, 1800 actually discounted. Two different calculations cause the mismatch, not max itself. Reading the discount from the final receipt fixes the reporting issue too.

Pricing.lean

-- clamp the total at cost
def clamped (i : Item) (ps : List Promo) : Nat :=
  max i.cost (stack i.price ps)

-- the report reads the promo engine and skips the receipt
def reported (i : Item) (ps : List Promo) : Nat :=
  i.price - stack i.price ps

#eval clamped sneakers promos
#eval reported sneakers promos
#eval sneakers.price - clamped sneakers promos

Output

3200
2187
1800

Step 8 of 16
State the rule
A theorem is a claim the compiler is obliged to check. First it has to be written down. Here is what the business wants: for any item and any set of promos, the total stays at or above cost. The ∀ reads "for all", and that is what separates this from a test, which speaks about one case. So far it is only a statement: neither proved nor disproved.
Pricing.lean
```
-- what the business meant all along:
-- no matter how many promos, the total never drops below cost
def never_below_cost : Prop :=
  ∀ (i : Item) (ps : List Promo), i.cost ≤ stack i.price ps
```

Step 9 of 16

Assume it holds

The pair already dropped the price to 28.13, but so far that is an observation: the compiler knows nothing about it and will not bring it up the next time someone edits the engine. To let it know, you state the negation of the rule as a theorem and prove it. In Lean ¬P is shorthand for P → False, so the job is to derive a contradiction from the assumption. That is what intro does — it takes the premise and gives it a name. Now rule is the assumption "the rule holds", and what is left to prove is False.

Step 10 of 16

Apply it to one item

rule speaks about every item and every set of promos at once. Apply it to one — these sneakers and that very pair. Out comes bad: 3200 ≤ 2813. The numbers plainly do not add up, and that is the point — bad rests on the assumption made a step earlier, and it falls together with it.

Step 11 of 16

Reach a contradiction

Take the line apart. bad is "3200 ≤ 2813", obtained from the assumption. (by decide) proves the opposite: Lean simply evaluates the same inequality and gets "false". absurd takes a claim together with its negation and produces anything at all — from a contradiction everything follows; what is needed from it here is False. exact hands that False to the goal, and the theorem is closed. So the assumption fails: the rule does not hold. The counterexample stays in the file, and the compiler re-runs it on every build.

Pricing.lean

-- "false" — which also has to be proved
theorem stack_breaks_the_rule : ¬ never_below_cost := by
  -- intro takes the premise and names it rule: "the rule holds"
  intro rule
  -- have applies rule to these sneakers: bad is 3200 ≤ 2813
  have bad := rule sneakers promos
  -- bad is 3200 ≤ 2813, and (by decide) computes it and proves it false
  -- absurd turns a claim and its negation into False, exact hands it to the goal
  exact absurd bad (by decide)

Pricing.lean

-- "false" — which also has to be proved
theorem stack_breaks_the_rule : ¬ never_below_cost := by
  -- intro takes the premise and names it rule: "the rule holds"
  intro rule
  -- have applies rule to these sneakers: bad is 3200 ≤ 2813
  have bad := rule sneakers promos
  -- bad is 3200 ≤ 2813, and (by decide) computes it and proves it false
  -- absurd turns a claim and its negation into False, exact hands it to the goal
  exact absurd bad (by decide)

Pricing.lean

-- "false" — which also has to be proved
theorem stack_breaks_the_rule : ¬ never_below_cost := by
  -- intro takes the premise and names it rule: "the rule holds"
  intro rule
  -- have applies rule to these sneakers: bad is 3200 ≤ 2813
  have bad := rule sneakers promos
  -- bad is 3200 ≤ 2813, and (by decide) computes it and proves it false
  -- absurd turns a claim and its negation into False, exact hands it to the goal
  exact absurd bad (by decide)

Output

Pricing.lean: no errors

Step 12 of 16

The pool the discounts are paid from

Everything the promos may spend is the margin: the gap between the list price and cost. On these sneakers that is 18.00. Until now promos were computed from the price and knew nothing about cost; now they share a wallet.

Step 13 of 16

You cannot draw on an empty wallet

spend takes the smaller of two amounts: what the promo requests and what remains in the pool. It subtracts taken from both the price and the pool. The next percentage still uses the already reduced price. The first promo takes 12.50; the second asks for 9.37 but receives only the remaining 5.50.

Step 14 of 16

A one-line proof

The total is cost plus the remaining pool. The remainder has type Nat and cannot be negative. Nat.le_add_right proves that a number is no greater than itself plus a non-negative number. One promo gives 37.50; the pair and three greedy promos give 32.00. The guarantee covers the receipt total, not every expense the shop incurs.

Pricing.lean

-- the entire discount pool is the margin
def margin (i : Item) : Nat := i.price - i.cost

-- take what you ask for, or what is left
def spend (price : Nat) : Nat → List Promo → Nat
  | budget, []      => budget
  | budget, p :: ps =>
      let taken := min (cut price p) budget
      spend (price - taken) (budget - taken) ps

-- total: cost plus whatever is left of the pool
def checkout (i : Item) (ps : List Promo) : Nat :=
  i.cost + spend i.price (margin i) ps

theorem checkout_never_below_cost (i : Item) (ps : List Promo) :
    i.cost ≤ checkout i ps :=
  Nat.le_add_right _ _

#eval checkout sneakers [categorySale]
#eval checkout sneakers promos
#eval checkout sneakers [.percent 50, .fixed 9000, .percent 90]

Output

3750
3200
3200

Pricing.lean

-- the entire discount pool is the margin
def margin (i : Item) : Nat := i.price - i.cost

-- take what you ask for, or what is left
def spend (price : Nat) : Nat → List Promo → Nat
  | budget, []      => budget
  | budget, p :: ps =>
      let taken := min (cut price p) budget
      spend (price - taken) (budget - taken) ps

-- total: cost plus whatever is left of the pool
def checkout (i : Item) (ps : List Promo) : Nat :=
  i.cost + spend i.price (margin i) ps

theorem checkout_never_below_cost (i : Item) (ps : List Promo) :
    i.cost ≤ checkout i ps :=
  Nat.le_add_right _ _

#eval checkout sneakers [categorySale]
#eval checkout sneakers promos
#eval checkout sneakers [.percent 50, .fixed 9000, .percent 90]

Output

3750
3200
3200

Pricing.lean

-- the entire discount pool is the margin
def margin (i : Item) : Nat := i.price - i.cost

-- take what you ask for, or what is left
def spend (price : Nat) : Nat → List Promo → Nat
  | budget, []      => budget
  | budget, p :: ps =>
      let taken := min (cut price p) budget
      spend (price - taken) (budget - taken) ps

-- total: cost plus whatever is left of the pool
def checkout (i : Item) (ps : List Promo) : Nat :=
  i.cost + spend i.price (margin i) ps

theorem checkout_never_below_cost (i : Item) (ps : List Promo) :
    i.cost ≤ checkout i ps :=
  Nat.le_add_right _ _

#eval checkout sneakers [categorySale]
#eval checkout sneakers promos
#eval checkout sneakers [.percent 50, .fixed 9000, .percent 90]

Output

3750
3200
3200

Step 15 of 16

The next mechanic

Marketing asks for cashback. The file stops compiling until someone says what this mechanic takes off the price. The proof needs no rewrite: it never looks inside a mechanic.

Pricing.lean

inductive Promo where
  | percent  (p : Nat)
  | fixed    (cents : Nat)
  -- a new mechanic from marketing
  | cashback (p : Nat)

def cut (price : Nat) : Promo → Nat
  | .percent p => price * p / 100
  | .fixed c   => c

Output

error: Missing cases:
(Promo.cashback _)

Step 16 of 16

Declare its share

Cashback is paid after the purchase, so it leaves the receipt total unchanged: cut returns 0. The file compiles again and the proof stays the same. It guarantees only that the receipt total is at least cost. A later cashback payment can reduce net proceeds below cost; accounting for it requires a different model and a separate rule.

Pricing.lean

inductive Promo where
  | percent  (p : Nat)
  | fixed    (cents : Nat)
  | cashback (p : Nat)

def cut (price : Nat) : Promo → Nat
  | .percent p => price * p / 100
  | .fixed c   => c
  -- cashback is paid back after the purchase — it takes nothing off the price
  | .cashback _ => 0

-- the proof is unchanged, nobody even had to open it
theorem checkout_never_below_cost (i : Item) (ps : List Promo) :
    i.cost ≤ checkout i ps :=
  Nat.le_add_right _ _

Output

Pricing.lean: no errors

Use ← and → to move between steps.

Check yourself

Why does the report disagree after clamping in this example?

Why can the budget version never go below cost?

Answered 0 of 2

Why Lean

It has already happened

Amazon Prime Day, July 2019: everything at $94.48

Amazon UK and RepricerExpress, December 2014: everything at a penny

Where else rules add up

Where the line is

An item has two prices

Marketing sets up the mechanics

The size of one discount

How they stack

One promo

What if two land together?

Clamp it at cost

State the rule

Assume it holds

Apply it to one item

Reach a contradiction

The pool the discounts are paid from

You cannot draw on an empty wallet

A one-line proof

The next mechanic

Declare its share

Check yourself