-- File: lean/PricingSpec.lean
-- E-Commerce Pricing Engine Specification
-- Agents migrate JavaScript source to Python.
-- The 5 theorems here are property-checked against agents' code.

namespace PricingSpec

structure LineItem where
  sku      : String
  quantity : Nat
  unitPrice : Int   -- cents, avoid Float
  deriving Repr, DecidableEq

structure Coupon where
  code           : String
  discountPercent : Nat    -- 0..100
  deriving Repr, DecidableEq

structure Order where
  items    : List LineItem
  coupons  : List Coupon
  regionId : String         -- for tax lookup
  loyaltyPoints : Nat
  deriving Repr, DecidableEq

-- Tax rates by region (basis points, e.g. 875 = 8.75%)
def taxRateBps : String → Nat
  | "US-CA" => 875
  | "US-TX" => 625
  | "US-NY" => 800
  | "UK"    => 2000
  | _       => 0

-- Subtotal before discounts
def subtotal (order : Order) : Int :=
  order.items.foldl (fun acc item =>
    acc + item.unitPrice * item.quantity) 0

-- Coupon discount (capped at subtotal, non-stackable beyond 50% total)
def couponDiscount (order : Order) : Int :=
  let sub := subtotal order
  let rawDiscount := order.coupons.foldl (fun acc c =>
    acc + (sub * c.discountPercent / 100)) 0
  min rawDiscount (sub / 2)   -- max 50% off via coupons

-- Loyalty points: 1 point = 1 cent off, max 10% of subtotal
def loyaltyDiscount (order : Order) : Int :=
  let sub := subtotal order
  min (order.loyaltyPoints : Int) (sub / 10)

-- Total discount
def totalDiscount (order : Order) : Int :=
  couponDiscount order + loyaltyDiscount order

-- Tax applied to post-discount amount
def tax (order : Order) : Int :=
  let afterDiscount := subtotal order - totalDiscount order
  afterDiscount * (taxRateBps order.regionId : Int) / 10000

-- Final price
def finalPrice (order : Order) : Int :=
  subtotal order - totalDiscount order + tax order

-- ── The 5 invariants agents' Python code must satisfy ──────────────

-- 1. Discount never exceeds subtotal
theorem discount_bounded (order : Order) (h : 0 ≤ subtotal order) :
    totalDiscount order ≤ subtotal order := by
  simp [totalDiscount, couponDiscount, loyaltyDiscount]
  omega

-- 2. Final price is non-negative
-- Strategy: afterDiscount ≥ 0 (from discount_bounded) × taxRate (Nat) ≥ 0 → tax ≥ 0
theorem no_negative_price (order : Order) (h : 0 ≤ subtotal order) :
    0 ≤ finalPrice order := by
  have hd := discount_bounded order h
  have hbd : 0 ≤ subtotal order - totalDiscount order := by omega
  -- taxRateBps returns Nat, so (↑rate : Int) ≥ 0 — omega knows Nat casts are nonneg
  have hrate : (0 : Int) ≤ ↑(taxRateBps order.regionId) := by omega
  have hnum : 0 ≤ (subtotal order - totalDiscount order) * ↑(taxRateBps order.regionId) :=
    Int.mul_nonneg hbd hrate
  simp only [finalPrice, tax]
  omega

-- 3. Tax is non-negative
theorem tax_nonneg (order : Order) (h : 0 ≤ subtotal order) :
    0 ≤ tax order := by
  have hd := discount_bounded order h
  have hbd : 0 ≤ subtotal order - totalDiscount order := by omega
  have hrate : (0 : Int) ≤ ↑(taxRateBps order.regionId) := by omega
  have hnum : 0 ≤ (subtotal order - totalDiscount order) * ↑(taxRateBps order.regionId) :=
    Int.mul_nonneg hbd hrate
  simp only [tax]
  omega

-- 4. Empty order has zero final price
theorem empty_order_zero :
    finalPrice { items := [], coupons := [], regionId := "US-CA",
                 loyaltyPoints := 0 } = 0 := by
  simp [finalPrice, subtotal, totalDiscount, couponDiscount,
    loyaltyDiscount, tax, taxRateBps]

-- 5. Adding items increases subtotal monotonically
theorem add_item_increases_subtotal
    (order : Order) (item : LineItem)
    (hpos : 0 < item.unitPrice) (hqty : 0 < item.quantity) :
    subtotal order < subtotal { order with items := order.items ++ [item] } := by
  simp [subtotal, List.foldl_append]
  -- goal reduces to: 0 < item.unitPrice * ↑item.quantity
  -- omega knows 0 < item.quantity (Nat) → (0 : Int) < ↑item.quantity
  have hq : (0 : Int) < ↑item.quantity := by omega
  have hprod : 0 < item.unitPrice * ↑item.quantity := Int.mul_pos hpos hq
  omega

end PricingSpec