More fine-grained util tactic files

Also, add [split_and]

1 files changed, 116 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.