Typeclasses uses tactics such as
simple apply during search. Am I able to replace these with refine based versions like
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).
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.
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?
The matching code is very buggy, I'd recommend against using filtered unification.
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))
Wait, it succeeded so matching succeded and it's evarconv/refine's unification that fails to instantiate ?Goal0 here it seems
Yes, the debug is misleading, it will keep printing "simple apply" even if the tactic is more
match_pattern p <*> refine lemma <*> shelve_unifiable
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
@Matthieu Sozeau the difference of behaviour is exactly an instance of this problem, IIUC.
The goal contains an evar, and the matching algorithm fails.
If you can't have evars in your typeclass resolution it makes the flag essentially useless.
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.
But if you look at the trace without filtered unif, unification succeeded to produce
IsEquiv f and
IsEquiv g constraints by (apply) unification
applying H0, but it is filtered early with the flag on.
IsEquiv (fun x => g (f x)) does not contain evars
Maybe in this instance there is more of an econstr problem
(oh, yes, and there is that.)
(pattern_of_constr delenda est.)
But yes you're right, as soon as the constraints will contain evars this will break too
We should at least patch
constr_matching to allow for the "right" behavior
Hint Extern is your friend Ali
I think we should use a dedicate algorithm, constr_matching is already too complex for its own good
(and also use something else than pattern_of_constr)
Due to the backtracking you mean ?
no, there are Ltac considerations hardwired in constr_matching
By the way, I just enabled filtered unification for the HoTT library if you are looking for examples.
Last updated: Sep 30 2023 at 05:01 UTC