Best way to express that a type is inhabited in a way that allows getting the habitant

Using Rocq
1

Hi,

Here is a small example demonstrating the gist of my question:

Definition injective {A B : Type} (f : A -> B)
  := forall a a', f a = f a' -> a = a'.

Definition infinite (T : Type) := exists (f : nat -> T), injective f.

Goal
  forall P,
    let S := {n : nat | P n} in
      (exists s : S, True) /\ (forall s : S, exists s' : S, proj1_sig s < proj1_sig s')
      -> infinite S.
Proof.
  intros P S H. destruct H as [init succ].
  unshelve eexists (fix f (n : nat) := (_ : S)).
  * Fail destruct init.
    (* “Case analysis on sort Set is not allowed for inductive definition ex.” *)

As you can see, the proof is stuck trying to destruct exists s : S, True to extract an s : S, because the result of this whole pattern matching needs to be of type S, to exhibit a function f : nat -> S, and as far as I understand, Coq does not allow a pattern matching on a Prop to yield a non-Prop in order to be able to erase Props during extraction.

I can work around that by replacing (exists s : S, True) /\ ... with prod S ..., but then for other parts of the proof I also need to replace the exists s : S', .... I suppose I could also define a myexists the same way as exists but not in Prop, then my custom forall so it accepts something not in Prop, and … Uh.

Is there a simple way to express and prove this theorem?

2

You can try to move your assumption to Type:

  forall P,
    let S := {n : nat | P n} in
      { s : S | True } -> (forall s : S, exists s' : S, proj1_sig s < proj1_sig s')
      -> infinite S.

but since the predicate used here is True, you could simply write:

  forall P,
    let S := {n : nat | P n} in
      forall s : S, (forall s : S, exists s' : S, proj1_sig s < proj1_sig s')
      -> infinite S.

and you will probably face the same problem with exists s' which could be put into Type as well:

  forall P,
    let S := {n : nat | P n} in
      forall s : S, (forall s : S, { s' : S | proj1_sig s < proj1_sig s'})
      -> infinite S.