Sym.simp simprocs of the grind normalizer

Ports of the Meta.simp simprocs in SimpUtil.lean and ForallProp.lean whose rewrite rules are not first-order (they bind variables or dispatch on the shape of the term). Results are built with the maximal-sharing builders (mkAppS, ...); proofs are built without inferType. The definitional reductions (beta, zeta, projections, matchers) are the shared ones in Lean.Meta.Sym.Simp.Reduce.

def Lean.Meta.Grind.NormSym.eraseMData : Sym.Simp.Simproc

Erases metadata. grind never internalizes Expr.mdata.

Equations

• Lean.Meta.Grind.NormSym.eraseMData (Lean.Expr.mdata data b) = do let __do_lift ← liftM (Lean.Meta.Sym.mkEqRefl b) pure (Lean.Meta.Sym.Simp.Result.step b __do_lift)
• Lean.Meta.Grind.NormSym.eraseMData e = pure Lean.Meta.Sym.Simp.Result.rfl

def Lean.Meta.Grind.NormSym.preMatchCond : Sym.Simp.Simproc

Grind.PreMatchCond p is left as is: p is a condition of a match equation and must keep the shape produced by annotateMatchEqnType; replacePreMatchCond turns it into Grind.MatchCond after normalization.

Equations

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

def Lean.Meta.Grind.NormSym.simpMatchDiscrsOnly : Sym.Simp.Simproc

Grind.simpMatchDiscrsOnly m, where m is a match application: only the discriminants of m are simplified, the alternatives are not visited. The annotation stays and is erased by eraseSimpMatchDiscrsOnly after normalization.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.NormSym.simpMatchDiscrsOnly e = pure Lean.Meta.Sym.Simp.Result.rfl

def Lean.Meta.Grind.NormSym.simpEq : Sym.Simp.Simproc

Normalizes equalities:

• Bool: true = b becomes b = true; (a && b) = c becomes ((a && b) = true) = (c = true).
• a = a becomes True, p = True becomes p, p = False becomes ¬p.

Equations

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

def Lean.Meta.Grind.NormSym.simpDIte : Sym.Simp.Simproc

Converts dite with non-dependent branches into ite.

Equations

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

def Lean.Meta.Grind.NormSym.pushNot : Sym.Simp.Simproc

Pushes negations inwards through the propositional connectives, ite, and the quantifiers. Negated arithmetic comparisons are handled by the rewrite rules Nat.not_le_eq and Int.not_le_eq.

Equations

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

def Lean.Meta.Grind.NormSym.simpOr : Sym.Simp.Simproc

Normalizes disjunctions: units, right-associativity, and universally quantified disjuncts moved to the front.

Equations

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

def Lean.Meta.Grind.NormSym.reduceCtorEq : Sym.Simp.Simproc

Reduces c₁ ... = c₂ ... to False for distinct constructors c₁ and c₂.

Equations

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

def Lean.Meta.Grind.NormSym.simpForall : Sym.Simp.Simproc

Normalizes universally quantified propositions and implications: Grind.imp_true_eq, Grind.imp_false_eq, Grind.true_imp_eq, Grind.false_imp_eq, Grind.imp_self_eq, Grind.forall_true, forall_false, Grind.forall_or_forall, Grind.forall_forall_or, Grind.forall_and (see forallImpAnd?).

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.NormSym.simpForall e = pure Lean.Meta.Sym.Simp.Result.rfl

def Lean.Meta.Grind.NormSym.simpExists : Sym.Simp.Simproc

Normalizes existentially quantified propositions: Grind.exists_or, Grind.exists_and_left, Grind.exists_and_right, Grind.exists_prop, Grind.exists_const.

Equations

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