Merge pull request HoTT#2199 from jdchristensen/decidable-exists

Variants of decidable_exists_nat; add leq_ind_l

theories/BoundedSearch.v

@@ -1,11 +1,15 @@
-Require Import HoTT.Basics HoTT.Types.
-Require Import HoTT.Truncations.Core.
-Require Import HoTT.Spaces.Nat.Core.
+(** * Bounded Search *)
+
+(** The main result of this file is [minimal_n], which say that if [P : nat -> Type] is a family such that each [P n] is decidable and [{n & P n}] is merely inhabited, then [{n & P n}] is inhabited.  Since [P n] is decidable, it is sufficient to prove [{n & merely (P n)}], and to do this, we prove the stronger claim that there is a *minimal* [n] satisfying [merely (P n)].  This stronger claim is a proposition, which is what makes the argument work.  Along the way, we also prove that [{ l : nat & (l <= n) * P l }] is decidable for each [n]. *)
+
+Require Import Basics.Overture Basics.Decidable Basics.Trunc Basics.Tactics.
+Require Import Types.Sigma Types.Prod.
+Require Import Truncations.Core.
+Require Import Spaces.Nat.Core.
 
 Section bounded_search.
 
-  Context (P : nat -> Type)
-          (P_dec : forall n, Decidable (P n)).
+  Context (P : nat -> Type) (P_dec : forall n, Decidable (P n)).
 
   (** We open type_scope again after nat_scope in order to use the product type notation. *)
   Local Open Scope nat_scope.
@@ -40,59 +44,56 @@ Section bounded_search.
   Local Definition bounded_search (n : nat) : smaller n + forall l : nat, (l <= n) -> not (P l).
   Proof.
     induction n as [|n IHn].
-    - assert (P 0 + not (P 0)) as X; [apply P_dec |].
-      destruct X as [h|].
+    - destruct (dec (P 0)) as [h|n].
       + left.
-        refine (0;(h,_,_)).
-        * intros ? ?. exact _.
+        exact (0; (h, fun _ _ => _, _)).
       + right.
         intros l lleq0.
-        assert (l0 : l = 0) by rapply leq_antisym.
-        rewrite l0; assumption.
-    - destruct IHn as [|n0].
-      + left. apply smaller_S. assumption.
-      + assert (P (n.+1) + not (P (n.+1))) as X by apply P_dec.
-        destruct X as [h|].
+        by rewrite (leq_antisym lleq0 _ : l = 0).
+    - destruct IHn as [s|n0].
+      + left; by apply smaller_S.
+      + destruct (dec (P n.+1)) as [h|nP].
         * left.
-          refine (n.+1;(h,_,_)).
-          -- intros m pm.
-             assert ((n.+1 <= m)+(n.+1>m)) as X by apply leq_dichotomy.
-             destruct X as [leqSnm|ltmSn].
-             ++ assumption.
-             ++ unfold gt, lt in ltmSn.
-                assert (m <= n) as X by rapply leq_pred'.
-                destruct (n0 m X pm).
-        * right. intros l q.
-          assert ((l <= n) + (l > n)) as X by apply leq_dichotomy.
-          destruct X as [h|h].
-          -- exact (n0 l h).
-          -- unfold lt in h.
-             assert (eqlSn : l = n.+1) by (apply leq_antisym; assumption).
-             rewrite eqlSn; assumption.
+          refine (n.+1; (h, _, _)).
+          intros m pm.
+          apply leq_iff_not_gt.
+          unfold gt, lt; intro leq_Sm_Sn.
+          apply leq_pred' in leq_Sm_Sn.
+          destruct (n0 m leq_Sm_Sn pm).
+        * right.
+          by apply leq_ind_l.
   Defined.
 
   Local Definition n_to_min_n (n : nat) (Pn : P n) : min_n_Type.
   Proof.
-    assert (smaller n + forall l, (l <= n) -> not (P l)) as X by apply bounded_search.
-    destruct X as [[l [[Pl ml] leqln]]|none].
-    - exact (l;(tr Pl,tr ml)).
+    destruct (bounded_search n) as [[l [[Pl ml] _]] | none].
+    - exact (l; (tr Pl, tr ml)).
     - destruct (none n (leq_refl n) Pn).
   Defined.
 
-  Local Definition prop_n_to_min_n (P_inhab : hexists (fun n => P n))
-    : min_n_Type.
+  Local Definition prop_n_to_min_n (P_inhab : hexists P) : min_n_Type.
   Proof.
-    refine (Trunc_rec _ P_inhab).
-    intros [n Pn]. exact (n_to_min_n n Pn).
+    strip_truncations.
+    exact (n_to_min_n (P_inhab.1) (P_inhab.2)).
   Defined.
 
-  Definition minimal_n (P_inhab : hexists (fun n => P n))
-    : { n : nat & P n }.
+  Definition minimal_n (P_inhab : hexists P) : { n : nat & P n }.
   Proof.
-    destruct (prop_n_to_min_n P_inhab) as [n pl]. destruct pl as [p _].
+    destruct (prop_n_to_min_n P_inhab) as [n [p _]].
     exact (n; fst merely_inhabited_iff_inhabited_stable p).
   Defined.
 
