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. 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.)
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$
calcthat 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$