General reduction tactic

[alxest]

(slightly outdated) performance comparison: https://gist.github.com/alxest/1764d7e80552e1a05dc9897b58e32a17

TODO: make interp_hCallE_mid/blah Opaque
TODO: hide interp_hCallE_mid definitions (and lemmas) from the user, (interp_hCallE_src lemmas too?)
TODO: IRed don't utilize sophisticated features of Red.v (it always uses "continue"; never "break"s); try using simpler engine and do performance comparison
TODO: move resub tactic to ITreelib

[alxest]

It seems "repeat" approach is prohibitively slow: https://github.com/alxest/SimComp/tree/ired-gen3-prw2

total time:    105.546s

 tactic                                   local  total   calls       max 
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─steps ---------------------------------   0.0%  83.2%      85   11.354s
─mred ----------------------------------   0.3%  57.3%     609    0.648s
─ired_both -----------------------------   0.1%  52.7%    3203    0.086s
─_prw2 ---------------------------------   0.6%  52.6%    1915    0.075s
─k1 ------------------------------------   0.1%  27.8%    5342    0.069s
─ired_l --------------------------------   0.2%  27.5%    3203    0.075s
─ired_r --------------------------------   0.1%  25.2%    3203    0.062s
─red_tac -------------------------------   0.1%  23.7%    5342    0.069s
─TAC -----------------------------------   0.3%  22.0%    2554    0.070s
─_red_interp ---------------------------   4.7%  21.6%    4520    0.069s
─__red_interp --------------------------   8.2%  16.9%   14118    0.065s
─des_ifs_safe_aux ----------------------   0.2%  14.4%     610    0.263s
─k0 ------------------------------------   0.2%  14.2%   17664    0.012s
─_ctx ----------------------------------   3.1%  13.9%   11421    0.012s
─done ----------------------------------   0.4%  13.1%    1783    0.053s
─sflib__clarify1 -----------------------   0.2%  12.6%     844    0.070s
─_step ---------------------------------  12.5%  12.5%    1358    0.136s
─clear_tac -----------------------------   0.0%  10.6%       2    6.454s
─eapply _einit -------------------------  10.1%  10.1%    8853    0.016s
─negate --------------------------------   0.0%   9.8%    2374    0.019s
─hide_goal -----------------------------   9.4%   9.4%    5124    0.018s
─replace (uconstr) with (constr) (clause   7.0%   8.9%    1305    0.017s
─cbn -----------------------------------   8.3%   8.3%   12004    0.402s
─apply f_equal -------------------------   7.9%   7.9%    5382    0.011s
─apply lemma ---------------------------   6.9%   6.9%    4907    0.064s
─clear_unused --------------------------   0.2%   5.7%       8    1.799s
─apply _equal_f ------------------------   5.4%   5.4%    2730    0.010s
─sflib__basic_done ---------------------   0.2%   5.4%    2511    0.014s
─under_forall --------------------------   0.1%   5.3%     616    0.027s
─gstep ---------------------------------   0.0%   5.2%     601    0.021s
─tac -----------------------------------   0.6%   4.7%    1403    0.014s
─eauto (nat_or_var_opt) (nat_or_var_opt)   4.5%   4.5%     931    0.022s
─clear_tautology -----------------------   0.1%   4.4%       8    1.072s
─apply bind_ext ------------------------   3.9%   3.9%    4520    0.008s
─simpls --------------------------------   0.0%   3.4%     706    0.146s
─trivial (auto_using) (hintbases) ------   3.4%   3.4%    7379    0.006s
─case H --------------------------------   3.0%   3.0%     956    0.033s
─discriminate --------------------------   2.7%   2.7%    1754    0.008s
─generalize pacotac_internal._paco_mark_   2.4%   2.4%     658    0.014s
─unshelve (tactic1) --------------------   1.4%   2.4%   20642    0.010s
─destruct x as [] eqn:Heq --------------   2.1%   2.1%     209    0.038s
─by (tactic) ---------------------------   0.0%   2.0%     783    0.011s
─_red_itree ----------------------------   0.1%   2.0%       0    0.009s
─split ---------------------------------   2.0%   2.0%    4443    0.008s
─gstep_ --------------------------------   0.1%   2.0%    2039    0.007s

 tactic                                   local  total   calls       max 
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─steps ---------------------------------   0.0%  83.2%      85   11.354s
 ├─mred --------------------------------   0.3%  56.9%     605    0.648s
 │ ├─ired_both -------------------------   0.1%  52.3%    3175    0.086s
 │ │ ├─ired_l --------------------------   0.2%  27.3%    3175    0.075s
 │ │ │└_prw2 ---------------------------   0.3%  26.9%     324    0.075s
 │ │ │ ├─k1 ----------------------------   0.1%  13.3%    2606    0.069s
 │ │ │ │└red_tac -----------------------   0.0%  12.4%    2606    0.069s
 │ │ │ │└_red_interp -------------------   1.1%  12.2%    1344    0.069s
 │ │ │ │└__red_interp ------------------   5.6%  11.1%    9401    0.065s
 │ │ │ │└apply lemma -------------------   5.1%   5.1%    3475    0.064s
 │ │ │ ├─k0 ----------------------------   0.1%   8.3%    9896    0.010s
 │ │ │ │└_ctx --------------------------   2.9%   8.2%    7494    0.010s
 │ │ │ │ ├─apply _equal_f --------------   5.3%   5.3%    2684    0.008s
 │ │ │ │ └─apply f_equal ---------------   2.4%   2.4%    2644    0.006s
 │ │ │ └─eapply _einit -----------------   5.0%   5.0%    4968    0.011s
 │ │ └─ired_r --------------------------   0.1%  25.0%    3175    0.062s
 │ │  └_prw2 ---------------------------   0.2%  24.8%    1557    0.062s
 │ │   ├─k1 ----------------------------   0.1%  14.1%    2644    0.055s
 │ │   │ ├─red_tac ---------------------   0.0%  10.9%    2644    0.052s
 │ │   │ │└_red_interp -----------------   3.5%   9.1%    3068    0.048s
 │ │   │ │ ├─__red_interp --------------   2.5%   5.6%    4477    0.045s
 │ │   │ │ └─apply bind_ext ------------   3.2%   3.2%    3068    0.008s
 │ │   │ └─cbn -------------------------   3.0%   3.0%    3731    0.009s
 │ │   ├─k0 ----------------------------   0.1%   5.6%    7468    0.011s
 │ │   │└_ctx --------------------------   0.2%   5.5%    3731    0.011s
 │ │   │└apply f_equal -----------------   5.3%   5.3%    2646    0.011s
 │ │   └─eapply _einit -----------------   4.9%   4.9%    3735    0.016s
 │ └─cbn -------------------------------   4.3%   4.3%    3175    0.402s
 ├─des_ifs_safe_aux --------------------   0.2%  13.7%     605    0.177s
 │└TAC ---------------------------------   0.1%  11.8%     787    0.070s
 │└sflib__clarify1 ---------------------   0.2%  11.7%     787    0.070s
 │└done --------------------------------   0.3%  10.2%     708    0.053s
 │ ├─sflib__basic_done -----------------   0.2%   3.9%    1344    0.010s
 │ │└discriminate ----------------------   2.2%   2.2%    1338    0.008s
 │ └─case H ----------------------------   2.9%   2.9%     738    0.033s
 └─_step -------------------------------  12.5%  12.5%    1358    0.136s
   ├─gstep -----------------------------   0.0%   5.2%     601    0.021s
   │└under_forall ----------------------   0.1%   5.1%     601    0.021s
   │ ├─tac -----------------------------   0.6%   2.6%     601    0.012s
   │ │└gstep_ --------------------------   0.1%   2.0%    2039    0.007s
   │ └─generalize pacotac_internal._paco   2.4%   2.4%     639    0.014s
   ├─eauto (nat_or_var_opt) (nat_or_var_   3.2%   3.2%     401    0.022s
   └─by (tactic) -----------------------   0.0%   2.0%     757    0.011s
    └tac -------------------------------   0.0%   2.0%     757    0.011s
─clear_tac -----------------------------   0.0%  10.6%       2    6.454s
 ├─clear_unused ------------------------   0.2%   5.7%       8    1.799s
 │└negate ------------------------------   0.0%   5.5%    1310    0.019s
 │└TAC ---------------------------------   0.0%   5.5%     821    0.019s
 │└hide_goal ---------------------------   5.3%   5.3%    2852    0.018s
 │└replace (uconstr) with (constr) (clau   3.9%   4.9%     713    0.017s
 └─clear_tautology ---------------------   0.1%   4.4%       8    1.072s
  └negate ------------------------------   0.0%   4.3%    1064    0.016s
  └TAC ---------------------------------   0.0%   4.3%     640    0.016s
  └hide_goal ---------------------------   4.1%   4.1%    2272    0.016s
  └replace (uconstr) with (constr) (clau   3.0%   3.8%     568    0.015s

It seems the problem can be mitigated by adopting this idea: #90