(* ###################################################################### *)
(** * Naming Cases *)

(** The fact that there is no explicit command for moving from
    one branch of a case analysis to the next can make proof scripts
    rather hard to read.  In larger proofs, with nested case analyses,
    it can even become hard to stay oriented when you're sitting with
    Coq and stepping through the proof.  (Imagine trying to remember
    that the first five subgoals belong to the inner case analysis and
    the remaining seven cases are what remains of the outer one...)
    Disciplined use of indentation and comments can help, but a better
    way is to use the [Case] tactic.

    [Case] is not built into Coq: we need to define it ourselves.
    There is no need to understand how it works -- just skip over the
    definition to the example that follows.  (It uses some facilities
    of Coq that we have not discussed -- the string library (just for
    the concrete syntax of quoted strings) and the [Ltac] command,
    which allows us to declare custom tactics.  Kudos to Aaron
    Bohannon for this nice hack!) *)

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | e : _ |- _ => try move x after e
  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" ].

Ltac Case name := Case_aux Case name.
Ltac SCase name := Case_aux SCase name.
Ltac SSCase name := Case_aux SSCase name.
Ltac SSSCase name := Case_aux SSSCase name.
Ltac SSSSCase name := Case_aux SSSSCase name.
Ltac SSSSSCase name := Case_aux SSSSSCase name.
Ltac SSSSSSCase name := Case_aux SSSSSSCase name.
Ltac SSSSSSSCase name := Case_aux SSSSSSSCase name.

(* Here's an example of how [Case] is used.  Step through the
   following proof and observe how the context changes. 

Theorem andb_true_elim1 : forall b c : bool,
  andb b c = true -> b = true.
Proof.
  intros b c e.
  destruct b.
  Case "b = true".
    reflexivity.
  Case "b = false".
    rewrite <- e. reflexivity.  
Qed.
*)

(** [Case] does something very trivial: It simply adds a string
    that we choose (tagged with the identifier "Case") to the context
    for the current goal.  When subgoals are generated, this string is
    carried over into their contexts.  When the last of these subgoals
    is finally proved and the next top-level goal (a sibling of the
    current one) becomes active, this string will no longer appear in
    the context and we will be able to see that the case where we
    introduced it is complete.  Also, as a sanity check, if we try to
    execute a new [Case] tactic while the string left by the previous
    one is still in the context, we get a nice clear error message.

    For nested case analyses (i.e., when we want to use a [destruct]
    to solve a goal that has itself been generated by a [destruct]),
    there is an [SCase] ("subcase") tactic. *)