Merge pull request #2062 from Alizter/ps/rr/prime_factorisation

prime factorization

theories/Basics.v

@@ -8,6 +8,7 @@ Require Export Basics.Utf8.
 Require Export Basics.Notations.
 Require Export Basics.Tactics.
 Require Export Basics.Classes.
+Require Export Basics.Iff.
 
 Require Export Basics.Nat.
 Require Export Basics.Numeral.

theories/Basics/Decidable.v

@@ -3,7 +3,8 @@ Require Import
   Basics.Overture
   Basics.PathGroupoids
   Basics.Trunc
-  Basics.Tactics.
+  Basics.Tactics
+  Basics.Iff.
 Local Open Scope trunc_scope.
 Local Open Scope path_scope.
 
@@ -85,6 +86,13 @@ Proof.
   exact (nnnp (fun np => np p)).
 Defined.
 
+Definition iff_stable P `(Stable P) : ~~P <-> P.
+Proof.
+  split.
+  - apply stable.
+  - exact (fun x f => f x).
+Defined.
+
 (**
   Because [vm_compute] evaluates terms in [PROP] eagerly
   and does not remove dead code we
@@ -122,21 +130,21 @@ Global Instance decidable_empty : Decidable Empty
 
 (** ** Transfer along equivalences *)
 
-Definition decidable_iff {A B} (f : A -> B) (f' : B -> A)
+Definition decidable_iff {A B} (f : A <-> B)
   : Decidable A -> Decidable B.
 Proof.
   intros [a|na].
-  - exact (inl (f a)).
-  - exact (inr (fun b => na (f' b))).
+  - exact (inl (fst f a)).
+  - exact (inr (fun b => na (snd f b))).
 Defined.
 
-Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
-  : Decidable A -> Decidable B
-  := decidable_iff f f^-1.
-
 Definition decidable_equiv' (A : Type) {B : Type} (f : A <~> B)
 : Decidable A -> Decidable B
-  := decidable_equiv A f.
+  := decidable_iff f.
+
+Definition decidable_equiv (A : Type) {B : Type} (f : A -> B) `{!IsEquiv f}
+: Decidable A -> Decidable B
+  := decidable_equiv' _ (Build_Equiv _ _ f _).
 
 Definition decidablepaths_equiv
            (A : Type) {B : Type} (f : A -> B) `{IsEquiv A B f}
@@ -261,3 +269,37 @@ Proof.
   - elim (nd d').
   - apply ap, path_forall; intros p; elim (nd p).
 Defined.
+
+(** ** Logical Laws *)
+
+(** Various logical laws don't hold constructively as they do classically due to a required use of excluded middle. For us, this means that some laws require further assumptions on the decidability of propositions. *)
+
+(** Here we give the dual De Morgan's Law which complements the one given in Iff.v.  One direction requires that one of the two propositions be decidable, while the other direction needs no assumption.  We state the latter property first, to avoid duplication in the proof. *)
+Definition not_prod_sum_not A B : ~ A + ~ B -> ~ (A * B).
+Proof.
+  intros [na|nb] [a b].
+  - exact (na a).
+  - exact (nb b).
+Defined.
+
+Definition iff_not_prod A B `{Decidable A}
+  : ~ (A * B) <-> ~ A + ~ B.
+Proof.
+  split.
+  - intros np.
+    destruct (dec A) as [a|na].
+    + exact (inr (fun b => np (a, b))).
+    + exact (inl na).
+  - apply not_prod_sum_not.
+Defined.
+
+Definition iff_not_prod' A B `{Decidable B}
+  : ~ (A * B) <-> ~ A + ~ B.
+Proof.
+  split.
+  - intros np.
+    destruct (dec B) as [b|nb].
+    + exact (inl (fun a => np (a, b))).
+    + exact (inr nb).
+  - apply not_prod_sum_not.
+Defined.

theories/Basics/Equivalences.v

@@ -80,9 +80,6 @@ Ltac change_apply_equiv_compose :=
     change ((f oE g) x) with (f (g x))
   end.
 
-Definition iff_equiv {A B : Type} (f : A <~> B)
-  : A <-> B := (equiv_fun f, f^-1).
-
 (** Transporting is an equivalence. *)
 Section EquivTransport.
 

theories/Basics/Iff.v

