Example : Inequalities between natural numbers
Suppose we want to inspect a goal to see if it is an inequality of the form a ≤ b, where a and b are natural numbers. If it is, we want to extract those values (to illustrate, we print these to the Infoview). Because this involves creating and assigning metavariables (temporary placeholders), we need to work inside the MetaM monad.
We will start by writing a function that takes an expression (Expr) as input. Its output will be an Option (Expr × Expr) wrapped inside the MetaM monad, allowing it to return the two sides of the inequality if a match is found, or none if it is not.
Therefore, the type signature of our function will be Expr → MetaM (Option (Expr × Expr)).
def matchNatLe? (e: Expr) :
MetaM <| Option (Expr × Expr) := do
let nat := mkConst ``Nat
let a ← mkFreshExprMVar nat
let b ← mkFreshExprMVar nat
let ineq ← mkAppM ``Nat.le #[a, b]
if (← isDefEq ineq e) then
return some (a, b)
else
return none
mkFreshExprMVar nat constructs a metavariable of the type nat, where nat is an expression. This creates a blank hole that Lean can fill in later. The expression isDefEq ineq e checks whether the constructed expression ineq and the target expression e are definitionally equal. Crucially, as it checks for equality, it attempts to unify them by assigning concrete values from e to our blank metavariables a and b.
Now, to see this function in action we write an elaborator that fetches the main goal during the proof and passes it to matchNatLe.
elab "matchNatLe?" : tactic => do
withMainContext do
let goal ← getMainTarget
match (← matchNatLe? (goal)) with
| some (a, b) => logInfo m!"The goal is an inequality
`a ≤ b` between natural numbers where a = {a}, b = {b}"
| _ => logInfo m!"The goal is not an inequality"
example: 123 ≤ 234 := ⊢ 123 ≤ 234
⊢ 123 ≤ 234
All goals completed! 🐙