diff options
| -rw-r--r-- | .gitlab-ci.yml | 11 | ||||
| -rw-r--r-- | CHANGELOG.md | 17 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 27 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 13 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 52 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnotations.v | 2 |
8 files changed, 113 insertions, 15 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3eae6fa..65a71ed 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -159,9 +159,14 @@ ci-fourcolor-dev: - make install ci-odd-order-8.7: - extends: .ci-odd-order - variables: - COQ_VERSION: "8.7" + extends: .ci-odd-order + variables: + COQ_VERSION: "8.7" + +ci-odd-order-8.8: + extends: .ci-odd-order + variables: + COQ_VERSION: "8.8" ci-odd-order-dev: extends: .ci-odd-order diff --git a/CHANGELOG.md b/CHANGELOG.md index 99f51ce..3361567 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,10 +9,24 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added +- `nonPropType`, an interface for non-`Prop` types, and `{pred T}` and + `relpre f r`, all of which will be in the Coq 8.11 core SSreflect library. + +- `deprecate old_id new_id`, notation for `new_id` that prints a deprecation + warning for `old_id`; `Import Deprecation.Silent` turns off those warnings, + `Import Deprecation.Reject` raises errors instead of only warning. + ### Changed +- definition of `PredType` which now takes only a `P -> pred T` function; + definition of `simpl_rel` to improve simplification by `inE`. Both these + changes will be in the Coq 8.11 SSReflect core library. + ### Renamed +- `leq_size_perm` -> `uniq_min_size` (permuting conclusions) +- `perm_uniq` -> `eq_uniq` (permuting assumptions) + ### Misc ## [1.8.0] - 2019-04-08 @@ -58,7 +72,8 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9. - a function `permutations` that computes a duplicate-free list of all permutations of a given sequence `s` over an `eqType`, along - whit its theory. + with its theory: `mem_permutations`, `size_permutations`, + `permutations_uniq`, `permutations_all_uniq`, `perm_permutations`. ### Changed diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 468aa66..65167b5 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -2412,7 +2412,7 @@ Proof. set Su := map _ S => sSuS freeS; have uniqS := free_uniq freeS. have uniqSu: uniq Su by rewrite (map_inj_uniq cfAut_inj). have{sSuS} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS. -have [|eqSuS _] := leq_size_perm uniqSu sSuS; first by rewrite size_map. +have [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map. by rewrite (perm_free (uniq_perm_eq uniqSu uniqS eqSuS)). Qed. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 459250f..ae54fa1 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -1332,9 +1332,9 @@ rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i. symmetry; rewrite (eq_big_perm (map x r)) /= ?(big_map x). by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC. have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj. -have /leq_size_perm: {subset map x r <= r}. +have /uniq_min_size: {subset map x r <= r}. by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM. -by rewrite (size_map x) perm_eq_sym; case=> // /uniq_perm_eq->. +by rewrite (size_map x) perm_eq_sym; case=> // _ /uniq_perm_eq->. Qed. Lemma mem_galTrace K E a : galois K E -> a \in E -> galTrace K E a \in K. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 5576355..3685c23 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1516,26 +1516,26 @@ move=> Us1 eqs12; apply/idP/idP=> [Us2 | /eqP eq_sz12]. by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12). Qed. -Lemma leq_size_perm s1 s2 : +Lemma uniq_min_size s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> - s1 =i s2 /\ size s1 = size s2. + (size s1 = size s2) * (s1 =i s2). Proof. move=> Us1 ss12 le_s21; have Us2: uniq s2 := leq_size_uniq Us1 ss12 le_s21. -suffices: s1 =i s2 by split; last by apply/eqP; rewrite -uniq_size_uniq. +suffices: s1 =i s2 by split; first by apply/eqP; rewrite -uniq_size_uniq. move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x. rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //. by apply/allP; rewrite /= s2x; apply/allP. Qed. -Lemma perm_uniq s1 s2 : s1 =i s2 -> size s1 = size s2 -> uniq s1 = uniq s2. +Lemma eq_uniq s1 s2 : size s1 = size s2 -> s1 =i s2 -> uniq s1 = uniq s2. Proof. -move=> Es12 Esz12. -by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?Esz12 ?eqxx. +move=> eq_sz12 eq_s12. +by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?eq_sz12 ?eqxx. Qed. Lemma perm_eq_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2. Proof. -by move=> eq_s12; apply: perm_uniq; [apply: perm_eq_mem | apply: perm_eq_size]. +by move=> eq_s12; apply/eq_uniq; [apply: perm_eq_size | apply: perm_eq_mem]. Qed. Lemma uniq_perm_eq s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2. @@ -3056,3 +3056,16 @@ Coercion all_iffP : all_iff >-> Funclass. Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..)) (at level 0, format "[ '<->' '[' P0 ; '/' P1 ; '/' .. ; '/' Pn ']' ]") : form_scope. + +Notation leq_size_perm := + ((fun T s1 s2 Us1 ss12 les21 => + let: (Esz12, Es12) := + deprecate leq_size_perm uniq_min_size T s1 s2 Us1 ss12 les21 + in conj Es12 Esz12) _ _ _) + (only parsing). +Notation perm_uniq := + ((fun T s1 s2 eq_s12 eq_sz12 => + deprecate perm_uniq eq_uniq T s1 s2 eq_sz12 eq_s12) + _ _ _) + (only parsing). + diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 7eb7fd9..54c74dd 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -1,6 +1,18 @@ From mathcomp Require Import ssreflect ssrfun. From Coq Require Export ssrbool. +(******************************************************************************) +(* Local additions: *) +(* {pred T} == a type convertible to pred T but that presents the *) +(* pred_sort coercion class. *) +(* PredType toP == the predType structure for toP : A -> pred T. *) +(* relpre f r == the preimage of r by f, simplifying to r (f x) (f y). *) +(* --> These will become part of the core SSReflect library with Coq 8.11. *) +(* This file also anticipates a v8.11 change in the definition of simpl_pred *) +(* to T -> simpl_pred T. This change ensures that inE expands the definition *) +(* of r : simpl_rel along with the \in, when rewriting in y \in r x. *) +(******************************************************************************) + Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0, format "{ 'pred' T }") : type_scope. @@ -37,4 +49,3 @@ Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] (at level 0, Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)). Definition relpre {T rT} (f : T -> rT) (r : rel rT) := [rel x y | r (f x) (f y)]. - diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index fe06c0d..95da9cd 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -5,6 +5,22 @@ Global Set SsrOldRewriteGoalsOrder. Global Set Asymmetric Patterns. Global Set Bullet Behavior "None". +(******************************************************************************) +(* Local additions: *) +(* nonPropType == an interface for non-Prop Types: a nonPropType coerces *) +(* to a Type, and only types that do _not_ have sort *) +(* Prop are canonical nonPropType instances. This is *) +(* useful for applied views. *) +(* --> This will become standard with the Coq v8.11 SSReflect core library. *) +(* deprecate old new == new, but warning that old is deprecated and new *) +(* should be used instead. *) +(* --> Usage: Notation old := (deprecate old new) (only parsing). *) +(* --> Caveat: deprecate old new only inherits new's maximal implicits; *) +(* on-demand implicits should be added after : (deprecate old new _). *) +(* Import Deprecation.Silent :: turn off deprecation warning messages. *) +(* Import Deprecation.Reject :: raise an error instead of only warning. *) +(******************************************************************************) + Module NonPropType. Structure call_of (condition : unit) (result : bool) := Call {callee : Type}. @@ -33,3 +49,39 @@ End Exports. End NonPropType. Export NonPropType.Exports. +Module Deprecation. + +Definition hidden (T : Type) := T. +Definition exposed (T : Type) & unit -> unit -> unit := T. +Definition hide T u (v : exposed T u) : hidden T := v. + +Ltac warn old_id new_id := + idtac "Warning:" old_id "is deprecated; use" new_id "instead". + +Ltac stop old_id new_id := + fail 1 "Error:" old_id "is deprecated; use" new_id "instead". + +Structure hinted := Hint {statement; hint : statement}. +Ltac check cond := let test := constr:(hint _ : cond) in idtac. + +Variant reject := Reject. +Definition reject_hint := Hint reject Reject. +Module Reject. Canonical reject_hint. End Reject. + +Variant silent := Silent. +Definition silent_hint := Hint silent Silent. +Module Silent. Canonical silent_hint. End Silent. + +Ltac flag old_id new_id := + first [check reject; stop old_id new_id | check silent | warn old_id new_id]. + +Module Exports. +Arguments hide {T} u v /. +Coercion hide : exposed >-> hidden. +Notation deprecate old_id new_id := + (hide (fun old_id new_id => ltac:(flag old_id new_id; exact tt)) new_id) + (only parsing). +End Exports. + +End Deprecation. +Export Deprecation.Exports. diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v index 4c55514..dbc7f3d 100644 --- a/mathcomp/ssreflect/ssrnotations.v +++ b/mathcomp/ssreflect/ssrnotations.v @@ -1,6 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) +(******************************************************************************) (* - Reserved notation for various arithmetic and algebraic operations: *) (* e.[a1, ..., a_n] evaluation (e.g., polynomials). *) (* e`_i indexing (number list, integer pi-part). *) @@ -27,6 +28,7 @@ (* [rec a1, ..., an] standard shorthand for hidden recursor (see prime.v). *) (* The interpretation of these notations is not defined here, but the *) (* declarations help maintain consistency across the library. *) +(******************************************************************************) (* Reserved notation for evaluation *) Reserved Notation "e .[ x ]" |