More fine-grained util tactic files

Also, add [split_and]

11 files changed, 273 insertions, 146 deletions

diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index 2c2533454..06a4f5b30 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -1,7 +1,8 @@
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Option.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Notations.
 
 Section language.
diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v
index dd0fb08a3..5b9f27f48 100644
--- a/src/Reflection/InlineWf.v
+++ b/src/Reflection/InlineWf.v
@@ -2,7 +2,7 @@
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.WfProofs.
 Require Import Crypto.Reflection.Inline.
-Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
+Require Import Crypto.Util.Tactics.SpecializeBy Crypto.Util.Tactics.DestructHead Crypto.Util.Sigma Crypto.Util.Prod.
 
 Local Open Scope ctype_scope.
 Section language.
diff --git a/src/Util/PartiallyReifiedProp.v b/src/Util/PartiallyReifiedProp.v
index ef1567bd8..023bcb9e0 100644
--- a/src/Util/PartiallyReifiedProp.v
+++ b/src/Util/PartiallyReifiedProp.v
@@ -5,7 +5,9 @@
 Require Import Coq.Setoids.Setoid.
 Require Import Coq.Program.Tactics.
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.DestructHyps.
+Require Import Crypto.Util.Tactics.BreakMatch.
 
 Delimit Scope reified_prop_scope with reified_prop.
 Inductive reified_Prop := rTrue | rFalse | rAnd (x y : reified_Prop) | rOr (x y : reified_Prop) | rImpl (x y : reified_Prop) | rForall {T} (f : T -> reified_Prop) | rEq {T} (x y : T) | inject (_ : Prop).
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 128fdcfd0..e6f5a1cac 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -1,5 +1,11 @@
 (** * Generic Tactics *)
 Require Export Crypto.Util.FixCoqMistakes.
+Require Export Crypto.Util.Tactics.BreakMatch.
+Require Export Crypto.Util.Tactics.Head.
+Require Export Crypto.Util.Tactics.DestructHyps.
+Require Export Crypto.Util.Tactics.DestructHead.
+Require Export Crypto.Util.Tactics.SpecializeBy.
+Require Export Crypto.Util.Tactics.SplitInContext.
 
 (** Test if a tactic succeeds, but always roll-back the results *)
 Tactic Notation "test" tactic3(tac) :=
@@ -11,15 +17,6 @@ Tactic Notation "not" tactic3(tac) := try ((test tac); fail 1 tac "succeeds").
 Ltac get_goal :=
   match goal with |- ?G => G end.
 
-(** 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'.
-
 (** [contains x expr] succeeds iff [x] appears in [expr] *)
 Ltac contains search_for in_term :=
   idtac;
@@ -63,59 +60,6 @@ Ltac subst_evars :=
 
 Ltac subst_let := repeat match goal with | x := _ |- _ => subst x end.
 
-(** 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 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 e
-       end
-  | [ |- appcontext[if ?e then _ else _] ]
-    => only_when e; destruct e eqn:?
-  | [ |- appcontext[match ?e with _ => _ end] ]
-    => only_when e; destruct e eqn:?
-  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 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:?
-  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.
-
 Ltac free_in x y :=
   idtac;
   match y with
@@ -211,86 +155,6 @@ Ltac inversion_all_matches matcher := inversion_all_matches_then matcher ltac:(
 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).
-
-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).
-
-Ltac destruct_sig_matcher HT :=
-  match eval hnf in HT with
-  | ex _ => idtac
-  | ex2 _ _ => idtac
-  | sig _ => idtac
-  | sig2 _ _ => idtac
-  | sigT _ => idtac
-  | sigT2 _ _ => idtac
-  | and _ _ => idtac
-  | prod _ _ => idtac
-  end.
-Ltac destruct_sig := destruct_all_matches destruct_sig_matcher.
-Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher.
-
-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 specialize_by' tac :=
-  idtac;
-  match goal with
-  | [ H : ?A -> ?B |- _ ] =>
-    match type of A with
-      Prop =>
-      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
-  end.
-
-Ltac specialize_by tac := repeat specialize_by' tac.
-
-(** [specialize_by auto] should not mean [specialize_by ltac:( 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.
-
 (** If [tac_in H] operates in [H] and leaves side-conditions before
     the original goal, then
     [side_conditions_before_to_side_conditions_after tac_in H] does
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).
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index d1e0177f2..b8a5c2738 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -3,7 +3,9 @@ Require Import Coq.Relations.Relation_Definitions.
 Require Import Coq.Lists.List.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Prod.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ListUtil.
 Require Export Crypto.Util.FixCoqMistakes.