Skip to main content

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.

Filter by
Sorted by
Tagged with
1 vote
1 answer

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 ...
smithers's user avatar
8 votes
2 answers

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. ...
tinlyx's user avatar
  • 2,034
9 votes
0 answers

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 ...
march's user avatar
  • 373
15 votes
3 answers

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 ...
tinlyx's user avatar
  • 2,034