Ricardo (Oct 24 2022 at 23:33): Ricardo (Oct 24 2022 at 23:33):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?
Shengyi Wang (Oct 25 2022 at 00:58):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.
Shengyi Wang (Oct 25 2022 at 02:59):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.
Ana de Almeida Borges (Oct 25 2022 at 13:13):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?
Ricardo (Oct 25 2022 at 21:02):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: Oct 13 2024 at 01:02 UTC