Questions tagged [forward-proof]

Forward proofs are the most common proof type. First, you state what you want to prove as a claim. Then, you begin to derive facts that you can use. As you go, write each key fact in a fact bank, which is just a place for you to collect known facts. At each step of the proof, consult the fact bank to see whether any of those facts are useful.

Filter by
Sorted by
Tagged with
1 vote
1 answer

How to write a low-level proof in Isar?

I would like to formalize ...
Gergely's user avatar
  • 299
1 vote
1 answer

How do I prove a record related lemma?

I'm new to coq. I would appreciate it if you could help me. Consider the following definition: Record person:= mk_person { p_name : t1; p_age : t2}. How to prove ...
B.Rolando's user avatar
8 votes
1 answer

Is there an elegant way of proving an equality A=B by going in both directions?

I would like to prove an equality by splitting it into a proof in each direction. Is there a more elegant style to start such a proof than this way:: ...
Mark Utting'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
  • 1,906
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
  • 1,906