The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

The function get_arg_min should be easy to define. However, your use of dependent pairs may cause some trouble.

You may have to prove that all proofs of m < n are equal, to ensure that f and g do not base their decisions merely on difference in the proof parts of their inputs.

Without axioms, proving this may be tricky at best, or may not even hold. There are workarounds, if you are interested.

So, you can instead have f and g be of type nat - > nat. You can instead modify your lemma minimal_exists to express that you are only interested in inputs smaller than some number.

With these hints, and maybe after reading the first 5 or more chapters of Software Foundations , you should be able to write this function and prove its correctness.

If not, please ask.

I am not sure what you meant by "how to transform this (function) into a lemma".

Here is an example of how a function (Z.opp) and its correctness proof (Z.add_opp_diag_r) can be used in a proof:

Require Import ZArith.

Open Scope Z_scope.

Lemma add_inv_exists_Z : forall a:Z, exists b:Z, a + b = 0.

Proof.

  intro. exists (Z.opp a).

SearchAbout (?x + (Z.opp ?x) = 0).  

  apply Z.add_opp_diag_r.

Qed.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

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

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.