ExtLib.Tactics.Cases

Require Import ExtLib.Tactics.Consider.

Set Implicit Arguments.
Set Strict Implicit.

Ltac forward' dst sol :=
  let check X :=
    match X with
      | match _ with _ => _ end => fail 1
      | if _ then _ else _ => fail 1
      | _ => idtac
    end
  in
  let go X :=
    first [ (dst X; try solve [ sol ]); [ intros ]
          | dst X; solve [ sol ] ]
  in
  repeat match goal with
           | [ H : context [ match ?X with _ => _ end ] |- _ ] =>
             go X
           | [ H : context [ if ?X then _ else _ ] |- _ ] =>
             go X
           | [ |- context [ match ?X with _ => _ end ] ] =>
             go X
           | [ |- context [ if ?X then _ else _ ] ] =>
             go X
         end.

Ltac forward :=
  forward'
    ltac:(fun x => consider x; intros)
    ltac:(intuition congruence).

Ltac forward_unsafe' dst sol :=
  let check X :=
    match X with
      | match _ with _ => _ end => fail 1
      | if _ then _ else _ => fail 1
      | _ => idtac
    end
  in
  let go X :=
      dst X; try solve [ sol ]
  in
  repeat match goal with
           | [ H : context [ match ?X with _ => _ end ] |- _ ] =>
             go X
           | [ H : context [ if ?X then _ else _ ] |- _ ] =>
             go X
           | [ |- context [ match ?X with _ => _ end ] ] =>
             go X
           | [ |- context [ if ?X then _ else _ ] ] =>
             go X
         end.

Ltac forward_unsafe :=
  forward_unsafe'
    ltac:(fun x => consider x; intros)
    ltac:(intuition congruence).

Ltac change_rewrite H :=
  match type of H with
    | ?X = _ =>
      match goal with
        | |- context [ ?Y ] =>
          change Y with X ; rewrite H
      end
  end.

Ltac change_rewrite_in H H' :=
  match type of H with
    | ?X = _ =>
      match type of H' with
        | context [ ?Y ] =>
          change Y with X in H' ; rewrite H in H'
      end
  end.

Tactic Notation "change_rewrite" hyp(H) := (change_rewrite H).
Tactic Notation "change_rewrite" hyp(H) "in" hyp(H') := (change_rewrite_in H H').

Ltac rewrite_all_goal :=
  repeat match goal with
           | [ H : _ |- _ ] =>
             progress (erewrite H by eauto with typeclass_instances)
         end.

Ltac rewrite_all_in H' :=
  repeat match goal with
           | [ H : _ |- _ ] =>
             progress (erewrite H in H' by eauto with typeclass_instances)
         end.

Ltac rewrite_all_star :=
  repeat match goal with
           | [ H : _ |- _ ] =>
             progress (erewrite H in * by eauto with typeclass_instances)
         end.

(*
Ltac rewrite_all := rewrite_all_goal.
*)