Cancel lemmas implicit #262
Conversation
|
Hi @ggonthier thanks, that's a change I had in mind for a while. (Indeed, it is preferred to rebase on top of master rather than to merge master into a branch, for the sake of cleaning the history and not confusing github) |
CohenCyril
added
kind: refactoring
|
Would it make sense to add an entry to ChangeLog in this PR to fix #258? Or should I open a new one? should be changed anyways. |
|
@anton-trunov , yes, one entry should suffice to cover both PRs, and it should be a little more precise than the on proposed. I'm working on extending slightly the PR to cover uses of the lemmas as suggested by @CohenCyril, and also to include partial function cancellation lemmas. |
Like injectivity lemmas, instances of cancellation lemmas (whose
conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or
`ocancel`) are passed to
generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should
not have trailing on-demand implicits _just before_ the `cancel`
conclusion, as these would be inconvenient to insert (requiring
essentially an explicit eta-expansion).
We therefore use `Arguments` or `Prenex Implicits` directives to make
all such arguments maximally inserted implicits. We don’t, however make
other arguments implicit, so as not to spoil direct instantiation of
the lemmas (in, e.g., `rewrite -[y](invmK injf)`).
We have also tried to do this with lemmas whose statement matches a
`cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern
unification will pick up `f = fun x => E[x]`).
We also adjusted implicits of a few stray injectivity
lemmas, and defined constants.
We provide a shorthand for reindexing a bigop with a permutation.
Finally we used the new implicit signatures to simplify proofs that
use injectivity or cancellation lemmas.
ggonthier
force-pushed
the
cancel-lemmas-implicit
branch
from
6b18a4f
to
0b1ea03
Compare
|
Added usage, partial function cancel ( |
CohenCyril
removed
the
needs: rebase
|
odd order is now part of Coq's CI and runs on each PR, so breaking it is not nice. What I do for elpi is to have Coq CI track a branch other than master that I synchronize with master when I'm sure (it is called coq-master). We could also improve CI here, so that we test odd-order too before merging. |
|
I've corrected the issue in odd-order, and also submitted #264 to correct related issues in |
Correct and improve implicits and documentation of MatrixGenField; also corrects changes in #262 to allow for a compatible fix in `odd-order`.
Make trailing implicit parameters of cancel f g and {in D, cancel f g} lemmas maximal, so that these lemmas are easier to pass to canLR, canLR_in, and similar.