Make `BiLaterContractive` a class instead of a notation.
This avoids unnecessary search on failed attempts. Contractive
is notation for Proper
, so previously, this caused a bunch of setoid instances to be used. In turn, this resulted in TC debug output that is hard to read.
Before
Goal ∀ PROP : bi, BiLaterContractive PROP.
Proof.
Typeclasses eauto := debug.
apply _.
(* Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = true
1: looking for (∀ (PROP : bi) (n : nat), Proper (dist_later n ==> dist n) bi_later) without backtracking
1: no match for (∀ (PROP : bi) (n : nat), Proper (dist_later n ==> dist n) bi_later), 334 possibilities
1.1-1: looking for (Contractive bi_later) without backtracking
1.1-1: no match for (Contractive bi_later), 334 possibilities
1.1-1.1-1: looking for (Proper (dist_later n ==> dist n) bi_later) without backtracking
1: looking for (Params bi_later ?H0) with backtracking
1: no match for (Params bi_later ?H0), 146 possibilities
1.1-1.1-1.1: (*external*) proper_reflexive on (Proper (dist_later n ==> dist n) bi_later), 1 subgoal(s)
1.1-1.1-1.1-1 : (ReflexiveProxy (dist_later n ==> dist n)%signature)
1.1-1.1-1.1-1: looking for (ReflexiveProxy (dist_later n ==> dist n)%signature) without backtracking
1.1-1.1-1.1-1.1: (*external*) (reflexive_proxy_tac A R) on
(ReflexiveProxy (dist_later n ==> dist n)%signature), 1 subgoal(s)
1.1-1.1-1.1-1.1-1 : (Reflexive (dist_later n ==> dist n)%signature)
1.1-1.1-1.1-1.1-1: looking for (Reflexive (dist_later n ==> dist n)%signature) without backtracking
1.1-1.1-1.1-1.1-1.1: simple apply @Equivalence_Reflexive on
(Reflexive (dist_later n ==> dist n)%signature), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.1-1 : (Equivalence (dist_later n ==> dist n)%signature)
1.1-1.1-1.1-1.1-1.1-1: looking for (Equivalence (dist_later n ==> dist n)%signature) without backtracking
1.1-1.1-1.1-1.1-1.1-1: no match for (Equivalence (dist_later n ==> dist n)%signature), 10 possibilities
1.1-1.1-1.1-1.1-1.2: simple apply @PreOrder_Reflexive on
(Reflexive (dist_later n ==> dist n)%signature), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.2-1 : (PreOrder (dist_later n ==> dist n)%signature)
1.1-1.1-1.1-1.1-1.2-1: looking for (PreOrder (dist_later n ==> dist n)%signature) without backtracking
1.1-1.1-1.1-1.1-1.2-1.1: simple apply @partial_order_pre on
(PreOrder (dist_later n ==> dist n)%signature), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.2-1.1-1 : (PartialOrder (dist_later n ==> dist n)%signature)
1.1-1.1-1.1-1.1-1.2-1.1-1: looking for (PartialOrder (dist_later n ==> dist n)%signature) without backtracking
1.1-1.1-1.1-1.1-1.2-1.1-1.1: simple apply @total_order_partial on
(PartialOrder (dist_later n ==> dist n)%signature), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.2-1.1-1.1-1 : (TotalOrder (dist_later n ==> dist n)%signature)
1.1-1.1-1.1-1.1-1.2-1.1-1.1-1: looking for (TotalOrder (dist_later n ==> dist n)%signature) without backtracking
1.1-1.1-1.1-1.1-1.2-1.1-1.1-1: no match for (TotalOrder (dist_later n ==> dist n)%signature), 0 possibilities
1.1-1.1-1.1-1.1-1.2-1.2: simple apply @Equivalence_PreOrder on
(PreOrder (dist_later n ==> dist n)%signature), 1 subgoal(s)
1.1-1.1-1.1-1.1-1.2-1.2-1 : (Equivalence (dist_later n ==> dist n)%signature)
1.1-1.1-1.1-1.1-1.2-1.2-1: looking for (Equivalence (dist_later n ==> dist n)%signature) without backtracking
1.1-1.1-1.1-1.1-1.2-1.2-1: no match for (Equivalence (dist_later n ==> dist n)%signature), 10 possibilities
*)
Now
Goal ∀ PROP : bi, BiLaterContractive PROP.
Proof.
Typeclasses eauto := debug.
apply _.
(*
Calling typeclass resolution with flags: depth = ∞,unique = false,do_split = true,fail = true
1: looking for (∀ PROP : bi, BiLaterContractive PROP) without backtracking
1: no match for (∀ PROP : bi, BiLaterContractive PROP), 0 possibilities
1.1-1: looking for (BiLaterContractive PROP) without backtracking
1.1-1: no match for (BiLaterContractive PROP), 0 possibilities
Cannot infer this placeholder of type "∀ PROP : bi, BiLaterContractive PROP" (no type class instance found).
*)
Consequences
For clients of BiLaterContractive
there are no changes, but if you might have to update proofs of BiLaterContractive
.