WhyПесочница

Зачем нужен Lean

ПроблемаДве акции сошлись на одном товаре и продали его дешевле закупки. Каждую согласовали и проверили по отдельности. Их сочетание не проверял никто.

Это уже случалось

  • Amazon Prime Day, июль 2019: всё по $94.48

    Официальные товары Amazon, включая объектив Canon за $13 000, продавались за $94.48. Один из покупателей предположил, что система должна была взять 94.48% цены после скидки, а вместо этого поставила $94.48 как итоговую сумму. Классическая путаница процента и абсолютного значения — ровно то, что ловится типами и доказательством. Многие такие заказы Amazon при этом выполнил.

    techspot.com

  • Amazon UK и RepricerExpress, декабрь 2014: всё по одному пенни

    Софт автоматического репрайсинга должен был держать цены чуть ниже конкурентов, но в пятницу с 19:00 до 20:00 из-за ошибки сотни товаров ушли за бесценок. Одна продавщица отдала 675 товаров обычной ценой £5–100 по пенни и потеряла £20 000. Отдельная боль: уже отправленные заказы Amazon отменить не смог — склады FBA отгружали товар, не глядя на цену. Инвариант «цена не ниже нижней границы» должен проверяться на границе системы, а не доверяться внешнему репрайсеру.

    iol.co.za

Тест — это высказывание про один случай. «Эта пара акций в порядке» проверяется и проходит. Акций становится больше, пар между ними — квадратично больше. Тестов столько не пишет никто.

Ничего при этом не падает. Заказ проходит обычным путём и в мониторинге выглядит успешной продажей. Находят это в конце месяца, когда кто-нибудь смотрит маржу по SKU. Или раньше, если сотрудник наткнётся на сочетание случайно.

Lean позволяет высказать другое: «никакой набор акций не опустит цену ниже закупочной». Это утверждение про все случаи сразу, и у него нет состояния «тесты зелёные» — оно либо доказано, либо опровергнуто конкретной парой.

Компилятор ловит и ещё одно. Если в какой-то момент мы захотим добавить новый тип скидки — скажем, кешбэк, — файл перестанет собираться. Размер скидки считает функция, которая разбирает типы акций по случаям; для нового случая ветки в ней нет, и Lean называет пропущенный случай по имени. Пока ветку не дописали, то есть не решили, сколько кешбэк снимает с цены, сборки не будет. Само правило при этом в безопасности: доказательство не заглядывает внутрь механик и гарантирует нижнюю границу суммы в чеке. Последующие выплаты кешбэка оно не учитывает.

Где ещё складываются правила

Правила доставки, тарифные планы, уровни лояльности, схемы комиссий. Везде, где правила складываются, а за сумму никто не отвечает.

Где проходит граница

Прайсинг прекрасно живёт без пруф-ассистента. Разговор о том, какого рода высказывание тебе нужно. «Эта пара в порядке» — тест, и их всегда будет мало. «Никакой набор акций не опустит цену ниже закупочной» — то, что бизнес просил с самого начала.

Здесь доказывается только нижняя граница суммы в чеке. Кешбэк после покупки, доставка и другие расходы в модель не входят: прибыльность продажи из этой теоремы не следует. Если прайс изначально ниже закупочной, эта модель поднимет итог до закупочной даже без акций — это выбранное правило, а не свойство Lean.

Файл Pricing.lean из этого разбора собирается целиком: Lean 4.34, ноль ошибок. Числа в выводе — то, что напечатал компилятор.

React Flow

  1. Шаг 1 из 16

    У товара две цены

    Одна — за сколько продаём, вторая — за сколько купили. Вторая обычно живёт в другой системе: в закупках, в 1С, в выгрузке от поставщика. Движок цен про неё не знает. В коде храним копейки: 5000 — это 50.00, 3200 — это 32.00.

    Pricing.lean
    -- за сколько продаём и за сколько купили
structure Item where
  price : Nat
  cost  : Nat

def sneakers : Item := { price := 5000, cost := 3200 }

  2. Шаг 2 из 16

    Механики заводит маркетинг

    Процент и фиксированная сумма. Обе заводятся через админку, минуя деплой и ревью: разработчик об этом просто не узнаёт.

    Pricing.lean
    -- две механики: процент и фиксированная сумма
inductive Promo where
  | percent (p : Nat)
  | fixed   (cents : Nat)

  3. Шаг 3 из 16

    Размер одной скидки

    cut берёт цену и одну акцию и возвращает размер скидки. Процент считается от той цены, что передали. Деньги храним в копейках, поэтому при делении размер скидки округляется вниз до целой копейки. Фиксированная сумма на цену не смотрит вовсе.

    Pricing.lean
    -- скидка в копейках: −25% от 50.00 это 12.50, фикс 5.00 это всегда 5.00
