Zulip Chat Archive

Stream: general

Topic: simp_lemmas


view this post on Zulip 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

view this post on Zulip Edward Ayers (Oct 10 2018 at 10:48):

My guess is that anything of the form lhs = rhs goes in add_congr so 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 = and <-> 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.

view this post on Zulip 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."

view this post on Zulip 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
:= ...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Oct 10 2018 at 12:19):

I think the most interesting example of a simp relation other than eq is equiv at the moment. Look at data/equiv.lean.

view this post on Zulip 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?

view this post on Zulip 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 congr tactic.

view this post on Zulip Edward Ayers (Oct 10 2018 at 12:27):

So you couldn't do simp with the < relation?

view this post on Zulip 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