17.4. Constraint Propagation🔗

Constraint propagation works on the True and False buckets of the whiteboard. Whenever a term is added to one of those buckets, grind fires dozens of small forward rules that derive further information from its logical consequences:

Boolean connectives

The truth tables of the Boolean connectives can be used to derive further true and false facts. For example:

If A is True, then A ∨ B becomes True.
If A ∧ B is True, then both A and B become True.
If A ∧ B is False, at least one of A, B becomes False.

Inductive Types

If terms formed by applications of two different constructors of the same inductive type (e.g. none and some) are placed in the same equivalence class, a contradiction is derived. If two terms formed by applications of the same constructor are placed in the same equivalence class, then their arguments are also made equal.

Projections

From h : (x, y) = (x', y') we derive x = x' and y = y'.

Casts

Any term cast h a : β is equated with a : α immediately (using heterogeneous equality).

Definitional equality

Definitional reduction is propagated, so (a, b).1 is equated with a. The η-equality rule for structures is not automatically used, so if p is an instance of a structure S with two fields, then p is not equated with ⟨p.1, p.2⟩. However, tagging S with @[grind ext] causes the E-matching engine to prove these goals.

Below is a representative slice of the propagators that demonstrates their overall style. Each follows the same skeleton.

It inspect the truth value of sub‑expressions.
If further facts can be derived, it either equates terms (connecting them on the metaphorical whiteboard) using (pushEq), or it indicates truth values using (pushEqTrue / pushEqFalse). These steps produce proof terms using internal helper lemmas such as Grind.and_eq_of_eq_true_left.
If a contradiction arises, the goal is closed using (closeGoal).

Upward propagation derives facts about a term from facts about sub-terms, while downward propagation derives facts about sub-terms from facts about a term.

/-- 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
    -- b = True  ⇒  (a ∧ b) = a
    pushEq e a <|
      mkApp3 (mkConst ``Grind.and_eq_of_eq_true_right)
        a b (← mkEqTrueProof b)
  else if (← isEqFalse a) then
    -- a = False  ⇒  (a ∧ b) = False
    pushEqFalse e <|
      mkApp3 (mkConst ``Grind.and_eq_of_eq_false_left)
        a b (← mkEqFalseProof a)
  else if (← isEqFalse b) then
    -- b = False  ⇒  (a ∧ b) = False
    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
    -- (a ∧ b) = True  ⇒  a = True
    pushEqTrue a <| mkApp3
      (mkConst ``Grind.eq_true_of_and_eq_true_left) a b h
    -- (a ∧ b) = True  ⇒  B = True
    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`	Uses the truth table for disjunction to derive further truth values
`propagateNotUp` / `propagateNotDown`	`¬ A`	Ensures that `¬ A` and `A` have opposite truth values
`propagateEqUp` / `propagateEqDown`	`a = b`	Bridges Booleans, detects constructor clash
`propagateIte` / `propagateDIte`	`ite` / `dite`	Equates the term with the chosen branch once the condition's truth value is known
`propagateEtaStruct`	Values of structures tagged `[grind ext]`	Generates η‑expansion `a = ⟨a.1, …⟩`

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

17.4.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 internalized. Setting the option trace.grind.eqc to true causes grind to print a line every time two equivalence classes merge, which is handy for seeing propagation in action.

The set of propagation rules is expanded and refined over time, so the InfoView will show increasingly rich True and False buckets. The full equivalence classes are displayed automatically only when grind fails, and only for the first subgoal that it could not close—use this output to inspect missing facts and understand why the subgoal remains open.

Identifying Missing Facts

In this example, grind fails:

example :
    x = y ∧ y = z →
    w = x ∨ w = v →
    w = z := byα✝:Sort u_1x:α✝y:α✝z:α✝w:α✝v:α✝⊢ x = y ∧ y = z → w = x ∨ w = v → w = z
  `grind` failed
grindα:Sort u_1x y z w v:αleft:x = yright:y = zh_1:w = x ∨ w = vh_2:¬w = z⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x = y
[prop] y = z
[prop] w = x ∨ w = v
[prop] ¬w = z
[eqc] True propositions
[prop] w = x ∨ w = v
[prop] w = v
[eqc] False propositions
[prop] w = x
[prop] w = z
[eqc] Equivalence classes
[eqc] {x, y, z}
[eqc] {w, v}grindα✝:Sort u_1x:α✝y:α✝z:α✝w:α✝v:α✝⊢ x = y ∧ y = z → w = x ∨ w = v → w = z

The resulting error message includes the identified equivalence classes along with the true and false propositions:

`grind` failed
grindα:Sort u_1x y z w v:αleft:x = yright:y = zh_1:w = x ∨ w = vh_2:¬w = z⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] x = y
[prop] y = z
[prop] w = x ∨ w = v
[prop] ¬w = z
[eqc] True propositions
[prop] w = x ∨ w = v
[prop] w = v
[eqc] False propositions
[prop] w = x
[prop] w = z
[eqc] Equivalence classes
[eqc] {x, y, z}
[eqc] {w, v}

Both x = y and y = z were discovered by constraint propagation from the x = y ∧ y = z premise. In this proof, grind performed a case split on w = x ∨ w = v. In the second branch, it could not place w and z in the same equivalence class.