Contexts.lean

import Fragments

namespace FPRD.Boundary

/-- Only bijective boundary renaming is a public context operation. -/
structure BoundaryEquiv (B C : Type) where
  toFun : B → C
  invFun : C → B
  left_inv : ∀ b, invFun (toFun b) = b
  right_inv : ∀ c, toFun (invFun c) = c

/-- A finite client expression, allowing zero, one or many uses of its input.
Each Join gives its two occurrences fresh private namespaces. -/
inductive Client (B : Type) : Type → Type 1 where
  | hole : Client B B
  | const {C : Type} (F : Fragment C) : Client B C
  | join {C : Type} (left right : Client B C) : Client B C
  | introduce {C : Type} (body : Client B C) : Client B (Option C)
  | forget {C : Type} (body : Client B (Option C)) : Client B C
  | rename {C D : Type} (e : BoundaryEquiv C D) (body : Client B C) : Client B D
  | pin {C : Type} (v : C) (value : Bool) (body : Client B C) : Client B C

namespace Client

def eval {B C : Type} (F : Fragment B) : Client B C → Fragment C
  | .hole => F
  | .const G => G
  | .join L R => (eval F L).join (eval F R)
  | .introduce K => (eval F K).introduce
  | .forget K => (eval F K).forget
  | .rename e K => (eval F K).renameBoundary e.toFun
  | .pin v value K => (eval F K).pin v value

end Client

/-- Equality of boundary relations, stated extensionally. -/
def RelEq {B : Type} (F G : Fragment B) : Prop :=
  ∀ a, F.rel a ↔ G.rel a

def Sat {B : Type} (F : Fragment B) : Prop := ∃ a, F.rel a

/-- Observations are only satisfiability of finite client expressions. -/
def ContextualEq {B : Type} (F G : Fragment B) : Prop :=
  ∀ (C : Type) (K : Client B C), Sat (K.eval F) ↔ Sat (K.eval G)

theorem client_congruence {B C : Type} {F G : Fragment B}
    (h : RelEq F G) (K : Client B C) : RelEq (K.eval F) (K.eval G) := by
  induction K with
  | hole => exact h
  | const P => intro a; rfl
  | join L R ihL ihR =>
      intro a
      simp only [Client.eval, Fragment.rel_join]
      exact and_congr (ihL a) (ihR a)
  | introduce K ih =>
      intro a
      simp only [Client.eval, Fragment.rel_introduce]
      exact ih _
  | forget K ih =>
      intro a
      simp only [Client.eval, Fragment.rel_forget]
      exact exists_congr (fun value => ih _)
  | rename e K ih =>
      intro a
      simp only [Client.eval, Fragment.rel_renameBoundary]
      exact ih _
  | pin v value K ih =>
      intro a
      simp only [Client.eval, Fragment.rel_pin]
      exact and_congr (ih a) Iff.rfl

theorem relEq_implies_contextualEq {B : Type} {F G : Fragment B}
    (h : RelEq F G) : ContextualEq F G := by
  intro C K
  exact exists_congr (client_congruence h K)

/-- Pin every listed boundary name, using a finite sequence of signed units. -/
def pinAll {B : Type} (xs : List B) (a : B → Bool) : Client B B :=
  match xs with
  | [] => .hole
  | v :: vs => .pin v (a v) (pinAll vs a)

theorem rel_pinAll {B : Type} (F : Fragment B) (xs : List B)
    (a b : B → Bool) :
    ((pinAll xs a).eval F).rel b ↔ F.rel b ∧ ∀ v ∈ xs, b v = a v := by
  induction xs with
  | nil => simp [pinAll, Client.eval]
  | cons v vs ih =>
      simp only [pinAll, Client.eval, Fragment.rel_pin, ih]
      constructor
      · intro h
        refine ⟨h.1.1, ?_⟩
        intro w hw
        cases List.mem_cons.mp hw with
        | inl heq => simpa [heq] using h.2
        | inr hm => exact h.1.2 w hm
      · intro h
        exact ⟨⟨h.1, fun w hw => h.2 w (List.mem_cons.mpr (Or.inr hw))⟩,
          h.2 v (List.mem_cons.mpr (Or.inl rfl))⟩

/-- A finite separating test: its SAT answer is exactly membership of a. -/
theorem sat_pinAll {B : Type} (F : Fragment B) (xs : List B)
    (covers : ∀ v, v ∈ xs) (a : B → Bool) :
    Sat ((pinAll xs a).eval F) ↔ F.rel a := by
  constructor
  · rintro ⟨b, hb⟩
    have q := (rel_pinAll F xs a b).mp hb
    have e : b = a := funext (fun v => q.2 v (covers v))
    simpa [e] using q.1
  · intro h
    exact ⟨a, (rel_pinAll F xs a a).mpr ⟨h, fun _ _ => rfl⟩⟩

/-- Complete boundary invariant for every finitely enumerated boundary.
Duplicates in xs are harmless. No bound on private variables or client depth. -/
theorem contextualEq_iff_relEq {B : Type} (xs : List B)
    (covers : ∀ v, v ∈ xs) (F G : Fragment B) :
    ContextualEq F G ↔ RelEq F G := by
  constructor
  · intro h a
    exact (sat_pinAll F xs covers a).symm.trans
      ((h B (pinAll xs a)).trans (sat_pinAll G xs covers a))
  · exact relEq_implies_contextualEq

/-- The same complete invariant stated as actual equality of predicates. -/
theorem contextualEq_iff_boundary_eq {B : Type} (xs : List B)
    (covers : ∀ v, v ∈ xs) (F G : Fragment B) :
    ContextualEq F G ↔ F.rel = G.rel := by
  constructor
  · intro h
    exact funext (fun a => propext
      ((contextualEq_iff_relEq xs covers F G).mp h a))
  · intro h
    apply relEq_implies_contextualEq
    intro a
    rw [h]

/-- The relation is a minimal exact invariant in the kernel-refinement sense:
any summary identifying only contextually equivalent fragments also identifies
only equal boundary relations. This does not assert a resource bound. -/
theorem exact_summary_refines_relation {B S : Type}
    (xs : List B) (covers : ∀ v, v ∈ xs) (summary : Fragment B → S)
    (sound : ∀ F G, summary F = summary G → ContextualEq F G)
    (F G : Fragment B) (same : summary F = summary G) : RelEq F G :=
  (contextualEq_iff_relEq xs covers F G).mp (sound F G same)

#print axioms client_congruence
#print axioms contextualEq_iff_relEq
#print axioms exact_summary_refines_relation

end FPRD.Boundary