Hi. I'm reading Ilya Sergey's Proofs and Programs and now trying to solve exercise 4.4 at the end of chapter 4. I tried the following.

```
Lemma addn_min_max m n : minn m n + maxn m n = m + n.
Proof. case: ltnP.
```

This produces the error `Could not fill dependent hole in "apply"`

. What does this error mean? I generally understand what the first part of the error means, but why apply? Why does this error show up here?

Could you please show more context? I tried in my machine, it looks OK:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Lemma my_addn_min_max m n : minn m n + maxn m n = m + n.
Proof. by case: ltnP => _; rewrite (addnC m n). Qed.
```

I'm happy to know it works for you. That means I'm probably doing things in a way that makes sense. The file starts like this.

```
From mathcomp
Require Import ssreflect ssrfun eqtype ssrnat ssrbool.
Module Rewriting.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
```

It is this file https://github.com/ilyasergey/pnp/blob/master/lectures/Rewriting.v.

I see. I'm using coq-mathcomp-ssreflect 1.15.0, so my original proof still works. I do not know how to prove in the setting of pnp.

I can't reproduce your error either. This can be either because of version mismatch (what are your Coq and mathcomp versions?) or because of definition mismatch. A cursory look at the file you quote shows that it redefines many relevant things. Can you try the example you shared with us in a fresh file?

Thank you @Ana de Almeida Borges and @Shengyi Wang. I'm using Coq 8.16.0 and math-comp 1.15.0. I tried in a fresh file and the line `case: ltnP`

works. Thank you both. I'm wondering if the point of exercise 4.4 is to not use `ltnP`

:thinking:

Last updated: Jul 25 2024 at 16:02 UTC