Fragments.lean

import Std

/-!
Boolean fragments with an explicit finite private namespace.

The names in the exposed boundary may have any type. Private names are generated
from Empty, Unit and disjoint sums, so every fragment has finitely many private
variables. Join always creates disjoint private copies, including when the same
fragment is supplied twice. No quotient by syntactic equality is used.
-/

namespace FPRD.Boundary

inductive Formula (V : Type) where
  | atom : V → Formula V
  | top : Formula V
  | bot : Formula V
  | conj : Formula V → Formula V → Formula V
  | disj : Formula V → Formula V → Formula V
  | neg : Formula V → Formula V

namespace Formula

def eval : Formula V → (V → Bool) → Bool
  | .atom v, a => a v
  | .top, _ => true
  | .bot, _ => false
  | .conj p q, a => p.eval a && q.eval a
  | .disj p q, a => p.eval a || q.eval a
  | .neg p, a => !(p.eval a)

def map (f : V → W) : Formula V → Formula W
  | .atom v => .atom (f v)
  | .top => .top
  | .bot => .bot
  | .conj p q => .conj (p.map f) (q.map f)
  | .disj p q => .disj (p.map f) (q.map f)
  | .neg p => .neg (p.map f)

@[simp] theorem eval_map (f : V → W) (p : Formula V) (a : W → Bool) :
    (p.map f).eval a = p.eval (a ∘ f) := by
  induction p <;> simp_all [map, eval]

theorem eval_congr (p : Formula V) {a b : V → Bool} (h : ∀ v, a v = b v) :
    p.eval a = p.eval b := by
  exact congrArg p.eval (funext h)

def literal (v : V) (value : Bool) : Formula V :=
  if value then .atom v else .neg (.atom v)

@[simp] theorem eval_literal_true (v : V) (value : Bool) (a : V → Bool) :
    (literal v value).eval a = true ↔ a v = value := by
  cases value <;> cases h : a v <;> simp [literal, eval, h]

end Formula

inductive PrivateShape where
  | empty
  | unit
  | sum : PrivateShape → PrivateShape → PrivateShape

def PrivateShape.Var : PrivateShape → Type
  | .empty => Empty
  | .unit => Unit
  | .sum s t => Sum s.Var t.Var

def PrivateShape.enumerate : (s : PrivateShape) → List s.Var
  | .empty => []
  | .unit => [()]
  | .sum s t => (s.enumerate.map Sum.inl) ++ (t.enumerate.map Sum.inr)

theorem PrivateShape.mem_enumerate (s : PrivateShape) (v : s.Var) :
    v ∈ s.enumerate := by
  induction s with
  | empty => exact Empty.elim v
  | unit => cases v; simp [enumerate]
  | sum s t hs ht =>
    cases v with
    | inl v =>
      apply List.mem_append_left
      exact List.mem_map.mpr ⟨v, hs v, rfl⟩
    | inr v =>
      apply List.mem_append_right
      exact List.mem_map.mpr ⟨v, ht v, rfl⟩

structure Fragment (B : Type) where
  shape : PrivateShape
  body : Formula (Sum B shape.Var)

namespace Fragment

def rel (F : Fragment B) (a : B → Bool) : Prop :=
  ∃ y : F.shape.Var → Bool, F.body.eval (Sum.elim a y) = true

def join (F G : Fragment B) : Fragment B where
  shape := .sum F.shape G.shape
  body := .conj
    (F.body.map (Sum.elim Sum.inl (fun v => Sum.inr (Sum.inl v))))
    (G.body.map (Sum.elim Sum.inl (fun v => Sum.inr (Sum.inr v))))

theorem eval_join (F G : Fragment B) (a : B → Bool)
    (y : (join F G).shape.Var → Bool) :
    (join F G).body.eval (Sum.elim a y) =
      (F.body.eval (Sum.elim a (fun v => y (.inl v))) &&
       G.body.eval (Sum.elim a (fun v => y (.inr v)))) := by
  simp only [join, Formula.eval, Formula.eval_map]
  congr 1
  · apply Formula.eval_congr
    intro v
    cases v <;> rfl
  · apply Formula.eval_congr
    intro v
    cases v <;> rfl

@[simp] theorem rel_join (F G : Fragment B) (a : B → Bool) :
    (join F G).rel a ↔ F.rel a ∧ G.rel a := by
  constructor
  · rintro ⟨y, hy⟩
    rw [eval_join] at hy
    rw [Bool.and_eq_true] at hy
    have h := hy
    exact ⟨⟨fun v => y (.inl v), h.1⟩, ⟨fun v => y (.inr v), h.2⟩⟩
  · rintro ⟨⟨y, hy⟩, ⟨z, hz⟩⟩
    refine ⟨Sum.elim y z, ?_⟩
    rw [eval_join]
    rw [Bool.and_eq_true]
    exact ⟨hy, hz⟩

def introduce (F : Fragment B) : Fragment (Option B) where
  shape := F.shape
  body := F.body.map (Sum.elim (fun b => Sum.inl (some b)) Sum.inr)

