# Proving that a minimum example exists if any example exists in nat

I'm trying to prove that if a function from nat -> bool is true for any natural number, then there exists a minimum natural number which the function is true for.

I've been trying to find a good min_prop function to find this minimum true value, but I've had trouble proving the result of the min_prop function is actually the minimum true value.

I've written one version of this min_prop function, which only checks the first n values.

Fixpoint min_pb (pb : nat -> bool) (max : nat) :=
match max with
| O => if pb O then Some O else None
| S max' =>
let r := min_pb pb max' in
match r with
| None => if pb max then Some max else None
| Some n => Some n
end
end.


Is there a better approach than using a minimum function, or a better minimum function, or easy proof of the one I've already written?

• What if you have min_pb have a return type that's something like {forall n, n < max -> pb n = false} + {exists n : nat, (n < max) /\ (pb n = true)}? Maybe easier said than done, but I think that'd help with the main proof if you can. Oct 5, 2023 at 19:20
• Good idea. I'll try something like that. Oct 5, 2023 at 19:29
• I'm going to try using sub to count up from 0 to max with this:  Fixpoint min_pb_rev (pb : nat -> bool) (max : nat) (cs : nat) := match cs with | O => if pb max then Some max else None | S cs' => if pb (sub max (S cs')) then Some (sub max (S cs')) else min_pb_rev pb max cs' end. Oct 5, 2023 at 19:37
• I thought about it and I came up with proving: forall (pb : nat -> bool) (n : nat), (forall (u : nat), le u n -> pb u = false) \/ (exists (min : nat), pb min = true /\ (forall (u : nat), lt u min -> pb u = false)), which works nicely with induction on n. Oct 6, 2023 at 10:34

If you can use MathComp, ssrnat provides ex_minn, which I think gives you exactly what you are trying to prove (e.g., see ExMinnSpec).

Here's the start of a cute solution:

Fixpoint minimise (f : nat -> bool) (max : nat) : nat :=
if f 0 then 0 else
match max with
| 0 => 0
| S max' => minimise (fun n => f (S n)) max'
end.

Theorem minimise_correct : forall (max : nat) (f : nat -> bool),
f max = true -> f (minimise f max) = true /\ (forall n, n < minimise f max -> f n = false).
Proof.
induction max.

• Looks like a good approach. I used induction to prove, Lemma min_prop : forall (pb : nat -> bool) (n : nat), (forall (u : nat), le u n -> pb u = false) \/ (exists (min : nat), pb min = true /\ (forall (u : nat), lt u min -> pb u = false)). Oct 6, 2023 at 18:11