From 7d507ed043f9060ed46c0847a5e4b446646fb0b4 Mon Sep 17 00:00:00 2001 From: Marco Maida Date: Tue, 30 Jun 2020 17:13:12 +0200 Subject: [PATCH] guidelines: add a section about backward vs forward reasoning --- doc/guidelines.md | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/doc/guidelines.md b/doc/guidelines.md index 9f6922d..b993796 100644 --- a/doc/guidelines.md +++ b/doc/guidelines.md @@ -96,6 +96,43 @@ Guideline: do not name proof terms in type classes to prevent explicit dependenc - Document the tactics that you use in the [list of tactics](doc/tactics.md). For new users, it can be quite difficult to identify the right tactics to use. This list is intended to give novices a starting to point in the search for the "right" tools. +### Forward vs backward reasoning +Although the primary focus of Prosa is on the quality of the overall structure and the specifications, good proofs are short and readable. Since Coq tends to favor backward reasoning, try to adhere to it. Forward reasoning tends to be more verbose and to generate needlessly convoluted proof trees. To get an idea, read the following snippet: +``` +(* Let's say A->B->C->D *) + Variable A B C D : Prop. + Hypothesis AB : A->B. + Hypothesis BC : B->C. + Hypothesis CD : C->D. + + (* And we want to prove A->D *) + Lemma AD_backward: + A->D. + Proof. + intros. + apply CD. + apply BC. + now apply AB. + Qed. + + Lemma AD_forward: + A->D. + Proof. + intros. + (* hmm, I have C->D. If only I had C... *) + have I_need_C: C. + { (* hmm, I have B->C. If only I had B... *) + have I_need_B: B by apply AB. + feed BC. + apply I_need_B. + now apply BC. + } + feed CD. + apply I_need_C. + now apply CD. + Qed. + ``` + *To be continuedâ€¦ Merge requests welcome: please feel free to propose new advice and better guidelines.* -- GitLab