(** * SfLib: Software Foundations Library *)

(** Here we collect together a few useful definitions from earlier
    chapters that are not provided as part of the Coq standard
    library.  Later chapters will [Import] or [Export] just this file,
    instead of cluttering the top-level environment with all the
    examples and false starts in those files. *)

Definition admit {T: Type} : T.  Admitted.

Tactic Notation "solve_by_inversion_step" tactic(t) :=
  match goal with
  | H : _ |- _ => solve [ inversion H; subst; t ]
  end
  || fail "because the goal is not solvable by inversion.".

Tactic Notation "solve" "by" "inversion" "1" :=
  solve_by_inversion_step idtac.
Tactic Notation "solve" "by" "inversion" "2" :=
  solve_by_inversion_step (solve by inversion 1).
Tactic Notation "solve" "by" "inversion" "3" :=
  solve_by_inversion_step (solve by inversion 2).
Tactic Notation "solve" "by" "inversion" :=
  solve by inversion 1.

(** $Date: 2016-02-17 17:39:13 -0500 (Wed, 17 Feb 2016) $ *)