Zulip Chat Archive

Stream: Lean Together 2021

Topic: Tactics

Lukas Stevens (Jan 06 2021 at 18:44):

In @Jannis Limperg 's talk, @Patrick Massot asked whether the new tactic framework would support simprocs and it was not clear what those exactly are. I'll try to clarify them to the best of my understanding: to define a simproc, you give a term pattern for which the simplifier should look for in the goal. Additionally you give a conversion, that is, a function that for a given term tt gives you a theorem ttt \equiv t' where tt' is a simplified version of tt.

I will explain why you would do this instead of using the simplifier by giving an example: suppose we register a simproc that looks for occurences of is_prime c\text{is\_prime}\ c where cc is a literal number. Then, our function looks at the number and efficiently (without going through the inference kernel) computes a certificate that proves whether the number is prime or not. We then use the simplifier to turn the certificiate into a proof of primality. With this approach we avoid using the simplifier to compute the certificate which is slow (at least in Isabelle).

The architecture that @Jannis Limperg talked about where you can register tactics as unsafe resolution rules roughly corresponds to what are called solvers/loopers in Isabelle. Those are tactics which are called when auto cannot make progress any more using the simplifier or resolution rules. I am not exactly sure about the order of those procedures in Isabelle but simprocs are also tried at that level, probably before loopers and solvers. Of course, the architecture could just make the pattern optional and thus unify the concept of a simproc and a solver. However, there should be some smart way to handle precedence between those procedures then. Maybe try from most specific to most general pattern first and then try those procedures without patterns or even with integer preferences?

Anyway, I hope you will find this (hopefully mostly correct) explanation useful.

Jannis Limperg (Jan 06 2021 at 21:36):

Thank you very much! This matches what I thought simprocs were (which I did not convey very well during the Q&A). I think of them as 'custom simp rules' in analogy with the 'custom resolution rules' I described: both are arbitrary tactics which effectively construct a rule on the fly.

The exact order of things in Isabelle is something I should definitely look at again. My initial impression was that Isabelle's architecture is a bit cumbersome; it seemed like it may have developed as piecemeal extensions of the simplifier more so than a bigger search procedure which incorporates the simplifier. But it is equally possible that I just don't understand the reasons why the architecture is what it is.

Patrick Massot (Jan 06 2021 at 21:42):

Can't you at least find out who wrote the Isabelle version? Or at least the name of someone knowing a lot about it. Talking to such people would certainly be much more productive than reading the source code, at least in the beginning.

Jacques Carette (Jan 06 2021 at 21:47):

I saw Makarius was attending multiple of the talks today. He'd be my first lead into the Isabelle community.

Sebastien Gouezel (Jan 06 2021 at 21:54):

I guess blast and auto (at least the first versions) were probably written by Larry Paulson.

Sebastien Gouezel (Jan 06 2021 at 21:56):

A keyword is tableau-prover.

Sebastien Gouezel (Jan 06 2021 at 21:56):


Jeremy Avigad (Jan 06 2021 at 22:05):

Yes, the credit for auto goes to Larry. It might also be worth taking a look at Bohua Zhan's auto2 . There are some good ideas there, though to some extent he was re-discovering existing methods, so his terminology is idiosyncratic.

I think a contemporary update to auto should make use of key ideas from SMT solvers, most importantly, e-matching and the use of triggers to instantiate quantifiers.

Yury G. Kudryashov (Jan 06 2021 at 23:30):

BTW, one more related feature I missed while porting some proof from Isabelle: ability to say that lemma

constant f : nat  nat
lemma foo : f n = f 0 + n * 3 := sorry

applies only if n is not exactly 0. I had to turn this lemma into ∃ c, ∀ n, f n = c + n * 3.

Eric Wieser (Jan 06 2021 at 23:34):

That would be useful for a lemma like foo [subsingleton A] [has_one A] (a : A) : a = 1 too, which today can't be simp as it loops

Yakov Pechersky (Jan 06 2021 at 23:36):

What about bar [subsingleton A] [has_zero A] (a : A) : a = 0

Yakov Pechersky (Jan 06 2021 at 23:37):

Neither can really be simp

Eric Wieser (Jan 06 2021 at 23:45):

Yeah, I guess you can't really have both, but if you picked just one and used a "don't apply if syntactically equal" rule you might be ok

Yakov Pechersky (Jan 06 2021 at 23:46):

What do you do about fin 1?

Eric Wieser (Jan 07 2021 at 00:05):

Perhaps then a canonical_subsingleton which specifies a canonical syntactic value

Eric Wieser (Jan 07 2021 at 00:05):

Which would obviously be 0 for fin 1

Mario Carneiro (Jan 07 2021 at 06:25):

Eric Wieser said:

That would be useful for a lemma like foo [subsingleton A] [has_one A] (a : A) : a = 1 too, which today can't be simp as it loops

Actually it can't be a simp lemma because it has a variable on the lhs, and even if it wasn't syntactically disallowed it would trigger on literally everything

Gabriel Ebner (Jan 07 2021 at 09:31):

Eric Wieser said:

That would be useful for a lemma like foo [subsingleton A] [has_one A] (a : A) : a = 1 too, which today can't be simp as it loops

As Mario has already said, the reason this doesn't work is because a is a variable and Lean ignores such lemmas. However, it wouldn't loop:

variables {α : Type*} [has_zero α]
def a : α := 0
lemma foo : (a : α) = @a _ has_zero.zero := rfl
set_option trace.simplify.rewrite true
example : a = a + 0 := by simp [foo] -- rewrites using foo, but doesn't loop

(This is known as Floris' trick and we also use it in mathlib.)

Gabriel Ebner (Jan 07 2021 at 09:32):

The eta-expansion of the instance is only necessary so that the simplifier doesn't reject the lemma outright.

Eric Wieser (Jan 07 2021 at 11:48):

Do you have an example of where this is used in mathlib in mind?

Gabriel Ebner (Jan 07 2021 at 12:49):

Here is the unit test: https://github.com/leanprover-community/mathlib/blob/95c70870d2e77bea6f74b23e339734b860375877/test/lint_simp_comm.lean#L24
And here is how it used in mathlib:

Gabriel Ebner (Jan 07 2021 at 12:49):

/- We can simplify an application of filter where the decidability is inferred in "the wrong way" -/
@[simp] lemma filter_congr_decidable {α} (s : finset α) (p : α  Prop) (h : decidable_pred p)
  [decidable_pred p] : @filter α p h s = s.filter p :=
by congr

Eric Wieser (Jan 07 2021 at 12:53):


Jannis Limperg (Jan 07 2021 at 13:46):

Thanks you for all the references. To the degree that auto is similar to blast, I understand what's going on, but it seems like auto is significantly more popular, so I'd like to know where that comes from. I'll track down Makarius or Larry. E-matching and triggers are on the reading queue, and auto2 on the re-reading queue, for when my CPP talk is done.

The discussion about simp lemmas that require some syntactic condition on the term is very interesting. Seems like there are some compelling use cases for 'simprocs', so I'll look into how hard it would be to add something like this.

Lukas Stevens (Jan 07 2021 at 13:50):

In auto2, it is quite easy to make rules conditional to avoid loops.

Last updated: Dec 20 2023 at 11:08 UTC