Library LibDefaultSimp


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 (∀ 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 (∀ 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 (∀ 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 (∀ 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 (∀ 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 (∀ x1 x2 x3 y1 y2 y3, f x1 x2 x3 = f y1 y2 y3 → False))
    | |- ?f _ _ = ?f _ _ ⇒
      core 4 ltac:(assert (∀ x1 x2 y1 y2, f x1 x2 = f y1 y2 → False))
    | |- ?f _ = ?f _ ⇒
      core 2 ltac:(assert (∀ 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].