This file defines propagators for Nat operators that have simprocs associated with them, but do not have support in satellite solvers. The goal is to workaround a nasty interaction between E-matching and normalization. Consider the following example:

@[grind] def mask := 15

@[grind =] theorem foo (x : Nat) : x &&& 15 = x % 16 := by sorry

example (x : Nat) : 3 &&& mask = 3 := by
  grind only [foo, mask]

This is a very simple version of issue #11498. The e-graph contains 3 &&& mask. E-matching finds that 3 &&& mask matches pattern x &&& 15 modulo the equality mask = 15, binding x := 3. Thus is produces the theorem instance 3 &&& 15 = 3 % 16, which simplifies to True using the builtin simprocs for &&& and %. So, nothing is learned. Tension: The invariant "all terms in e-graph are normalized" conflicts with congruence needing the intermediate term 3 &&& 15 to make the connection. This is yet another example that shows how tricky is to combine e-matching with a normalizer. It is yet another reason for not letting users to extend the normalizer. If we do, we should be able to mark which ones should be used not normalize theorem instances. The following propagator ensure that 3 &&& mask is merged with the equivalence class 3 if mask = 15.

def Lean.Meta.Grind.Arith.propagateNatBinOp (declName congrThmName : Name) (op : Nat → Nat → Nat) (e : Expr) : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.propagateNatAnd : Propagator

Equations

• Lean.Meta.Grind.Arith.propagateNatAnd = Lean.Meta.Grind.Arith.propagateNatBinOp `HAnd.hAnd `Lean.Grind.Nat.and_congr fun (x1 x2 : Nat) => x1 &&& x2

def Lean.Meta.Grind.Arith.propagateNatOr : Propagator

Equations

• Lean.Meta.Grind.Arith.propagateNatOr = Lean.Meta.Grind.Arith.propagateNatBinOp `HOr.hOr `Lean.Grind.Nat.or_congr fun (x1 x2 : Nat) => x1 ||| x2

def Lean.Meta.Grind.Arith.propagateNatXOr : Propagator

Equations

• Lean.Meta.Grind.Arith.propagateNatXOr = Lean.Meta.Grind.Arith.propagateNatBinOp `HXor.hXor `Lean.Grind.Nat.xor_congr fun (x1 x2 : Nat) => x1 ^^^ x2

def Lean.Meta.Grind.Arith.propagateNatShiftLeft : Propagator

Equations

• Lean.Meta.Grind.Arith.propagateNatShiftLeft = Lean.Meta.Grind.Arith.propagateNatBinOp `HShiftLeft.hShiftLeft `Lean.Grind.Nat.shiftLeft_congr fun (x1 x2 : Nat) => x1 <<< x2

def Lean.Meta.Grind.Arith.propagateNatShiftRight : Propagator

Equations

• Lean.Meta.Grind.Arith.propagateNatShiftRight = Lean.Meta.Grind.Arith.propagateNatBinOp `HShiftRight.hShiftRight `Lean.Grind.Nat.shiftRight_congr fun (x1 x2 : Nat) => x1 >>> x2

def Lean.Meta.Grind.Arith.propagateMul : Propagator

Propagator for the 0*a, 1*a, a*0, a*1 for semirings that do not have good support in grind ring. We need this propagator because have normalization rules for them, and users were surprised when using grind [zero_mul] did not have any effect. In this scenario, grind was correctly instantiating zero_mul : 0*a = 0, but the normalizer reduces the instance to True.

Alternative approach: We improve the support for equality reasoning for non-commutative rings and semirings in grind ring. For example, we could just replace equalities and keep renormalizing. If we implement this feature, this propagator can be deleted.

Equations

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