The Coq mailing list

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

On 03/16/2016 04:09 PM, Emilio Jesús Gallego Arias wrote:

Dear David,

David Asher <asher AT informatik.hu-berlin.de> writes:

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

How does the paper proof look?

It is an indirect proof. My actual proof goal is "forall x, f(x)>=g(x)". From the opposite assumption "exists x, f(x)<g(x)" plus the statement that x to be chosen s.t. f(x) is minimal, I can derive a contradiction.

It is enough to assume that either such a minimal element exists, and if
not derive a contradiction from non-existance?

If that is the case, the following code may help:

 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.

Variable n : nat.
Variable f : 'I_n -> nat.
Variable g : 'I_n -> nat.

Lemma arg_min_inequality x (f_lt_g : f x < g x) :
   exists m, (f m < g m) &&
             [forall y, (f y < f m) ==> (g y <= f y)].
Proof.
pose P m := (f m < g m) && [forall y, (f y < f m) ==> (g y <= f y)].
case: (pickP P) => [m pm|]; first by exists m.
rewrite /P {P} => h.

E.

(Available online at https://x80.org/collacoq/osipiyesim.coq)

Therefore I'm not sure if I can derive a contradiction from assuming the non-existence.

David