Summaries.lean

import Contexts

namespace FPRD.Boundary

/-- Exactness constrains collisions of summary values, not their computation. -/
def ExactSummary {B S : Type} (summary : Fragment B → S) : Prop :=
  ∀ F G, summary F = summary G → ContextualEq F G

/-- A mathematical decoder, with no claim of executable or cheap evaluation. -/
def decodeSummary {B S : Type} (summary : Fragment B → S)
    (s : S) (a : B → Bool) : Prop :=
  ∃ F, summary F = s ∧ F.rel a

theorem decodeSummary_correct {B S : Type} (xs : List B)
    (covers : ∀ v, v ∈ xs) (summary : Fragment B → S)
    (exactness : ExactSummary summary) (F : Fragment B) (a : B → Bool) :
    decodeSummary summary (summary F) a ↔ F.rel a := by
  constructor
  · rintro ⟨G, same, hg⟩
    exact ((contextualEq_iff_relEq xs covers G F).mp
      (exactness G F same) a).mp hg
  · intro hf
    exact ⟨F, rfl, hf⟩

/-- Exact summaries are precisely those from which boundary behavior factors.
The decoder is propositional; no algorithm, size or locality is asserted. -/
theorem exactSummary_iff_decoder {B S : Type} (xs : List B)
    (covers : ∀ v, v ∈ xs) (summary : Fragment B → S) :
    ExactSummary summary ↔
      ∃ decode : S → (B → Bool) → Prop,
        ∀ F a, decode (summary F) a ↔ F.rel a := by
  constructor
  · intro h
    exact ⟨decodeSummary summary, decodeSummary_correct xs covers summary h⟩
  · rintro ⟨decode, correct⟩ F G same
    apply relEq_implies_contextualEq
    intro a
    exact (correct F a).symm.trans (by rw [same]; exact correct G a)

/-- A SAT-only summary is not exact whenever it merges different relations. -/
theorem unequal_relations_force_distinct_summaries {B S : Type}
    (xs : List B) (covers : ∀ v, v ∈ xs) (summary : Fragment B → S)
    (exactness : ExactSummary summary) (F G : Fragment B)
    (different : ¬ RelEq F G) : summary F ≠ summary G := by
  intro same
  exact different ((contextualEq_iff_relEq xs covers F G).mp
    (exactness F G same))

#print axioms decodeSummary_correct
#print axioms exactSummary_iff_decoder
#print axioms unequal_relations_force_distinct_summaries

end FPRD.Boundary