10.1 Introduction
Coq is an open proof environment, in the sense that the collection of proof strategies offered by the system can be extended by the user. This feature has two important advantages. First, the user can develop his/her own ad-hoc proof procedures, customizing the system for a particular domain of application. Second, the repetitive and tedious aspects of the proofs can be abstracted away implementing new tactics for dealing with them. For example, this may be useful when a theorem needs several lemmas which are all proven in a similar but not exactly the same way. Let us illustrate this with an example.Consider the problem of deciding the equality of two booleans. The theorem establishing that this is always possible is state by the following theorem:
Coq < Theorem decideBool : (x,y:bool){x=y}+{~x=y}.The proof proceeds by case analysis on both x and y. This yields four cases to solve. The cases x=y= true and x=y= false are immediate by the reflexivity of equality. The other two cases follow by discrimination. The following script describes the proof:
Coq < Destruct x.Coq < Destruct y.Coq < Left ; Reflexivity.Coq < Right; Discriminate.Coq < Destruct y.Coq < Right; Discriminate.Coq < Left ; Reflexivity.Now, consider the theorem stating the same property but for the following enumerated type:
Coq < Inductive Set Color := Blue:Color | White:Color | Red:Color.Coq < Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}.This theorem can be proven in a very similar way, reasoning by case analysis on c1 and c2. Once more, each of the (now six) cases is solved either by reflexivity or by discrimination:
Coq < Destruct c1. Coq < Destruct c2.Coq < Left ; Reflexivity.Coq < Right ; Discriminate.Coq < Right ; Discriminate.Coq < Destruct c2. Coq < Right ; Discriminate.Coq < Left ; Reflexivity.Coq < Right ; Discriminate.Coq < Destruct c2. Coq < Right ; Discriminate.Coq < Right ; Discriminate.Coq < Left ; Reflexivity.If we face the same theorem for an enumerated datatype corresponding to the days of the week, it would still follow a similar pattern. In general, the general pattern for proving the property (x,y:R){x=y}+{¬ x =y} for an enumerated type R proceeds as follow:
- Analyze the cases for x.
- For each of the sub-goals generated by the first step, analyze the cases for y.
- The remaining subgoals follow either by reflexivity or by discrimination.
Let us describe how this general proof procedure can be introduced in Coq.