The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Kathrin,

  sorry for the delayed response. The pattern matching filtering phase is a purely syntactic operation, it cannot unify subterms as you expect, so here it fails to match because 0 and ?n are not syntactically equal. To avoid this, you can use a less refined pattern like so (actually, without filtered unification on, it's as if you used that pattern instead, where just the head of the application matters):

Class Test (x y : nat) := testeqn : x = y.

Set Typeclasses Filtered Unification.

Instance: forall n, Test n n | (Test _ _). (** This sets the pattern used by the filtering phase *)

Proof. reflexivity. Qed.

Set Typeclasses Debug Verbosity 2.

Goal True.

  eassert (Test 0 ?[n]). try typeclasses eauto.

  (* Here we get:

Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded

Debug: 1: looking for (Test 0 ?n) with backtracking

Debug: 1.1: simple apply Test_instance_0 with pattern (Test _ _) on (Test 0 ?n), 0 subgoal(s)

Debug: 1.1: after simple apply Test_instance_0 with pattern (Test _ _) finished, 0 goals are shelved and unsolved ( )

  exact I.

Qed.

Cheers,

-- Matthieu

On Wed, Jun 28, 2017 at 11:43 AM Kathrin Stark <kathrin.stark AT rz-online.de> wrote:

Hello,

I have a question concerning the "Typeclasses Filtered Unification"
option.

Using the typeclasses eauto tactic, I would like to unify a pattern of
the form
Test 0 ?n with another pattern of the form Test ?m ?m
  - however, Coq complains that the patterns do not match:
pattern (Test ?META158 ?META158) on (Test 0 ?n) failed with: pattern
does not match

I don't understand why - I would have guessed it could unify ?META158
with ?n with 0.
(Without the above option activated, it works out of course.)
So I wondered how exactly the pattern matching algorithm works? -
Unfortunately I didn't find an answer to that.

The minimal code example can be found below.

Thank you very much!

Best,
Kathrin S.


------------------------------------------------------
Class Test (x y : nat) := testeqn : x = y.

Unset Typeclasses Filtered Unification.
Instance: forall n, Test n n.
Proof. reflexivity. Qed.
Set Typeclasses Filtered Unification.

Set Typeclasses Debug Verbosity 2.

Goal True.
   evar (n : nat).
   assert (Test 0 ?n). try typeclasses eauto.
  (* Here we get:
  simple apply Test_instance_0 with pattern (Test ?META158 ?META158) on
(Test 0 ?n) failed with: pattern does not match *)
Abort.