`eval`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge
domain: Foundation
line: 30 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  50      simp [eval]
  51  | atomU =>
  52      refine ⟨0, 1, 0, 0, ?_⟩
  53      intro u v
  54      simp [eval]
  55  | atomV =>
  56      refine ⟨0, 0, 1, 0, ?_⟩
  57      intro u v
  58      simp [eval]
  59  | both =>
  60      refine ⟨0, 0, 0, 1, ?_⟩

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.