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