15
$\begingroup$

I have only very limited learning experience with Isabelle and Coq. An issue while learning to use proof assistants is that forward proof is cumbersome or difficult. For example, the first time I saw Coq's apply tactic, I thought they used the word in the wrong/opposite way. When I apply modus ponens, I think in the forward direction: the premises therein hold, therefore the conclusion holds. When a rule is applied in Coq, it works backwards from sub-goals to their premises.

Similarly, when I prove the existence of something and have somehow constructed a witness, my mind usually thinks in the forward direction. That is, I just plug in the witness and verify if the goal holds or not. It's as if I have plugged in a value into a function or formula. However, both Coq and Isabelle seem to require existential introduction, and some additional ritual.

My understanding from reading is that the backward reasoning is needed by the inference systems (such as natural deduction). But it's still different from my usual of reasoning.

I noticed that I can assert subgoals and use auto tactics to make the proof look like a forward reasoning, although the automatic tactics are still not very transparent to me. Isabelle has some ways of explicitly instantiating things using OF and of. But it's more like writing a program than a proof and it's not as easy to understand or to get it right.

My question is:

Are there proof assistants nowadays that are more friendly to forward reasoning/proofs?

(I understand the necessity of backward proofs. But I just hope that there is also easier ways for forward proofs, and forward proofs can be done with the same ease as backward proofs.)

Improve this question
$\endgroup$
11
  • 2
    $\begingroup$ Would Isar count? It is still Isabelle and the rules of backward reasoning apply, but it has neat mechanisms (chaining, transitivity of binary relations etc.) that can hide it a bit. $\endgroup$
    – Wno-all
    Feb 11, 2022 at 3:28
  • 1
    $\begingroup$ @Wno-all I think frule is the closest. But I think it's now considered old feature in the manual. Isar kind of counts. I can organize things in a forward order and fill in the blanks with auto. But I once traced what the auto does. And what I thought was a direct application turned out to be a big detour. What I was looking for is an atomic, forward-style apply that can automatically "unify" things. Maybe I just need to learn Isar more. $\endgroup$
    – tinlyx
    Feb 11, 2022 at 4:06
  • 1
    $\begingroup$ In Lean, there are tactics like have and calc that allow you to do forward reasoning, but I also find that in Lean, backwards reasoning is in some sense "easier" and more elegant. In my admittedly limited experience, it seems like forwards reasoning requires one to know where they're going and how to get there, whereas backwards reasoning does some of the thinking for you. Backwards reasoning, basically, makes it feel more like a game rather than math. Sometimes, though, it mirrors my thinking: start from the goal and reason backwards to figure out what to do. $\endgroup$
    – march
    Feb 11, 2022 at 4:07
  • 1
    $\begingroup$ @march I totally agree. I also feel that forwarding reasoning works often when you vaguely know the answer. Backward proofs help you find the answer. But if I already know the answer roughly, as is the case sometimes in college calculus, then forward proofs seem direct and nice. Going back to first principles such as induction seems cumbersome to me. $\endgroup$
    – tinlyx
    Feb 11, 2022 at 4:12
  • 2
    $\begingroup$ The part "My understanding from reading is that the backward reasoning is needed by the inference systems." is definitely wrong, at least in usual provers. What is true is that backward reasoning helps you to leave more implicit things to be figured out by the assistant. Maybe it would help to add to your question an example proof that you find difficult to express. $\endgroup$
    – Patrick Massot
    Feb 11, 2022 at 12:16

3 Answers 3

Reset to default
11
$\begingroup$

Disclaimer: I'm a mathematician using Isabelle/ZF, with relatively little exposure to other assistants.

My first experience self-learning Isabelle was similar to yours. Using apply style proofs got me thinking things in a rather twisted way. When I realized this reversal got inside my head, I knew something was wrong.

Then I learned how to use the Isar dialect of Isabelle (it is available for all of its logics, not only ZF). Isar allows you to write “completely” forward proofs---I'm using quotes here because we actually use backward-reasoning (perhaps without noticing it) several times in the course of an informal proof.

Isar has several constructs that allow you to gather facts and combine them in order to obtain a linearly-readable proof. There's the already mentioned have that states a subgoal (and expects a proof for it), but some others are provided:

  • then, which is used to recall the last proved fact.
  • moreover...ultimately (one of my favorites) that allows you to accumulate facts to be used to prove the last assertion.
  • also...finally for “transitive“ reasoning (e.g. prove $a<b$, also $b\leq c$, also $c=d$ to finally conclude $a<d$).

I would believe that backward reasoning is at the heart of all proof assistants, and that's why more tools are readily available for this type of proof. Also, I feel that a downside of completely forward proofs (not just Isar) is that you need to have it completely ready in your mind / paper to formalize in that way, because I believe that exploration goes backwards most of the times, and for this writing backwards proofs is faster (but reading them... a pain in the neck, and much deeper!).

It took me while to first learn how to use Isar but I'm very happy with it. The Isabelle reference manual explains, albeit in a bit cryptic language for the newbie, how the switch from “backward” to “forward” and back happens amidst a proof.

Improve this answer
$\endgroup$
4
  • $\begingroup$ I might add that up to this point, my interest has been in formalizing proofs that I know that work. So, my prime objective is that the resulting text can be read by other humans (this is one of the design principles of Isar). I have not tried too hard to come up with new mathematics with the aid of the proof assistant. $\endgroup$
    – Pedro Sánchez Terraf
    Feb 11, 2022 at 16:44
  • $\begingroup$ For a comparison of a textbook proof (from the new Kunen's Set Theory) to the corresponding Isar script, you can check my slides of a recent presentation (starting on page 66 / slide 20). $\endgroup$
    – Pedro Sánchez Terraf
    Feb 11, 2022 at 16:46
  • $\begingroup$ I don't know why, but I'm having difficulty getting your slides (it's probably my inferior internet connection). But the Wayback machine has a copy of them, happily. $\endgroup$
    – Alex Nelson
    Feb 11, 2022 at 16:56
  • $\begingroup$ @AlexNelson the link will also lead you to my email address, you can contact me there if you have trouble downloading other stuff! $\endgroup$
    – Pedro Sánchez Terraf
    Feb 11, 2022 at 16:58
5
$\begingroup$

Most declarative-style provers use forward reasoning. Perhaps the most famous example is Mizar. For an introduction to Mizar, see:

Some provers have a "Mizar mode" or declarative-style input, for example:

Coq had a declarative proof style (called Czar) which has fallen into disuse.

Improve this answer
$\endgroup$
4
$\begingroup$

The Metamath proof explorer is well-suited to forward reasoning. It has many thousands of proofs in its library, mainly based on standard ZFC set theory, presented in forward style on the website.

Its companion mmj2 tool in particular works well for developing proofs in a forward style. See the Metamath home page for links to information about mmj2, or view the Introduction to Metamath and mmj2 on YouTube.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.