@@ -0,0 +1,60 @@
+Require Import Basics.Overture Basics.Tactics.
+
+Local Set Universe Minimization ToSet.
+
+(** * If and only if *)
+
+(** ** Definition *)
+
+(** [iff A B], written [A <-> B], expresses the logical equivalence of [A] and [B] *)
+Definition iff (A B : Type) := prod (A -> B) (B -> A).
+
+Notation "A <-> B" := (iff A B) : type_scope.
+
+(** ** Basic Properties *)
+
+(** Everything is logically equivlaent to itself. *)
+Definition iff_refl {A} : A <-> A
+  := (idmap , idmap).
+
+(** [iff] is a reflexive relation. *)
+Global Instance iff_reflexive : Reflexive iff | 1
+  := @iff_refl.
+
+(** Logical equivalences can be inverted. *)
+Definition iff_inverse {A B} : (A <-> B) -> (B <-> A)
+  :=  fun f => (snd f , fst f).
+
+(** [iff] is a symmetric relation. *)
+Global Instance symmetric_iff : Symmetric iff | 1
+  := @iff_inverse.
+
+(** Logical equivalences can be composed. *)
+Definition iff_compose {A B C} (f : A <-> B) (g : B <-> C) : A <-> C
+  := (fst g o fst f , snd f o snd g).
+
+(** [iff] is a transitive relation. *)
+Global Instance transitive_iff : Transitive iff | 1
+  := @iff_compose.
+
+(** Any equivalence can be considered a logical equivalence by discarding everything but the maps. We make this a coercion so that equivalences can be used in place of logical equivalences. *)
+Coercion iff_equiv {A B : Type} (f : A <~> B)
+  : A <-> B := (equiv_fun f, f^-1).
+
+(** ** Logical Laws *)
+
+(** One of De Morgan's Laws.  The dual statement about negating a product appears in Decidable.v due to decidability requirements. *)
+Definition iff_not_sum A B : ~ (A + B) <-> ~ A * ~ B.
+Proof.
+  split.
+  - intros ns.
+    exact (ns o inl, ns o inr).
+  - by intros []; snrapply sum_ind.
+Defined.
+
+Definition iff_contradiction A : A * ~A <-> Empty.
+Proof.
+  split.
+  - intros [a na]; exact (na a).
+  - intros e; exact (Empty_rec _ e).
+Defined.

theories/Basics/Overture.v

@@ -73,13 +73,6 @@ Notation conj := pair (only parsing).
 
 #[export] Hint Resolve pair inl inr : core.
 
-(** If and only if *)
-
-(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
-Definition iff (A B : Type) := prod (A -> B) (B -> A).
-
-Notation "A <-> B" := (iff A B) : type_scope.
-
 (** ** Type classes *)
 
 (** This command prevents Coq from trying to guess the values of existential variables while doing typeclass resolution.  If you don't know what that means, ignore it. *)
@@ -224,20 +217,6 @@ Notation "g 'o' f" := (compose g%function f%function) : function_scope.
 (** This definition helps guide typeclass inference. *)
 Definition Compose {A B C : Type} (g : B -> C) (f : A -> B) : A -> C := compose g f.
 
-(** Composition of logical equivalences *)
-Global Instance iff_compose : Transitive iff | 1
-  := fun A B C f g => (fst g o fst f , snd f o snd g).
-Arguments iff_compose {A B C} f g : rename.
-
-(** While we're at it, inverses of logical equivalences *)
-Global Instance iff_inverse : Symmetric iff | 1
-  := fun A B f => (snd f , fst f).
-Arguments iff_inverse {A B} f : rename.
-
-(** And reflexivity of them *)
-Global Instance iff_reflexive : Reflexive iff | 1
-  := fun A => (idmap , idmap).
-
 (** Dependent composition of functions. *)
 Definition composeD {A B C} (g : forall b, C b) (f : A -> B) := fun x : A => g (f x).
 

theories/Basics/Trunc.v

@@ -7,7 +7,8 @@ Require Import
   Basics.Contractible
   Basics.Equivalences
   Basics.Tactics
-  Basics.Nat.
+  Basics.Nat
+  Basics.Iff.
 
 Local Set Universe Minimization ToSet.
 

theories/Categories/Structure/IdentityPrinciple.v

@@ -2,7 +2,7 @@
 Require Import Category.Core Category.Univalent Category.Morphisms.
 Require Import Structure.Core.
 Require Import Types.Sigma Trunc Equivalences.
-Require Import Basics.Tactics.
+Require Import Basics.Iff Basics.Tactics.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.

theories/PropResizing/Nat.v

@@ -149,8 +149,7 @@ Section AssumeStuff.
     Qed.
 
     Definition graph_unsucc_equiv_vert@{} : vert A <~> vert B
-      := equiv_unfunctor_sum_l@{s s s s s  s Set Set Set Set}
-                              f Ha Hb.
+      := equiv_unfunctor_sum_l@{s s s s s s} f Ha Hb.
 
     Definition graph_unsucc_equiv_edge@{} (x y : vert A)
       : iff@{s s s} (edge A x y) (edge B (graph_unsucc_equiv_vert x) (graph_unsucc_equiv_vert y)).

theories/Spaces/Finite/Fin.v

@@ -267,7 +267,7 @@ Proof.
   assert (p' := (moveL_equiv_V _ _ p)^).
   exists y.
   destruct y as [y|[]].
-  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set}
+  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set}
               (fin_transpose_last_with m (inl y) oE e)
               _ _ ; _).
     { intros a. ev_equiv.
@@ -286,7 +286,7 @@ Proof.
     * rewrite unfunctor_sum_l_beta.
       apply fin_transpose_last_with_invol.
     * refine (fin_transpose_last_with_last _ _ @ p^).
-  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set} e _ _ ; _).
+  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set} e _ _ ; _).
     { intros a.
       destruct (is_inl_or_is_inr (e (inl a))) as [l|r].
       - exact l.

theories/Spaces/Int.v

@@ -124,8 +124,9 @@ Proof.
   2-4,6-8: right; intros; discriminate.
   2: by left.
   1,2: nrapply decidable_iff.
-  1,4: nrapply ap.
-  1,3: intros H; by injection H.
+  1,3: split.
+  1,3: nrapply ap.
+  1,2: intros H; by injection H.
   1,2: exact _.
 Defined.
 

theories/Spaces/List/Core.v

@@ -193,3 +193,12 @@ Fixpoint for_all@{i j|} {A : Type@{i}} (P : A -> Type@{j}) l : Type@{j} :=
   | nil => Unit
   | x :: l => P x /\ for_all P l
   end.
+
+(** ** Exists *)
+
+(** Apply a predicate to all elements of a list and take their disjunction. *)
+Fixpoint list_exists@{i j|} {A : Type@{i}} (P : A -> Type@{j}) l : Type@{j} :=
+  match l with
+  | nil => Empty
+  | x :: l => P x + list_exists P l
+  end.