Edward Ayers (Oct 10 2018 at 10:45):
What is the difference between a 'simp' and a 'congr' below?
meta constant simp_lemmas.add_simp : simp_lemmas → name → tactic simp_lemmas meta constant simp_lemmas.add_congr : simp_lemmas → name → tactic simp_lemmas
Edward Ayers (Oct 10 2018 at 10:48):
My guess is that anything of the form
lhs = rhs goes in
simp knows its a congruence relation.
In the C++, I can see that there is a pair of tables for each equivalence relation we have simp lemmas for. One table contains congruences and the other contains simps. So I guess for
<-> the simps table would be empty? What would be an example of a relation where both the congr and simps table would be occupied?
I remember hearing somewhere that simp can support arbitrary congruence relations.
Edward Ayers (Oct 10 2018 at 10:50):
I'm interested in expanding on this from
simp.md in mathlib's docs.
### Something that could be added later on:
"Re: documentation. If you mention congruence, you could show off simp's support for congruence relations. If you show reflexivity and transitivity for cong, and have congruence lemmas for +, etc., then you can rewrite with congruences as if they were equations."
Edward Ayers (Oct 10 2018 at 11:02):
What is on the lhs and rhs for the simp lemma made from this:
@[simp] theorem ne_zero (u : units α) : (u : α) ≠ 0 := ...
Edward Ayers (Oct 10 2018 at 11:48):
Ok now that I've printed out the congruence rules and simp rules for the default set of simp_lemmas I am just confused.
Edward Ayers (Oct 10 2018 at 11:54):
Ah ok, congruence lemmas let you move between different relations:
[if_simp_congr] #11 (?x_1 ↔ ?x_2) (?x_4 = ?x_6) (?x_5 = ?x_7), ite ?x_1 ?x_4 ?x_5 = ite ?x_2 ?x_6 ?x_7
Whereas simps don't. I am now curious about whether simp lemmas can be defined for other relations. They have to be transitive and reflexive, but I don't know if it has to be congruent
x = y -> f x = f y. Would it be possible to define simp lemmas for the relation
<? What about integer conguence mod n?
Gabriel Ebner (Oct 10 2018 at 12:15):
Simp lemmas and congruence lemmas are very different. 1) They have different variable constraints: for simp lemmas, all variables of the rhs must occur on the lhs. E.g.
g x y = f x is a simp lemma, but
f x = g x y is not. Congruence lemmas on the hand impose a requirement on the hypotheses: e.g.
x = y -> f x = f y is a congruence lemma, but
x = h x -> f x = f x is not (because the rhs of
x = h x is just wrong).
Gabriel Ebner (Oct 10 2018 at 12:16):
2) Their purpose is different. You use congruence lemmas to specify where to rewrite, and simp lemmas tell you the result of the rewriting.
Gabriel Ebner (Oct 10 2018 at 12:18):
Ideally you could use simp to rewrite modulo integer congruence. As far as I remember there was a technical problem preventing this though. But there's no fundamental reason why this can't work.
Gabriel Ebner (Oct 10 2018 at 12:19):
I think the most interesting example of a simp relation other than
equiv at the moment. Look at
Edward Ayers (Oct 10 2018 at 12:25):
Thanks! As far as I can tell,
x = y -> f x = f y is not explicitly in simp_lemmas. simp is assuming the relation is congruent. Is this right?
Gabriel Ebner (Oct 10 2018 at 12:26):
That's a congruence lemma. And yes, it is generated on-demand using the same tool that powers the
Edward Ayers (Oct 10 2018 at 12:27):
So you couldn't do simp with the
Gabriel Ebner (Oct 10 2018 at 13:47):
No, because 1)
< is not reflexive and 2)
has_lt.lt is not transitive in general. I think you can turn
nat.le into a simplification relation though.
Last updated: May 13 2021 at 18:26 UTC