Variants of decidable_exists_nat

[jdchristensen]

I noticed that there are two ways to prove that it's decidable whether a bounded natural satisfies a decidable predicate. One is already in List/Theory, which I extended with decidable_exists_bounded_nat. But BoundedSearch essentially proves this as well, as I illustrate with decidable_search.

On the one hand, it's nice that BoundedSearch avoids needing to use lists. On the other hand, BoundedSearch requires merely, which currently requires Modalities (although I suspect this dependency can easily be removed with some reorganization).

Maybe it's worth having both? If so, I'll add comments pointing each one to the other. Or, we could just keep one.

Incidentally, the one in List/Theory is hard to find. Since the statement of the lemma doesn't involve lists, it's not an obvious place to look. Is there somewhere else that would make sense to put it? (The reason I proved the version using bounded search is because I didn't remember that there was a version already in List/Theory.)

[Alizter]

The use of merely in BoundedSearch appears to be a red-herring. The only use is for showing min_n_Type is a hprop, which it can be if you just truncate it when needed. For bounded search itself, it is not required.

[Alizter]

I think we should simplify BoundedSearch by removing the truncation. As for the two implementations, I think its useful to keep both of them, but we should add some comments pointing to both cases. The imports in BoundedSearch can be reduced too.

[jdchristensen]

The use of merely in BoundedSearch appears to be a red-herring. The only use is for showing min_n_Type is a hprop, which it can be if you just truncate it when needed. For bounded search itself, it is not required.
I think we should simplify BoundedSearch by removing the truncation.

I'm not sure what you mean. "truncate it when needed" means that you will need merely, and it needs to be truncated in the proof of prop_n_to_min_n. So I don't see how BoundedSearch.v can avoid depending on Truncations.Core. (It's true that bounded_search and the new decidable_search don't depend on merely, but they are in the same file, so if you want to use them, you'll depend on merely.

Anyways, I don't think this dependency is that big of a deal. I just think it's interesting to notice that the proof in Lists/Theory.v doesn't have this dependency, but instead depends on lists.

As for the two implementations, I think its useful to keep both of them, but we should add some comments pointing to both cases.

I think this is a good solution. I'll push some changes.

The imports in BoundedSearch can be reduced too.

You mean by splitting up the Basics and Types imports? Ok.

[Alizter]

Here are the changes for removing truncation that I had:

diff --git a/theories/BoundedSearch.v b/theories/BoundedSearch.v
index 994402289..b2ddb3d8b 100644
--- a/theories/BoundedSearch.v
+++ b/theories/BoundedSearch.v
@@ -1,5 +1,4 @@
 Require Import HoTT.Basics HoTT.Types.
-Require Import HoTT.Truncations.Core.
 Require Import HoTT.Spaces.Nat.Core.
 
 Section bounded_search.
@@ -14,9 +13,9 @@ Section bounded_search.
   Local Definition minimal (n : nat) : Type := forall m : nat, P m -> n <= m.
 
   (** If we assume [Funext], then [minimal n] is a proposition.  But to avoid needing [Funext], we propositionally truncate it. *)
-  Local Definition min_n_Type : Type := { n : nat & merely (P n) * merely (minimal n) }.
+  Local Definition min_n_Type : Type := { n : nat & P n * minimal n }.
 
-  Local Instance ishpropmin_n : IsHProp min_n_Type.
+  (* Local Instance ishpropmin_n : IsHProp min_n_Type.
   Proof.
     apply ishprop_sigma_disjoint.
     intros n n' [p m] [p' m'].
@@ -24,7 +23,7 @@ Section bounded_search.
     apply leq_antisym.
     - exact (m n' p').
     - exact (m' n p).
-  Defined.
+  Defined. *)
 
   Local Definition smaller (n : nat) := { l : nat & P l * minimal l * (l <= n) }.
 
@@ -86,22 +85,25 @@ Section bounded_search.
   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)).
+    - exact (l;((Pl, ml))).
     - destruct (none n (leq_refl n) Pn).
   Defined.
 
-  Local Definition prop_n_to_min_n (P_inhab : hexists (fun n => P n))
+  Local Definition prop_n_to_min_n (P_inhab : exists n, P n)
     : min_n_Type.
   Proof.
-    refine (Trunc_rec _ P_inhab).
-    intros [n Pn]. exact (n_to_min_n n Pn).
+    destruct P_inhab as [n Pn].
+    snrapply n_to_min_n.
+    - exact n.
+    - exact Pn.
   Defined.
 
-  Definition minimal_n (P_inhab : hexists (fun n => P n))
+  Definition minimal_n (P_inhab : exists n, P n)
     : { n : nat & P n }.
   Proof.
     destruct (prop_n_to_min_n P_inhab) as [n pl]. destruct pl as [p _].
-    exact (n; fst merely_inhabited_iff_inhabited_stable p).
+    exists n.
+    exact p.
   Defined.
 
 End bounded_search.
@@ -112,16 +114,15 @@ 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 : exists x, P x).
 
   (** 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)).
+    assert (P'_inhab : exists n, P' n).
     {
-      strip_truncations. apply tr.
       destruct P_inhab as [x p].
       exists (e ^-1 x).
       unfold P'.

[jdchristensen]

Here are the changes for removing truncation that I had:

But that changes the assumption to (P_inhab : exists x, P x). which makes results like minimal_n trivial. I think the point is that knowing mere existence is enough to get honest existence if the search is bounded, so the truncation is essential to the results in this file.

[jdchristensen]

BTW, I'm in the middle of some cleanups throughout the file, which I'll push later today.

[jdchristensen]

Ok, I also made a lot of cleanups, and added one idiom as a general result leq_ind_l in Nat/Core. This is ready for review.

[Alizter]

Not so bad:

Definition leq_ind_l' {n : nat} (Q : forall (m : nat) (l : m <= n.+1), Type)
  (H_Sn : Q n.+1 _)
  (H_m : forall (m : nat) (l : m <= n), Q m _)
  : forall (m : nat) (l : m <= n.+1), Q m _.
Proof.
  intros m leq_m_Sn.
  inversion leq_m_Sn as [p |k H p].
  - rapply (transportDD _ Q p^ (path_ishprop _ _) H_Sn).
  - destruct p^; clear p.
    rapply (transportDD _ Q 1 (path_ishprop _ _) (H_m _ _)).
Defined.

It needs to come after ishprop_leq though.

[jdchristensen]

Yes, I realized that we could do it that way, but I was trying to prove it directly from the induction principle for leq, as it feels like it should be possible. But maybe it's best to make it more general and put it after ishprop_leq. I did find a proof that only uses leq_refl_inj, but it also turns out that leq_ind_l' isn't strong enough to prove the other injectivity, so I don't think there's much point in phrasing it that way.

[Alizter]

Either way we can ignore this comment since we don't need this lemma anywhere, if we wish to find it in the future we can come back to this comment.

[Alizter]

I'm happy with these changes, feel free to merge.

[jdchristensen]

@Alizter You don't think it's better to have the more general leq_ind_l?

[Alizter]

@jdchristensen Until it is needed, I don't see a point in trying to generalise it.

[jdchristensen]

Well, your proof tidied up to be very concise, so I decided to go for it. Does this look ok?

[Alizter]

Looks good