def Lean.Meta.Grind.preprocessLight (e : Expr) : GoalM Expr

A lighter version of preprocess which produces a definitionally equal term, but ensures assumptions made by grind are satisfied.

Equations

• One or more equations did not get rendered due to their size.

abstractGroundMismatches? is an auxiliary function for creating auxiliary equality proofs. When trying to prove lhs = rhs, we use two different approaches. In the first one, we just internalize the terms, propagate, and then check whether they are in the same equivalence class. The function abstractGroundMismatches? is used to implement the second approach that focus on terms containing binders. Here is a motivating example, suppose we are trying to prove that (b : Bool) → a[i]? = some b → Nat is equal to (b : Bool) → some v = some b → Nat and the goal contains the equivalence class {a[i]?, some v}. Congruence closure does not process terms containing free variables, and fails to prove the equality. abstractGroundMismatches? extracts ground terms that are equal in the current goal, and creates an auxiliary function. In the example above, the following two terms are generated.

• (fun x => (b : Bool) → x = some b → Nat) a[i]?
• (fun x => (b : Bool) → x = some b → Nat) (some v)

The two new terms are definitionally equal to the original ones, but congruence closure will now detect the equality.

The motivation for this infrastructure is match-expression equalities. Suppose we have

match h : assign[v]? with
| none => ...
| some b => ...

When instantiating the match-expr equations for the none and some cases, we need to introduce casts.

Helper functions for creating equalities proofs.

def Lean.Meta.Grind.proveEq? (lhs rhs : Expr) (abstract : Bool := false) : GoalM (Option Expr)

Try to construct a proof that lhs = rhs using the information in the goal state. If lhs and rhs have not been internalized, this function will internalize then, process propagated equalities, and then check whether they are in the same equivalence class or not. The goal state is not modified by this function. This function mainly relies on congruence closure, and constraint propagation. It will not perform case analysis.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.proveEq?.tryAbstract (lhs₀ rhs₀ : Expr) : GoalM (Option Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.proveHEq? (lhs rhs : Expr) : GoalM (Option Expr)

Similar to proveEq?, but for heterogeneous equality.

Equations

• One or more equations did not get rendered due to their size.