Stream: Coq users

Topic: Customize tactics used in typeclass search


view this post on Zulip Ali Caglayan (Jun 17 2021 at 14:26):

Typeclasses uses tactics such as simple apply during search. Am I able to replace these with refine based versions like rapply?

view this post on Zulip Matthieu Sozeau (Jun 17 2021 at 15:32):

That's a common request. Set Typeclasses Filtered Unification uses refine instead but also imposes to use syntactic filtering first, with the inferred pattern for the hint (or one you specify yourself).

view this post on Zulip Ali Caglayan (Jun 17 2021 at 22:15):

This seems to break a lot of things for me however. Typeclasses Debug also says that simple apply is still being used with filtered unification.

view this post on Zulip Ali Caglayan (Jun 17 2021 at 22:18):

Here is with filtered unification:

1: looking for (IsEquiv (g o f)) without backtracking
1.1: unfold pointwise_paths on (IsEquiv (g o f)), 1 subgoal(s)
1.1-1 : (IsEquiv (fun x : A => g (f x)))
1.1-1: looking for (IsEquiv (fun x : A => g (f x))) without backtracking
1.1-1.1: simple apply @isequiv_compose with pattern
(IsEquiv (fun x : ?META93 => ?META98 (?META95 x))) on
(IsEquiv (fun x : A => g (f x))), 2 subgoal(s)
1.1-1.1-1 : (IsEquiv ?Goal0)
1.1-1.1-1: looking for (IsEquiv ?Goal0) with backtracking
1.1-1.1-1: no match for (IsEquiv ?Goal0), 7 possibilities

Here is without:

1: looking for (IsEquiv (g o f)) without backtracking
1.1: unfold pointwise_paths on (IsEquiv (g o f)), 1 subgoal(s)
1.1-1 : (IsEquiv (fun x : A => g (f x)))
1.1-1: looking for (IsEquiv (fun x : A => g (f x))) without backtracking
1.1-1.1: simple apply @isequiv_compose on
(IsEquiv (fun x : A => g (f x))), 2 subgoal(s)
1.1-1.1-1 : (IsEquiv f)
1.1-1.1-1: looking for (IsEquiv f) without backtracking
1.1-1.1-1.1: exact H0 on (IsEquiv f), 0 subgoal(s)
1.1-1.1-2 : (IsEquiv g)
1.1-1.1-2: looking for (IsEquiv g) without backtracking
1.1-1.1-2.1: exact H on (IsEquiv g), 0 subgoal(s)
Finished run 1 of resolution.
equiv_compose is defined

Why is filtered unification failing?

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 05:00):

The matching code is very buggy, I'd recommend against using filtered unification.

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 05:02):

Essentially it doesn't take evars properly into account, so the type of H0 is too constrained to match isEquiv (fun x => (g (f x))

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:29):

Wait, it succeeded so matching succeded and it's evarconv/refine's unification that fails to instantiate ?Goal0 here it seems

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:30):

Yes, the debug is misleading, it will keep printing "simple apply" even if the tactic is more match_pattern p <*> refine lemma <*> shelve_unifiable

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:33):

But @Pierre-Marie Pédrot has a good point. Pattern matching is broken when the pattern contains evars. Though there are only metas generated here, so it should avoid that pitfall in general

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:41):

@Matthieu Sozeau the difference of behaviour is exactly an instance of this problem, IIUC.

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:42):

The goal contains an evar, and the matching algorithm fails.

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:42):

If you can't have evars in your typeclass resolution it makes the flag essentially useless.

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:43):

It's not super hard to fix, but this will change everything. So anyone using the flag (are there any?) will have to adapt the code.

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:43):

But if you look at the trace without filtered unif, unification succeeded to produce IsEquiv f and IsEquiv g constraints by (apply) unification

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:43):

applying H0, but it is filtered early with the flag on.

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:43):

The goal IsEquiv (fun x => g (f x)) does not contain evars

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:44):

Maybe in this instance there is more of an econstr problem

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:45):

(oh, yes, and there is that.)

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:45):

(pattern_of_constr delenda est.)

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:45):

But yes you're right, as soon as the constraints will contain evars this will break too

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:46):

We should at least patch constr_matching to allow for the "right" behavior

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:48):

Until then, Hint Extern is your friend Ali

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:49):

I think we should use a dedicate algorithm, constr_matching is already too complex for its own good

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:49):

(and also use something else than pattern_of_constr)

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 07:49):

Due to the backtracking you mean ?

view this post on Zulip Pierre-Marie Pédrot (Jun 18 2021 at 07:49):

no, there are Ltac considerations hardwired in constr_matching

view this post on Zulip Ali Caglayan (Jun 18 2021 at 12:29):

By the way, I just enabled filtered unification for the HoTT library if you are looking for examples.


Last updated: Jan 27 2023 at 00:03 UTC