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/ssreflect/finfun.v | 41 +++++++++++++++++++++--------------------
 1 file changed, 21 insertions(+), 20 deletions(-)

(limited to 'mathcomp/ssreflect')

diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 9a8c723..db03671 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -239,34 +239,35 @@ Notation family F := (family_mem (fmem F)).
 Section InheritedStructures.
 
 Variable aT : finType.
+Notation dffun_aT rT rS := {dffun forall x : aT, rT x : rS}.
 
-Definition finfun_eqMixin (rT : _ -> eqType) :=
-  @PcanEqMixin {dffun finPi aT rT} _ _ _ tfgraphK.
+Local Remark eqMixin rT : Equality.mixin_of (dffun_aT rT eqType).
+Proof. exact: PcanEqMixin tfgraphK. Qed.
 Canonical finfun_eqType (rT : eqType) :=
-  EqType {ffun aT -> rT} (finfun_eqMixin _).
-Canonical dfinfun_eqType (rT : _ -> eqType) :=
-  EqType {dffun finPi aT rT} (finfun_eqMixin _).
+  EqType {ffun aT -> rT} (eqMixin (fun=> rT)).
+Canonical dfinfun_eqType rT :=
+  EqType (dffun_aT rT eqType) (eqMixin rT).
 
-Definition finfun_choiceMixin (rT : _ -> choiceType) :=
-  @PcanChoiceMixin _ {dffun finPi aT rT} _ _ tfgraphK.
+Local Remark choiceMixin rT : Choice.mixin_of (dffun_aT rT choiceType).
+Proof. exact: PcanChoiceMixin tfgraphK. Qed.
 Canonical finfun_choiceType (rT : choiceType) :=
-  ChoiceType {ffun aT -> rT} (finfun_choiceMixin _).
-Canonical dfinfun_choiceType (rT : _ -> choiceType) :=
-  ChoiceType {dffun finPi aT _} (finfun_choiceMixin rT).
+  ChoiceType {ffun aT -> rT} (choiceMixin (fun=> rT)).
+Canonical dfinfun_choiceType rT :=
+  ChoiceType (dffun_aT rT choiceType) (choiceMixin rT).
 
-Definition finfun_countMixin (rT : _ -> countType) :=
-  @PcanCountMixin _ {dffun finPi aT rT} _ _ tfgraphK.
+Local Remark countMixin rT : Countable.mixin_of (dffun_aT rT countType).
+Proof. exact: PcanCountMixin tfgraphK. Qed.
 Canonical finfun_countType (rT : countType) :=
-  CountType {ffun aT -> rT} (finfun_countMixin _).
-Canonical dfinfun_countType (rT : _ -> countType) :=
-  CountType {dffun finPi aT rT} (finfun_countMixin _).
+  CountType {ffun aT -> rT} (countMixin (fun => rT)).
+Canonical dfinfun_countType rT :=
+  CountType (dffun_aT rT countType) (countMixin rT).
 
-Definition finfun_finMixin (rT : _ -> finType) :=
-  @PcanFinMixin (dfinfun_countType rT) _ _ _ tfgraphK.
+Local Definition finMixin rT :=
+  PcanFinMixin (tfgraphK : @pcancel _ (dffun_aT rT finType) _ _).
 Canonical finfun_finType (rT : finType) :=
-  FinType {ffun aT -> rT} (finfun_finMixin _).
-Canonical dfinfun_finType (rT : _ -> finType) :=
-  FinType {dffun finPi aT rT} (finfun_finMixin _).
+  FinType {ffun aT -> rT} (finMixin (fun=> rT)).
+Canonical dfinfun_finType rT :=
+  FinType (dffun_aT rT finType) (finMixin rT).
 
 End InheritedStructures.
 
-- 
cgit v1.2.3