More fine-grained util tactic files

Also, add [split_and]

6 files changed, 258 insertions, 0 deletions

diff --git a/src/Util/Tactics/BreakMatch.v b/src/Util/Tactics/BreakMatch.v
new file mode 100644
index 000000000..5ad882c6f
--- /dev/null
+++ b/src/Util/Tactics/BreakMatch.v
@@ -0,0 +1,116 @@
+Require Export Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Tactics.Head.
+
+(** destruct discriminees of [match]es in the goal *)
+(* Prioritize breaking apart things in the context, then things which
+   don't need equations, then simple matches (which can be displayed
+   as [if]s), and finally matches in general. *)
+Ltac set_match_refl v' only_when :=
+  lazymatch goal with
+  | [ |- context G[match ?e with _ => _ end eq_refl] ]
+    => only_when e;
+       let T := fresh in
+       evar (T : Type); evar (v' : T);
+       subst T;
+       let vv := (eval cbv delta [v'] in v') in
+       let G' := context G[vv] in
+       let G''' := context G[v'] in
+       lazymatch goal with |- ?G'' => unify G' G'' end;
+       change G'''
+  end.
+Ltac set_match_refl_hyp v' only_when :=
+  lazymatch goal with
+  | [ H : context G[match ?e with _ => _ end eq_refl] |- _ ]
+    => only_when e;
+       let T := fresh in
+       evar (T : Type); evar (v' : T);
+       subst T;
+       let vv := (eval cbv delta [v'] in v') in
+       let G' := context G[vv] in
+       let G''' := context G[v'] in
+       let G'' := type of H in
+       unify G' G'';
+       change G''' in H
+  end.
+Ltac destruct_by_existing_equation match_refl_hyp :=
+  let v := (eval cbv delta [match_refl_hyp] in match_refl_hyp) in
+  lazymatch v with
+  | match ?e with _ => _ end (@eq_refl ?T ?e)
+    => let H := fresh in
+       let e' := fresh in
+       pose e as e';
+       change e with e' in (value of match_refl_hyp) at 1;
+       first [ pose (@eq_refl T e : e = e') as H;
+               change (@eq_refl T e) with H in (value of match_refl_hyp);
+               clearbody H e'
+             | pose (@eq_refl T e : e' = e) as H;
+               change (@eq_refl T e) with H in (value of match_refl_hyp);
+               clearbody H e' ];
+       destruct e'; subst match_refl_hyp
+  end.
+Ltac destruct_rewrite_sumbool e :=
+  let H := fresh in
+  destruct e as [H|H];
+  try lazymatch type of H with
+      | ?LHS = ?RHS
+        => rewrite ?H; rewrite ?H in *;
+           repeat match goal with
+                  | [ |- context G[LHS] ]
+                    => let LHS' := fresh in
+                       pose LHS as LHS';
+                       let G' := context G[LHS'] in
+                       change G';
+                       replace LHS' with RHS by (subst LHS'; symmetry; apply H);
+                       subst LHS'
+                  end
+      end.
+Ltac break_match_step only_when :=
+  match goal with
+  | [ |- appcontext[match ?e with _ => _ end] ]
+    => only_when e; is_var e; destruct e
+  | [ |- appcontext[match ?e with _ => _ end] ]
+    => only_when e;
+       match type of e with
+       | sumbool _ _ => destruct_rewrite_sumbool e
+       end
+  | [ |- appcontext[if ?e then _ else _] ]
+    => only_when e; destruct e eqn:?
+  | [ |- appcontext[match ?e with _ => _ end] ]
+    => only_when e; destruct e eqn:?
+  | _ => let v := fresh in set_match_refl v only_when; destruct_by_existing_equation v
+  end.
+Ltac break_match_hyps_step only_when :=
+  match goal with
+  | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+    => only_when e; is_var e; destruct e
+  | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+    => only_when e;
+       match type of e with
+       | sumbool _ _ => destruct_rewrite_sumbool e
+       end
+  | [ H : appcontext[if ?e then _ else _] |- _ ]
+    => only_when e; destruct e eqn:?
+  | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+    => only_when e; destruct e eqn:?
+  | _ => let v := fresh in set_match_refl_hyp v only_when; destruct_by_existing_equation v
+  end.
+Ltac break_match := repeat break_match_step ltac:(fun _ => idtac).
+Ltac break_match_hyps := repeat break_match_hyps_step ltac:(fun _ => idtac).
+Ltac break_match_when_head_step T :=
+  break_match_step
+    ltac:(fun e => let T' := type of e in
+                   let T' := head T' in
+                   constr_eq T T').
+Ltac break_match_hyps_when_head_step T :=
+  break_match_hyps_step
+    ltac:(fun e => let T' := type of e in
+                   let T' := head T' in
+                   constr_eq T T').
+Ltac break_match_when_head T := repeat break_match_when_head_step T.
+Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T.
+Ltac break_innermost_match_step :=
+  break_match_step ltac:(fun v => lazymatch v with
+                                  | appcontext[match _ with _ => _ end] => fail
+                                  | _ => idtac
+                                  end).
+Ltac break_innermost_match := repeat break_innermost_match_step.
diff --git a/src/Util/Tactics/DestructHead.v b/src/Util/Tactics/DestructHead.v
new file mode 100644
index 000000000..5620a72c9
--- /dev/null
+++ b/src/Util/Tactics/DestructHead.v
@@ -0,0 +1,29 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.DestructHyps.
+
+Ltac destruct_head_matcher T HT :=
+  match head HT with
+  | T => idtac
+  end.
+Ltac destruct_head T := destruct_all_matches ltac:(destruct_head_matcher T).
+Ltac destruct_one_head T := destruct_one_match ltac:(destruct_head_matcher T).
+Ltac destruct_head' T := destruct_all_matches' ltac:(destruct_head_matcher T).
+
+Ltac inversion_head T := inversion_all_matches ltac:(destruct_head_matcher T).
+Ltac inversion_one_head T := inversion_one_match ltac:(destruct_head_matcher T).
+Ltac inversion_head' T := inversion_all_matches' ltac:(destruct_head_matcher T).
+
+
+Ltac head_hnf_matcher T HT :=
+  match head_hnf HT with
+  | T => idtac
+  end.
+Ltac destruct_head_hnf T := destruct_all_matches ltac:(head_hnf_matcher T).
+Ltac destruct_one_head_hnf T := destruct_one_match ltac:(head_hnf_matcher T).
+Ltac destruct_head_hnf' T := destruct_all_matches' ltac:(head_hnf_matcher T).
+
+Ltac inversion_head_hnf T := inversion_all_matches ltac:(head_hnf_matcher T).
+Ltac inversion_one_head_hnf T := inversion_one_match ltac:(head_hnf_matcher T).
+Ltac inversion_head_hnf' T := inversion_all_matches' ltac:(head_hnf_matcher T).
diff --git a/src/Util/Tactics/DestructHyps.v b/src/Util/Tactics/DestructHyps.v
new file mode 100644
index 000000000..8ab6215c2
--- /dev/null
+++ b/src/Util/Tactics/DestructHyps.v
@@ -0,0 +1,48 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+(** given a [matcher] that succeeds on some hypotheses and fails on
+    others, destruct any matching hypotheses, and then execute [tac]
+    after each [destruct].
+
+    The [tac] part exists so that you can, e.g., [simpl in *], to
+    speed things up. *)
+Ltac do_one_match_then matcher do_tac tac :=
+  idtac;
+  match goal with
+  | [ H : ?T |- _ ]
+    => matcher T; do_tac H;
+       try match type of H with
+           | T => clear H
+           end;
+       tac
+  end.
+
+Ltac do_all_matches_then matcher do_tac tac :=
+  repeat do_one_match_then matcher do_tac tac.
+
+Ltac destruct_all_matches_then matcher tac :=
+  do_all_matches_then matcher ltac:(fun H => destruct H) tac.
+Ltac destruct_one_match_then matcher tac :=
+  do_one_match_then matcher ltac:(fun H => destruct H) tac.
+
+Ltac inversion_all_matches_then matcher tac :=
+  do_all_matches_then matcher ltac:(fun H => inversion H; subst) tac.
+Ltac inversion_one_match_then matcher tac :=
+  do_one_match_then matcher ltac:(fun H => inversion H; subst) tac.
+
+Ltac destruct_all_matches matcher :=
+  destruct_all_matches_then matcher ltac:( simpl in * ).
+Ltac destruct_one_match matcher := destruct_one_match_then matcher ltac:( simpl in * ).
+Ltac destruct_all_matches' matcher := destruct_all_matches_then matcher idtac.
+
+Ltac inversion_all_matches matcher := inversion_all_matches_then matcher ltac:( simpl in * ).
+Ltac inversion_one_match matcher := inversion_one_match_then matcher ltac:( simpl in * ).
+Ltac inversion_all_matches' matcher := inversion_all_matches_then matcher idtac.
+
+(* matches anything whose type has a [T] in it *)
+Ltac destruct_type_matcher T HT :=
+  match HT with
+  | context[T] => idtac
+  end.
+Ltac destruct_type T := destruct_all_matches ltac:(destruct_type_matcher T).
+Ltac destruct_type' T := destruct_all_matches' ltac:(destruct_type_matcher T).
diff --git a/src/Util/Tactics/Head.v b/src/Util/Tactics/Head.v
new file mode 100644
index 000000000..fa7a301d6
--- /dev/null
+++ b/src/Util/Tactics/Head.v
@@ -0,0 +1,10 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+(** find the head of the given expression *)
+Ltac head expr :=
+  match expr with
+  | ?f _ => head f
+  | _ => expr
+  end.
+
+Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'.
diff --git a/src/Util/Tactics/SpecializeBy.v b/src/Util/Tactics/SpecializeBy.v
new file mode 100644
index 000000000..72cf5d52f
--- /dev/null
+++ b/src/Util/Tactics/SpecializeBy.v
@@ -0,0 +1,33 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+Ltac transparent_specialize_one H arg :=
+  first [ let test := eval unfold H in H in idtac;
+          let H' := fresh in rename H into H'; pose (H' arg) as H; subst H'
+         | specialize (H arg) ].
+
+(** try to specialize all non-dependent hypotheses using [tac], maintaining transparency *)
+Ltac guarded_specialize_by' tac guard_tac :=
+  idtac;
+  match goal with
+  | [ H : ?A -> ?B |- _ ]
+    => guard_tac H;
+       let H' := fresh in
+       assert (H' : A) by tac;
+       transparent_specialize_one H H';
+       try clear H' (* if [H] was transparent, [H'] will remain *)
+  end.
+Ltac specialize_by' tac := guarded_specialize_by' tac ltac:(fun _ => idtac).
+
+Ltac specialize_by tac := repeat specialize_by' tac.
+
+(** [specialize_by auto] should not mean [specialize_by ( auto
+    with * )]!!!!!!! (see
+    https://coq.inria.fr/bugs/show_bug.cgi?id=4966) We fix this design
+    flaw. *)
+Tactic Notation "specialize_by" tactic3(tac) := specialize_by tac.
+
+(** A marginally faster version of [specialize_by assumption] *)
+Ltac specialize_by_assumption :=
+  repeat match goal with
+         | [ H : ?T, H' : (?T -> ?U)%type |- _ ] => specialize (H' H)
+         end.
diff --git a/src/Util/Tactics/SplitInContext.v b/src/Util/Tactics/SplitInContext.v
new file mode 100644
index 000000000..c2bf364a0
--- /dev/null
+++ b/src/Util/Tactics/SplitInContext.v
@@ -0,0 +1,22 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+(* Coq's build in tactics don't work so well with things like [iff]
+   so split them up into multiple hypotheses *)
+Ltac split_in_context_by ident funl funr tac :=
+  repeat match goal with
+         | [ H : context p [ident] |- _ ] =>
+           let H0 := context p[funl] in let H0' := eval simpl in H0 in assert H0' by (tac H);
+                                          let H1 := context p[funr] in let H1' := eval simpl in H1 in assert H1' by (tac H);
+                                                                         clear H
+         end.
+Ltac split_in_context ident funl funr :=
+  split_in_context_by ident funl funr ltac:(fun H => apply H).
+
+Ltac split_iff := split_in_context iff (fun a b : Prop => a -> b) (fun a b : Prop => b -> a).
+
+Ltac split_and' :=
+  repeat match goal with
+         | [ H : ?a /\ ?b |- _ ] => let H0 := fresh in let H1 := fresh in
+                                                       assert (H0 := fst H); assert (H1 := snd H); clear H
+         end.
+Ltac split_and := split_and'; split_in_context and (fun a b : Type => a) (fun a b : Type => b).