Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
rapply diverges when apply succeeds
At https://github.com/mikeshulman/HoTT/blob/wildcat/theories/Basics/WildCat.v#L287 if apply is replaced by rapply, Coq diverges in typeclass search with repeated opposites. (erapply, srapply, and serapply also diverge, but ntc_rapply works.) This seems to be because rapply tries refine (Build_Is0Coh2Functor _ _ _ _ _ _ _ _) (8 arguments) before the correct refine (Build_Is0Coh2Functor _ _ _ _ _ _ _ _ _) (9 arguments), and the former diverges. But why doesn't the former fail immediately, since its type is a function and can't possible match the goal? Is it because Coq tries to fill in the underscores in the term (with typeclass search) before refine gets ahold of it? But if so, then why doesn't it do the same for the one with 9 arguments?
I feel like if rapply were smart enough to look at the goal and guess immediately how many holes are needed, a lot of these problems wouldn't occur. @JasonGross didn't you have a version of rapply with that kind of behavior sitting around somewhere?
@JasonGross OK, I guess I was confusing it with the unspecified number of holes version then?
It wouldn't have to inspect the goal either; for the most common use case it would be sufficient to inspect the constructor being rapplied and see how many arguments it takes. I'd like to have a tactic like rconstructor that just has a list of all the constructors of records and classes, each refined with an appropriate number of holes; the problem is that as we define new records and classes there's no way to "add to" such a tactic. AFAIK the only "dynamic variables" in Ltac are hint databases, and they can only be called when they completely solve the goal.
@mikeshulman Are there actually cases where econstructor doesn't work? In any case, it should be pretty easy to write a tactic that adds n underscores to a term given a nat n, and it shouldn't be too hard to write a tactic that computes the number of arrows in a type.
econstructor is pretty good, but sometimes it leaves over arguments as unsolved evars rather than returning them as subgoals.
Don't we have a tactic constructor that does this? I only found out last week.
According to the refman, constructor is equivalent to intros; apply Build_X, which is rarely sufficient.
I'll try unshelve econstructor next time and see if it works better, thanks.
FWIW, I've recently been using simple refine (ci _ _ ...), filling some of the holes, and it works great: doesn't shelve anything.
Yes, simple refine (or, in some cases, simple notypeclasses refine) usually works. The goal here is to have a tactic that doesn't require counting the number of arguments to give exactly the right number of underscores (and is therefore less fragile when the number of arguments changes).
unshelve econstructor does seem to work, but it ends up with the goals in the wrong order.
I reported that issue as https://github.com/coq/coq/issues/4729 a bit under four years ago :-/
Actually unshelve econstructor doesn't always do what I want. In at least some cases, if the constructor has two fields X and Y, such that Y is a typeclass instance that can be solved in a way that instantiates X, then unshelve econstructor does that rather than letting me specify X manually.
Try this:
(* we don't use tactics in terms at all so as to allow this tactic to be multi-success *)
Ltac ntc_rconstructor :=
idtac; (* thunk the tactic, so if we pass it to another tactic, we don't get the goal too early *)
let rec to_uconstr v := lazymatch v with
| (fun x : ?A => ?f ?v)
=> let f' := to_uconstr (fun x : A => f) in
uconstr:(f' _)
| (fun _ => ?v) => v
end in
let G := match goal with |- ?G => G end in
let tmp := fresh in
let x := fresh in
simple refine (let tmp : (forall T : Type, T) -> G := _ in
_);
[ intro x;
unshelve econstructor; exact (x _)
| let v := (eval cbv delta [tmp] in tmp) in
clear tmp;
let v := to_uconstr v in
simple notypeclasses refine v ].
I haven't tried this yet, but it just occurred to me that I would really like to be able to manually control what counts as the "constructor" for a given type. That is, what I really want is a tactic that looks up the type of the goal in an alist somewhere to find a "constructor" to apply and the number of arguments to give it, where the alist can be dynamically added to as needed.
You can make a typeclass for "is a constructor of". Since typeclasses eauto is multisuccess, you can proably make a version of the tactic that uses that.
The key ingredients are:
- Use
simple refine+econstructorto get access to all the constructors in a multisuccess way- use a hypothesis of type
forall T, Tto fill any holes remaining fromeconstructor(note that this might not be enough due to lack of universe polymorphism), so we don't have dangling evars that we don't know how to fill
- use a hypothesis of type
- use recursion to replace each argument to the constructor with a uconstr
_
Does that explain things sufficiently, or do you want me to explain some bit in more detail?
Also, here's your typeclass-based tactic:
Class constructor_of {T} (type_family : T) {ctor_T} (ctor : ctor_T) := dummy_ctr : True.
Ltac head x :=
lazymatch x with
| ?f _ => head f
| _ => x
end.
Ltac count_arrows T :=
lazymatch (eval hnf in T) with
| forall x : ?A, @?T x
=> lazymatch constr:(
fun x : A
=> ltac:(let n := count_arrows (T x) in
exact n)) with
| fun _ => ?n => constr:(S n)
end
| _ => O
end.
Ltac wrap_with_underscores v n :=
lazymatch n with
| O => v
| S ?n => let v := wrap_with_underscores v n in
uconstr:(v _)
end.
Ltac ntc_rconstructor_by_tc :=
idtac;
let G := match goal with |- ?G => G end in
let type_family := head G in
let tmp := fresh in
let ctor := fresh in
simple notypeclasses refine (let ctor := _ in
let tmp : constructor_of type_family ctor := _ in
_);
[ shelve (* ctor type *)
| shelve (* ctor *)
| subst ctor; typeclasses eauto (* tmp *)
| let v := (eval cbv delta [ctor] in ctor) in
clear tmp ctor;
let T := type of v in
let n := count_arrows T in
let v := wrap_with_underscores v n in
simple notypeclasses refine v ].
Then you can do
Instance: constructor_of sum (@inl) := I.
Instance: constructor_of sum (@inr) := I.
Instance: constructor_of prod (@pair) := I.
Goal nat * nat.
ntc_rconstructor_by_tc.
I don't think we managed to come up with a good solution to this specific problem in the end, but we did change how we use rapply in the library. The current defacto convention is to prefer nrapply over rapply by default which works in 99% of cases (since ntc_rapply worked). There are very few cases where nrapply is insufficient and a typeclass search is required for unification to succeed. In those cases it is typically better to use a refine anyway.