CountedOnceResourceExpr

formal source

  16/-- Normal-form counted-once resource expressions.  The constructor `both`
  17represents the joint interaction `u*v`; there are no constructors for `u^2`,
  18`v^2`, square roots, branch choices, or infinite series. -/
  19inductive CountedOnceResourceExpr where
  20  | const : ℝ → CountedOnceResourceExpr
  21  | atomU : CountedOnceResourceExpr
  22  | atomV : CountedOnceResourceExpr
  23  | both : CountedOnceResourceExpr
  24  | add : CountedOnceResourceExpr → CountedOnceResourceExpr → CountedOnceResourceExpr
  25  | scale : ℝ → CountedOnceResourceExpr → CountedOnceResourceExpr
  26
  27namespace CountedOnceResourceExpr
  28
  29/-- Evaluation of a counted-once resource expression. -/
  30def eval : CountedOnceResourceExpr → ℝ → ℝ → ℝ
  31  | const a, _, _ => a
  32  | atomU, u, _ => u
  33  | atomV, _, v => v
  34  | both, u, v => u * v
  35  | add e f, u, v => eval e u v + eval f u v
  36  | scale k e, u, v => k * eval e u v
  37
  38/-- A semantic bi-affine representation. -/
  39def HasBiAffineForm (e : CountedOnceResourceExpr) : Prop :=
  40  ∃ a b c d : ℝ, ∀ u v, eval e u v = a + b*u + c*v + d*u*v
  41
  42/-- Every counted-once resource expression is bi-affine. -/
  43theorem counted_once_expr_biaffine :
  44    ∀ e : CountedOnceResourceExpr, HasBiAffineForm e := by
  45  intro e
  46  induction e with
  47  | const a =>
  48      refine ⟨a, 0, 0, 0, ?_⟩
  49      intro u v