diff options
Diffstat (limited to 'src/Fancy/Prod.v')
| -rw-r--r-- | src/Fancy/Prod.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Fancy/Prod.v b/src/Fancy/Prod.v index a3f72f17d..a46a7a4f0 100644 --- a/src/Fancy/Prod.v +++ b/src/Fancy/Prod.v @@ -375,4 +375,15 @@ Ltac push_value_unused := | _ => apply not_in_cons; split; [ try assumption; symmetry; assumption | ] | _ => apply in_nil + end. + +(* Solves subgoals for commutativity proofs and simplifies register +lookup expressions *) +Ltac simplify_with_register_properties := + repeat match goal with + | _ => rewrite reg_eqb_refl + | _ => rewrite reg_eqb_neq by congruence + | H : ?y = _ mod ?m |- 0 <= ?y < _ => + rewrite H; apply Z.mod_pos_bound; lia + | _ => assumption end.
\ No newline at end of file |