diff options
| author | Georges Gonthier | 2019-03-04 13:20:33 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2019-04-01 17:42:37 +0200 |
| commit | 4d59fa0c4fb418b17394fa53fa8e8ee3f52d840f (patch) | |
| tree | bf4a2878e061e80cfc68aa29f875179691378f6c /mathcomp/character | |
| parent | c5763504783b51bb5def88c82f55a0b99ebf9d67 (diff) | |
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.
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/character.v | 6 |
1 files changed, 4 insertions, 2 deletions
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. |