# Questions tagged [backward-proof]

Backward proofs are a type of proofs and logical reasoning that start from the goal and then use a set of inference rules backwards to obtain a set of sub-goals. The end goal is proved if all its subgoals (and their sub-subgoals etc.) are proved. Use this tag for proofs or reasoning processing in the backward direction.

4 questions
Filter by
Sorted by
Tagged with
1 vote
94 views

### How to apply constructor injectivity in the goal

Suppose I have a goal Goal forall m n, S m = S n -> m = n. intros m n H. 1 goal m, n : nat H : S m = S n ============================ m = n I know ...
291 views

### Proof assistants for forward reasoning?

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 ...
207 views

### How to prove Gauss summation of integers with proof assistants using forward reasoning?

As shown in an exercise here, we can prove the Gauss summation (that $\Sigma_{i=0..n}{i} = n \cdot (n + 1)/2$ ) in Isabelle/Isar using mathematical induction, as follows. ...
132 views

### Has there been any work on automated translation of tactic proofs to everyday language?

There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...