From 0b1ea03dafcf36880657ba910eec28ab78ccd018 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Thu, 13 Dec 2018 12:55:43 +0100 Subject: Adjust implicits of 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. --- ChangeLog | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'ChangeLog') diff --git a/ChangeLog b/ChangeLog index 4f17072..b82a0f4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -24,7 +24,20 @@ from eqtype.v. They were already in ssrfun.v. * Specialized `bool_irrelevance` so that the statement reflects - the name + the name. + + * Changed the shape of the type of FieldMixin to allow one-line + in-proof definition of bespoke fieldType structure. + + * Refactored and extended Arguments directives to provide more + comprehensive signature information. + + * Added maximal implicits to reflection, injectivity and cancellation + lemmas so that they are easier to pass to combinator lemmas such as + sameP, inj_eq or canLR. + + * Added reindex_inj s shorthand for reindexing a bigop with a + permutation s. * Added lemma `eqmxMunitP`: two matrices with the same shape represent the same subspace iff they differ only by a change of -- cgit v1.2.3