prime factorization

theories/Basics/Decidable.v

@@ -85,6 +85,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 +129,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}

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/Overture.v

@@ -75,7 +75,7 @@ Notation conj := pair (only parsing).
 
 (** If and only if *)
 
-(** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
+(** [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.
@@ -225,14 +225,18 @@ Notation "g 'o' f" := (compose g%function f%function) : function_scope.
 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.
+Definition iff_compose {A B C} (f : A <-> B) (g : B <-> C) : A <-> C
+  := (fst g o fst f , snd f o snd g).
+
+Global Instance transitive_iff : Transitive iff | 1
+  := @iff_compose.
 
 (** 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.
+Definition iff_inverse {A B} : (A <-> B) -> (B <-> A)
+  :=  fun f => (snd f , fst f).
+
+Global Instance symmetric_iff : Symmetric iff | 1
+  := @iff_inverse.
 
 (** And reflexivity of them *)
 Global Instance iff_reflexive : Reflexive iff | 1
@@ -532,6 +536,9 @@ Notation "f ^-1" := (@equiv_inv _ _ f _) : function_scope.
 Definition ap10_equiv {A B : Type} {f g : A <~> B} (h : f = g) : f == g
   := ap10 (ap equiv_fun h).
 
+Coercion iff_equiv {A B : Type} (f : A <~> B)
+  : A <-> B := (equiv_fun f, f^-1).
+
 (** ** Contractibility and truncation levels *)
 
 (** Truncation measures how complicated a type is.  In this library, a witness that a type is n-truncated is formalized by the [IsTrunc n] typeclass.  In many cases, the typeclass machinery of Coq can automatically infer a witness for a type being n-truncated.  Because [IsTrunc n A] itself has no computational content (that is, all witnesses of n-truncation of a type are provably equal), it does not matter much which witness Coq infers.  Therefore, the primary concerns in making use of the typeclass machinery are coverage (how many goals can be automatically solved) and speed (how long does it take to solve a goal, and how long does it take to error on a goal we cannot automatically solve).  Careful use of typeclass instances and priorities, which determine the order of typeclass resolution, can be used to effectively increase both the coverage and the speed in cases where the goal is solvable.  Unfortunately, typeclass resolution tends to spin for a while before failing unless you're very, very, very careful.  We currently aim to achieve moderate coverage and fast speed in solvable cases.  How long it takes to fail typeclass resolution is not currently considered, though it would be nice someday to be even more careful about things.

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.

theories/Spaces/List/Theory.v

@@ -719,7 +719,7 @@ Defined.
 (** *** Filter *)
 
 (** Produce the list of elements of a list that satisfy a decidable predicate. *)
-Fixpoint list_filter {A : Type} (l : list A) (P : A -> Type)
+Fixpoint list_filter@{u v|} {A : Type@{u}} (l : list A) (P : A -> Type@{v})
   (dec : forall x, Decidable (P x))
   : list A
   := match l with
@@ -729,33 +729,37 @@ Fixpoint list_filter {A : Type} (l : list A) (P : A -> Type)
         else list_filter l P dec
     end.
 
-Definition inlist_filter {A : Type} (l : list A) (P : A -> Type)
-  (dec : forall x, Decidable (P x)) (x : A)
-  : InList x (list_filter l P dec) <-> InList x l /\ P x.
+Definition inlist_filter@{u v k | u <= k, v <= k} {A : Type@{u}} (l : list A)
+  (P : A -> Type@{v}) (dec : forall x, Decidable (P x)) (x : A)
+  : iff@{u k k} (InList x (list_filter l P dec)) (InList x l /\ P x).
 Proof.
   simple_list_induction l a l IHl.
   - simpl.
-    symmetry.
+    apply iff_inverse.
     apply iff_equiv.
-    snrapply prod_empty_l.
+    snrapply prod_empty_l@{v}.
   - simpl.
-    etransitivity.
-    2: { apply iff_equiv.
-         exact ((sum_distrib_r _ _ _)^-1%equiv). }
+    nrapply iff_compose.
+    2: { apply iff_inverse.
+         apply iff_equiv.
+         exact (sum_distrib_r@{k k k _ _ _ k k} _ _ _). }
     destruct (dec a) as [p|p].
     + simpl.
-      transitivity ((a = x) + InList x l * P x).
+      snrapply iff_compose.
+      1: exact (sum (a = x) (prod (InList@{u} x l) (P x))).
       1: split; apply functor_sum; only 1,3: exact idmap; apply IHl.
-      split; apply functor_sum; only 2,4: apply idmap.
-      * intros []; by split.
+      split; apply functor_sum@{k k k k}; only 2,4: apply idmap.
+      * intros [].
+        exact (idpath, p).
       * exact fst.
-    + etransitivity.
+    + nrapply iff_compose.
       1: apply IHl.
+      apply iff_inverse.
       apply iff_equiv.
-      nrefine (_ oE (sum_empty_l _)^-1%equiv).
-      snrapply equiv_functor_sum'.
-      2: reflexivity.
-      symmetry; apply equiv_to_empty.
+      nrefine (equiv_compose'@{k k k} (sum_empty_l@{k} _) _).
+      snrapply equiv_functor_sum'@{k k k k k k}.
+      2: exact equiv_idmap.
+      apply equiv_to_empty.
       by intros [[] r].
 Defined.
 
@@ -920,7 +924,7 @@ Proof.
   nrefine (_ oE (equiv_inlist_app _ _ _)^-1).
   nrefine (_ oE equiv_functor_sum' (B':=x = n) IHn _).
   2: { simpl.
-       exact (equiv_path_inverse _ _ oE sum_empty_r@{Set Set Set} _). }
+       exact (equiv_path_inverse _ _ oE sum_empty_r@{Set} _). }
   nrefine (_ oE equiv_leq_lt_or_eq^-1).
   rapply equiv_iff_hprop.
 Defined.
@@ -993,7 +997,7 @@ Proof.
   by apply for_all_list_map.
 Defined.
 
-(** If a predicate [P] and a prediate [Q] together imply a predicate [R], then [for_all P l] and [for_all Q l] together imply [for_all R l]. There are also some side conditions for the default elements. *)
+(** If a predicate [P] and a predicate [Q] together imply a predicate [R], then [for_all P l] and [for_all Q l] together imply [for_all R l]. There are also some side conditions for the default elements. *)
 Lemma for_all_list_map2 {A B C : Type}
   (P : A -> Type) (Q : B -> Type) (R : C -> Type)
   (f : A -> B -> C) (Hf : forall x y, P x -> Q y -> R (f x y))
@@ -1111,11 +1115,67 @@ Global Instance decidable_for_all {A : Type} (P : A -> Type)
   `{forall x, Decidable (P x)} (l : list A)
   : Decidable (for_all P l).
 Proof.
-  induction l as [|x l IHl].
-  - exact (inl tt).
-  - destruct IHl as [Hl | Hl].
-    + destruct (dec (P x)) as [Hx | Hx].
-      * exact (inl (Hx, Hl)).
-      * exact (inr (fun H => Hx (fst H))).
-    + exact (inr (fun H => Hl (snd H))).
+  simple_list_induction l x l IHl; exact _.
+Defined.
+
+(** If a predicate [P] is decidable then so is [list_exists P]. *)
+Global Instance decidable_list_exists {A : Type} (P : A -> Type)
+  `{forall x, Decidable (P x)} (l : list A)
+  : Decidable (list_exists P l).
+Proof.
+  simple_list_induction l x l IHl; exact _.
+Defined.
+
+Definition inlist_list_exists {A : Type} (P : A -> Type) (l : list A)
+  : list_exists P l -> exists (x : A), InList x l /\ P x.
+Proof.
+  simple_list_induction l x l IHl.
+  1: done.
+  simpl.
+  intros [Px | ex].
+  - exists x.
+    by split; [left|].
+  - destruct (IHl ex) as [x' [H Px']].
+    exists x'.
+    by split; [right|].
+Defined.
+
+Definition list_exists_inlist {A : Type} (P : A -> Type) (l : list A)
+  : forall (x : A), InList x l -> P x -> list_exists P l.
+Proof.
+  simple_list_induction l x l IHl.
+  1: trivial.
+  simpl; intros y H p; revert H.
+  apply functor_sum.
+  - exact (fun r => r^ # p).
+  - intros H.
+    by apply (IHl y).
+Defined.
+
+Definition list_exists_seq {n : nat} (P : nat -> Type)
+  (H : forall k, P k -> (k < n)%nat)
+  : (exists k, P k) <-> list_exists P (seq n).
+Proof.
+  split.
+  - intros [k p].
+    snrapply (list_exists_inlist P _ k _ p).
+    apply inlist_seq, H.
+    exact p.
+  - intros H1.
+    apply inlist_list_exists in H1.
+    destruct H1 as [k [Hk p]].
+    exists k.
+    exact p.
+Defined.
+
+(** An upper bound on witnesses of a decidable predicate makes the sigma type decidable. *)
+Definition decidable_exists_nat (n : nat) (P : nat -> Type)
+  (H1 : forall k, P k -> (k < n)%nat)
+  (H2 : forall k, Decidable (P k))
+  : Decidable (exists k, P k).
+Proof.
+  nrapply decidable_iff.
+  1: apply iff_inverse; nrapply list_exists_seq.
+  1: exact H1.
+  exact _.
 Defined.

theories/Spaces/Nat/Core.v

@@ -487,6 +487,14 @@ Global Instance antisymmetric_leq : AntiSymmetric leq := @leq_antisym.
 Global Instance antisymemtric_geq : AntiSymmetric geq
   := fun _ _ p q => leq_antisym q p.
 
+(** Every natural number is zero or greater than zero. *)
+Definition nat_zero_or_gt_zero n : (0 = n) + (0 < n).
+Proof.
+  induction n as [|n IHn].
+  1: left; reflexivity.
+  right; exact _.
+Defined.
+
 (** Being less than or equal to [0] implies being [0]. *)
 Definition path_zero_leq_zero_r n : n <= 0 -> n = 0.
 Proof.
@@ -590,6 +598,7 @@ Hint Immediate leq_lt : typeclass_instances.
 
 Definition lt_trans {n m k} : n < m -> m < k -> n < k
   := fun H1 H2 => leq_lt (lt_leq_lt_trans H1 H2).
+Hint Immediate lt_trans : typeclass_instances.
 
 Global Instance transitive_lt : Transitive lt := @lt_trans.
 Global Instance ishprop_lt n m : IsHProp (n < m) := _.