Rework and speed up arithmetic simplifier proofs

Induction is so much faster than brute force.

After    | File Name                                     | Before   || Change
--------------------------------------------------------------------------------
6m15.02s | Total                                         | 7m14.18s || -0m59.15s
--------------------------------------------------------------------------------
0m11.62s | Compilers/Z/ArithmeticSimplifierWf            | 0m42.97s || -0m31.35s
0m06.52s | Compilers/Z/ArithmeticSimplifierInterp        | 0m34.28s || -0m27.76s
2m47.55s | Specific/IntegrationTestLadderstep            | 2m48.14s || -0m00.58s
1m09.50s | Specific/IntegrationTestKaratsubaMul          | 1m08.86s || +0m00.64s
1m03.53s | Specific/IntegrationTestLadderstep130         | 1m04.05s || -0m00.51s
0m16.39s | Specific/IntegrationTestFreeze                | 0m16.29s || +0m00.10s
0m13.60s | Specific/IntegrationTestMul                   | 0m13.60s || +0m00.00s
0m11.58s | Specific/IntegrationTestSub                   | 0m11.36s || +0m00.22s
0m09.79s | Specific/IntegrationTestSquare                | 0m09.71s || +0m00.07s
0m03.64s | Compilers/Z/Bounds/Pipeline/Definition        | 0m03.54s || +0m00.10s
0m00.75s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.05s
0m00.55s | Compilers/Z/Bounds/Pipeline                   | 0m00.58s || -0m00.02s

2 files changed, 167 insertions, 249 deletions

diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v
index 06143255b..8314b991e 100644
--- a/src/Compilers/Z/ArithmeticSimplifierInterp.v
+++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v
@@ -1,6 +1,7 @@
 Require Import Coq.micromega.Psatz.
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.TypeInversion.
 Require Import Crypto.Compilers.ExprInversion.
 Require Import Crypto.Compilers.RewriterInterp.
@@ -44,131 +45,89 @@ Local Ltac break_t_step :=
         | progress break_innermost_match_step
         | progress break_match_hyps ].
 
+Definition interpf_as_expr_or_const {t}
+  : interp_flat_type (@inverted_expr interp_base_type) t -> interp_flat_type interp_base_type t
+  := SmartVarfMap
+       (fun t z => match z with
+                   | const_of z => cast_const (t1:=TZ) z
+                   | gen_expr e => interpf interp_op e
+                   | neg_expr e => interpf interp_op (Op (Opp _ _) e)
+                   end).
 
-Lemma interp_as_expr_or_const_correct_base {t} e z
-  : @interp_as_expr_or_const interp_base_type (Tbase t) e = Some z
-    -> interpf interp_op e = match z with
-                             | const_of z => cast_const (t1:=TZ) z
-                             | gen_expr e => interpf interp_op e
-                             | neg_expr e => interpf interp_op (Op (Opp _ _) e)
-                             end.
+Lemma interp_as_expr_or_const_correct {t} e z
+  : @interp_as_expr_or_const interp_base_type t e = Some z
+    -> interpf interp_op e = interpf_as_expr_or_const z.
 Proof.
