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
- A pair of
l ~> r. The rb map is indexed by the name of
- A proof that
l = ror
l ↔ r.
- A list of the metavariables that must be filled before the proof can be applied.
- A priority number
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.
pmust have the type
Π (h₁ : _) ... (hₙ : _), LHS ~ RHSfor some reflexive, transitive relation (usually
- Any of the hypotheses
hᵢshould either be present in
LHSor otherwise a
Propor a typeclass instance.
LHSshould not occur within
LHSshould not occur within a hypothesis
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
For examples of congruence simp lemmas look for lemmas with the
simp_lemmas.rewrite s e prove R apply a simplification lemma from 's'
- 'e' is the expression to be "simplified"
- 'prove' is used to discharge proof obligations.
- 'r' is the equivalence relation being used (e.g., 'eq', 'iff')
- 'md' is the transparency; how aggresively should the simplifier perform reductions.
Result (new_e, pr) is the new expression 'new_e' and a proof (pr : e R new_e)
(Definitional) Simplify the given expression using only reflexivity equality lemmas from the given set of lemmas. The resulting expression is definitionally equal to the input.
u contains defintions to be delta-reduced, and projections to be reduced.
simplify s e cfg r prove simplify
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
to_unfold specifies definitions that should be delta-reduced,
and projection applications that should be unfolded.
ext_simplify_core a c s discharger pre post r e:
a : α- initial user data
c : simp_config- simp configuration options
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 eis invoked before visiting the children of subterm 'e'.
ais the current user data
sis the updated set of lemmas if 'contextual' is
ris the simplification relation being used,
pis the "parent" expression (if there is one).
eis the current subexpression in question.
- if it succeeds the result is
(new_a, new_e, new_pr, flag)where
new_ais the new value for the user data
new_eis a new expression s.t.
r e new_e
new_pris a proof for
r e new_e, If it is none, the proof is assumed to be by reflexivity
new_echildren should be visited, and
(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.
ris the simplification relation. Usually
eis the input expression to be simplified.
The method returns
ais the final user data
eis the new expression
pris the proof that the given expression equals the input expression.
ext_simplify_core will succeed even if
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
post where errors matter, and then use
tactic.unwrap a on the result.
ext_simplify_core does not propagate changes made to the tactic state by
post. If it is desirable to propagate changes to the tactic state in addition to errors, usetactic.resume
Example usage: #
-- make a new simp attribute called "my_reduction" run_cmd mk_simp_attr `my_reduction -- Add "my_reduction" attributes to these if-reductions attribute [my_reduction] if_pos if_neg dif_pos dif_neg -- will return the simp_lemmas with the `my_reduction` attribute. #eval get_user_simp_lemmas `my_reduction ```