diff options
| -rw-r--r-- | mathcomp/algebra/vector.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 32 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 16 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnat.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 7 |
5 files changed, 41 insertions, 22 deletions
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index a2346a2..cda2876 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1302,7 +1302,7 @@ Section LfunZmodType. Variables (R : ringType) (aT rT : vectType R). Implicit Types f g h : 'Hom(aT, rT). -Canonical lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:]. +Definition lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:]. Canonical lfun_eqType := EqType 'Hom(aT, rT) lfun_eqMixin. Definition lfun_choiceMixin := [choiceMixin of 'Hom(aT, rT) by <:]. Canonical lfun_choiceType := ChoiceType 'Hom(aT, rT) lfun_choiceMixin. diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index cd907ce..76b0521 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -107,7 +107,7 @@ Require Import ssrfun ssrbool. (* [eqMixin of S by <:] *) (* construct to declare the equality mixin; this pattern is repeated for all *) (* the combinatorial interfaces (Choice, Countable, Finite). As noted above, *) -(* such mixins should not be mad Canonical. *) +(* such mixins should not be made Canonical. *) (* We add the following to the standard suffixes documented in ssrbool.v: *) (* 1, 2, 3, 4 -- explicit enumeration predicate for 1 (singleton), 2, 3, or *) (* 4 values. *) @@ -155,6 +155,17 @@ Export Equality.Exports. Definition eq_op T := Equality.op (Equality.class T). +(* eqE is a generic lemma that can be used to fold back recursive comparisons *) +(* after using partial evaluation to simplify comparisons on concrete *) +(* instances. The eqE lemma can be used e.g. like so: rewrite !eqE /= -!eqE. *) +(* For instance, with the above rewrite, n.+1 == n.+1 gets simplified to *) +(* n == n. For this to work, we need to declare equality _mixins_ *) +(* as canonical. Canonical declarations remove the need for specific *) +(* inverses to eqE (like eqbE, eqnE, eqseqE, etc.) for new recursive *) +(* comparisons, but can only be used for manifest mixing with a bespoke *) +(* comparison function, and so is incompatible with PcanEqMixin and the like *) +(* - this is why the tree_eqMixin for GenTree.tree in library choice is not *) +(* declared Canonical. *) Lemma eqE T x : eq_op x = Equality.op (Equality.class T) x. Proof. by []. Qed. @@ -745,7 +756,7 @@ Section ProdEqType. Variable T1 T2 : eqType. -Definition pair_eq := [rel u v : T1 * T2 | (u.1 == v.1) && (u.2 == v.2)]. +Definition pair_eq : rel (T1 * T2) := fun u v => (u.1 == v.1) && (u.2 == v.2). Lemma pair_eqP : Equality.axiom pair_eq. Proof. @@ -753,7 +764,7 @@ move=> [x1 x2] [y1 y2] /=; apply: (iffP andP) => [[]|[<- <-]] //=. by do 2!move/eqP->. Qed. -Definition prod_eqMixin := EqMixin pair_eqP. +Canonical prod_eqMixin := EqMixin pair_eqP. Canonical prod_eqType := Eval hnf in EqType (T1 * T2) prod_eqMixin. Lemma pair_eqE : pair_eq = eq_op :> rel _. Proof. by []. Qed. @@ -770,9 +781,8 @@ Proof. by case/andP. Qed. End ProdEqType. -Arguments pair_eqP [T1 T2]. - -Prenex Implicits pair_eqP. +Arguments pair_eq {T1 T2} _ _ /. +Arguments pair_eqP {T1 T2}. Definition predX T1 T2 (p1 : pred T1) (p2 : pred T2) := [pred z | p1 z.1 & p2 z.2]. @@ -797,6 +807,8 @@ Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin. End OptionEqType. +Arguments opt_eq {T} !_ !_. + Section TaggedAs. Variables (I : eqType) (T_ : I -> Type). @@ -841,8 +853,8 @@ Proof. by rewrite -tag_eqE /tag_eq eqxx tagged_asE. Qed. End TagEqType. -Arguments tag_eqP [I T_ x y]. -Prenex Implicits tag_eqP. +Arguments tag_eq {I T_} !_ !_. +Arguments tag_eqP {I T_ x y}. Section SumEqType. @@ -865,5 +877,5 @@ Lemma sum_eqE : sum_eq = eq_op. Proof. by []. Qed. End SumEqType. -Arguments sum_eqP [T1 T2 x y]. -Prenex Implicits sum_eqP. +Arguments sum_eq {T1 T2} !_ !_. +Arguments sum_eqP {T1 T2 x y}. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 4e4c77b..9c13df3 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1309,14 +1309,14 @@ Definition inE := (mem_seq1, in_cons, inE). Prenex Implicits mem_seq1 uniq undup index. -Arguments eqseqP [T x y]. -Arguments hasP [T a s]. -Arguments hasPn [T a s]. -Arguments allP [T a s]. -Arguments allPn [T a s]. -Arguments nseqP [T n x y]. -Arguments count_memPn [T x s]. -Prenex Implicits eqseqP hasP hasPn allP allPn nseqP count_memPn. +Arguments eqseq {T} !_ !_. +Arguments eqseqP {T x y}. +Arguments hasP {T a s}. +Arguments hasPn {T a s}. +Arguments allP {T a s}. +Arguments allPn {T a s}. +Arguments nseqP {T n x y}. +Arguments count_memPn {T x s}. Section NthTheory. diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index f7cd700..78d50b6 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -174,8 +174,8 @@ Qed. Canonical nat_eqMixin := EqMixin eqnP. Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin. -Arguments eqnP [x y]. -Prenex Implicits eqnP. +Arguments eqn !_ !_. +Arguments eqnP {x y}. Lemma eqnE : eqn = eq_op. Proof. by []. Qed. @@ -1454,6 +1454,8 @@ Qed. Canonical bin_nat_eqMixin := EqMixin eq_binP. Canonical bin_nat_eqType := Eval hnf in EqType N bin_nat_eqMixin. +Arguments N.eqb !_ !_. + Section NumberInterpretation. Import BinPos. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 64585f6..38e3dbe 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -360,7 +360,12 @@ Section UseFinTuple. Variables (n : nat) (T : finType). -Canonical tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T). +(* tuple_finMixin could, in principle, be made Canonical to allow for folding *) +(* Finite.enum of a finite tuple type (see comments around eqE in eqtype.v), *) +(* but in practice it will not work because the mixin_enum projector *) +(* has been burried under an opaque alias, to avoid some performance issues *) +(* during type inference. *) +Definition tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T). Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin. Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T]. |