The Coq mailing list

[David Asher <asher AT informatik.hu-berlin.de>]

Dear Coq-Club,

I asked a similar question a while ago. I have an existentially quantified Proposition in my hypothesis set, say "exists x, f(x) < g(x)", where f and g are functions of type "{x : nat | x < n} -> nat". Now I want, as I did my pencil and paper proof, to instantiate x such that "f(x) < g(x)" holds and for every y < x implies that f(y)>=g(y). In other words I'm trying to proof the following:

Variable x : nat.
Variable f : {n : nat | n < x} -> nat.
Variable g : {n : nat | n < x} -> nat.

Lemma arg_min_inequality : forall x,
  (f x < g x) -> (exists x, f x < g x /\
                            forall y, f y < f x -> f y >= g y).

I suspect that the answer will have to do something with well founded induction on natural numbers. At least that was the answer to my previous question, where I wanted to know how to instantiate x for a Relation s.t. x is minimal. Xavier Leroy pointed me into the right direction to use well-founded induction on natural numbers with the lt-relation:

Lemma P_upto_n_dec:
forall n, (exists m, m < n /\ P m) \/ (forall m, m < n -> ~ P m).
Proof.
intros.
destruct (classic(exists m, m < n /\ P m)) ; firstorder.
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.

However, I think for my Problem this won't work. I suspect, I have to define my own relation, proving that it is well-founded and than using this relation in order to perform a well-founded induction on natural numbers. Unfortunately I don't have any clue how to do this.

Thank you
David