Simplifier Features

Problems with the current classical approach to the simplifier:

• It does not support reduction: rewrite rules need to match syntactically, definitional equality is not used.

• If we want to use a fully unbundled approach, a la is_commutative a rule like is_commutative t op ==> op a b = ... can not match, as there is no head constant.

• Generally it would be nice to have equivalence classes of constants. For example list.nil would be in the equivalence class list.nil, 0, bot, emptyc. 0 for an additive monoid with list.append, bot with regard to the prefix order, emptyc for insert and union, etc...

• It may be interesting to support matching module symmetry, A, and AC. Examples: ~ 0 = 1 would be nice to have symmetry on =. etc...

Here is a list of classical extensions to the simplifier, i.e. assuming a Isabelle like 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. I guess this is already possible as the core methods already provide a plug-in method to solve conditional rewrite rules.

• 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.

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.

Solver

A plugin tactic, which is called to simplify a subgoal after simplification, or for the premises of a congruence rule. In the later case, the solver is the actual tactic instantiating the meta-variable on the right-hand side of the congruence rules premises.

Looper

A plugin tactic, which is called if the solver fails. It is the one responsible for splitting.