Simplifying Application Arguments #
Unlike Sym.Simp.App, dsimp does not need to respect the congruence-info split
(fixedPrefix, interlaced, congrTheorem). That split exists in simp to make proof
construction efficient — but here there is no proof to build.
dsimp can rewrite every argument, subject only to the rules:
- Skip proof arguments. It is often a waste of time because of proof irrelevance. In some cases, users may want to reduce proofs to eliminate dependencies. Users can accomplish this by rewriting their own simproc.
- Skip instance arguments. Instances are not usually meaningful to simplify structurally. Moreover, we would be producing non-standard instances. This behavior may be overriden by the dsimp configuration.
Both classes are read from ProofInstInfo (per-declName, cached in SymM). When the
head is not a .const (e.g. an .fvar-headed application), we have no signature info
and rewrite every argument.
Walks the application spine and dsimps each argument unless ProofInstInfo marks it
as a proof or instance. The function head itself is not recursively simplified, so
pre/post simprocs that rewrite heads (e.g. zetaDelta for let-bound .fvar heads,
or beta for lambda heads) must match on the whole application.
Equations
- One or more equations did not get rendered due to their size.