-  destruct z.
-  { repeat first [ fin_t
+  induction e;
+    repeat first [ progress subst
+                 | progress inversion_option
                  | progress simpl in *
-                 | progress intros
-                 | break_t_step
-                 | progress invert_expr
-                 | progress invert_op ]. }
-  { do 2 (invert_expr; break_innermost_match; intros);
-      repeat first [ fin_t
-                   | progress simpl in *
-                   | progress intros
-                   | break_t_step
-                   | progress invert_op ]. }
-  { do 2 (invert_expr; break_innermost_match; intros);
-      repeat first [ fin_t
-                   | progress simpl in *
-                   | progress intros
-                   | break_t_step
-                   | progress invert_op ]. }
-Qed.
-
-Local Ltac rewrite_interp_as_expr_or_const_correct_base _ :=
-  match goal with
-  | [ |- context[interpf _ ?e] ]
-    => erewrite !(@interp_as_expr_or_const_correct_base _ e) by eassumption; cbv beta iota
-  end.
-
-Lemma interp_as_expr_or_const_correct_prod_base {A B} e (v : _ * _)
-  : @interp_as_expr_or_const interp_base_type (Prod (Tbase A) (Tbase B)) e = Some v
-    -> interpf interp_op e = (match fst v with
-                              | const_of z => cast_const (t1:=TZ) z
-                              | gen_expr e => interpf interp_op e
-                              | neg_expr e => interpf interp_op (Op (Opp _ _) e)
-                              end,
-                              match snd v with
-                              | const_of z => cast_const (t1:=TZ) z
-                              | gen_expr e => interpf interp_op e
-                              | neg_expr e => interpf interp_op (Op (Opp _ _) e)
-                              end).
-Proof.
-  invert_expr;
-    repeat first [ fin_t
-                 | progress simpl in *
-                 | progress intros
-                 | break_t_step
-                 | rewrite_interp_as_expr_or_const_correct_base () ].
+                 | progress cbn [interpf_as_expr_or_const SmartVarfMap smart_interp_flat_map]
+                 | reflexivity
+                 | break_innermost_match_hyps_step
+                 | intro
+                 | match goal with
+                   | [ H : forall z, Some _ = Some z -> _ |- _ ] => specialize (H _ eq_refl)
+                   | [ H : interpf _ ?e = interpf_as_expr_or_const _ |- _ ]
+                     => rewrite H
+                   | [ |- context[match ?e with _ => _ end] ]
+                     => is_var e; invert_one_op e
+                   end
+                 | break_innermost_match_step ].
 Qed.
 
-Local Ltac rewrite_interp_as_expr_or_const_correct_prod_base _ :=
+Local Ltac rewrite_interp_as_expr_or_const_correct _ :=
   match goal with
   | [ |- context[interpf _ ?e] ]
