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

6 questions
Filter by
Sorted by
Tagged with
1 vote
64 views

### How to write a low-level proof in Isar?

I would like to formalize ...
• 299
1 vote
131 views

### 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 ...
176 views

### 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:: ...
192 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. ...
• 1,906
129 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