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 :)

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`

)

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).`

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

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

Thanks for the explanation!

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