IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison
   3
   4/-!
   5# Resource-sensitive syntax for counted-once comparison
   6
   7This module formalises the normal-form version of counted-once resource
   8syntax.  Each constituent comparison may appear at most once, so the only
   9scalar monomials are `1`, `u`, `v`, and `u*v`.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace LogicAsFunctionalEquation
  15
  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
  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
  70  | scale k e ihe =>
  71      rcases ihe with ⟨a,b,c,d,h⟩
  72      refine ⟨k*a, k*b, k*c, k*d, ?_⟩
  73      intro u v
  74      simp [eval, h u v]
  75      ring
  76
  77/-- A counted-once resource expression induces a counted-once combiner. -/
  78theorem expr_induces_counted_once_combiner
  79    (e : CountedOnceResourceExpr) :
  80    CountedOnceCombiner (fun u v => eval e u v) := by
  81  exact counted_once_expr_biaffine e
  82
  83/-- Searchable alias: resource-linearity gives bi-affinity. -/
  84theorem resource_linearity_gives_biaffinity
  85    (e : CountedOnceResourceExpr) :
  86    HasBiAffineForm e :=
  87  counted_once_expr_biaffine e
  88
  89end CountedOnceResourceExpr
  90
  91end LogicAsFunctionalEquation
  92end Foundation
  93end IndisputableMonolith
  94