# 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
91 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 ...
• 13
204 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. ...
• 2,034
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 ...
• 373