theorem eval_introduce (F : Fragment B) (a : Option B → Bool)
    (y : F.shape.Var → Bool) :
    (introduce F).body.eval (Sum.elim a y) =
      F.body.eval (Sum.elim (fun b => a (some b)) y) := by
  simp only [introduce, Formula.eval_map]
  apply Formula.eval_congr
  intro v
  cases v <;> rfl

@[simp] theorem rel_introduce (F : Fragment B) (a : Option B → Bool) :
    (introduce F).rel a ↔ F.rel (fun b => a (some b)) := by
  unfold rel
  simp only [eval_introduce]
  rfl

def forget (F : Fragment (Option B)) : Fragment B where
  shape := .sum .unit F.shape
  body := F.body.map (Sum.elim
    (fun ob => match ob with
      | none => Sum.inr (Sum.inl ())
      | some b => Sum.inl b)
    (fun v => Sum.inr (Sum.inr v)))

theorem eval_forget (F : Fragment (Option B)) (a : B → Bool)
    (y : (forget F).shape.Var → Bool) :
    (forget F).body.eval (Sum.elim a y) =
      F.body.eval (Sum.elim (fun ob => ob.elim (y (.inl ())) a)
        (fun v => y (.inr v))) := by
  simp only [forget, Formula.eval_map]
  apply Formula.eval_congr
  intro v
  cases v with
  | inl ob => cases ob <;> rfl
  | inr v => rfl

@[simp] theorem rel_forget (F : Fragment (Option B)) (a : B → Bool) :
    (forget F).rel a ↔ ∃ bit : Bool, F.rel (fun ob => ob.elim bit a) := by
  constructor
  · rintro ⟨y, hy⟩
    rw [eval_forget] at hy
    exact ⟨y (.inl ()), fun v => y (.inr v), hy⟩
  · rintro ⟨bit, y, hy⟩
    refine ⟨Sum.elim (fun _ => bit) y, ?_⟩
    rw [eval_forget]
    exact hy

def renameBoundary (F : Fragment B) (f : B → C) : Fragment C where
  shape := F.shape
  body := F.body.map (Sum.elim (fun b => Sum.inl (f b)) Sum.inr)

theorem eval_renameBoundary (F : Fragment B) (f : B → C) (a : C → Bool)
    (y : F.shape.Var → Bool) :
    (renameBoundary F f).body.eval (Sum.elim a y) =
      F.body.eval (Sum.elim (a ∘ f) y) := by
  simp only [renameBoundary, Formula.eval_map]
  apply Formula.eval_congr
  intro v
  cases v <;> rfl

@[simp] theorem rel_renameBoundary (F : Fragment B) (f : B → C) (a : C → Bool) :
    (renameBoundary F f).rel a ↔ F.rel (a ∘ f) := by
  unfold rel
  simp only [eval_renameBoundary]
  rfl

def renamePrivate (F : Fragment B) (s : PrivateShape)
    (f : F.shape.Var → s.Var) : Fragment B where
  shape := s
  body := F.body.map (Sum.elim Sum.inl (fun v => Sum.inr (f v)))

theorem eval_renamePrivate (F : Fragment B) (s : PrivateShape)
    (f : F.shape.Var → s.Var) (a : B → Bool) (y : s.Var → Bool) :
    (renamePrivate F s f).body.eval (Sum.elim a y) =
      F.body.eval (Sum.elim a (y ∘ f)) := by
  simp only [renamePrivate, Formula.eval_map]
  apply Formula.eval_congr
  intro v
  cases v <;> rfl

/- A private renaming equipped with a left inverse preserves the relation.
   This includes every bijective alpha-renaming and also allows extra unused
   private names. Both maps and the inverse equation are explicit hypotheses. -/
theorem rel_renamePrivate (F : Fragment B) (s : PrivateShape)
    (f : F.shape.Var → s.Var) (g : s.Var → F.shape.Var)
    (h : ∀ v, g (f v) = v) (a : B → Bool) :
    (renamePrivate F s f).rel a ↔ F.rel a := by
  constructor
  · rintro ⟨y, hy⟩
    rw [eval_renamePrivate] at hy
    exact ⟨y ∘ f, hy⟩
  · rintro ⟨y, hy⟩
    refine ⟨y ∘ g, ?_⟩
    rw [eval_renamePrivate]
    have ha : Sum.elim a ((y ∘ g) ∘ f) = Sum.elim a y := by
      funext v
      cases v with
      | inl b => rfl
      | inr v => simp [Function.comp_def, h v]
    exact (congrArg F.body.eval ha).trans hy

def pin (F : Fragment B) (v : B) (value : Bool) : Fragment B where
  shape := F.shape
  body := .conj F.body (Formula.literal (.inl v) value)

@[simp] theorem rel_pin (F : Fragment B) (v : B) (value : Bool) (a : B → Bool) :
    (pin F v value).rel a ↔ F.rel a ∧ a v = value := by
  unfold rel
  simp only [pin, Formula.eval, Bool.and_eq_true, Formula.eval_literal_true, Sum.elim_inl]
  constructor
  · rintro ⟨y, hy, hv⟩
    exact ⟨⟨y, hy⟩, hv⟩
  · rintro ⟨⟨y, hy⟩, hv⟩
    exact ⟨y, hy, hv⟩

end Fragment
end FPRD.Boundary