Definition by minimization in Coq

Question

Assume P: nat -> T -> Prop is a proposition that for any given t: T,

• either there exists a k: nat such that P holds for all numbers greater than or equal to k and no number less than k.
• or P k t is false for all k : nat.

I want to define min_k : T -> nat + undef to be the minimum number k such that P k t holds, and undef otherwise.

Is that even possible? I tried to define something like

Definition halts (t : T) := exists k : nat, P k t.

Or maybe

Definition halts (t : T) := exists! k : nat, (~ P k t /\ P (S k) t).

and then use it like

Definition min_k (t : T) := match halts T with
  | True => ??
  | False => undef
end.

but I don't know how to go further from there.

Any ideas would be appreciated.

Answer 1

You can't match on a Prop. If you want to do case analysis then you need something in Type, typically bool or something like sumbool or sumor. In other words, you can do what you want as long as you have a pretty strong hypothesis.

Variable T : Type.
Variable P : nat -> T -> Prop.

Hypothesis PProperty : forall (t : T),
  {k : nat | forall n, (k <= n -> P n t) /\ (n < k -> ~ P n t)}
  +
  {forall k, ~ P k t}.

Definition min_k (t : T) : option nat :=
  match PProperty t with
  | inleft kH => Some (proj1_sig kH)
  | inright _ => None
  end.

Crucially, this wouldn't have worked if PProperty was a Prop disjunction, i.e., if it was of the form _ \/ _ instead of the form _ + { _ }.

By the way, the idiomatic way of describing foo + undef in Coq is to use option foo, which is what I did above, but you can adapt it as you wish.

Answer 2

In addition to Ana's excellent answer, I think it is worth pointing out that option nat is essentially the same thing as {k : nat | ...} + {forall k, ~ P k t} if you erase the proofs of the latter type: in the first case (Some or inleft), you get a natural number out; in the second (None or inright) you get nothing at all.