-    => erewrite !(@interp_as_expr_or_const_correct_prod_base _ _ e) by eassumption; cbv beta iota
-  end.
-
-Lemma interp_as_expr_or_const_correct_prod3_base {A B C} e (v : _ * _ * _)
-  : @interp_as_expr_or_const interp_base_type (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e = Some v
-    -> interpf interp_op e = (match fst (fst v) with
-                              | const_of z => cast_const (t1:=TZ) z
-                              | gen_expr e => interpf interp_op e
-                              | neg_expr e => interpf interp_op (Op (Opp _ _) e)
-                              end,
-                              match snd (fst v) with
-                              | const_of z => cast_const (t1:=TZ) z
-                              | gen_expr e => interpf interp_op e
-                              | neg_expr e => interpf interp_op (Op (Opp _ _) e)
-                              end,
-                              match snd v with
-                              | const_of z => cast_const (t1:=TZ) z
-                              | gen_expr e => interpf interp_op e
-                              | neg_expr e => interpf interp_op (Op (Opp _ _) e)
-                              end).
-Proof.
-  invert_expr;
-    repeat first [ fin_t
-                 | progress simpl in *
-                 | progress intros
-                 | break_t_step
-                 | rewrite_interp_as_expr_or_const_correct_base ()
-                 | rewrite_interp_as_expr_or_const_correct_prod_base () ].
-Qed.
-
-Local Ltac rewrite_interp_as_expr_or_const_correct_prod3_base _ :=
-  match goal with
-  | [ |- context[interpf _ ?e] ]
-    => erewrite !(@interp_as_expr_or_const_correct_prod3_base _ _ _ e) by eassumption; cbv beta iota
+    => erewrite !(@interp_as_expr_or_const_correct _ e) by eassumption; cbv beta iota;
+       cbn [interpf_as_expr_or_const SmartVarfMap smart_interp_flat_map]
   end.
 
 Local Arguments Z.mul !_ !_.
 Local Arguments Z.add !_ !_.
 Local Arguments Z.sub !_ !_.
 Local Arguments Z.opp !_.
+Local Arguments interp_op _ _ !_ _ / .
+Local Arguments lift_op / .
 
 Lemma InterpSimplifyArith {convert_adc_to_sbb} {t} (e : Expr t)
   : forall x, Interp interp_op (SimplifyArith convert_adc_to_sbb e) x = Interp interp_op e x.
 Proof.
   apply InterpRewriteOp; intros; unfold simplify_op_expr.
-  break_innermost_match;
-    repeat first [ fin_t
-                 | progress cbv [LetIn.Let_In Z.zselect IdfunWithAlt.id_with_alt]
-                 | progress simpl in *
+  Time break_innermost_match;
+    repeat first [ reflexivity
                  | progress subst
-                 | progress subst_prod
-                 | rewrite_interp_as_expr_or_const_correct_base ()
-                 | rewrite_interp_as_expr_or_const_correct_prod_base ()
-                 | rewrite_interp_as_expr_or_const_correct_prod3_base ()
-                 | rewrite FixedWordSizesEquality.ZToWord_wordToZ
-                 | rewrite FixedWordSizesEquality.ZToWord_wordToZ_ZToWord by reflexivity
-                 | rewrite FixedWordSizesEquality.wordToZ_ZToWord_0
-                 | progress unfold interp_op, lift_op
-                 | progress Z.ltb_to_lt
-                 | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r
-                 | rewrite !Z.sub_with_borrow_to_add_get_carry
-                 | progress autorewrite with zsimplify_fast
-                 | break_innermost_match_step
+                 | progress simpl in *
+                 | progress inversion_prod
+                 | progress invert_expr_subst
                  | inversion_base_type_constr_step
-                 | progress cbv [cast_const ZToInterp interpToZ] ].
+                 | match goal with
+                   | [ |- context[match ?e with _ => _ end] ]
+                     => is_var e; invert_one_op e;
+                        repeat match goal with
+                               | [ |- match ?T with _ => _ end _ ]
+                                 => break_innermost_match_step; try exact I
+                               end
+                   end
+                 | break_innermost_match_step
+                 | rewrite_interp_as_expr_or_const_correct ()
+                 | intro ].
+  all:repeat first [ reflexivity
+                   | omega
+                   | discriminate
+                   | progress cbv [LetIn.Let_In Z.zselect IdfunWithAlt.id_with_alt]
+                   | progress subst
+                   | progress simpl in *
+                   | progress Z.ltb_to_lt
+                   | break_innermost_match_step
+                   | rewrite FixedWordSizesEquality.ZToWord_wordToZ
+                   | rewrite FixedWordSizesEquality.ZToWord_wordToZ_ZToWord by reflexivity
+                   | rewrite FixedWordSizesEquality.wordToZ_ZToWord_0
+                   | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r
+                   | rewrite !Z.sub_with_borrow_to_add_get_carry
+                   | progress autorewrite with zsimplify_fast
+                   | progress cbv [cast_const ZToInterp interpToZ]
+                   | nia ].
 Qed.
 
 Hint Rewrite @InterpSimplifyArith : reflective_interp.
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index 176301e06..33f3c3335 100644
--- a/src/Compilers/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Wf.
 Require Import Crypto.Compilers.WfInversion.
 Require Import Crypto.Compilers.TypeInversion.
@@ -8,6 +9,7 @@ Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Z.OpInversion.
 Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
 Require Import Crypto.Compilers.Z.Syntax.Equality.
+Require Import Crypto.Compilers.Z.Syntax.Util.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sum.
@@ -99,130 +101,55 @@ Local Ltac pret_step :=
             => is_var e; destruct (interp_as_expr_or_const e) eqn:?
           end ].
 
-Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2}
-      (Hwf : @wff var1 var2 G (Tbase t) e1 e2)
-  : @interp_as_expr_or_const var1 (Tbase t) e1 = Some v1
-    -> @interp_as_expr_or_const var2 (Tbase t) e2 = Some v2
-    -> match v1, v2 with
-       | const_of z1, const_of z2 => z1 = z2
-       | gen_expr e1, gen_expr e2
-       | neg_expr e1, neg_expr e2
-         => wff G e1 e2
-       | const_of _, _
-       | gen_expr _, _
-       | neg_expr _, _
-         => False
-       end.
-Proof.
-  invert_one_expr e1; intros; break_innermost_match; intros;
-    try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
-         invert_one_expr e2); intros;
-      repeat first [ fin_t
-                   | progress simpl in *
-                   | progress intros
-                   | break_t_step
-                   | match goal with
-                     | [ H : wff _ _ ?e |- _ ] => is_var e; invert_one_expr e
-                     end ].
-Qed.
-
-Local Ltac pose_wff_base :=
-  match goal with
-  | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
-    => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2
-  end.
-
-Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _ * _}
-      (Hwf : wff G e1 e2)
-  : @interp_as_expr_or_const var1 (Prod (Tbase A) (Tbase B)) e1 = Some v1
-    -> @interp_as_expr_or_const var2 (Prod (Tbase A) (Tbase B)) e2 = Some v2
-    -> match fst v1, fst v2 with
-       | const_of z1, const_of z2 => z1 = z2
-       | gen_expr e1, gen_expr e2
-       | neg_expr e1, neg_expr e2
-         => wff G e1 e2
-       | const_of _, _
-       | gen_expr _, _
-       | neg_expr _, _
-         => False
-       end
-       /\ match snd v1, snd v2 with
-          | const_of z1, const_of z2 => z1 = z2
-          | gen_expr e1, gen_expr e2
-          | neg_expr e1, neg_expr e2
-            => wff G e1 e2
-          | const_of _, _
-          | gen_expr _, _
-          | neg_expr _, _
-            => False
-          end.
-Proof.
-  invert_one_expr e1; intros; break_innermost_match; intros; try exact I;
-    try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
-         invert_one_expr e2);
-    intros; break_innermost_match; intros; try exact I;
-      repeat first [ pret_step
-                   | pose_wff_base
-                   | break_t_step
-                   | apply conj ].
-Qed.
-
-Local Ltac pose_wff_prod :=
-  match goal with
-  | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
-    => pose proof (wff_interp_as_expr_or_const_prod_base Hwf H1 H2); clear H1 H2
-  end.
+Fixpoint wff_as_expr_or_const {var1 var2} G {t}
+  : interp_flat_type (@inverted_expr var1) t
+    -> interp_flat_type (@inverted_expr var2) t
+    -> Prop
+  := match t with
+     | Tbase T
+       => fun z1 z2 => match z1, z2 return Prop with
+                       | const_of z1, const_of z2 => z1 = z2
+                       | gen_expr e1, gen_expr e2
+                       | neg_expr e1, neg_expr e2
+                         => wff G e1 e2
+                       | const_of _, _
+                       | gen_expr _, _
+                       | neg_expr _, _
+                         => False
+                       end
+     | Unit => fun _ _ => True
+     | Prod A B => fun a b : interp_flat_type _ A * interp_flat_type _ B
+                   => and (@wff_as_expr_or_const var1 var2 G A (fst a) (fst b))
+                          (@wff_as_expr_or_const var1 var2 G B (snd a) (snd b))
+     end.
 
