ReflectiveSubuniverse: add a couple of things and simplify one proof

[jdchristensen]

This contains very minor changes. The main reason I'm making this an independent PR is that I have another question about typeclass resolution. I'll add a comment beside the relevant spot in the code, and will attach the verbose typeclasses debug log here.
debug.log

[jdchristensen]

srapply (cancelL_isequiv (to O B)). generates three goals:

?X259 : (PreReflects O B)
?X261 : (IsEquiv (to O B))
?X262 : (IsEquiv (to O B o O_rec f))

The third needs a proof (line 584), but the first two are instances. And the debug.log file shows that typeclass search finds the instances for those two, and then fails for the third (as expected). But for some reason I'm left with all three goals, instead of just the last one. Can someone explain? Earlier in the file (e.g. on line 566) the same goals are solved and stay solved.

[jdchristensen]

BTW, exactly the same thing happens with simple refine (cancelL_isequiv (to O B))., so this has nothing to do with the srapply tactic. I have also attached the less verbose version of the log, in case that is already enough to see the issue.
debug1.txt

[jdchristensen]

One difference I noticed is that in the cases where something like this succeeds, the debug log has all of the top-level goals numbered as "1:". But in this case, where two solvable goals are left unsolved, the top-level goals are numbered "1:", "2:" and "3:". Maybe this indicates that Coq thinks that they are dependent in some sense, so if 3 can't be solved, it backtracks and doesn't solve 1 and 2?

And some more experimenting found that if I provide the implicit argument C, the problem goes away, with the goals all numbered "1:". But C should be clear from the provided argument to O B.

In any case, I'd like to merge this, but even after merging, if anyone can explain the behaviour to me, that would be great.

[Alizter]

I think you've correctly identified the dependency behaviour but perhaps @SkySkimmer can confirm this is the case.

[SkySkimmer]

IDK

[jdchristensen]

@SkySkimmer Here's a standalone example that doesn't require the HoTT library. Should I create an issue on the Coq github?

Class IsEquiv {A B : Type} (f : A -> B) := foo : True.

Class Reflects (B : Type) := baz : True.

Global Instance reflects : forall B, Reflects B.
Admitted.

Definition to_O (B : Type) `{Reflects B} : B -> B.
Admitted.

Global Instance isequiv_to_O (B : Type) `{Reflects B} : IsEquiv (to_O B).
Admitted.

Definition cancelL_isequiv {A B C} (g : B -> C) {f : A -> B}
  `{IsEquiv B C g} `{IsEquiv A C (fun a => g (f a))}
  : IsEquiv f.
Admitted.

Definition isequiv_O_rec_O_inverts
       {A B : Type} (f : A -> B)
  : IsEquiv f.
Proof.
  Typeclasses eauto := debug.
  simple refine (cancelL_isequiv (to_O B)).
  1, 2: exact _. (* Coq finds these instances but then ignores them. *)
Abort.

[jdchristensen]

It can be simplified a bit further:

Class IsEquiv {A B : Type} (f : A -> B) := {}.

Class Reflects (B : Type) := {}.

Definition to_O (B : Type) `{Reflects B} : B -> B.
Admitted.

Global Instance isequiv_to_O (B : Type) `{Reflects B} : IsEquiv (to_O B).
Admitted.

Definition cancelL_isequiv {A B C} (g : B -> C) {f : A -> B}
  `{IsEquiv B C g} `{IsEquiv A C (fun a => g (f a))}
  : IsEquiv f.
Admitted.

Definition isequiv_O_rec_O_inverts
       {A B : Type} `{Reflects B} (f : A -> B)
  : IsEquiv f.
Proof.
  Typeclasses eauto := debug.
  simple refine (cancelL_isequiv (to_O B)).
  1, 2: exact _. (* Coq finds these instances but then ignores them. *)
Abort.

[Alizter]

@jdchristensen I think that would be worth reporting.

[jdchristensen]

In coq/coq#18526, it was explained that when there are dependencies between typeclass goals, earlier solutions are thrown away if later goals can't be automatically solved. I can see how this might be reasonable in some situations, but also think the behaviour I expected could be good. I also figured out that the reason that the version with (C:=O B) works is that unification solves the early typeclass goal, so it isn't part of the typeclass search. As an experiment, I tried redefining to O to take an RSU O instead of a subuniverse, so it no longer requires typeclass search. (I renamed the current to to to', and had to add primes whenever we had to O with O a subuniverse.) That allowed me to remove the annotation (C:=O B) here, but had no other effects. I thought that the library might build faster, but it was unchanged, and I thought that maybe some goals would be solved automatically, but none were. So I won't make a PR for that.