Bhargav Kulkarni (Jul 01 2022 at 11:04): 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 :)
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)
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).
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
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
Bhargav Kulkarni (Jul 01 2022 at 11:19):Thanks for the explanation!
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: Sep 23 2023 at 08:01 UTC