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

theories/Basics/Overture.v

@@ -2,7 +2,7 @@
 
 (** * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)
 (** Import the file of reserved notations so we maintain consistent level notations throughout the library *)
 Require Export Basics.Settings Basics.Notations.
 
 Local Set Polymorphic Inductive Cumulativity.
 
@@ -75,7 +75,7 @@
 
 (** 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 @@
 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

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/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@{k k k} (InList@{k} x (list_filter@{u v} l P dec)) (InList@{u} x l /\ P x).
 Proof.
   simple_list_induction l a l IHl.
   - simpl.
-    symmetry.
-    apply iff_equiv.
-    snrapply prod_empty_l.
+    apply iff_inverse@{k k k}.
+    apply iff_equiv@{k k k}.
+    snrapply prod_empty_l@{k k k}.
   - simpl.
-    etransitivity.
-    2: { apply iff_equiv.
-         exact ((sum_distrib_r _ _ _)^-1%equiv). }
+    nrapply iff_compose@{k k k k k k}.
+    2: { apply iff_inverse@{k k k}.
+         apply iff_equiv@{k k k}.
+         exact (sum_distrib_r@{k k k k k k k k} _ _ _). }
     destruct (dec a) as [p|p].
     + simpl.
-      transitivity ((a = x) + InList 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.
+      snrapply iff_compose@{k k k k k k}.
+      1: exact (sum@{k k} (a = x) (prod@{k k} (InList@{u} x l) (P x))).
+      1: split; apply functor_sum@{k k k k}; only 1,3: exact idmap; apply IHl.
+      split; apply functor_sum@{k k k k}; only 2,4: apply idmap.
+      * intros [].
+        exact (idpath, p).
       * exact fst.
-    + etransitivity.
+    + nrapply iff_compose@{k k k k k k}. 
       1: apply IHl.
-      apply iff_equiv.
-      nrefine (_ oE (sum_empty_l _)^-1%equiv).
-      snrapply equiv_functor_sum'.
-      2: reflexivity.
-      symmetry; apply equiv_to_empty.
+      apply iff_inverse@{k k k}.
+      apply iff_equiv@{k k k}.
+      nrefine (equiv_compose'@{k k k} (sum_empty_l@{k} _) _).
+      snrapply equiv_functor_sum'@{k k k k k k}.
+      2: exact (equiv_idmap@{k}).
+      apply equiv_to_empty@{k}.
       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.
@@ -1111,11 +1115,39 @@ 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.

theories/Spaces/Nat/Core.v

@@ -590,6 +590,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) := _.