Simplifier Features

Here we list some suggestions / possible features for Lean's simplifier.

• Add pre- and/or post-processing methods to the simpset (called simproc in Isabelle). The idea is to install methods which are called when the current term matches certain patterns (see the section about Isabelle's simplifier for applications)

• Support the auto_param in the simplifier. Applications: (1) solve assumption in conditional rewrite rules, and (2) synthesize parts of the right-hand side.

• Preprocess hypothesis (either provided by the user, or by congruence rules) Isabelle's simplifier rewrites hypothesis and then adds them to the simpset. For congruence rules there is a special implication H =simp=> G which forces the simplifier to rewrite H before adding it to the context.

• Isabelle has the marker ASSUMPTION(p): it forces the simplifier to solve a condition of a simp-rule to be solved by an assumption and not be touched by rewriting. I guess in Lean this would be done by an auto_param: (H : p . assumption).

• Often users want to enforce the application of a conditional rule: if the simplifier cannot solve the conditions it should be added as new goals to the interactive state. This would require quite some additions to the state in which the pre- and post-processing methods work: they need to return informations (new mvars are introduced), and the methods might also get some information (maybe an enforced rule should be only applied once)

Isabelle's simplifier

Simprocs in Isabelle's simplifer are activated when the current term matches certain pattern. But the pattern can be very generic ?x : ?t.

The simplifier is also parameterized by loopers and solvers, they are not explaind here.

Simpprocs

• NO_MATCH(x, t) Fails if the pattern x matches t. Otherwise NO_MATCH is definitionally true. Allows more control over the simplifcation process. For example it can be used to always rewrite t : unit to ().

• Diverse cancellation procedures. Try to cancel common terms from (in)equalities. For example when a term a * b >= c * b is reached it is tried to derive 0 <= b from the assumptions and simplified to a >= c.

• Fast linear arithmetic

• sup and inf cancellation. Example: Reduce sup a (sup b (-a)) to top.

• Collect_mem: simplify {(x1, ..., xn) | (x1, ..., xn) \in S} to S

• Let_simp: reduce let x := t in t' under cetrain conditions: either t is small (variable or constant) or x appears only once in t'

• list_eq / list_neq: cancel common terms at start or end of both sides of an equation

• unit_eq: Rewrite t : unit to () (could be done now my NO_MATCH)

• prove (y = x) = false from ~ (y = x)

• record evaluation / updates normalization. I guess this is done by Lean's elaborator / kernel

• Remove equality from quantifiers. Example: forall x, p x --> x = t --> q x reduces to p t --> q t

Congruence rules

• Setup by the datatype package case_* (in Lean type.case_on): provide the simplifier with additional assumption about the new variables in each case. For example match xs with [] := t | (x :: xs') := t' end, by congruence we get xs = [] -> t = ?t and forall x xs', xs = x :: xs' -> t' x xs' = ?t x xs'.

• =simp=>: One often wants to rewrite the additional hypothesis introduced by introduction rules this is done by =simp=>: (forall x, x \in s =simp=> p x) --> (forall x \in s, p x). Here =simp=> allows that x \in s can be rewritten

• Expected rules for: -->, if _ then _ else, bounded all, and bounded ex

Splitter

Split up if and case (i.e. match) statements. The splitter is parameterized by rules like

C (if p then a else b) <-> (p -> C a) /\ (~ p -> C b).

Then it will replace an occurrences of if _ then _ else _ by its logical representation. The hope is that with the additional hypothesis C can be rewritten in both cases, and that C a and C b can be further reduced.

This is not restricted to constructs like if, another possible rule is

C (a - b) <-> (a <= b --> C 0) /\ (forall c > 0, b = a + c --> C c)

where a and b are natural numbers.