Library Batteries

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 (S^n<8)Case.
  • A simple tactic(al) 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.

Require Import String.
Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.

Example annotation_example:
  forall A B, B /\ A -> (B /\ A).
Proof.
  intros A B Hab.
  split.
  Case "Let's prove the left side of the conjunction: B".
    apply Hab.
  Case "Let's prove the right side of the conjunction: A".
    apply Hab.
Qed.


Inductive awesome_definition : Type :=
  | Constructor1 : awesome_definition
  | Constructor2 : awesome_definition.

Tactic Notation "awesome_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "1st Constructor"
  | Case_aux c "2nd Constructor" ].


Example induction_example:
  forall a, a = Constructor1 \/ a = Constructor2.
Proof.
  intros.
  awesome_cases (induction a) Case.
   Case "1st Constructor".
     left; auto.
   Case "2nd Constructor".
     right; auto.
Qed.


Tactic Notation "thus" tactic(H) := solve [H; auto].


Lemma test: forall n : nat, n <= n.
Proof.
  intro.
  thus auto.
Qed.


Tactic Notation "refl" := simpl; reflexivity.


Function neg_bool (b:bool) : bool :=
  match b with
   | true => false
   | false => true
  end.

Notation "'~~' b" := (neg_bool b) (at level 60).

Lemma testing_bool_negation:
  forall b, ~~b = ~~ (~~ (~~ b)).
Proof.
  induction b.
  Case "b is true".
    reflexivity.
  Case "b is false".
    reflexivity.
Qed.


Require Import List.
Set Implicit Arguments.
Fixpoint fold_left2 (A:Type) (B:Type) (C:Type)
                    (f : A -> B -> C -> A)
                    (accu: A)
                    (l1: list B) (l2: list C) : option A :=
  match l1, l2 with
      nil, nil => Some accu
    | cons a1 l1, cons a2 l2 => fold_left2 f (f accu a1 a2) l1 l2
    | _, _ => None
  end.



Require Import Coq.Sorting.Permutation.

Lemma member_of_permutation:
  forall l l' (e:Type),
        In e l ->
        Permutation l l' ->
        In e l'.
Proof.
  intros.
  apply Permutation_in with (l:=l); auto.
Qed.

Lemma symmetry_permut:
  forall (l l':list Type),
        Permutation l l' ->
        Permutation l' l.
Proof.
  intros.
  apply Permutation_sym; auto.
Qed.

Hint Resolve member_of_permutation symmetry_permut.

Lemma permut_w_nil:
  forall (X:Type) (l: list X),
        Permutation l (l ++ nil).
Proof.
  intros.
  assert (l ++ nil = l).
    apply app_nil_r.
  rewrite H.
  apply Permutation_refl.
Qed.

Hint Resolve permut_w_nil.


Lemma In_app_cons : forall A x (a : A) bs cs,
  In x ((a :: bs) ++ cs) <-> In x (bs ++ (a :: cs)).
Proof.
intros A x a bs cs ; split ; intro H ; apply in_or_app ;
  assert (H2 := in_app_or _ _ _ H) ; destruct H2.
   destruct H0.
    right ; constructor ; assumption.
    left ; assumption.
    do 2 right ; assumption.
    left ; right ; assumption.
   destruct H0.
   left ; constructor ; assumption.
   right ; assumption.
Qed.