def Lean.Grind.nestedProof (p : Prop) {h : p} : p

A helper gadget for annotating nested proofs in goals.

Equations

• ⋯ = h

def Lean.Grind.nestedDecidable {p : Prop} (h : Decidable p) : Decidable p

A helper gadget for annotating nested decidable instances in goals.

Equations

• Lean.Grind.nestedDecidable h = h

def Lean.Grind.simpMatchDiscrsOnly {α : Sort u} (a : α) : α

Gadget for marking match-expressions that should not be reduced by the grind simplifier, but the discriminants should be normalized. We use it when adding instances of match-equations to prevent them from being simplified to true.

Remark: it must not be marked as [reducible]. Otherwise, simp will reduce

simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true

using eq_self.

Equations

• Lean.Grind.simpMatchDiscrsOnly a = a

def Lean.Grind.offset (a b : Nat) : Nat

Gadget for representing offsets t+k in patterns.

Equations

• a + b = a + b

def Lean.Grind.eqBwdPattern {α : Sort u_1} (a b : α) : Prop

Gadget for representing a = b in patterns for backward propagation.

Equations

• Lean.Grind.eqBwdPattern a b = (a = b)

@[reducible, inline]

abbrev Lean.Grind.EqMatch {α : Sort u_1} (a b : α) {_origin : α} : Prop

Gadget for annotating the equalities in match-equations conclusions. _origin is the term used to instantiate the match-equation using E-matching. When EqMatch a b origin is True, we mark origin as a resolved case-split.

Equations

• (a = b) = (a = b)

@[reducible, inline]

abbrev Lean.Grind.MatchCond (p : Prop) : Prop

Gadget for annotating conditions of match equational lemmas. We use this annotation for two different reasons:

• We don't want to normalize them.
• We have a propagator for them.

Equations

• p = p

def Lean.Grind.PreMatchCond (p : Prop) : Prop

Similar to MatchCond, but not reducible. We use it to ensure simp will not eliminate it. After we apply simp, we replace it with MatchCond.

Equations

• Lean.Grind.PreMatchCond p = p

theorem Lean.Grind.nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : ⋯ ≍ ⋯

theorem Lean.Grind.nestedDecidable_congr (p q : Prop) (h : p = q) (hp : Decidable p) (hq : Decidable q) : nestedDecidable hp ≍ nestedDecidable hq

def Lean.Grind.nestedProofUnexpander : PrettyPrinter.Unexpander

Equations

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

def Lean.Grind.matchCondUnexpander : PrettyPrinter.Unexpander

Equations

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

def Lean.Grind.eqMatchUnexpander : PrettyPrinter.Unexpander

Equations

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

def Lean.Grind.offsetUnexpander : PrettyPrinter.Unexpander

Equations

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

def Lean.Grind.natCastUnexpander : PrettyPrinter.Unexpander

Equations

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

def Lean.Grind.alreadyNorm (p : Prop) : Prop

A marker to indicate that a proposition has already been normalized and should not be processed again.

This prevents issues when case-splitting on the condition c of an if-then-else expression. Without this marker, the negated condition ¬c might be rewritten into an alternative form c', which grind may not recognize as equivalent to ¬c. As a result, grind could fail to propagate that if c then a else b simplifies to b in the ¬c branch.

Equations

• Lean.Grind.alreadyNorm p = p

theorem Lean.Grind.em (p : Prop) : alreadyNorm p ∨ alreadyNorm ¬p

Classical.em variant where disjuncts are marked with alreadyNorm gadget. See comment at alreadyNorm