Skip to content

Make `BiLaterContractive` a class instead of a notation.

Robbert Krebbers requested to merge robbert/bi_later_contractive into master

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.

Merge request reports