HasBiAffineForm

formal source

  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, ?_⟩
  61      intro u v
  62      simp [eval]
  63  | add e f ihe ihf =>
  64      rcases ihe with ⟨a₁,b₁,c₁,d₁,h₁⟩
  65      rcases ihf with ⟨a₂,b₂,c₂,d₂,h₂⟩
  66      refine ⟨a₁+a₂, b₁+b₂, c₁+c₂, d₁+d₂, ?_⟩
  67      intro u v
  68      simp [eval, h₁ u v, h₂ u v]
  69      ring