; ============================================================
; Lojban equality-saturation rewrite rules
; Loaded after egglog_schema.egg and after all facts are asserted.
; ============================================================
; ============================================================
; Logical simplification
; ============================================================
; Double negation elimination
(rewrite (PNot (PNot p)) p)
; Contradiction / tautology with Eet
; Not(Eet) acts as "falsum" in Haskell bigAnd — but we keep Eet
; as a neutral element here.
(rewrite (PAnd p (Eet)) p)
(rewrite (PAnd (Eet) p) p)
(rewrite (POr p (Eet)) (Eet))
(rewrite (POr (Eet) p) (Eet))
; Idempotency
(rewrite (PAnd p p) p)
(rewrite (POr p p) p)
; Commutativity (birewrite so both directions are explored)
(birewrite (PAnd p q) (PAnd q p))
(birewrite (POr p q) (POr q p))
; Associativity
(birewrite (PAnd (PAnd p q) r) (PAnd p (PAnd q r)))
(birewrite (POr (POr p q) r) (POr p (POr q r)))
; De Morgan
(rewrite (PNot (PAnd p q)) (POr (PNot p) (PNot q)))
(rewrite (PNot (POr p q)) (PAnd (PNot p) (PNot q)))
; Implication elimination
(rewrite (PImpl p q) (POr (PNot p) q))
; Equivalence expansion
(rewrite (PEquiv p q) (PAnd (PImpl p q) (PImpl q p)))
; ============================================================
; Lojban-specific transformations
; ============================================================
; se-conversion: PermutedRel with place 1 (se) applied twice cancels
; se(se(r)) = r (double inversion)
(rewrite (PermutedRel 1 (PermutedRel 1 r)) r)
; Scalar negation of Equal: na'e du = not equal (approximation)
(rewrite (PRel (ScalarNegRel "nai" (Brivla b)) tl)
(PNot (PRel (Brivla b) tl)))
; Double scalar negation cancellation (to'e to'e = identity, approximation)
(rewrite (ScalarNegRel s1 (ScalarNegRel s2 r))
r
:when ((= s1 "to'e") (= s2 "to'e")))
; Tanru of a single brivla with itself is just the brivla
(rewrite (Tanru (Brivla a) (Brivla b))
(Brivla b)
:when ((= a b)))
; Among(x) applied to one arg is a membership test — no simplification,
; but mark as canonical by normalising the relation position.
; (no rule needed beyond schema declaration)
; Modal absorption: nested identical tense tags merge
; Tagged(t, Unfilled) applied twice — keep outermost
(rewrite (PModal (TaggedNoTerm tag) (PModal (TaggedNoTerm tag) p))
(PModal (TaggedNoTerm tag) p))
; NonVeridical double wrapping
(rewrite (PModal (NonVeridical) (PModal (NonVeridical) p))
(PModal (NonVeridical) p))
; ============================================================
; Quantifier normalisation
; ============================================================
; Exists over a conjunction where the restriction is vacuous:
; ∃x. (True ∧ body) → ∃x. body
(rewrite (PQuant q restr_id (PAnd (Eet) body) v)
(PQuant q restr_id body v))
(rewrite (PQuant q restr_id (PAnd body (Eet)) v)
(PQuant q restr_id body v))
; Negation push through existential: ¬∃x.P ↔ ∀x.¬P
(rewrite (PNot (PQuant (Exists) restr_id body v))
(PQuant (Forall) restr_id (PNot body) v))
(rewrite (PNot (PQuant (Forall) restr_id body v))
(PQuant (Exists) restr_id (PNot body) v))
; ============================================================
; Anaphora: ri/ra resolution hints
; ============================================================
; These are Datalog-style rules that propagate antecedent
; bindings. The actual substitution is done on the Rust side;
; these rules mark equivalences once the binding is known.
; If two terms are known equal (merged into the same e-class),
; a BoundVar reference to one is equal to the other.
; (egglog union-find already handles this automatically once
; lower.rs calls egraph.union(bound_var_id, antecedent_id))
; ============================================================
; Extraction schedule
; ============================================================
; Run rules until saturation (up to 1000 iterations).
; Callers invoke this via the Rust EGraph::run_program API,
; so we do NOT emit (run …) here — the Rust side controls it.