2
$\begingroup$

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?

$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$ Oct 5, 2023 at 19:20
  • $\begingroup$ Good idea. I'll try something like that. $\endgroup$ Oct 5, 2023 at 19:29
  • $\begingroup$ 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.` $\endgroup$ Oct 5, 2023 at 19:37
  • $\begingroup$ 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. $\endgroup$ Oct 6, 2023 at 10:34

2 Answers 2

1
$\begingroup$

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).

$\endgroup$
1
2
$\begingroup$

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.
$\endgroup$
1
  • $\begingroup$ 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)). $\endgroup$ Oct 6, 2023 at 18:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.