Ali Caglayan (Jun 17 2021 at 14:26): 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?
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).
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.
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?
Pierre-Marie Pédrot (Jun 18 2021 at 05:00):The matching code is very buggy, I'd recommend against using filtered unification.
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))
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
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
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
Pierre-Marie Pédrot (Jun 18 2021 at 07:41):@Matthieu Sozeau the difference of behaviour is exactly an instance of this problem, IIUC.
Pierre-Marie Pédrot (Jun 18 2021 at 07:42):The goal contains an evar, and the matching algorithm fails.
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.
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.
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
Pierre-Marie Pédrot (Jun 18 2021 at 07:43):applying H0, but it is filtered early with the flag on.
Matthieu Sozeau (Jun 18 2021 at 07:43):The goal IsEquiv (fun x => g (f x)) does not contain evars
Matthieu Sozeau (Jun 18 2021 at 07:44):Maybe in this instance there is more of an econstr problem
Pierre-Marie Pédrot (Jun 18 2021 at 07:45):(oh, yes, and there is that.)
Pierre-Marie Pédrot (Jun 18 2021 at 07:45):(pattern_of_constr delenda est.)
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
Matthieu Sozeau (Jun 18 2021 at 07:46):We should at least patch constr_matching to allow for the "right" behavior
Matthieu Sozeau (Jun 18 2021 at 07:48):Until then, Hint Extern is your friend Ali
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
Pierre-Marie Pédrot (Jun 18 2021 at 07:49):(and also use something else than pattern_of_constr)
Matthieu Sozeau (Jun 18 2021 at 07:49):Due to the backtracking you mean ?
Pierre-Marie Pédrot (Jun 18 2021 at 07:49):no, there are Ltac considerations hardwired in constr_matching
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: Apr 19 2024 at 12:02 UTC