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.
8 questions
2
votes
2
answers
187
views
I'm implementing somewhat of a proof assistant from scratch and would like to know how the goal splitting algo works in proof mode
So when you're operating Coq, Lean, or any other standard proof assistant, there's a concept of a proof goal: the proposition you'd like to arrive at given some assumptions. The user then applies ...
0
votes
1
answer
162
views
Forward and backward reasoning completeness
Proof assistants can consist of both forward and backward tactics. I have several questions in regards to this below which I would be grateful if someone had answers to.
Is it correct that if only ...
- 101
3
votes
2
answers
138
views
1
vote
1
answer
267
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 ...
- 11
8
votes
1
answer
227
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::
...
- 81
8
votes
2
answers
284
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.
...
- 3,340
9
votes
0
answers
155
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 ...
- 383
16
votes
3
answers
396
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 ...
- 3,340