17.6. Constraint Propagation

Constraint propagation works on the True and False buckets of the white‑board. Whenever a literal is added to one of those buckets, grind fires dozens of small forward rules to push its logical consequences:

Boolean connectives — e.g. if A is True, mark A ∨ B True; if A ∧ B is True, mark both A and B True; if A ∧ B is False, at least one of A, B becomes False.
Inductive datatypes — two different constructors (none vs some _) collapsing into the same class yield contradiction; equal tuples yield equal components.
Projections and casts — from h : (x, y) = (x', y') we derive x = x' and y = y'; any term cast h a is merged with a immediately (using a heterogeneous equality) so both live in the same class.
Structural eta and definitional equalities — ⟨a, b⟩.1 propagates to a, etc.

Below is a representative slice of the propagators so you can see the style they follow. Each follows the same skeleton: inspect the truth‑value of sub‑expressions, push equalities (pushEq) or truth‑values (pushEqTrue / pushEqFalse), and optionally close the goal if a contradiction (closeGoal) arises. A few high‑signal examples:

/-- Propagate equalities *upwards* for conjunctions. -/
builtin_grind_propagator propagateAndUp ↑And := fun e => do
  let_expr And a b := e | return ()
  if (← isEqTrue a) then
    -- a = True  ⇒  (a ∧ b) = b
    pushEq e b <|
      mkApp3 (mkConst ``Grind.and_eq_of_eq_true_left)
        a b (← mkEqTrueProof a)
  else if (← isEqTrue b) then
    pushEq e a <|
      mkApp3 (mkConst ``Grind.and_eq_of_eq_true_right)
        a b (← mkEqTrueProof b)
  else if (← isEqFalse a) then
    pushEqFalse e <|
      mkApp3 (mkConst ``Grind.and_eq_of_eq_false_left)
        a b (← mkEqFalseProof a)
  else if (← isEqFalse b) then
    pushEqFalse e <|
      mkApp3 (mkConst ``Grind.and_eq_of_eq_false_right)
        a b (← mkEqFalseProof b)

/--
Truth flows *down* when the whole `And` is proven `True`.
-/
builtin_grind_propagator propagateAndDown ↓And :=
  fun e => do
  if (← isEqTrue e) then
    let_expr And a b := e | return ()
    let h ← mkEqTrueProof e
    pushEqTrue a <| mkApp3
      (mkConst ``Grind.eq_true_of_and_eq_true_left) a b h
    pushEqTrue b <| mkApp3
      (mkConst ``Grind.eq_true_of_and_eq_true_right) a b h

Other frequently‑triggered propagators follow the same pattern:

| Propagator | Handles | Notes | | ------------------------------------------------- | ------------------------------- | ---------------------------------------------- | | propagateOrUp / propagateOrDown | a ∨ b | True/False pushes for disjunctions | | propagateNotUp / propagateNotDown | ¬ a | Links ¬ a with the Boolean of a | | propagateEqUp / propagateEqDown | a = b | Bridges Booleans, detects constructor clash | | propagateIte / propagateDIte | ite / dite | Replaces chosen branch once condition is fixed | | propagateEtaStruct | structures tagged [grind ext] | Generates η‑expansion a = ⟨a.1, …⟩ |

Many specialised variants for Bool mirror these rules exactly (e.g. propagateBoolAndUp).

17.6.1. Propagation‑only examples

These goals are closed purely by constraint propagation—no case splits, no theory solvers:

example (a : Bool) : (a && !a) = false := bya:Bool⊢ (a && !a) = false
  grindAll goals completed! 🐙

-- Conditional (ite):
-- once the condition is true, ite picks the 'then' branch.
example (c : Bool) (t e : Nat) (h : c = true) :
    (if c then t else e) = t := byc:Boolt:Nate:Nath:c = true⊢ (if c = true then t else e) = t
  grindAll goals completed! 🐙

-- Negation propagates truth downwards.
example (a : Bool) (h : (!a) = true) : a = false := bya:Boolh:(!a) = true⊢ a = false
  grindAll goals completed! 🐙

These snippets run instantly because the relevant propagators (propagateBoolAndUp, propagateIte, propagateBoolNotDown) fire as soon as the hypotheses are internalised.

Note If you toggle set_option trace.grind.eqc true, grind will print a line every time two equivalence classes merge—handy for seeing propagation in action.

Implementation tip grind is still under active development. Until the API has stabilised we recommend refraining from custom elaborators or satellite solvers. If you really need a project‑local propagator, use the user‑facing grind_propagator command rather than builtin_grind_propagator (the latter is reserved for Lean’s own code). When adding new propagators keep them small and orthogonal—they should fire in ≤1 µs and either push one fact or close the goal. This keeps the propagation phase predictable and easy to debug.

We continuously expand and refine the rule set—expect the Info View to show increasingly rich True/False buckets over time. The full equivalence classes are displayed automatically only when grind fails, and only for the first subgoal it could not close—use this output to inspect missing facts and understand why the subgoal remains open.