The Coq mailing list

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

On 03/16/2016 05:21 PM, Abhishek Anand wrote:
> Your functions f and g have a finite domain. So you can write down a 
> recursive function that computes f and g for all possible inputs and 
> gives you the input you are after.
>
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/%7Eaa755/>
Thank you for the hint. So you mean something like this?

Fixpoint get_arg_min
  (n : nat)
  (f : {m : nat | m < n} -> nat)
  (g : {m : nat | m < n} -> nat) : list (nat * nat) :=
match n with
| O    => nil
| S n' => ??
end.

And afterwards filtering applying two filters one that extracts the 
pairs, where left is smaller than the right and a filter that extracts 
the pair with the maximal left value? I see the point but I'm clueless, 
though, how to transform this into a lemma.

David.