Stream: Coq users

Topic: unification errors


view this post on Zulip Bhargav Kulkarni (Jul 01 2022 at 11:04):

Hello everyone,
I am having a couple of issues trying to write down a inductive relation that uses a record:

(* imports omitted *)
Record dfa: Type := {
  statesType: Type;
  ΣType: Type;
  states: list statesType;
  Σ: list ΣType;
  s: statesType;
  F: statesType -> bool;
  δ: statesType -> ΣType -> statesType;
}.

Definition words M := list M.(ΣType).

Reserved Notation "p /~(M) q" (at level 80).
Inductive distinguishable (M: dfa) (p q: M.(statesType)): Prop :=
| distBase: forall M p q, M.(F) p <> M.(F) q -> p /~(M) q
where "p /~(M) q" := (distinguishable M p q).

When I try to define the distinguishable inductive relation I get a unification error:

In environment
distinguishable : forall M : dfa, statesType M -> statesType M -> Prop
M : dfa
p : statesType M
q : statesType M
M0 : dfa
p0 : statesType M0
q0 : statesType M0
n : F M0 p0 <> F M0 q0
Unable to unify "distinguishable M0 p0 q0" with "distinguishable M p q".

Any help to figure out why this is happening would be appreciated :)

view this post on Zulip Gaëtan Gilbert (Jul 01 2022 at 11:09):

try

Inductive distinguishable (M: dfa) (p q: M.(statesType)): Prop :=
| distBase: M.(F) p <> M.(F) q -> p /~(M) q

(ie without the forall M p q)

view this post on Zulip Bhargav Kulkarni (Jul 01 2022 at 11:12):

Oh, I tried that and the unification errors seem to have gone. Could you please explain why doing this stopped the error?
I also seem to have a new error regarding the notation

Reserved Notation "p /~(M) q" (at level 80).
Inductive distinguishable (M: dfa) (p q: M.(statesType)): Prop :=
| distBase: M.(F) p <> M.(F) q -> p /~(M) q
where "p /~(M) q" := (distinguishable M p q).

now gives me:

The reference M was not found in the current environment.

referring to the second M in where "p /~(M) q" := (distinguishable M p q).

view this post on Zulip Yannick Forster (Jul 01 2022 at 11:14):

you need spaces around the M, both when reserving the notation and when declaring it. Otherwise /~(M) becomes a symbol of the notation and Coq doesn't recognise that M` is supposed to be a variable

view this post on Zulip Yannick Forster (Jul 01 2022 at 11:17):

To see why the first thing fails, notice that it's equivalent to

Inductive distinguishable (M: dfa) (p q: M.(statesType)): Prop :=
| distBase: forall M' p' q', M'.(F) p' <> M'.(F) q' -> p' /~(M') q'
where "p /~(M) q" := (distinguishable M p q).

so you are saying that you define what it means to be distinguishable for M, p and q, but then really define it for different M', p', and q'`. The alternative to make it work is

Inductive distinguishable : forall (M : dfa), M.(statesType) -> M.(statesType) -> Prop :=
| distBase: forall M p q, M.(F) p <> M.(F) q -> p /~(M) q
where "p /~( M ) q" := (distinguishable M p q).

i.e. make all arguments indices rather than parameters

view this post on Zulip Bhargav Kulkarni (Jul 01 2022 at 11:19):

Thanks for the explanation!

view this post on Zulip Gaëtan Gilbert (Jul 01 2022 at 11:20):

with that alternative destruct/matching will be a lot more annoying so don't use it


Last updated: Jan 29 2023 at 03:28 UTC