Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

prime factorization #2062

Merged
merged 18 commits into from
Aug 29, 2024
Merged

prime factorization #2062

Changes from 1 commit
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
1e5f9aa
prime factorisation
Alizter Aug 18, 2024
28ccbaf
Types/Prod: fewer universe vars in prod_empty_l/r; adjust List/Theory
jdchristensen Aug 19, 2024
1321592
Types/Prod: get rid of a free universe variable in decidable_prod
jdchristensen Aug 19, 2024
73b4831
List/Theory: remove some universe annotations and fix typo
jdchristensen Aug 19, 2024
7e9a44b
Nat/Division: simplify proof of prime_factorization
jdchristensen Aug 19, 2024
7ed8566
modify prime_factorization condition
Alizter Aug 26, 2024
d9bb286
move iff_equiv and make coercion
Alizter Aug 26, 2024
21a475d
chnage decidable_iff to take an iff
Alizter Aug 26, 2024
f636050
add decidability of exists for nat pred with upper bounds on witnesses
Alizter Aug 26, 2024
37191ca
Show IsPrime is a hprop under funext
Alizter Aug 26, 2024
e816daf
tighten not_isprime_iff_iscomposite
Alizter Aug 26, 2024
a6b91ff
Fix typo: iff_contradiciton -> iff_contradiction
jdchristensen Aug 28, 2024
8209a09
Types/Sum: simplify a couple of proofs
jdchristensen Aug 28, 2024
8bfcd83
Nat/Division: change k to a in one spot
jdchristensen Aug 28, 2024
4e44bd1
Consolidate iff results in one palce
Alizter Aug 28, 2024
7def66f
remove moved lemmas
Alizter Aug 28, 2024
31758a0
add further comments about seperation of de morgan laws
Alizter Aug 28, 2024
a68adca
Decidable.v: One of De Morgan's laws only needs one arg to be decidable
jdchristensen Aug 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 16 additions & 0 deletions theories/Spaces/Nat/Division.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -673,6 +673,22 @@ Class IsPrime (n : nat) : Type0 := {

Definition issig_IsPrime n : _ <~> IsPrime n := ltac:(issig).

Global Instance ishprop_isprime `{Funext} n : IsHProp (IsPrime n).
jdchristensen marked this conversation as resolved.
Show resolved Hide resolved
Proof.
nrapply istrunc_equiv_istrunc.
1: apply issig_IsPrime.
rapply istrunc_sigma.
intros H1.
snrapply istrunc_forall.
intros m.
snrapply istrunc_forall.
intros d.
rapply ishprop_sum.
intros p q.
nrapply (snd neq_iff_lt_or_gt _ (p^ @ q)).
by left.
Defined.

(** [0] is not a prime number. *)
Definition not_isprime_zero : ~ IsPrime 0.
Proof.
Expand Down