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
Last updated: Feb 08 2023 at 08:02 UTC