Adaptive.lean

import Contexts

namespace FPRD.Boundary

/-- Finite adaptive clients branch only on SAT queries of legal expressions. -/
inductive Observer (B : Type) : Type 1 where
  | answer (value : Bool) : Observer B
  | query {C : Type} (expr : Client B C) (yes no : Observer B) : Observer B

/-- Relational evaluation avoids assuming a decision procedure for SAT. -/
def Outcome {B : Type} (F : Fragment B) : Observer B → Bool → Prop
  | .answer value, result => result = value
  | .query expr yes no, result =>
      (Sat (expr.eval F) ∧ Outcome F yes result) ∨
      (¬ Sat (expr.eval F) ∧ Outcome F no result)

def AdaptiveEq {B : Type} (F G : Fragment B) : Prop :=
  ∀ (P : Observer B) result, Outcome F P result ↔ Outcome G P result

theorem contextualEq_implies_adaptiveEq {B : Type} {F G : Fragment B}
    (h : ContextualEq F G) : AdaptiveEq F G := by
  intro P
  induction P with
  | answer value => intro result; rfl
  | query expr yes no iy ino =>
      intro result
      exact or_congr (and_congr (h _ expr) (iy result))
        (and_congr (not_congr (h _ expr)) (ino result))

theorem adaptiveEq_implies_contextualEq {B : Type} {F G : Fragment B}
    (h : AdaptiveEq F G) : ContextualEq F G := by
  intro C K
  have q := h (.query K (.answer true) (.answer false)) true
  simpa [Outcome] using q

theorem adaptiveEq_iff_relEq {B : Type} (xs : List B)
    (covers : ∀ v, v ∈ xs) (F G : Fragment B) :
    AdaptiveEq F G ↔ RelEq F G := by
  constructor
  · intro h
    exact (contextualEq_iff_relEq xs covers F G).mp
      (adaptiveEq_implies_contextualEq h)
  · intro h
    exact contextualEq_implies_adaptiveEq (relEq_implies_contextualEq h)

#print axioms contextualEq_implies_adaptiveEq
#print axioms adaptiveEq_iff_relEq

end FPRD.Boundary