Simp lemmas are used by the "simplifier" family of tactics.
simp_lemmas is essentially a pair of tables rb_map (expr_type × name) (priority_list simp_lemma).
One of the tables is for congruences and one is for everything else.
An individual simp lemma is:
A kind which can be Refl, Simp or Congr.
A pair of exprs l ~> r. The rb map is indexed by the name of get_app_fn(l).
A proof that l = r or l ↔ r.
A list of the metavariables that must be filled before the proof can be applied.
Add a simplification lemma by an expression p. Some conditions on p must hold for it to be added, see list below.
If your lemma is not being added, you can see the reasons by setting set_option trace.simp_lemmas true.
p must have the type Π (h₁ : _) ... (hₙ : _), LHS ~ RHS for some reflexive, transitive relation (usually =).
Any of the hypotheses hᵢ should either be present in LHS or otherwise a Prop or a typeclass instance.
Adds a congruence simp lemma to simp_lemmas.
A congruence simp lemma is a lemma that breaks the simplification down into separate problems.
For example, to simplify a ∧ b to c ∧ d, we should try to simp a to c and b to d.
For examples of congruence simp lemmas look for lemmas with the @[congr] attribute.
get_eqn_lemmas_for deps d returns the automatically generated equational lemmas for definition d.
If deps is tt, then lemmas for automatically generated auxiliary declarations used to define d are also included.
simplify s e cfg r prove simplify e using s using bottom-up traversal.
discharger is a tactic for dischaging new subgoals created by the simplifier.
If it fails, the simplifier tries to discharge the subgoal by simplifying it to true.
The parameter to_unfold specifies definitions that should be delta-reduced,
and projection applications that should be unfolded.
s : simp_lemmas - the set of simp_lemmas to use. Remark: the simplification lemmas are not applied automatically like in the simplify tactic. The caller must use them at pre/post.
discharger : α → tactic α - tactic for dischaging hypothesis in conditional rewriting rules. The argument 'α' is the current user data.
pre a s r p e is invoked before visiting the children of subterm 'e'.
a is the current user data
s is the updated set of lemmas if 'contextual' is tt,
r is the simplification relation being used,
p is the "parent" expression (if there is one).
e is the current subexpression in question.
if it succeeds the result is (new_a, new_e, new_pr, flag) where
new_a is the new value for the user data
new_e is a new expression s.t. r e new_e
new_pr is a proof for r e new_e, If it is none, the proof is assumed to be by reflexivity
flag if tt new_e children should be visited, and post invoked.
(post a s r p e) is invoked after visiting the children of subterm e,
The output is similar to (pre a r s p e), but the 'flag' indicates whether the new expression should be revisited or not.
r is the simplification relation. Usually = or ↔.
e is the input expression to be simplified.
The method returns (a,e,pr) where
a is the final user data
e is the new expression
pr is the proof that the given expression equals the input expression.
Note that ext_simplify_core will succeed even if pre and post fail, as failures are used to indicate that the method should move on to the next subterm.
If it is desirable to propagate errors from pre, they can be propagated through the "user data".
An easy way to do this is to call tactic.capture (do ...) in the parts of pre/post where errors matter, and then use tactic.unwrap a on the result.
Additionally, ext_simplify_core does not propagate changes made to the tactic state by pre and post. If it is desirable to propagate changes to the tacticstate in addition to errors, usetactic.resumeinstead oftactic.unwrap`.
-- make a new simp attribute called "my_reduction"run_cmdmk_simp_attr`my_reduction-- Add "my_reduction" attributes to these if-reductionsattribute[my_reduction]if_posif_negdif_posdif_neg-- will return the simp_lemmas with the `my_reduction` attribute.#evalget_user_simp_lemmas`my_reduction```