proposal for `backwards_reasoning`

Stream: general

[Scott Morrison]

I'd like to propose an interactive partner for solve_by_elim. The idea is that it will be a tool for applying "backwards reasoning" (i.e. applying lemmas against the goal).

The idea is that we'll tag certain lemmas with an attribute, perhaps back, that are "safe" for backwards reasoning. A good example would be min_fac_dvd : ∀ (n : ℕ), min_fac n ∣ n. If you can unify that conclusion with the goal, you can't possibly be unhappy --- the only parameters are determined by unification, so no new goals can appear.

backwards_reasoning [x, y, z], will apply all lemmas marked with @[back] against the goal, as well as applying x, y, z. It will then apply solve_by_elim afterwards (so also applying all hypotheses). The key difference from just using solve_by_elim is that backwards_reasoning will succeed even if it doesn't close the goal, as long as it manages to apply at least one of the specified lemmas.

Here's an example of it in action:

[Scott Morrison]

import data.nat.prime
import tactic.backwards_reasoning

open nat

-- These are all lemmas which it is sufficiently safe to `apply`
-- that they can be automatically applied by backwards_reasoning.
attribute [back] succ_lt_succ
                 fact_pos dvd_fact
                 min_fac_prime min_fac_dvd

theorem infinitude_of_primes (N : ℕ) : ∃ p ≥ N, prime p :=
begin
  let M := fact N + 1,
  let p := min_fac M,
  have pp : prime p, sorry,
  sorry,

Now we replace that first sorry with backwards_reasoning, and the goal prime p is replaced with M \neq 1.
(If we replace backwards_reasoning with backwards_reasoning#, it prints out what it did: apply min_fac_prime.)

We then realise that a good way to proceed isapply ne_of_gt, so we modify the tactic to backwards_reasoning [ne_of_gt].
This succeeds, discharging the goal! If we replace the tactic with backwards_reasoning# [ne_of_gt], it prints what it did:
exact min_fac_prime (ne_of_gt (succ_lt_succ (fact_pos N))).

If you prefer you can then copy and paste that output, replacing entirely the call to backwards_reasoning.

[Scott Morrison]

(The rest of the proof of infinitude_of_primes can be proved in the same style.)

[Johan Commelin]

Looks really good @Scott Morrison

[Kenny Lau]

looks like inversion™ in Coq

[Scott Morrison]

Having this be really useful requires some judicious tagging of lemmas with back. My suggestion to start off just by having a smattering of attributes added in the tactics/backwards_reasoning.lean file itself, and to consider later moving them to the point of definition if it seems useful.

[Scott Morrison]

@Kenny Lau, can you point me to some examples? The documentation I found for inversion is not super helpful. :-(

[Kenny Lau]

you're looking at the wrong part

[Kenny Lau]

inversion ident

Let the type of ident in the local context be (I t), where I is a (co)inductive predicate. Then, inversion applied to ident derives for each possible constructor c i of (I t), all the necessary conditions that should hold for the instance (I t) to be proved by c i.

[Scott Morrison]

Glad you like it, @Johan Commelin. :-) I may wait until I hear something from @Simon Hudon or @Mario Carneiro before I bother cleaning it up for a PR.

[Scott Morrison]

But in any case I'll need some version of it before I'm willing to PR my work on limits in category theory. :-)

[Kenny Lau]

and in any case one should be noted that I do not know Coq at all.

[Scott Morrison]

Ok. It seems in any case inversion in Coq is quite different; whatever exactly it's doing, it's only doing one step, it's not something that chains together a whole sequence of applications.

[Mario Carneiro]

I don't see what inversion has to do with it - inversion is the equivalent of lean cases

[Mario Carneiro]

How does backwards_reasoning select the lemmas to apply? Does it just go through the whole list every time?

[Mario Carneiro]

also backwards_reasoning has way too many letters in it

[Scott Morrison]

Yes, it just runs through the whole list every time. I have not tested this at really big scale, but (a version of this) has been in my category theory library for a while, with maybe ~50 lemmas, and it never shows up in profiling. I think apply fails very fast.

[Mario Carneiro]

I think that if we used it in mathlib we would want to use it large scale, and then this would become a concern

[Scott Morrison]

also backwards_reasoning has way too many letters in it

I could rename it br, if you prefer. :-). How about just back?

[Mario Carneiro]

indeed I get the sense that it's not very useful unless it is marked everywhere

[Sebastien Gouezel]

If I understand correctly, you're creating a version of apply_rules on steroids, with additionally a set of default rules to be applied, right?

[Scott Morrison]

That sounds about right.

[Mario Carneiro]

I admit I don't understand apply_rules usage

[Scott Morrison]