-Lemma wff_interp_as_expr_or_const_prod3_base {var1 var2 A B C} {G e1 e2} {v1 v2 : _ * _ * _}
-      (Hwf : wff G e1 e2)
-  : @interp_as_expr_or_const var1 (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e1 = Some v1
-    -> @interp_as_expr_or_const var2 (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e2 = Some v2
-    -> match fst (fst v1), fst (fst v2) with
-       | const_of z1, const_of z2 => z1 = z2
-       | gen_expr e1, gen_expr e2
-       | neg_expr e1, neg_expr e2
-         => wff G e1 e2
-       | const_of _, _
-       | gen_expr _, _
-       | neg_expr _, _
-         => False
-       end
-       /\ match snd (fst v1), snd (fst v2) with
-          | const_of z1, const_of z2 => z1 = z2
-          | gen_expr e1, gen_expr e2
-          | neg_expr e1, neg_expr e2
-            => wff G e1 e2
-          | const_of _, _
-          | gen_expr _, _
-          | neg_expr _, _
-            => False
-          end
-       /\ match snd v1, snd v2 with
-          | const_of z1, const_of z2 => z1 = z2
-          | gen_expr e1, gen_expr e2
-          | neg_expr e1, neg_expr e2
-            => wff G e1 e2
-          | const_of _, _
-          | gen_expr _, _
-          | neg_expr _, _
-            => False
-          end.
+Lemma wff_interp_as_expr_or_const {var1 var2 t} {G e1 e2 v1 v2}
+      (Hwf : @wff var1 var2 G t e1 e2)
+  : @interp_as_expr_or_const var1 t e1 = Some v1
+    -> @interp_as_expr_or_const var2 t e2 = Some v2
+    -> wff_as_expr_or_const G v1 v2.
 Proof.
-  invert_one_expr e1; intros; break_innermost_match; intros; try exact I;
-    try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in
-         invert_one_expr e2);
-    intros; break_innermost_match; intros; try exact I;
-      repeat first [ pret_step
-                   | pose_wff_base
-                   | pose_wff_prod
-                   | break_t_step
-                   | apply conj ].
+  induction Hwf;
+    repeat first [ progress subst
+                 | progress inversion_option
+                 | progress simpl in *
+                 | progress cbn [wff_as_expr_or_const]
+                 | reflexivity
+                 | break_innermost_match_hyps_step
+                 | intro
+                 | match goal with
+                   | [ H : forall z, Some _ = Some z -> _ |- _ ] => specialize (H _ eq_refl)
+                   | [ |- context[match ?e with _ => _ end] ]
+                     => is_var e; invert_one_op e
+                   end
+                 | break_innermost_match_step
+                 | solve [ auto with wf ] ].
 Qed.
 
-Local Ltac pose_wff_prod3 :=
+Local Ltac pose_wff _ :=
   match goal with
   | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
-    => pose proof (wff_interp_as_expr_or_const_prod3_base Hwf H1 H2); clear H1 H2
+    => pose proof (wff_interp_as_expr_or_const Hwf H1 H2); clear H1 H2
   end.
 
 Lemma Wf_SimplifyArith {convert_adc_to_sbb} {t} (e : Expr t)
@@ -230,32 +157,64 @@ Lemma Wf_SimplifyArith {convert_adc_to_sbb} {t} (e : Expr t)
   : Wf (SimplifyArith convert_adc_to_sbb e).
 Proof.
   apply Wf_RewriteOp; [ | assumption ].
-  intros ???????? Hwf'; unfold simplify_op_expr;
-    repeat match goal with
-           | [ H : ?T |- ?T ] => exact H
-           | [ H : False |- _ ] => exfalso; assumption
-           | [ H : false = true |- _ ] => exfalso; clear -H; discriminate
-           | [ H : true = false |- _ ] => exfalso; clear -H; discriminate
-           | _ => pose_wff_base
-           | _ => pose_wff_prod
-           | _ => pose_wff_prod3
-           | _ => progress destruct_head'_and
-           | _ => progress subst
-           | _ => inversion_base_type_constr_step
-           | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ]
-             => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2
-           | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
-             => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2
-           | [ |- wff _ (Op _ _) (LetIn _ _) ] => exfalso
-           | [ |- wff _ (LetIn _ _) (Op _ _) ] => exfalso
-           | [ |- wff _ (Pair _ _) (LetIn _ _) ] => exfalso
-           | [ |- wff _ (LetIn _ _) (Pair _ _) ] => exfalso
-           | [ |- wff _ _ _ ] => constructor; intros
-           | [ |- List.In _ _ ] => progress (simpl; auto)
-           | _ => rewrite FixedWordSizesEquality.ZToWord_wordToZ
-           | _ => rewrite FixedWordSizesEquality.ZToWord_wordToZ_ZToWord by reflexivity
-           | _ => break_innermost_match_step; simpl in *
-           end.
+  intros ???????? Hwf'; unfold simplify_op_expr.
+  repeat match goal with
+         | [ H : ?T |- ?T ] => exact H
+         | [ H : False |- _ ] => exfalso; assumption
+         | [ |- True ] => exact I
+         | [ H : false = true |- _ ] => exfalso; clear -H; discriminate
+         | [ H : true = false |- _ ] => exfalso; clear -H; discriminate
+         | [ H : None = Some _ |- _ ] => exfalso; clear -H; discriminate
+         | [ H : Some _ = None |- _ ] => exfalso; clear -H; discriminate
+         | [ H : TT = Op _ _ |- _ ] => exfalso; clear -H; discriminate
+         | [ H : invert_Op ?e = None, H' : wff _ (Op ?opc _) ?e |- _ ]
+           => progress (exfalso; clear -H H'; generalize dependent opc; intros; try (is_var e; destruct e))
+         | [ H : invert_Op ?e = None, H' : wff _ ?e (Op ?opc _) |- _ ]
+           => progress (exfalso; clear -H H'; generalize dependent opc; intros; try (is_var e; destruct e))
+         | _ => progress destruct_head'_and
+         | _ => progress subst
+         | _ => progress destruct_head'_prod
+         | _ => progress destruct_head'_sig
+         | _ => progress destruct_head'_sigT
+         | _ => inversion_base_type_constr_step
+         | _ => inversion_wf_step_constr
+         | _ => progress invert_expr_subst
+         | _ => progress rewrite_eta_match_base_type_impl
+         | [ H : ?x = ?x |- _ ] => clear H || (progress eliminate_hprop_eq)
+         | [ H : match ?e with @const_of _ _ _ => _ = _ | _ => _ end |- _ ]
+           => is_var e; destruct e
+         | [ H : match ?e with @const_of _ _ _ => False | _ => _ end |- _ ]
+           => is_var e; destruct e
+         | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ]
+           => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2
+         | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ]
+           => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2
+         | [ |- wff _ (Op _ _) (LetIn _ _) ] => exfalso
+         | [ |- wff _ (LetIn _ _) (Op _ _) ] => exfalso
+         | [ |- wff _ (Pair _ _) (LetIn _ _) ] => exfalso
+         | [ |- wff _ (LetIn _ _) (Pair _ _) ] => exfalso
+         | _ => pose_wff ()
+         | _ => progress cbn [fst snd projT1 projT2 interp_flat_type wff_as_expr_or_const eq_rect invert_Op] in *
+         | [ |- wff _ _ _ ] => constructor; intros
+         | [ H : match ?e with @const_of _ _ _ => _ | _ => _ end |- _ ]
+           => is_var e; destruct e
+         | [ |- context[match @interp_as_expr_or_const ?var ?t ?e with _ => _ end] ]
+           => destruct (@interp_as_expr_or_const var t e) eqn:?
+         | [ |- context[match base_type_eq_semidec_transparent ?t1 ?t2 with _ => _ end] ]
+           => destruct (base_type_eq_semidec_transparent t1 t2)
+         | [ |- context[match @invert_Op ?base_type ?op ?var ?t ?e with _ => _ end] ]
+           => destruct (@invert_Op base_type op var t e) eqn:?
+         | [ |- context[if BinInt.Z.eqb ?x ?y then _ else _] ]
+           => destruct (BinInt.Z.eqb x y) eqn:?
+         | [ |- context[if BinInt.Z.ltb ?x ?y then _ else _] ]
+           => destruct (BinInt.Z.ltb x y) eqn:?
+         | [ |- context[match ?e with @OpConst _ _ => _ | _ => _ end] ]
+           => is_var e; destruct e
+         | [ |- context[match ?e with @OpConst _ _ => _ | _ => _ end] ]
+           => is_var e; invert_one_op e; try exact I; break_innermost_match_step; intros
+         | [ |- List.In _ _ ] => progress (simpl; auto)
+         | _ => break_innermost_match_step
+         end.
 Qed.
 
 Hint Resolve Wf_SimplifyArith : wf.