Examples.lean

import Adaptive

/-!
Kernel-checked semantic controls, not a finite test suite for the general theorem.
These isolate freshness, signed observations and finite ordered boundaries.
-/

namespace FPRD.Boundary

/-- The complete-invariant theorem specializes uniformly to every finite width. -/
theorem finite_boundary_contextualEq_iff_relEq (n : Nat)
    (F G : Fragment (Fin n)) : ContextualEq F G ↔ RelEq F G :=
  contextualEq_iff_relEq (List.finRange n) List.mem_finRange F G

theorem finite_boundary_adaptiveEq_iff_relEq (n : Nat)
    (F G : Fragment (Fin n)) : AdaptiveEq F G ↔ RelEq F G :=
  adaptiveEq_iff_relEq (List.finRange n) List.mem_finRange F G

namespace Examples

def truth (B : Type) : Fragment B := ⟨.empty, .top⟩

theorem rel_truth {B : Type} (a : B → Bool) : (truth B).rel a :=
  ⟨Empty.elim, rfl⟩

def privatePositive : Fragment Empty := ⟨.unit, .atom (.inr ())⟩
def privateNegative : Fragment Empty := ⟨.unit, .neg (.atom (.inr ()))⟩

/-- Private syntax is not part of the SAT observation interface. -/
theorem distinct_private_syntax_same_future :
    privatePositive.body ≠ privateNegative.body ∧
      ContextualEq privatePositive privateNegative := by
  constructor
  · intro h
    cases h
  · apply relEq_implies_contextualEq
    intro a
    constructor
    · intro _
      exact ⟨fun _ => false, rfl⟩
    · intro _
      exact ⟨fun _ => true, rfl⟩

/-- Each conjunct may choose its own private witness. -/
theorem fresh_private_join_sat : Sat (privatePositive.join privateNegative) := by
  refine ⟨Empty.elim, (Fragment.rel_join _ _ _).mpr ?_⟩
  exact ⟨⟨fun _ => true, rfl⟩, ⟨fun _ => false, rfl⟩⟩

def aliasedPrivate : Fragment Empty :=
  ⟨.unit, .conj (.atom (.inr ())) (.neg (.atom (.inr ())))⟩

/-- Erroneously sharing those two private names changes the SAT answer. -/
theorem aliased_private_unsat : ¬ Sat aliasedPrivate := by
  rintro ⟨a, y, hy⟩
  cases h : y () <;> simp [aliasedPrivate, Formula.eval, h] at hy

def boundaryPositive : Fragment Unit := ⟨.empty, .atom (.inl ())⟩

theorem boundary_positive_sat : Sat boundaryPositive :=
  ⟨fun _ => true, Empty.elim, rfl⟩

theorem truth_sat : Sat (truth Unit) := ⟨fun _ => false, rel_truth _⟩

theorem truth_pin_false_sat : Sat ((truth Unit).pin () false) := by
  exact ⟨fun _ => false, (Fragment.rel_pin _ _ _ _).mpr ⟨rel_truth _, rfl⟩⟩

theorem boundary_positive_pin_false_unsat : ¬ Sat (boundaryPositive.pin () false) := by
  rintro ⟨a, ha⟩
  obtain ⟨⟨y, hy⟩, hv⟩ := (Fragment.rel_pin _ _ _ _).mp ha
  simp [boundaryPositive, Formula.eval, hv] at hy

/-- SAT of the current fragment alone is strictly weaker than future-context SAT. -/
theorem both_sat_but_not_contextualEq :
    Sat (truth Unit) ∧ Sat boundaryPositive ∧
      ¬ ContextualEq (truth Unit) boundaryPositive := by
  refine ⟨truth_sat, boundary_positive_sat, ?_⟩
  intro h
  have q := h Unit (.pin () false .hole)
  exact boundary_positive_pin_false_unsat (q.mp truth_pin_false_sat)

/-- A deliberately restricted observation language: no negative units and no
arbitrary fragment constants. This exact restriction matters. -/
inductive PositiveClient where
  | hole
  | truth
  | join (left right : PositiveClient)
  | pinTrue (body : PositiveClient)

def PositiveClient.eval (F : Fragment Unit) : PositiveClient → Fragment Unit
  | .hole => F
  | .truth => FPRD.Boundary.Examples.truth Unit
  | .join L R => (L.eval F).join (R.eval F)
  | .pinTrue K => (K.eval F).pin () true

theorem positive_client_preserves_all_true {F : Fragment Unit}
    (h : F.rel (fun _ => true)) (K : PositiveClient) :
    (K.eval F).rel (fun _ => true) := by
  induction K with
  | hole => exact h
  | truth => exact rel_truth _
  | join L R ihL ihR => exact (Fragment.rel_join _ _ _).mpr ⟨ihL, ihR⟩
  | pinTrue K ih => exact (Fragment.rel_pin _ _ _ _).mpr ⟨ih, rfl⟩

/-- All clients in the restricted positive language accept both fragments,
although the legal signed language above separates them. -/
theorem positive_clients_cannot_separate (K : PositiveClient) :
    Sat (K.eval (truth Unit)) ∧ Sat (K.eval boundaryPositive) := by
  exact ⟨⟨fun _ => true, positive_client_preserves_all_true (rel_truth _) K⟩,
    ⟨fun _ => true, positive_client_preserves_all_true ⟨Empty.elim, rfl⟩ K⟩⟩

def exposedPositive : Fragment (Option Empty) :=
  ⟨.empty, .atom (.inl none)⟩

/-- Forget binds the old name privately; Introduce allocates a fresh boundary
name, so the new name is unconstrained even though the hidden old one is true. -/
theorem forget_then_introduce_free (a : Option Empty → Bool) :
    exposedPositive.forget.introduce.rel a := by
  apply (Fragment.rel_introduce _ _).mpr
  apply (Fragment.rel_forget _ _).mpr
  exact ⟨true, Empty.elim, rfl⟩

theorem forgotten_name_not_reexposed :
    Sat (exposedPositive.forget.introduce.pin none false) := by
  exact ⟨fun _ => false,
    (Fragment.rel_pin _ _ _ _).mpr ⟨forget_then_introduce_free _, rfl⟩⟩

theorem original_name_cannot_be_false : ¬ Sat (exposedPositive.pin none false) := by
  rintro ⟨a, ha⟩
  obtain ⟨⟨y, hy⟩, hv⟩ := (Fragment.rel_pin _ _ _ _).mp ha
  simp [exposedPositive, Formula.eval, hv] at hy

#print axioms fresh_private_join_sat
#print axioms distinct_private_syntax_same_future
#print axioms aliased_private_unsat
#print axioms both_sat_but_not_contextualEq
#print axioms positive_clients_cannot_separate
#print axioms forgotten_name_not_reexposed
#print axioms original_name_cannot_be_false

end Examples

#print axioms finite_boundary_contextualEq_iff_relEq
#print axioms finite_boundary_adaptiveEq_iff_relEq

end FPRD.Boundary