diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-14 17:44:28 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-14 17:44:51 -0400 |
commit | 933562afe15d37fa95f0b20810e47e683dc384fb (patch) | |
tree | 08cd73a5182eb5e5a789677fe757ed9d62a62c59 /src | |
parent | 48b388b7fb3e866ded35aeb427535aff44a82025 (diff) |
Split up solve_op_mod_eq
This way, we can reuse it even when we can't fully compute the values
Diffstat (limited to 'src')
-rw-r--r-- | src/Arithmetic/Core.v | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 854b912df..97986091c 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1087,13 +1087,17 @@ Ltac F_mod_eq := cbv [Positional.Fdecode]; autorewrite with pull_FofZ; apply mod_eq_Z2F_iff. -Ltac solve_op_mod_eq wt x := +Ltac presolve_op_mod_eq wt x := transitivity (Positional.eval wt x); repeat autounfold; - [|autorewrite with uncps push_id push_basesystem_eval; - reflexivity]; - cbv [mod_eq]; apply f_equal2; [|reflexivity]; - apply f_equal; - basesystem_partial_evaluation_RHS; - do_replace_match_with_destructuring_match_in_goal. + [ cbv [mod_eq]; apply f_equal2; [|reflexivity]; + apply f_equal + | autorewrite with uncps push_id push_basesystem_eval ]. + +Ltac solve_op_mod_eq wt x := + presolve_op_mod_eq; + [ basesystem_partial_evaluation_RHS; + do_replace_match_with_destructuring_match_in_goal + | reflexivity ]. Ltac solve_op_F wt x := F_mod_eq; solve_op_mod_eq wt x. +Ltac presolve_op_F wt x := F_mod_eq; presolve_op_mod_eq wt x. |