LibDefaultSimp.v

(* This file is distributed under the terms of the MIT License, also
   known as the X11 Licence.  A copy of this license is in the README
   file that accompanied the original distribution of this file.

   Based on code written by:
     Brian Aydemir *)

(** A library that provides tactics for "simplifying" goals using
    a combination of common proof steps. *)

Require Import Coq.Program.Equality.
Require Import Coq.Program.Tactics.
Require Import Coq.omega.Omega.


(* *********************************************************************** *)
(** * Variants on standard tactics *)

(** [n_intros n] performs [n] introductions. *)

Ltac n_intros n :=
  match n with
    | O => idtac
    | S ?n' => intros ?; n_intros n'
  end.

(** [safe_f_equal] is a variant of [f_equal] that progresses only if
    it can be "proved" that the function is injective.  An ad hoc
    method is used to determine whether the function is injective.
    Unlike [f_equal], [safe_f_equal] only works on functions up to
    some particular arity; see the implementation.

    Implementation note: Our test for injectivity of a function uses
    the [injection] tactic.  Specifically, if [injection] generates a
    new equality, then we assume that the function is injective.  We
    play tricks with the [try] and [fail] tactics so that we can
    "temporarily" introduce a subgoal that lets us test the function
    using [injection]. *)

Ltac safe_f_equal :=
  let rec inj_test :=
        let H := fresh "H" in intros H; injection H;
        let J := fresh "J" in intros J;
        match goal with
          | _ : ?x = ?y, _ : ?x = ?y |- _ => fail 1
          | _ => idtac
        end
  in
  let core n t1 :=
    first [ first [ t1; [ n_intros n; inj_test | ]; fail 1
                  | fail 2 ]
          | f_equal
          | fail 1 ]
  in
  match goal with
    | |- ?f _ _ _ _ _ _ _ _ = ?f _ _ _ _ _ _ _ _ =>
      core 16 ltac:(assert (forall x1 x2 x3 x4 x5 x6 x7 x8 y1 y2 y3 y4 y5 y6 y7 y8, f x1 x2 x3 x4 x5 x6 x7 x8 = f y1 y2 y3 y4 y5 y6 y7 y8 -> False))
    | |- ?f _ _ _ _ _ _ _ = ?f _ _ _ _ _ _ _ =>
      core 14 ltac:(assert (forall x1 x2 x3 x4 x5 x6 x7 y1 y2 y3 y4 y5 y6 y7, f x1 x2 x3 x4 x5 x6 x7 = f y1 y2 y3 y4 y5 y6 y7 -> False))
    | |- ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ =>
      core 12 ltac:(assert (forall x1 x2 x3 x4 x5 x6 y1 y2 y3 y4 y5 y6, f x1 x2 x3 x4 x5 x6 = f y1 y2 y3 y4 y5 y6 -> False))
    | |- ?f _ _ _ _ _ = ?f _ _ _ _ _ =>
      core 10 ltac:(assert (forall x1 x2 x3 x4 x5 y1 y2 y3 y4 y5, f x1 x2 x3 x4 x5 = f y1 y2 y3 y4 y5 -> False))
    | |- ?f _ _ _ _ = ?f _ _ _ _ =>
      core 8 ltac:(assert (forall x1 x2 x3 x4 y1 y2 y3 y4, f x1 x2 x3 x4 = f y1 y2 y3 y4 -> False))
    | |- ?f _ _ _ = ?f _ _ _ =>
      core 6 ltac:(assert (forall x1 x2 x3 y1 y2 y3, f x1 x2 x3 = f y1 y2 y3 -> False))
    | |- ?f _ _ = ?f _ _ =>
      core 4 ltac:(assert (forall x1 x2 y1 y2, f x1 x2 = f y1 y2 -> False))
    | |- ?f _ = ?f _ =>
      core 2 ltac:(assert (forall x1 y1, f x1 = f y1 -> False))
  end.


(* *********************************************************************** *)
(** * Tactics for inversion *)

(** [find_easy_inversion] finds a non-equality hypothesis that
    when inverted (using [inversion]) leads to zero or one subgoals. *)

Ltac find_easy_inversion :=
  let is_ok H :=
    (subst;
     match goal with
       | _ : _ = _ |- _ => fail 1
       | _ => idtac
     end;
     clear H)
  in
  match goal with
    | H : _ |- _ =>
      match type of H with
        | @eq _ _ _ => fail 1
        | _ => (inversion H; [ idtac ]; is_ok H) || (inversion H; fail)
      end
  end.

(** [destruct_exists] finds an element of a dependent product type anywhere
    in the goal and destructs it. *)

Ltac destruct_exists :=
  let rec main x :=
    match type of x with
      | ex _ => destruct x
      | sig _ => destruct x
      | sigT _ => destruct x
    end
  in
  match goal with
    | |- context [?x] => main x
    | H : _ |- _ => main H
    | _ : context [?x] |- _ => main x
  end.

(** [destruct_sum] finds an element of a disjoint sum anywhere in the
    goal and destructs it, i.e., performs a case analysis. *)

Ltac destruct_sum :=
  let rec main x :=
    match type of x with
      | or _ _ => destruct x
      | sumbool _ _ => destruct x
      | sumor _ _ => destruct x
    end
  in
  match goal with
    | |- context [?x] => main x
    | H : _ |- _ => main H
    | _ : context [?x] |- _ => main x
  end.

(** [find_injection] finds an equality in the current context and
    supplies it to the [injection] tactic.  It succeeds only if there
    is an equality in the context such that [injection] generates
    non-trivial equalities.  On success, the equality is removed from
    the context, and the equalities generated by [injection] are left
    in the goal. *)

Ltac find_injection :=
  match goal with
    | H : _ = _ |- _ =>
      let J := fresh in
      injection H;
      intros J;
      match goal with
        | H : ?x = ?y, J : ?x = ?y |- _ => fail 1
        | _ => idtac
      end;
      revert J; clear H
  end.


(* *********************************************************************** *)
(** * Putting it all together *)

(** [default_step] is a default collection of "steps" intended to be
    applied to the goal over and over again.  None of the steps should
    lead to multiple subgoals.

    The ordering of the steps is important!  While no step is unsafe
    (in the sense that it might produce an unprovable goal state),
    whether one step is applied before another can affect whether some
    other step applies in the future.  For example, [auto] is
    sensitive to the exact form of the goal, hence why it is tried
    first.

    Implementation note: The "[auto]" step is pulled out into a tactic
    named [default_auto], which can be redefined if different behavior
    is desired.  We do similarly for the [autorewrite]. *)

Ltac default_auto        := auto; tauto.
Ltac default_autorewrite := fail.

Ltac default_step :=
  first
    [ solve [default_auto]
    | progress intros
    | progress simpl in *
    | progress subst*
    | find_injection
    | discriminates
    | find_easy_inversion
    | destruct_exists
    | progress default_autorewrite
    | solve [let H := fresh in assert (H : False) by omega; elim H]
    ].

(** [default_case_split] is similar to [default_step], except that the
    steps it tries lead to case splits. *)

Ltac default_case_split :=
  first
    [ progress destruct_sum
    | progress safe_f_equal
    ].

(** We now combine everything above. *)

Ltac default_steps :=
  repeat default_step.

Ltac default_case_splits :=
  repeat default_case_split.

Ltac default_simp :=
  repeat first [default_step | default_case_split].