The Coq mailing list

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

On 03/16/2016 05:16 PM, Emilio Jesús Gallego Arias wrote:
> David Asher 
> <asher AT informatik.hu-berlin.de>
>  writes:
>
> > > > 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.
> Umm, as the domain of f is finite you can actually search for the
> minimal:
>
> Variable n : nat.
> Variable f : 'I_n -> nat.
> Variable g : 'I_n -> nat.
>
> Lemma arg_min_U x (f_lt_g : f x < g x) :
>    exists y, forall z, f y <= f z.
> Proof.
> exists [arg min_(y < x | true ) f y] => z.
> by case: arg_minP => // i _; apply.
> Qed.
>
> E.
Thank you. Seems we're on the right track, Abhisheck Anand also proposed 
to enumerate all values. Can you give me a hint though, how to do this 
with the on board means of Coq (I'm not familiar with ssreflect).

David.