diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-02-15 13:18:40 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
commit | 0a6e65e3cec0a8f00f357d82489532203f315389 (patch) | |
tree | b7bc706ce46b38e3c43f9375fd5a2dd9859d056a /src/Util | |
parent | 0a9ea9df752b078bbd89f765cf760081036bd51a (diff) |
address some code review comments
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Factorize.v | 73 | ||||
-rw-r--r-- | src/Util/Tactics.v | 11 |
2 files changed, 79 insertions, 5 deletions
diff --git a/src/Util/Factorize.v b/src/Util/Factorize.v new file mode 100644 index 000000000..8ccb7d119 --- /dev/null +++ b/src/Util/Factorize.v @@ -0,0 +1,73 @@ +Require Import Coq.Bool.Sumbool. +Require Import Coq.micromega.Psatz. +Require Import Coq.NArith.NArith. +Require Import Coq.PArith.PArith. +Require Import Coq.Lists.List. +Require Import Coq.Init.Wf. + +Local Open Scope positive_scope. + +(* given [n] and [d₀], returns, possibly, [d, v] where [d ≥ d₀] is small and [d * v = n] + + Precondition: [d₀] is either 2, or an odd number > 2 *) +Definition find_N_factor (factor_val : N) (d0 : N) : option (N * N). +Proof. + refine (let (d', r) := N.div_eucl factor_val d0 in (* special-case the first one, which might be 2 *) + if N.eqb 0 r + then Some (d0, d') + else + let sfactor_val := N.sqrt factor_val in + Fix + (Acc_intro_generator (S (S (S (N.to_nat (N.div2 sfactor_val))))) (@N.gt_wf sfactor_val)) (fun _ => option (N * N)%type) + (fun d find_N_factor + => let (d', r) := N.div_eucl factor_val d in + if N.eqb 0 r + then Some (d, d') + else let d' := (d + 2)%N in + if Sumbool.sumbool_of_bool (N.leb d' sfactor_val) + then find_N_factor d' _ + else None) + (if N.eqb 2%N d0 then 3%N else (d0 + 2)%N)). + { subst sfactor_val d'. + clear find_N_factor. + let H := match goal with H : _ = true |- _ => H end in + clear -H; + abstract ( + apply N.leb_le in H; + split; try assumption; + lia + ). } +Defined. + +(* given [n] and [d₀], gives a list of factors of [n] which are ≥ d₀, lowest to highest *) +Definition factorize' (n : N) : N -> list N. +Proof. + refine (Fix + (Acc_intro_generator (S (S (S (S (N.to_nat (N.div2 (N.sqrt n))))))) N.lt_wf_0) (fun _ => N -> list N) + (fun n factorize cur_max_factor + => _) + n). + refine match find_N_factor n cur_max_factor with + | Some (d, n') => if Sumbool.sumbool_of_bool (n' <? n)%N + then d :: factorize n' _ d + else d :: n' :: nil + | None => n::nil + end. + { let H := match goal with H : _ = true |- _ => H end in + clear -H; + abstract ( + apply N.ltb_lt in H; + assumption + ). } +Defined. + +Definition factorize (n : N) : list N := factorize' n 2%N. + +Definition factorize_or_fail (n:N) : option (list N) := + let factors := factorize n in + if N.eqb (List.fold_right N.mul 1%N factors) n then Some factors else None. +Lemma product_factorize_or_fail (n:N) (factors:list N) + (H:Logic.eq (factorize_or_fail n) (Some factors)) + : Logic.eq (List.fold_right N.mul 1%N factors) n. +Proof. cbv [factorize_or_fail] in H; destruct ((fold_right N.mul 1 (factorize n) =? n)%N) eqn:?; + try apply N.eqb_eq; congruence. Qed.
\ No newline at end of file diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 5f7ad65cc..d98ac1bd4 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -32,11 +32,12 @@ Ltac debuglevel := constr:(0%nat). Ltac solve_debugfail tac := solve [tac] || - let dbg := debuglevel in - match dbg with - | O => idtac - | _ => match goal with |- ?G => idtac "couldn't prove" G end - end. + ( let dbg := debuglevel in + match dbg with + | O => idtac + | _ => match goal with |- ?G => idtac "couldn't prove" G end + end; + fail). Ltac set_evars := repeat match goal with |