Module docstring
{}
Lean.Grind.nestedProof
definition
(p : Prop) {h : p} : p
Full source
/-- A helper gadget for annotating nested proofs in goals. -/
def nestedProof (p : Prop) {h : p} : p := hInformal description
Given a proposition $p$ and a proof $h$ of $p$, the term `nestedProof p h` returns the proof $h$ itself. This is a helper construct used for annotating nested proofs in goals.
Lean.Grind.simpMatchDiscrsOnly
definition
{α : Sort u} (a : α) : α
Full source
/--
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`.
-/
def simpMatchDiscrsOnly {α : Sort u} (a : α) : α := aInformal description
The function `simpMatchDiscrsOnly` takes an element `a` of type `α` and returns `a` unchanged. It is used as a marker for `match`-expressions to prevent them from being simplified by the `grind` simplifier while still normalizing the discriminants.
Lean.Grind.offset
definition
(a b : Nat) : Nat
Informal description
The function `offset` takes two natural numbers `a` and `b` and returns their sum `a + b`. This is used as a gadget for representing offsets of the form `t + k` in patterns.
Lean.Grind.eqBwdPattern
definition
(a b : α) : Prop
Full source
/-- Gadget for representing `a = b` in patterns for backward propagation. -/
def eqBwdPattern (a b : α) : Prop := a = bInformal description
The proposition `eqBwdPattern a b` represents the equality `a = b` and is used as a gadget for pattern matching in backward propagation.
Lean.Grind.EqMatch
abbrev
(a b : α) {_origin : α} : Prop
Full source
/--
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.
-/
abbrev EqMatch (a b : α) {_origin : α} : Prop := a = bInformal description
Given elements $a, b$ of type $\alpha$ and an origin term $\mathit{origin}$, the proposition $\text{EqMatch}(a, b, \mathit{origin})$ is used to annotate equality conclusions in match-equations. When this proposition is true, it marks $\mathit{origin}$ as a resolved case-split during E-matching.
Lean.Grind.MatchCond
abbrev
(p : Prop) : Prop
Full source
/--
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.
-/
abbrev MatchCond (p : Prop) : Prop := pInformal description
The abbreviation `MatchCond` is a gadget used to annotate conditions in `match` equational lemmas. It serves two purposes:
1. To prevent normalization of these conditions.
2. To provide a propagator for them.
Lean.Grind.PreMatchCond
definition
(p : Prop) : Prop
Full source
/--
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`.
-/
def PreMatchCond (p : Prop) : Prop := pInformal description
The function `PreMatchCond` takes a proposition `p` and returns `p` itself. It is similar to `MatchCond` but is not reducible, ensuring that `simp` will not eliminate it. After applying `simp`, it is replaced with `MatchCond`.
Lean.Grind.nestedProof_congr
theorem
(p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nestedProof p hp) (@nestedProof q hq)
Full source
theorem nestedProof_congr (p q : Prop) (h : p = q) (hp : p) (hq : q) : HEq (@nestedProof p hp) (@nestedProof q hq) := by
subst h; apply HEq.reflInformal description
For any propositions $p$ and $q$, if $p = q$ and we have proofs $hp : p$ and $hq : q$, then the nested proof annotations $\text{nestedProof } p \ hp$ and $\text{nestedProof } q \ hq$ are heterogeneously equal.
Lean.Grind.nestedProofUnexpander
definition
: PrettyPrinter.Unexpander
Full source
@[app_unexpander nestedProof]
def nestedProofUnexpander : PrettyPrinter.Unexpander := fun stx => do
match stx with
| `($_ $p:term) => `(‹$p›)
| _ => throw ()Informal description
The unexpander function for nested proof annotations in the Lean Grind module. When applied to syntax of the form `nestedProof p`, it transforms it into the notation `‹p›` (which represents a term of type `p`). For any other syntax form, it fails to unexpand.
Lean.Grind.matchCondUnexpander
definition
: PrettyPrinter.Unexpander
Full source
@[app_unexpander MatchCond]
def matchCondUnexpander : PrettyPrinter.Unexpander := fun stx => do
match stx with
| `($_ $p:term) => `($p)
| _ => throw ()Informal description
The unexpander function for match conditions in the Lean pretty printer attempts to reverse the expansion of match condition syntax. Given a syntax tree node representing a match condition, it returns the original pattern `p` if the input matches the expected form, otherwise it fails.
Lean.Grind.eqMatchUnexpander
definition
: PrettyPrinter.Unexpander
Full source
@[app_unexpander EqMatch]
def eqMatchUnexpander : PrettyPrinter.Unexpander := fun stx => do
match stx with
| `($_ $lhs:term $rhs:term) => `($lhs = $rhs)
| _ => throw ()Informal description
The unexpander function for equality matching in the Lean pretty-printer transforms syntax nodes of the form `matchCond lhs rhs` into the standard equality syntax `lhs = rhs`. If the input syntax does not match this pattern, the function fails silently.
Lean.Grind.offsetUnexpander
definition
: PrettyPrinter.Unexpander
Full source
@[app_unexpander offset]
def offsetUnexpander : PrettyPrinter.Unexpander := fun stx => do
match stx with
| `($_ $lhs:term $rhs:term) => `($lhs + $rhs)
| _ => throw ()Informal description
The unexpander function transforms syntax trees representing expressions of the form `offset lhs rhs` into the equivalent form `lhs + rhs`. If the input syntax doesn't match this pattern, the function fails silently.
Lean.Grind.natCastUnexpander
definition
: PrettyPrinter.Unexpander
Full source
@[app_unexpander NatCast.natCast]
def natCastUnexpander : PrettyPrinter.Unexpander := fun stx => do
match stx with
| `($_ $a:term) => `(↑$a)
| _ => throw ()Informal description
The unexpander function for natural number casts takes a syntax tree representing a natural number cast operation and attempts to rewrite it to use the standard up-arrow notation `↑a` for casts. If the input syntax doesn't match the expected pattern of a natural number cast, the function fails silently.
Lean.Grind.alreadyNorm
definition
(p : Prop) : Prop
Full source
/--
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.
-/
def alreadyNorm (p : Prop) : Prop := pInformal description
The function `alreadyNorm` marks a proposition $p$ as already normalized, indicating that it should not be processed further by normalization procedures. This prevents redundant processing and ensures consistency when handling negated conditions in logical expressions.
Lean.Grind.em
theorem
(p : Prop) : alreadyNorm p ∨ alreadyNorm (¬p)
Full source
/--
`Classical.em` variant where disjuncts are marked with `alreadyNorm` gadget.
See comment at `alreadyNorm`
-/
theorem em (p : Prop) : alreadyNormalreadyNorm p ∨ alreadyNorm (¬ p) :=
Classical.em pInformal description
For any proposition $p$, either $p$ is marked as already normalized or its negation $\neg p$ is marked as already normalized.