def cut (price : Nat) : Promo → Nat
  | .percent p => price * p / 100
  | .fixed c   => c

  4. Шаг 4 из 16

    Как они складываются

    stack идёт по списку и на каждом шаге передаёт cut уже сниженную цену. После первой скидки 25% остаётся 37.50; следующая акция будет считаться от этой суммы. Про закупочную здесь не сказано ни слова.

    Pricing.lean
    -- по очереди: каждый процент — от уже сниженной цены
def stack (price : Nat) : List Promo → Nat
  | []      => price
  | p :: ps => stack (price - cut price p) ps

  5. Шаг 5 из 16

    Одна акция

    Категорийная акция и купон дают по 25%. Каждая по отдельности снижает цену с 50.00 до 37.50 — выше закупки 32.00. Проверяем именно те две акции, которые дальше применим вместе: оба теста проходят.

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

-- каждая из этих двух акций по отдельности оставляет цену выше закупочной
example : stack sneakers.price [categorySale] = 3750 := by decide
example : stack sneakers.price [coupon] = 3750 := by decide

    Вывод

    Pricing.lean: no errors

  6. Шаг 6 из 16

    А если применить две сразу?

    Категорийную акцию завёл один маркетолог в мае. Купон — другой, в июне. По отдельности обе безопасны. А вместе? Акций 30, пар между ними 435, и эту пару никто не проверил. После первой акции осталось 37.50 при закупке 32.00. Как думаешь, останемся выше закупочной после купона?

    Получилось 28.13 — ниже закупочной на 3.87. Вторые 25% считаются от 37.50: скидка 9.375 округляется вниз до 9.37. Именно сочетание двух безопасных по отдельности акций нарушило правило.

    −25% купон
    Pricing.lean
    def promos : List Promo := [categorySale, coupon]

#eval stack sneakers.price promos

    Вывод

    2813

  7. Шаг 7 из 16

    Обрезать по закупочной

    Клиент теперь платит 32.00. Но отчёт по-прежнему считает скидку через старый движок, мимо чека: заплачено 3200, в отчёте скидка 2187, фактически выдано 1800. Причина расхождения — два разных расчёта, а не сам max. Если отчёт берёт скидку из итоговой суммы чека, обрезка решает и эту проблему.

    Pricing.lean
    -- обрезаем итог по закупочной
def clamped (i : Item) (ps : List Promo) : Nat :=
  max i.cost (stack i.price ps)

-- отчёт берёт число из движка акций, мимо чека
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

    Вывод

    3200
2187
1800

  8. Шаг 8 из 16

    Сформулировать правило

    Теорема — это утверждение, которое компилятор обязан проверить. Сначала его надо записать. Вот то, чего хочет бизнес: для любого товара и любого набора акций итог не ниже закупочной. Значок ∀ читается «для всех» — он и отличает это от теста, который говорит про один случай. Пока это только формулировка: не доказана и не опровергнута.

    Pricing.lean
    -- то, что бизнес имел в виду с самого начала:
-- сколько скидок ни применяй, итог не ниже закупочной
def never_below_cost : Prop :=
  ∀ (i : Item) (ps : List Promo), i.cost ≤ stack i.price ps

  9. Шаг 9 из 16

    Допустить, что оно верно

    Пара акций уже уронила цену до 28.13, но пока это наблюдение: компилятор о нём не знает и при следующей правке движка о нём не напомнит. Чтобы знал, отрицание правила записывают теоремой и доказывают. ¬P в Lean — это сокращение для P → False, значит надо из допущения вывести противоречие. Этим занят intro — он забирает посылку и даёт ей имя. Теперь rule — это предположение «правило выполняется», а доказать осталось False.

    Шаг 10 из 16

    Применить к одному товару

    rule говорит про все товары и все наборы акций сразу. Применяем его к одному — к этим кроссовкам и к той самой паре. Получаем bad: 3200 ≤ 2813. Числа здесь заведомо не сходятся, и так и задумано — bad держится на допущении, сделанном шагом раньше, и рухнет вместе с ним.

    Шаг 11 из 16

    Получить противоречие

    Разберём строку по частям. bad — это «3200 ≤ 2813», полученное из допущения. (by decide) доказывает обратное: Lean честно считает то же неравенство и получает «ложь». absurd принимает утверждение вместе с его отрицанием и выдаёт что угодно — из противоречия следует всё; здесь от него нужен False. exact отдаёт этот False как доказательство цели, и на этом теорема закрыта. Значит, допущение неверно: правило не выполняется. Контрпример остаётся в файле, и компилятор пересчитывает его при каждой сборке.

    Pricing.lean
    -- «неправда» — и это тоже надо доказать
