Lessness (May 06 2022 at 15:40): Lessness (May 06 2022 at 15:40):How would you approach proving that the two functions return the same result or all_prime_factors n = prime_divisors n. The first approach is to with k going from 2 to n and removing k from the factors of n, the second approach is simply taking the list 0..n and filtering divisors of n which happens to be primes.
Coq code appended.
It feels like I don't know basic math... :sweat_smile: I have no idea yet about the correct approach to this when doing the paper proof. I would appreciate any suggestions.
Require Import VST.floyd.proofauto.
Require Import FunInd.
Require Import Znumtheory.
Open Scope Z.
Definition prime_divisors n := filter prime_dec (filter (fun x => Zdivide_dec x n) (upto (Z.to_nat n + 1))).
Theorem all_prime_divisors_thm n (H: 0 < n):
forall k, (Z.divide k n /\ prime k) <-> In k (prime_divisors n).
Proof.
Admitted. (* I have proven this, but put Admitted to make code shorter. *)
Definition biggest_prime_divisor n := fold_left Z.max (prime_divisors n).
Function remove_factor (n k: Z) {measure Z.to_nat n}: Z :=
if Z_le_gt_dec k 1 then n else
if Z_le_gt_dec n 1 then n else
if Zdivide_dec k n
then remove_factor (Z.div n k) k
else n.
Proof.
intros. clear teq teq0 teq1. destruct anonymous1. subst. rewrite Z.div_mul; try lia. nia.
Defined.
Theorem remove_factor_decreasing (n k: Z) (H: k > 1) (H0: n > 1) (H1: Z.divide k n): remove_factor n k < n.
Proof.
Admitted. (* Same thing as previously. *)
Function find_factors (n k s: Z) { measure Z.to_nat s }: list Z :=
if Z_le_gt_dec s 0 then nil else
if Z_le_gt_dec k 1 then nil else
if Z_le_gt_dec n 1 then nil else
if Z_le_gt_dec n k then n :: nil else
if Zdivide_dec k n
then k :: find_factors (remove_factor n k) (k + 1) (s - 1)
else find_factors n (k + 1) (s - 1).
Proof.
+ intros. lia.
+ intros. lia.
Defined.
Definition all_prime_factors (n: Z) := find_factors n 2 (n - 2).
Theorem equivalence n: all_prime_factors n = prime_divisors n.
Proof.
Admitted. (* Not proven yet. *)
this seems slightly incorrect, all_prime_factors 2 computes to nil (and in general it seems it computes to nil on primes)
I think you want something like Definition all_prime_factors (n: Z) := find_factors n 2 n.
then you want to prove something about find_factors on more general arguments, I think it would be something like
forall n k s, P n k s -> find_factors n k s = filter (fun x => Z_le_gt_dec k x) (prime_divisors n)
where P n k s is something true for P n 2 n and if P n k s then P is also true on the arguments used for recursive calls
Gaëtan Gilbert (May 06 2022 at 16:05):(P probably looks like "s is big enough that my recursion won't stop too early")
Lessness (May 06 2022 at 16:08):Gaëtan Gilbert said:
this seems slightly incorrect,
all_prime_factors 2computes tonil(and in general it seems it computes to nil on primes)
Yes, you are right. I increased it to n-1 - then it works on primes too.
Gaëtan Gilbert (May 06 2022 at 16:14):Gaëtan Gilbert said:
(P probably looks like "s is big enough that my recursion won't stop too early")
also "everything is nonnegative", I forgot this was Z for a bit
Lessness (May 09 2022 at 06:27):No success for now. :|
Sooner or later I will think of smth, though.
Lessness (May 09 2022 at 10:54):So far so good. I have theorem aux01 from which the equality follows. But it is filled with admit for now and aux00 has to be proved too. (Ah, and In_upto too.)
Require Import VST.floyd.proofauto.
Require Import FunInd.
Require Import Znumtheory.
Open Scope Z.
Function upto_aux (p: Z * Z) { measure (fun p => match p with (a, b) => Z.to_nat (b - a) end) p }: list Z :=
match p with (a, b) => if Z_lt_ge_dec a b then a :: upto_aux (a + 1, b) else nil end.
Proof. intros. lia. Defined.
Definition upto (a b: Z) := upto_aux (a, b).
Theorem In_upto (a b: Z): forall x, In x (upto a b) <-> a <= x < b.
Proof.
Admitted.
Definition prime_divisors m n := filter prime_dec (filter (fun x => Zdivide_dec x n) (upto m (n + 1))).
Theorem all_prime_divisors_thm n (H: 0 < n):
forall k, (Z.divide k n /\ prime k) <-> In k (prime_divisors 2 n).
Proof.
split; intros.
+ unfold prime_divisors. destruct H0. apply filter_In. split.
- apply filter_In. split.
* apply In_upto. split.
++ inversion H1. lia.
++ apply Z.divide_pos_le in H0; auto. lia.
* destruct (Zdivide_dec k n); auto.
- destruct (prime_dec k); auto.
+ unfold prime_divisors in H0. apply filter_In in H0. destruct H0. apply filter_In in H0. destruct H0.
destruct (Zdivide_dec k n); intuition. destruct (prime_dec k); intuition.
Qed.
Definition biggest_prime_divisor n := fold_left Z.max (prime_divisors 2 n).
Function remove_factor (n k: Z) {measure Z.to_nat n}: Z :=
if Z_le_gt_dec k 1 then n else
if Z_le_gt_dec n 1 then n else
if Zdivide_dec k n
then remove_factor (Z.div n k) k
else n.
Proof.
intros. clear teq teq0 teq1. destruct anonymous1. subst. rewrite Z.div_mul; try lia. nia.
Defined.
Theorem remove_factor_gt_0 (n k: Z): 1 <= n -> 1 <= remove_factor n k.
Proof.
intros. assert (0 <= n) by lia. revert H. pattern n. apply Z_lt_induction.
+ intros. rewrite remove_factor_equation. repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec.
- apply H. destruct d. subst. rewrite Z.div_mul; try lia. nia. destruct d. subst. rewrite Z.div_mul; try lia.
- auto.
+ auto.
Qed.
Theorem remove_factor_thm00 n k: 1 < n -> 1 < k -> Z.divide k (remove_factor n k) -> False.
Proof.
intros. assert (0 <= n) by lia. revert H H1. pattern n. apply Z_lt_induction.
+ intros. rewrite remove_factor_equation in H3. repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec.
- apply H in H3; auto. destruct d. subst. rewrite Z.div_mul; try lia. nia.
destruct d. subst. rewrite Z.div_mul in *; try lia. rewrite remove_factor_equation in H3.
repeat destruct Z_le_gt_dec; try lia. destruct H3. subst.
clear g g0 g1 H. exfalso. assert (x <= 0) by nia. nia.
- tauto.
+ auto.
Qed.
Theorem remove_factor_decreasing (n k: Z) (H: k > 1) (H0: n > 1) (H1: Z.divide k n): remove_factor n k < n.
Proof.
assert (0 <= n) by lia. revert H0 H1. pattern n. apply Z_lt_induction.
+ intros. destruct H3. subst. rewrite remove_factor_equation.
repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec.
- rewrite Z.div_mul; try lia. clear d g g0.
assert (0 <= x0 < x0 * k) by nia.
destruct (Z_le_gt_dec x0 1).
* assert (x0 = 0 \/ x0 = 1) by lia. destruct H4.
++ subst. lia.
++ subst. rewrite remove_factor_equation. destruct Z_le_gt_dec.
-- lia.
-- destruct Z_le_gt_dec. lia. lia.
* destruct (Zdivide_dec k x0).
++ pose (H0 _ H3 g d). nia.
++ rewrite remove_factor_equation. repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec; intuition.
- exfalso. apply n0. exists x0. auto.
+ auto.
Qed.
Function find_factors (n k s: Z) { measure Z.to_nat s }: list Z :=
if Z_le_gt_dec s 0 then nil else
if Z_le_gt_dec k 1 then nil else
if Z_le_gt_dec n 1 then nil else
if Zdivide_dec k n
then k :: find_factors (remove_factor n k) (k + 1) (s - 1)
else find_factors n (k + 1) (s - 1).
Proof.
+ intros. lia.
+ intros. lia.
Defined.
Definition all_prime_factors (n: Z) := find_factors n 2 n.
Eval vm_compute in all_prime_factors 29.
Eval vm_compute in (find_factors 123 2 2).
Fixpoint remove_factors_list (n: Z) (L: list Z): Z :=
match L with
| [] => n
| x :: t => if Zdivide_dec x n then remove_factors_list (remove_factor n x) t else remove_factors_list n t
end.
Definition remove_factors_list_gt_0 (n: Z) (L: list Z):
1 <= n -> (forall x, In x L -> 1 < x) -> 0 < remove_factors_list n L.
Proof.
intros. assert (0 <= n) by lia. revert L H H0. pattern n. apply Z_lt_induction; auto.
intros. induction L.
+ simpl. lia.
+ simpl in *. destruct Zdivide_dec.
- apply H.
* split.
++ pose proof (remove_factor_gt_0 x a H0). lia.
++ apply remove_factor_decreasing; auto; try lia.
-- assert (1 < a) by (apply H2; auto). lia.
-- assert (1 < a) by (apply H2; auto). assert (0 < x) by lia. pose proof (Z.divide_pos_le a x H4 d). lia.
* apply remove_factor_gt_0; auto.
* intros. apply H2. auto.
- apply IHL. intros. apply H2. auto.
Qed.
Fixpoint remove_factors_list' (n: Z) (L: list Z): list Z :=
match L with
| [] => []
| x :: t => if Zdivide_dec x n then x :: remove_factors_list' (remove_factor n x) t else remove_factors_list' n t
end.
Eval compute in find_factors (remove_factors_list (2*3*5*7*11*13) (upto 2 3)) 3 13.
Eval compute in find_factors 10 2 10.
Theorem aux00 (n k: Z): 1 < k -> 1 <= n -> Z.divide k (remove_factors_list n (upto 2 k)) -> prime k.
Proof.
Admitted.
Theorem aux01 (n k s: Z):
1 <= n -> 1 < k -> n <= s ->
find_factors (remove_factors_list n (upto 2 k)) k s = prime_divisors k (remove_factors_list n (upto 2 k)).
Proof.
intros. assert (0 <= n) by lia. revert s k H H0 H1. pattern n. apply Z_lt_induction.
+ intros. rewrite find_factors_equation. repeat destruct Z_le_gt_dec; try lia.
- assert (remove_factors_list x (upto 2 k) = 1).
{ pose proof (remove_factors_list_gt_0 x (upto 2 k) H0).
assert (forall x, In x (upto 2 k) -> 1 < x).
{ intros. rewrite In_upto in H5. lia. }
pose proof (H4 H5). lia. }
rewrite H4.
unfold prime_divisors. assert (upto k 2 = []).
{ assert (forall x, In x (upto k 2) -> False).
{ intros. apply In_upto in H5. lia. }
destruct (upto k 2); auto. simpl in H5. exfalso. eapply H5. left. reflexivity. }
simpl. rewrite H5. simpl. auto.
- destruct Zdivide_dec.
* assert (prime k) by (apply aux00 in d; auto).
replace (prime_divisors k (remove_factors_list x (upto 2 k))) with (k :: prime_divisors (k + 1) (remove_factors_list (remove_factor x k) (upto 2 (k + 1)))) by admit.
f_equal. erewrite <- H with (s:=s - 1); try lia.
++ f_equal. admit.
++ admit.
++ apply remove_factor_gt_0; auto.
++ admit.
* rewrite find_factors_equation. repeat destruct Z_le_gt_dec; try lia.
++ admit.
++ destruct Zdivide_dec.
-- admit.
-- admit.
+ auto.
Admitted.
Theorem equivalence (n k s: Z):
1 <= n -> 1 < k -> n <= s ->
find_factors n 2 s = prime_divisors 2 n.
Proof.
intros. replace n with (remove_factors_list n (upto 2 2)).
+ rewrite aux01; auto. lia.
+ simpl. auto.
Qed.
Hmm, this direction seems to be wrong or at least not correct enough. :(
Lessness (May 15 2022 at 18:40):One possibility could be generalizing that 2 in the upto 2 k... but then find_factors (remove_factors_list n (upto w k)) k s (with w instead of 2) starts behaving weirdly/not-so-nice and that messes everything up. My math skills aren't good enough to describe what happens then, therefore no hope in this direction.
Maybe I should take a step back and rethink the hint of Gaëtan Gilbert... The current path seems unproductive. At least I proved lots of potentially useful lemmas.
Lessness (May 15 2022 at 19:04):The current state of that can be seen here: https://github.com/LessnessRandomness/PE/blob/main/tinkering_with_EP3.v
I'm taking a pause until some new idea appears.
Paolo Giarrusso (May 15 2022 at 21:28):Why does find_factor take fuel s instead of using measure n - k? That seems like adding extra complexity (since you will need to prove that the fuel s is enough)
Paolo Giarrusso (May 15 2022 at 21:34):more importantly, I wonder how easy/hard it is to derive this from the unicity of prime decomposition. Alternatively, I do not see lemmas using properties of prime numbers.
Paolo Giarrusso (May 15 2022 at 21:41):AFAICT, all your lemmas would indeed hold for arbitrary predicates…
Paolo Giarrusso (May 15 2022 at 21:41):I haven’t done number theory in Coq, but thinking about a paper proof, a fundamental property you will need is that dividing n by prime a will not remove prime b from the list. This is only true for prime numbers.
Paolo Giarrusso (May 15 2022 at 21:44):(I also don't think you should expect so many proofs by induction on n in this problem)
Paolo Giarrusso (May 15 2022 at 21:48):in fact, it’s not even trivial that find_factors list is composed entirely of primes.
Paolo Giarrusso (May 15 2022 at 21:49):here is my first suggestion: assume that all naturals n have a unique decomposition into powers of primes — beware a formal statement requires some care!
Paolo Giarrusso (May 15 2022 at 21:49):Then, describe the effects of the two functions in terms of the prime decomposition.
Paolo Giarrusso (May 15 2022 at 21:50):prime_divisors just lists the primes with nonzero exponents in the decomposition.
Paolo Giarrusso (May 15 2022 at 21:54):to show that find_factors returns the same, you should proceed by induction on the decomposition, assuming that k <= the smallest decomposition factor with nonzero exponent — call that p0. You need this side condition because if k > p0, then you can output a non-prime k in the list!
Paolo Giarrusso (May 15 2022 at 21:58):if 1 < k < p0, then k does not divide any of the prime factors of n in the given decomposition. Hence you should show that k does not divide n itself — and this step seems to rely on the unicity of the prime decomposition: indeed, in “variants of the integers” without this unicity (such as IIRC m + n * sqrt(-5)), the overall theorem would fail.
Lessness (May 16 2022 at 11:27):Thank you very much!
Paolo Giarrusso (May 16 2022 at 11:42):@Lessness BTW, that unicity is also a nontrivial theorem — https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic seems to have decent sketches (also for the needed Euclid's lemma).
Karl Palmskog (May 16 2022 at 11:43):if this is related to FTA, you have FTA in CoRN: https://github.com/coq-community/corn/tree/master/fta
Paolo Giarrusso (May 16 2022 at 11:46):wait, is that the fundamental theorem of _algebra_ or _arithmetic_? We need the latter but the readme mentions the former...
Paolo Giarrusso (May 16 2022 at 11:48):okay, https://github.com/coq-community/corn/blob/master/fta/FTA.v#L188 looks closer to the algebra one — ditto Kneser's lemma and mentions of complex numbers: https://github.com/coq-community/corn/blob/master/fta/CPoly_Contin1.v#L115.
Karl Palmskog (May 16 2022 at 11:49):ah, I thought the first FTA needed the second FTA, but I may have been wrong
Paolo Giarrusso (May 16 2022 at 11:56):No idea... https://github.com/coq-contribs/fundamental-arithmetics/blob/master/primes.v#L518 is an older formalization; https://madiot.fr/coq100/ links to https://math-comp.github.io/htmldoc/mathcomp.ssreflect.prime.html but I can't see an FTA statement.
Karl Palmskog (May 16 2022 at 11:59):this looks like unique prime factorization to me (https://math-comp.github.io/htmldoc/mathcomp.ssreflect.prime.html#divisors_correct)
Lemma divisors_correct n : n > 0 →
[/\ uniq (divisors n), sorted leq (divisors n)
& ∀ d, (d \in divisors n) = (d %| n)].
Definition divisors n := foldr add_divisors [:: 1] (prime_decomp n).
I'm confused because uniq just asserts "no duplicates"
Paolo Giarrusso (May 16 2022 at 12:23):what I'm looking for is "any two prime factorizations are permutation-equal" — and they have a fancy factorization algorithm instead.
Karl Palmskog (May 16 2022 at 12:25):but it's very mathcomp-y, no? Factorization is defined as: the result of this function
Paolo Giarrusso (May 16 2022 at 12:26):no :-)
Paolo Giarrusso (May 16 2022 at 12:27):what you quote seems plausible even outside of unique factorization domains, where the same number has _different_ factorizations
Karl Palmskog (May 16 2022 at 12:41):One strange thing about divisors is that even though it's pointed to by the Coq 100 list, it doesn't output just primes.
Karl Palmskog (May 16 2022 at 12:56):ah, I think one is supposed to use the following lemmas, and the pointer in the Coq 100 list is misleading:
primes_uniq: forall n : nat, uniq (primes n)
sorted_primes: forall n : nat, sorted ltn (primes n)
primes_prime: forall [p : nat], prime p -> primes p = [:: p]
mem_primes: forall p n, (p \in primes n) = [&& prime p, 0 < n & p %| n]
All of those still hold outside unique factorization domain. They don't even imply that the product of all primes divides n.
Paolo Giarrusso (May 16 2022 at 13:18):For instance, take image.png
Paolo Giarrusso (May 16 2022 at 13:19):hmm:
However, it was also discovered that unique factorization does not always hold. An example is given by
Z[sqrt(-5)]. In this ring one has[12]6 = 2 * 3 = (1 + sqrt(-5)) (1 - sqrt(-5))`
Paolo Giarrusso (May 16 2022 at 13:21):and if you collect all irreducible divisors of 6 — (2, 3, 1 + sqrt(-5), 1 - sqrt(-5) ) and multiply them, you get 36 which doesn't divide 6.
Paolo Giarrusso (May 16 2022 at 13:23):coming back to the original question, this means that "collect all irreducible divisors of n" and "keep dividing n by irreducible divisors and recurse on the result" would give different results here
Guillaume Melquiond (May 16 2022 at 13:32):Karl Palmskog said:
ah, I think one is supposed to use the following lemmas, and the pointer in the Coq 100 list is misleading:
primes_uniq: forall n : nat, uniq (primes n) sorted_primes: forall n : nat, sorted ltn (primes n) primes_prime: forall [p : nat], prime p -> primes p = [:: p] mem_primes: forall p n, (p \in primes n) = [&& prime p, 0 < n & p %| n]
I didn't quite follow the discussion, but if you are interested in the uniqueness of decomposition into prime factors, the following lemma is the way to go:
prime_decompE n : prime_decomp n = [seq (p, logn p n) | p <- primes n]
(You also need mem_primes to make sure you have all the relevant primes and prime_decomp_correct to make sure that the product of the powered prime factors is equal to n.)
Paolo Giarrusso (May 16 2022 at 13:43):That's nicer, and it'd fail outside unique factorization domains! There's probably some extra work to show other factorization functions give the same result as well, but hopefully there's enough infrastructure for it... guess @Lessness will find out :-)
Lessness (Jul 03 2022 at 15:17):Summer started and I have more free time now.
I proved the fundamental theorem of arithmetic this way (basically following Wikipedia):
Require Import VST.floyd.proofauto.
Require Import FunInd.
Require Import Znumtheory.
Open Scope Z.
Fixpoint product (L: list Z): Z :=
match L with
| [] => 1
| x :: t => x * product t
end.
Theorem product_app (L1 L2: list Z): product (L1 ++ L2) = product L1 * product L2.
Proof.
induction L1; simpl; lia.
Qed.
Theorem prime_divisor_existence (n: Z) (H: 2 <= n):
exists p, prime p /\ Z.divide p n.
Proof.
assert (0 <= n) by lia. revert H. pattern n. apply Z_lt_induction; auto. clear n H0. intros.
destruct (prime_dec x).
+ exists x. split; auto. exists 1. lia.
+ apply not_prime_divide in n; try lia. destruct n as [n [H1 H2]]. destruct H2.
subst. assert (0 <= x0 < x0 * n) by nia. assert (2 <= x0) by nia. pose proof (H _ H2 H3).
destruct H4 as [p [H4 H5]]. exists p. split; auto. destruct H5. subst. exists (x * n). lia.
Qed.
Theorem fta_existence (n: Z) (H: 1 <= n): exists (L: list Z), Forall prime L /\ product L = n.
Proof.
assert (0 <= n) by lia. revert H. pattern n. apply Z_lt_induction; auto. intros. clear n H0.
assert (x = 1 \/ 1 < x) by lia. destruct H0.
+ subst. exists nil. simpl. repeat try split. constructor.
+ assert (2 <= x) by lia. destruct (prime_divisor_existence x H2) as [p [H3 H4]].
destruct H4. assert (1 < p) by (inversion H3; auto).
assert (0 <= x0 < x) by nia. assert (1 <= x0) by nia.
assert (x0 = 1 \/ 1 < x0) by lia. destruct H8.
- assert (x = p) by lia. exists [x]. split.
* constructor; auto. congruence.
* simpl. lia.
- assert (0 <= p < x) by nia. assert (1 <= p) by nia.
pose proof (H _ H6 H7). pose proof (H _ H9 H10). destruct H11 as [L1 H11], H12 as [L2 H12].
exists (L1 ++ L2). destruct H11, H12. split.
* apply Forall_app. auto.
* rewrite product_app. lia.
Qed.
Theorem prime_divisor_of_prime_product (p: Z) (H: prime p) (L: list Z) (H0: Forall prime L):
Z.divide p (product L) -> In p L.
Proof.
induction L.
+ simpl in *. intros. destruct H1. assert (1 < p) by (inversion H; auto).
symmetry in H1. rewrite Zmult_comm in H1. assert (p >= 0) by lia. pose proof (Zmult_one _ _ H3 H1).
lia.
+ simpl in *. inversion H0; subst; clear H0. intros. apply prime_mult in H0; auto. destruct H0.
- apply prime_div_prime in H0; auto.
- auto.
Qed.
Theorem prime_product_one_empty_list (L: list Z): Forall prime L -> product L = 1 -> L = [].
Proof.
intros. destruct L; auto. simpl in *. inversion H; subst; clear H. exfalso.
assert (1 < z) by (inversion H3; auto). assert (z >= 0) by lia. pose proof (Zmult_one _ _ H1 H0).
lia.
Qed.
Theorem Forall_elt2 A (L1 L2: list A) (x: A) (P: A -> Prop):
Forall P (L1 ++ x :: L2) -> Forall P (L1 ++ L2).
Proof.
induction L1.
+ simpl. intros. inversion H; subst; clear H. auto.
+ simpl. intros. inversion H; subst; clear H. apply IHL1 in H3. constructor; auto.
Qed.
Theorem prime_product_ge_one (L: list Z): Forall prime L -> product L >= 1.
Proof.
induction L; intros.
+ simpl. lia.
+ simpl. inversion H; subst; clear H. inversion H2. pose proof (IHL H3). nia.
Qed.
Theorem product_split (L1 L2: list Z) (x: Z): x * product (L1 ++ L2) = product (L1 ++ x :: L2).
Proof.
induction L1.
+ simpl. auto.
+ simpl. lia.
Qed.
Theorem fta_unique (n: Z) (H: 1 <= n) (L1 L2: list Z):
Forall prime L1 -> product L1 = n ->
Forall prime L2 -> product L2 = n ->
Permutation L1 L2.
Proof.
assert (0 <= n) by lia. revert H L1 L2. pattern n. apply Z_lt_induction; auto. intros. clear n H0.
assert (x = 1 \/ 2 <= x) by lia. destruct H0.
+ subst. assert (L1 = []).
{ apply prime_product_one_empty_list; auto. }
assert (L2 = []).
{ rewrite H0 in H5. apply prime_product_one_empty_list; auto. }
subst. constructor.
+ pose proof (prime_divisor_existence _ H0). destruct H6. destruct H6.
assert (Z.divide x0 (product L1)) by congruence.
assert (Z.divide x0 (product L2)) by congruence.
apply prime_divisor_of_prime_product in H8; auto.
apply prime_divisor_of_prime_product in H9; auto.
apply in_split in H8. apply in_split in H9.
destruct H8 as [l1 [l2 H8]]. destruct H9 as [l3 [l4 H9]].
rewrite H8, H9. apply Permutation_elt. destruct H7. rewrite H7 in *.
assert (product (l1 ++ l2) = x1).
{ pose proof (product_split l1 l2 x0). rewrite <- H8 in H10. rewrite H3 in H10.
assert (0 < x0) by (inversion H6; lia). nia. }
assert (product (l3 ++ l4) = x1).
{ pose proof (product_split l3 l4 x0). rewrite <- H9 in H11. rewrite H5 in H11.
assert (0 < x0) by (inversion H6; lia). nia. }
assert (Forall prime (l1 ++ l2)) by (apply Forall_elt2 with (x:=x0); congruence).
assert (Forall prime (l3 ++ l4)) by (apply Forall_elt2 with (x:=x0); congruence).
assert (1 <= x1).
{ rewrite <- H10. pose proof (prime_product_ge_one (l1 ++ l2) H12). lia. }
assert (1 < x0) by (inversion H6; lia).
assert (0 <= x1 < x1 * x0) by nia.
apply (H x1); auto.
Qed.
I hope that I proved the correct thing. :sweat_smile:
Lessness (Jul 08 2022 at 14:10):Paolo Giarrusso said:
Why does
find_factortake fuelsinstead of using measuren - k? That seems like adding extra complexity (since you will need to prove that the fuelsis enough)
Can someone help with definition of find_factor_aux where I try to use measure n - k.
Require Import VST.floyd.proofauto.
Require Import FunInd.
Require Import Znumtheory.
Open Scope Z.
Function remove_factor (n k: Z) {measure Z.to_nat n}: Z :=
if Z_le_gt_dec k 1 then n else
if Z_le_gt_dec n 1 then n else
if Zdivide_dec k n
then remove_factor (Z.div n k) k
else n.
Proof.
intros n k H _ H0 _ H1 _. destruct H1. subst. rewrite Z.div_mul; try lia. nia.
Defined.
Theorem remove_factor_ge_1 (n k: Z): 1 <= n -> 1 <= remove_factor n k.
Proof.
intros. assert (0 <= n) by lia. revert H. pattern n. apply Z_lt_induction.
+ intros. rewrite remove_factor_equation. repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec.
- apply H. destruct d. subst. rewrite Z.div_mul; try lia. nia. destruct d. subst. rewrite Z.div_mul; try lia.
- auto.
+ auto.
Qed.
Theorem remove_factor_decreasing (n k: Z) (H: k > 1) (H0: n > 1) (H1: Z.divide k n): remove_factor n k < n.
Proof.
assert (0 <= n) by lia. revert H0 H1. pattern n. apply Z_lt_induction.
+ intros. destruct H3. subst. rewrite remove_factor_equation.
repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec.
- rewrite Z.div_mul; try lia. clear d g g0.
assert (0 <= x0 < x0 * k) by nia.
destruct (Z_le_gt_dec x0 1).
* assert (x0 = 0 \/ x0 = 1) by lia. destruct H4.
++ subst. lia.
++ subst. rewrite remove_factor_equation. destruct Z_le_gt_dec.
-- lia.
-- destruct Z_le_gt_dec. lia. lia.
* destruct (Zdivide_dec k x0).
++ pose (H0 _ H3 g d). nia.
++ rewrite remove_factor_equation. repeat destruct Z_le_gt_dec; try lia.
destruct Zdivide_dec; intuition.
- exfalso. apply n0. exists x0. auto.
+ auto.
Qed.
Function find_factors_aux (p: Z * Z) { measure (fun p => match p with (k, n) => Z.to_nat (n - k) end) p }: list Z :=
match p with (k, n) =>
if Z_le_gt_dec k 1 then nil else
if Z_le_gt_dec n 1 then nil else
if Z_lt_ge_dec n k then nil else
if Zdivide_dec k n
then k :: find_factors_aux (k + 1, remove_factor n k)
else find_factors_aux (k + 1, n)
end.
Proof.
Admitted.
This seems to be correct.
Function find_factors_aux (p: Z * Z) { measure (fun p => match p with (k, n) => Z.to_nat (n - k) end) p }: list Z :=
match p with (k, n) =>
if Z_le_gt_dec k 1 then nil else
if Z_le_gt_dec n 1 then nil else
if Z_lt_ge_dec n k then nil else
if Zdivide_dec k n
then if Z_le_gt_dec (remove_factor n k) k
then k :: nil
else k :: find_factors_aux (k + 1, remove_factor n k)
else find_factors_aux (k + 1, n)
end.
Proof.
+ intros _ k n _ H _ H0 _ H1 _ H2 _ H3 _. pose proof (remove_factor_decreasing _ _ H H0 H2). lia.
+ intros _ k n _ H _ H0 _ H1 _ H2 _. assert (n = k \/ n > k) by lia. destruct H3.
- exfalso. apply H2. exists 1. lia.
- lia.
Defined.
FWIW, see also https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/.E2.9C.94.20Unicity.20of.20prime.20decomposition
Last updated: Oct 03 2023 at 01:35 UTC