(I have not used apply_rules, but I've seen the implementation.)

[Scott Morrison]

I guess we could have 'sub-attributes', to mark lemmas as relevant in certain domains.

[Scott Morrison]

The other solution is just to accept that backwards_reasoning is a slow tactic, and you're meant to switch to backwards_reasoning# once you've discovered the proof, and copy-paste the trace output.

[Scott Morrison]

(And just not worry about slow tactics, because we all have 30 cores, right?)

[Sebastien Gouezel]

If you want to go even further in this direction, let me mention the syntax of the Isabelle swiss army knife auto. Some rules in Isabelle are marked [intro], or [intro!] (the first one would be unsafe rules to be applied in backward reasoning, the second one for safe rules). In the same way there are simp rules. And all of this can be combined with

auto (simp: foo_simp, bar_simp, intro:  foo_intro, bar_intro)

which will apply eagerly the rules foo_intro or bar_intro and the rules marked [intro!] in the library (and also the [intro] ones if their assumptions can be checked right away), simplify everything using the simplifier with the additional rules foo_simp and bar_simp, and go over again. All this with some amount of backtracking that can be controlled. 90% of Isabelle proofs are autoproofs...

[Scott Morrison]

Thanks for this description, @Sebastien Gouezel!

[Scott Morrison]

My version of tidy in the category theory library has been using backwards_reasoning all along, and the main loop of tidy causes it to bounce back and forth between backwards_reasoning and simp. :-) Good to know I was re-inventing auto.

[Johan Commelin]

@Sebastien Gouezel And do those proofs remain auto, or do they get replaced by some unreadable proof that auto found? In other words: is this fast, and how does Isabelle solve the speed issues that we are hitting now in Lean?

[Scott Morrison]

(Of course, tidy does many other things in the loop, for better or worse.)

[Scott Morrison]

My private backwards_reasoning also makes the distinction analogous to [intro] vs [intro!], but I haven't reimplemented that completely in the new backwards_reasoning I've just been describing.

[Sebastien Gouezel]

@Sebastien Gouezel And do those proofs remain auto, or do they get replaced by some unreadable proof that auto found? In other words: is this fast, and how does Isabelle solve the speed issues that we are hitting now in Lean?

There are no speed issues in Isabelle. auto is extremely fast, but this is certainly related to the lack of dependent types and unification, which makes everything much simpler.

[Kevin Buzzard]

Anyone who watched @Scott Morrison 's video of his Adelaide talk will have seen a pretty stunning application of backwards_reasoning. It was very well-delivered too. He was formalising proof of infinitely many primes and getting his hands dirty. "Oh we'll just skip this", "oh we'll come back to this later", "Oh Ok so now we've proved there are infinitely many primes modulo 5 sorries which clearly are going to be the hard work", "oh look, globally replacing sorry with backwards_reasoning closes the goal!"

[Mario Carneiro]

what do you mean lack of unification?

[Scott Morrison]

Okay, that demo in Adelaide was a bit misleading. Way too many things were marked @[back], that in practice we couldn't avoid.

[Scott Morrison]

It's going to be a little while before backwards_reasoning or friends really does what it appeared to do there...

[Kevin Buzzard]

That doesn't matter. The point was made.

[Kevin Buzzard]

I will be doing the same thing in Sheffield; showing the audience how proving $(x+y)^3=x^3+3x^2y+...$ is really hard from the axioms and then solving it using automation

[Kevin Buzzard]

Mathematicians need to understand that doing simple maths might be simple in Lean.

[Kevin Buzzard]

The more we say it's true and the more we work on cases where it is not true (like $A\cong B\to Spec(A)\cong Spec(B)$) the more it will become true

[Kevin Buzzard]

If it's easy in maths, we need to try and make it easy in Lean.

[Patrick Massot]

I also liked the backward reasoning demo in Adelaide, but I struggled with the name. Of course I'm not a native English speaker but, to me, backward_reasoning sounds like we are doing something wrong (like using P -> Q to prove P from Q).

[Johan Commelin]

How far are we from this turning into a PR?

[Scott Morrison]

Close.

[Scott Morrison]

But I have grumpy coauthors back in the real world. :-)

[Simon Hudon]

Hi @Scott Morrison! Sorry I got distracted by this sleeping thing. This looks really cool! I think we can do things much faster than going through the whole list of lemmas and we may not hit the performance wall that we did with simp.

A bit like simp, we can index back lemmas using the head symbol of the rhs of its pi type. Then, the number of candidate at each step should be much smaller. I'd have to think some more about further optimizations but I think Isabelle suggests it must be possible to do things really fast

[Scott Morrison]

Hi @Simon Hudon, indexing sounds great. How hard do you think this would be? I'm not confident I could implement it efficiently, but especially if you can give me a pointer to something similar I can give it a try. If I pushed a branch, I'd be very happy if you wanted to look at doing this.

[Scott Morrison]

I also want to implement two attributes, analogous to [intro] and [intro!] in Isabelle, for lemmas that it's always safe to apply, vs lemmas that should only be applied if their hypotheses can immediately be solved. I already had this in my original implementation of back, but it's not in the current one. Perhaps I should do this first, and then we can think about indexing?

[Simon Hudon]

Sure, no problems. You can also have a look at the user attribute for extensionality if you want to try it before I get into it

[Simon Hudon]

Sure

[Simon Hudon]

You can do one intro attribute and use ! as a parameter

[Scott Morrison]

@Simon Hudon , can you point me to examples of using a token like ! as a parameter to an attribute?

[Mario Carneiro]

intro! is an attribute

[Mario Carneiro]

but I think the parsing for that is in core

[Mario Carneiro]

The parsing for an attribute is just a regular lean.parser monad thing, so you can use tk "!"? to get a possible ! token

[Mario Carneiro]

If you want an example of an attribute with arguments, look at to_additive_attr in algebra.group. You specify the type of the parsed result in one of the optional arguments to user_attribute, and you give the parser itself in the parser := field

[Scott Morrison]

Thanks. I've just made a PR at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/subject/.23410.20backwards.20reasoning, so perhaps anything further on this thread can go there.