PADEC - Coq Library

Library Padec.Tools.ComputeMax

From Coq Require Import Lia.
From Coq Require Import Nat.

Set Implicit Arguments.

Compute a maximum value

Compute a maximum value for which a given property exists

Property P: nat -> Prop

=> prove: there exists k_star < k_up, P(k_star) and for every k in {k_star+1, ... k_up}, not P(k)

i.e., k_star = max { k < k_up, P(k) }

Section ComputeMax.

  Variable (P: nat -> Prop) (P_class: forall i, P i \/ ~P i) .

  Variable (k_up: nat) (Hk_up: ~P k_up).

  Variable (k_witness: nat)
    (Hk_witness_bound: k_witness < k_up)
    (Hk_witness_P: P k_witness).

  Lemma ComputeMax:
    exists k_star , k_star < k_up /\ P k_star /\
                     forall k, k_star < k -> k <= k_up -> ~P k.
End ComputeMax.

Unset Implicit Arguments.