The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 26/11/15 17:34, Pierre-Marie Pédrot wrote:
> On 26/11/2015 17:06, David Asher wrote:
>> But I need some additional information [ somethig like "~ (exists m,
>> m < n /\ P m)" ] in the context. Any ideas how to solve this?
> 
> If P is decidable, you can prove by induction on n that
> 
> P n -> exists m, P m /\ (forall p, p < m -> ~ P p)

Not sure structural induction will suffice here.  Slightly more
complex proof sketch below.

Or, just dig into the standard library: in Arith.Wf_nat, there is the
scarily-named theorem "dec_inh_nat_subset_has_unique_least_element"
that can be used here (take R x x' := x <= x').

> I don't think that this is intuitionistically provable when P is not
> decidable though.

My thought too.

- Xavier Leroy


Section MINIMAL_EXISTS.

Variable P: nat -> Prop.
Hypothesis P_dec: forall n, P n \/ ~ P n.

Lemma P_upto_n_dec:
  forall n, (exists m, m < n /\ P m) \/ (forall m, m < n -> ~ P m).
Proof.
  (* left as an exercise *)
Qed.

Lemma minimal_exists:
  forall n, P n -> exists m, P m /\ forall p, p < m -> ~ P p.
Proof.
  induction n using lt_wf_ind; intros.
  destruct (P_upto_n_dec n) as [[m [A B]] | C].
- eauto.
- exists n; auto.
Qed.

End MINIMAL_EXISTS.