theorem stack_breaks_the_rule : ¬ never_below_cost := by
  -- intro забирает посылку и даёт ей имя rule: «правило верно»
  intro rule
  -- have применяет rule к этим кроссовкам: bad — это 3200 ≤ 2813
  have bad := rule sneakers promos
  -- bad — это 3200 ≤ 2813, а (by decide) считает и доказывает, что оно ложно
  -- absurd из утверждения и его отрицания даёт False, exact отдаёт его цели
  exact absurd bad (by decide)
    Pricing.lean
    -- «неправда» — и это тоже надо доказать
theorem stack_breaks_the_rule : ¬ never_below_cost := by
  -- intro забирает посылку и даёт ей имя rule: «правило верно»
  intro rule
  -- have применяет rule к этим кроссовкам: bad — это 3200 ≤ 2813
  have bad := rule sneakers promos
  -- bad — это 3200 ≤ 2813, а (by decide) считает и доказывает, что оно ложно
  -- absurd из утверждения и его отрицания даёт False, exact отдаёт его цели
  exact absurd bad (by decide)
    Pricing.lean
    -- «неправда» — и это тоже надо доказать
theorem stack_breaks_the_rule : ¬ never_below_cost := by
  -- intro забирает посылку и даёт ей имя rule: «правило верно»
  intro rule
  -- have применяет rule к этим кроссовкам: bad — это 3200 ≤ 2813
  have bad := rule sneakers promos
  -- bad — это 3200 ≤ 2813, а (by decide) считает и доказывает, что оно ложно
  -- absurd из утверждения и его отрицания даёт False, exact отдаёт его цели
  exact absurd bad (by decide)

    Вывод

    Pricing.lean: no errors

  10. Шаг 12 из 16

    Запас, из которого платят скидки

    Вся сумма, которой акции могут распоряжаться, — это маржа: разница между прайсом и закупочной. На этих кроссовках 18.00. Раньше акции считались от цены и о закупочной не знали вовсе; теперь у них появился общий кошелёк.

    Шаг 13 из 16

    Из пустого кошелька не берут

    spend берёт меньшую из двух сумм: сколько акция просит и сколько осталось в запасе. taken вычитается и из цены, и из запаса. Поэтому следующий процент, как и раньше, считается от уже сниженной цены. Первая акция берёт 12.50, вторая просит 9.37, но получает только оставшиеся 5.50.

    Шаг 14 из 16

    Доказательство в одну строку

    Итог — закупочная плюс остаток запаса. Остаток имеет тип Nat и не бывает отрицательным. Nat.le_add_right доказывает, что число не больше суммы себя с неотрицательным числом. Одна акция даёт 37.50; пара и три жадные акции — 32.00. Гарантия относится к сумме в чеке, а не ко всем расходам магазина.

    Pricing.lean
    -- весь запас скидок — это маржа
def margin (i : Item) : Nat := i.price - i.cost

-- берём сколько просим или сколько осталось
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

-- итог: закупочная плюс остаток запаса
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]

    Вывод

    3750
3200
3200
    Pricing.lean
    -- весь запас скидок — это маржа
def margin (i : Item) : Nat := i.price - i.cost

-- берём сколько просим или сколько осталось
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

-- итог: закупочная плюс остаток запаса
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]

    Вывод

    3750
3200
3200
    Pricing.lean
    -- весь запас скидок — это маржа
def margin (i : Item) : Nat := i.price - i.cost

-- берём сколько просим или сколько осталось
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

-- итог: закупочная плюс остаток запаса
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]

    Вывод

    3750
3200
3200

  11. Шаг 15 из 16

    Следующая механика

    Маркетинг просит кешбэк. Файл перестаёт собираться, пока кто-нибудь не скажет, сколько эта механика снимает с цены. Доказательство при этом переписывать не нужно: оно не заглядывает внутрь механик.

    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

    Вывод

    error: Missing cases:
(Promo.cashback _)

  12. Шаг 16 из 16

    Объявить долю

    Кешбэк выплачивают после покупки, поэтому сумму в чеке он не меняет: cut возвращает 0. Файл снова собирается, а доказательство осталось прежним. Оно гарантирует только то, что сумма в чеке не ниже закупочной. Выплата кешбэка может уменьшить доход ниже закупочной; для её учёта нужны другая модель и отдельное правило.

    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 _ => 0

-- доказательство осталось прежним, его даже не пришлось открывать
theorem checkout_never_below_cost (i : Item) (ps : List Promo) :
    i.cost ≤ checkout i ps :=
  Nat.le_add_right _ _

    Вывод

    Pricing.lean: no errors

Листать шаги можно стрелками ← и →.

Проверь себя

Почему в этом примере после обрезки расходится отчёт?

Почему бюджетная версия не может пробить закупочную?

Отвечено 0 из 2