+  (** As a consequence of [bounded_search] we deduce that bounded existence is decidable.  See also [decidable_exists_bounded_nat] in Spaces/Lists/Theory.v for a similar result with different dependencies. *)
+  Definition decidable_search (n : nat) : Decidable { l : nat & (l <= n) * P l }.
+  Proof.
+    destruct (bounded_search n) as [s | no_l].
+    - destruct s as [l [[Pl min] l_leq_n]].
+      exact (inl (l; (l_leq_n, Pl))).
+    - right.
+      intros [l [l_leq_n Pl]].
+      exact (no_l l l_leq_n Pl).
+  Defined.
+
 End bounded_search.
 
 Section bounded_search_alt_type.
@@ -101,14 +102,14 @@ Section bounded_search_alt_type.
           (e : nat <~> X)
           (P : X -> Type)
           (P_dec : forall x, Decidable (P x))
-          (P_inhab : hexists (fun x => P x)).
+          (P_inhab : hexists P).
 
   (** Bounded search works for types equivalent to the naturals even without full univalence. *)
   Definition minimal_n_alt_type : {x : X & P x}.
   Proof.
-    set (P' n := P (e n)).
-    assert (P'_dec : forall n, Decidable (P' n)) by apply _.
-    assert (P'_inhab : hexists (fun n => P' n)).
+    pose (P' n := P (e n)).
+    pose (P'_dec n := P_dec (e n) : Decidable (P' n)).
+    assert (P'_inhab : hexists P').
     {
       strip_truncations. apply tr.
       destruct P_inhab as [x p].
@@ -117,7 +118,7 @@ Section bounded_search_alt_type.
       rewrite (eisretr e). exact p.
     }
     destruct (minimal_n P' P'_dec P'_inhab) as [n p'].
-    exists (e n). exact p'.
+    exact ((e n); p').
   Defined.
 
 End bounded_search_alt_type.

theories/Spaces/List/Theory.v

@@ -1249,3 +1249,9 @@ Proof.
   1: exact H1.
   exact _.
 Defined.
+
+(** A common special case.  See also [decidable_search] in BoundedSearch.v for a similar result with different dependencies. *)
+Definition decidable_exists_bounded_nat (n : nat) (P : nat -> Type)
+  (H2 : forall k, Decidable (P k))
+  : Decidable { k : nat & prod (k < n) (P k) }
+  := decidable_exists_nat n _ (fun k => fst) _.

theories/Spaces/Nat/Core.v

@@ -434,12 +434,15 @@ Proof.
 Defined.
 Global Existing Instance leq_zero_l | 10.
 
+Global Instance pred_leq {m} : nat_pred m <= m.
+Proof.
+  destruct m; exact _.
+Defined.
+
 (** A predecessor is less than or equal to a predecessor if the original number is less than or equal. *)
 Global Instance leq_pred {n m} : n <= m -> nat_pred n <= nat_pred m.
 Proof.
-  intros H; induction H.
-  1: exact _.
-  destruct m; exact _.
+  intros H; induction H; exact _.
 Defined.
 
 (** A successor is less than or equal to a successor if the original numbers are less than or equal. *)
@@ -501,6 +504,12 @@ Proof.
   exact _.
 Defined.
 
+(** [n.+1 <= m] implies [n <= m]. *)
+Definition leq_succ_l {n m} : n.+1 <= m -> n <= m.
+Proof.
+  intro l; apply leq_pred'; exact _.
+Defined.
+
 (** A general form for injectivity of this constructor *)
 Definition leq_refl_inj_gen n k (p : n <= k) (r : n = k) : p = r # leq_refl n.
 Proof.
@@ -568,10 +577,16 @@ Proof.
       apply equiv_leq_succ.
 Defined.
 
-(** [n.+1 <= m] implies [n <= m]. *)
-Definition leq_succ_l {n m} : n.+1 <= m -> n <= m.
+(** The default induction principle for [leq] applies to a type family depending on the second variable.  Here is a version involving a type family depending on the first variable. *)
+Definition leq_ind_l {n : nat} (Q : forall (m : nat) (l : m <= n.+1), Type)
+  (H_Sn : Q n.+1 (leq_refl n.+1))
+  (H_m : forall (m : nat) (l : m <= n), Q m (leq_succ_r l))
+  : forall (m : nat) (l : m <= n.+1), Q m l.
 Proof.
-  intro l; apply leq_pred'; exact _.
+  intros m leq_m_Sn.
+  inversion leq_m_Sn as [p | k H p]; destruct p^; clear p.
+  - exact (path_ishprop _ _ # H_Sn).
+  - exact (path_ishprop _ _ # H_m _ _).
 Defined.
 
 (** *** Basic properties of [<] *)
@@ -995,6 +1010,14 @@ Proof.
   1: right; exact _.
 Defined.
 
+(** A variant. *)
+Definition leq_succ_dichotomy {n m : nat} (l : m <= n.+1) : (m = n.+1) + (m <= n).
+Proof.
+  inversion l.
+  - left; reflexivity.
+  - right; assumption.
+Defined.
+
 (** *** Trichotomy *)
 
 (** Any two natural numbers are either equal, less than, or greater than each other. *)