simp lemmas

Stream: general

[Alex J. Best]

Can someone explain to me why set_of_eq_eq_singleton is not a simp lemma it seems like a decent candidate to me, or indeed if it should be?

[Alex J. Best]

Same question for list.pairwise.nil !

[Floris van Doorn]

set_of_eq_eq_singleton seems like a good candidate for a simp-lemma. You will notice that not everything is properly marked as a simp lemma. Feel free to make a PR.

We don't usually mark non-equalities, like list.pairwise.nil as a simp-lemma. I don't think that simp solves things like (0 : nat) <= n. list.pairwise.nilmight be an exception, though: searching through mathlib, it's used quite frequently in simp.

[Alex J. Best]

Will do. Okay succ_pos was what I was thinking of also w.r.t. non-equality, but it seems like such lemmas marked simp are rare.

[Jeremy Avigad]

I don't see any reason to limit simp to equations. In Isabelle, simp is often used to prove simple facts. Here is an example:

import data.nat.prime
open nat

attribute [simp] nat.prime.ge_two

example (p : nat) (h : prime p) : p ≥ 2 :=
by simp *

Better examples are that abs (x^2) and abs (exp x) should simplify tox^2 and exp x, respectively, because the simplifier can show that these are nonnegative. In Isabelle, the simplifier is really good at proving theorems of the form finite t, where t is a subset of an arbitrary type, and this is really useful for conditional rewrites with sums and products. (It will also call linarith to dispel side conditions, which means that it can simplify abs(x^2 + exp x + 7).)

By the way, library_search fails on the example above because of the annoying issue with >= and <=. We should probably get in the habit of expressing all our theorems in the <= form, in which case library_search works.

import data.nat.prime
open nat

@[simp] theorem nat.prime.two_le (p : nat) (h : prime p) : 2 ≤ p :=
nat.prime.ge_two h

example (p : nat) (h : prime p) : p ≥ 2 :=
by library_search

But this doesn't replace the utility of using simp to do similar things. The point is that simp is a conditional simplifier, and so it is useful if it can show p ≥ 2 when it is simplifying something like p - 2 + 2 on nat.