Batteries is a general purpose library for Coq development. It is essentially aimed at improving Coq Proof scripts' readability and maintainability. As of now, it features the following:

• An easy way to annotate/comment proof goals. This is achieved by using the Case command. For instance,
  • Case "Goal 1 of 5"
  will allow to seamlessly to include a text information in your proof script, but will also put the given string on top of your hypotheses. Of course, there is also 'SCase string' for subgoals, 'SSCase string' for subsubgoals, and so forth, until a depth of 8. Moreover, you can leverage this by indenting your code according to your use of Case.
• A simple tactic(al) - thus - that fails if it doesn't solve the current goal. This is useful for maintaining your scripts. If you keep the rationale of always using this tactic to conclude your goals, whenever updating your Coq scripts, you will know exactly where it breaks.

Annotating your Proofs

The following definitions will allow us to annotate our proof scripts. These were taken from Software Foundations.

For instance, we can now annotate our proofs as the following:

The above example was trivial. Let's see now something more interesting. Consider the following definition:

We will now associate annotations to the goals generated by some given tactic. It is also possible to specify whether we are in 'Case's, 'SCase's, etc

Generally speaking, this will serve the purpose of automatically associating the given strings foreach constructors of some given inductive definition. With this tactical defined, we can use it as follows:

And just like that, we get our goals already annotated at the top of our hypotheses. Moreover, the strings given on the '(S)Case's must be consistent with a possible annotation already present.

A Few Tactics

A Conclude-the-current-goal-or-Fail Tactic

The above increases proof scripts' readability. Here, we want to help the mantainability of always evolving proof scripts. The idea is simple, following the rationale of always concluding (sub)goals with the last tactic prefixed by the tactical 'thus', and making it fail if the (sub)goal is not discharged by this tactic. This makes possible to exactly detect the point where the proof script breakes when updating something. I've first seen this kind of approach in ssreflect.

The above tactical fails if it doesn't solve the current goal. Here it is in action.

Reflexivity-like Tactic

Our own reflexivity tactic. Nothing fancy here, just improving automation a tiny bit.

Type-fast-Functional-induction Tactic

Well I do functional induction quite a lot, and I would rather write something that doesn't take that long to type :-) TODO: FIX the following: f needs to be a list

Assert-False-and-solve Tactic

A tactic to make proofs by being able to prove False faster

Some Functions and Facts on Lists

Coq standard library doesn't include a definition for Fold_left2. We shall use the following one whenever needed.

For instance, we can use this definition for computations as follows: Definition listAcc := (nil:list nat). Definition listB := 1::2::3::nil. Definition listC := 3::2::1::nil. Eval compute in fold_left2 (fun a b c => (b+c)::a) listAcc listB listC. Eval compute in fold_left2 (fun a b c => (b+c)::a) listAcc listB (0 :: listC). A fact about list that may become handy. Got it from a thread in the Coq mailing list.

On Naturals and Strings!

implementation of: (n <= m) ? true : false

Let's make it reflect into Prop!

A notion of Identifier

Let us start by defining a notion of identifier. It will be a simple constructor that takes a string.

For instance, we can define some identifiers in the following manner:

We will a function to determine whether to identifiers are equal. Since our identifiers are simple constructions that take a string, we simply need to check whether the given identifiers have identical strings.

For the sake of readability, we define a notation to our comparison over identifiers operator close to what one would see in a standard programming language. We shall use it seamlessly in the remaining of this development.

We can right now see our first proof. Let's start with something simple: decidability on identifiers.

Moreover, we shall prove an obvious, yet very useful lemma about our ident equality operator: it is symmetric.

Another useful definition is the not-equal operator. Simply defined as follows:

As you can guess, comparison operators like beq_ident and bneq_ident will be useful for other types of structures that we will define at a more advanced stage. Of course, one would prefer to maintain the same notation for these other comparison operators. Unfortunately for us, Coq will not be always able to infer to which actual definition the notation is referring to. As such, we will need to define scopes. This is the purpose of the following two lines. Their real significance will become clear with examples.

Warming up: Some Simple Proof Examples

So far, we just defined the notion of identifiers, let's see what can we prove about them.

Generic comparison function over lists.

Simple ArrayList type