Library hydras.Prelude.First_toggle

First_toggle

Computes the first l between n and p (excluded) such that P l = true and P (S l) = false.

Pierre Castéran, Univ. Bordeaux and LaBRI

From Coq Require Import Arith Lia Inclusion Inverse_Image.
From hydras Require Import DecPreOrder.

Section Hypos.
  Context (P : nat → Prop) `{Pdec: ∀ n, Decision (P n)} (n p : nat).

  Hypotheses (Hnp : n < p) (Hn : P n) (Hp : ¬ P p).

  Let spec := {l : nat | n ≤ l ∧ l < p ∧
                          (∀ i: nat, n ≤ i → i ≤ l → P i ) ∧
               (¬ P (S l ))}.

  Definition first_toggle : spec.

End Hypos.

Arguments first_toggle : clear implicits.