Tactics

Stream: Lean Together 2021

[Lukas Stevens]

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 $t$ gives you a theorem $t \equiv t'$ where $t'$ is a simplified version of $t$.

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 $\text{is\_prime}\ c$ where $c$ 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]

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]

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]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

A keyword is tableau-prover.

[Sebastien Gouezel]

https://www.cl.cam.ac.uk/~lp15/papers/Isabelle/blast.pdf

[Jeremy Avigad]

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]

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]

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]

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

[Yakov Pechersky]

Neither can really be simp

[Eric Wieser]

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]

What do you do about fin 1?

[Eric Wieser]

Perhaps then a canonical_subsingleton which specifies a canonical syntactic value

[Eric Wieser]

Which would obviously be 0 for fin 1

[Mario Carneiro]

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]

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]

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

[Eric Wieser]

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

[Gabriel Ebner]

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:
https://github.com/leanprover-community/mathlib/blob/afbf47d5739ec69e6fdbb66fac2ce1d478f0ae64/src/data/finset/basic.lean#L1213

[Gabriel Ebner]

/- 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]

Thanks!

[Jannis Limperg]

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]

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