From c5763504783b51bb5def88c82f55a0b99ebf9d67 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Mon, 4 Mar 2019 11:49:56 +0100 Subject: Compatibility fix for Coq issue coq/#9663 Coq currently fails to resolve Miller patterns against open evars (issue coq/#9663), in particular it fails to unify `T -> ?R` with `forall x : T, ?dR x` even when `?dR` does not have `x` in its context. As a result canonical structures and constructor notations for the new generalised dependent `finfun`s fail for the non-dependent use cases, which is an unacceptable regression. This commit mitigates the problem by specialising the canonical instances and most of the constructor notation to the non-dependent case, and introducing an alias of the `finfun_of` type that has canonical instances for the dependent case, to allow experimentation with that feature. With this fix the whole `MathComp` library compiles, with a few minor changes. The change in `integral_char` fixes a performance issue that appears to be the consequence of insufficient locking of both `finfun_eqType` and `cfIirr`; this will be explored in a further commit. --- mathcomp/character/integral_char.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index 3c2b0d6..d73f938 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -423,7 +423,7 @@ Theorem dvd_irr1_index_center gT (G : {group gT}) i : ('chi[G]_i 1%g %| #|G : 'Z('chi_i)%CF|)%C. Proof. without loss fful: gT G i / cfaithful 'chi_i. - rewrite -{2}[i](quo_IirrK _ (subxx _)) ?mod_IirrE ?cfModE ?cfker_normal //. + rewrite -{2}[i](quo_IirrK _ (subxx _)) 1?mod_IirrE ?cfModE ?cfker_normal //. rewrite morph1; set i1 := quo_Iirr _ i => /(_ _ _ i1) IH. have fful_i1: cfaithful 'chi_i1. by rewrite quo_IirrE ?cfker_normal ?cfaithful_quo. -- cgit v1.2.3 From 4d59fa0c4fb418b17394fa53fa8e8ee3f52d840f Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Mon, 4 Mar 2019 13:20:33 +0100 Subject: locking definitions to address `integral.v` divergence Line 426 in `integral.v` diverged to over 40 minutes with the new `finfun.v`, because matching `mod_Iirr` to `quo_Iirr` goes into exponential backtracking. This is currently averted by limiting the repetition of `mod_IirrE` in this `rewrite` line. Making `finfun` mixing opaque brings this down to 40 seconds, and locking `cfIirr` to a tractable 0.15 seconds, hopefully improving the instances. This line also takes 47 seconds to execute in the master branch, so this is likely an undetected Coq performance regression. --- mathcomp/character/character.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'mathcomp/character') diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 783c46f..eda6f5a 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -667,11 +667,13 @@ Proof. by rewrite eqr_le ltr_geF ?irr1_gt0. Qed. Lemma irr_neq0 i : 'chi_i != 0. Proof. by apply: contraNneq (irr1_neq0 i) => ->; rewrite cfunE. Qed. -Definition cfIirr B (chi : 'CF(B)) : Iirr B := inord (index chi (irr B)). +Local Remark cfIirr_key : unit. Proof. by []. Qed. +Definition cfIirr : forall B, 'CF(B) -> Iirr B := + locked_with cfIirr_key (fun B chi => inord (index chi (irr B))). Lemma cfIirrE chi : chi \in irr G -> 'chi_(cfIirr chi) = chi. Proof. -move=> chi_irr; rewrite (tnth_nth 0) inordK ?nth_index //. +move=> chi_irr; rewrite (tnth_nth 0) [cfIirr]unlock inordK ?nth_index //. by rewrite -index_mem size_tuple in chi_irr. Qed. -- cgit v1.2.3