The Coq mailing list

[Lars Rasmusson <Lars.Rasmusson AT sics.se>]

Please disregard that... (*embarrassed shrug*) 

On Wed, Mar 16, 2016 at 7:44 PM, Lars Rasmusson <Lars.Rasmusson AT sics.se> wrote:

Hi, 

if you can prove that there is an x for which f takes a minimal value, 

    Hypothesis Hmin: exists x, forall y, f x < f y.

(which should be doable) then you can prove it like this.

Require Import Omega.

Variable x : nat. 

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

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

Hypothesis Hmin: exists x, forall y, f x < f y.

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

  intros x0 H. clear x0 H. (* not needed *)

  destruct Hmin as [x1 H1]; exists x1. (* get the x for the smallest element *)

  split.

  specialize (H1 x1); omega.

  intro y; specialize (H1 y); omega.

Qed.

On Wed, Mar 16, 2016 at 2:35 PM, David Asher <asher AT informatik.hu-berlin.de> wrote:

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