Hey,

there exists this trick where you can "overload" notation by instancing on typeclasses.

I'm making use of this with the hope to "overload" notation of certain step relations of different programming languages that I'm modeling in Coq. It looks like this:

```
Class Expr (Expr : Type) := {}.
Class TraceEvent (Ev : Type) := {}.
Class PrimStep (A : Type) (Ev : Type) `{Expr A} `{TraceEvent Ev} := pstep__class : A -> Ev -> A -> Prop.
#[global]
Notation "e0 '--[' a ']-->' e1" := (pstep__class e0 a e1) (at level 82, e1 at next level).
Variant event : Type := empty : event.
#[local]
Instance event__Instance : TraceEvent event := {}.
Inductive expr :=
| lit : nat -> expr
| add : expr -> expr -> expr
.
#[local]
Instance expr__Instance : Expr expr := {}.
Inductive pstep : PrimStep :=
| pstep_add : forall (n1 n2 : nat), (add (lit n1) (lit n2)) --[ empty ]--> (lit(n1 + n2))
.
```

Unfortunately, I'm a bit stuck when it comes to doing a proof about such an inductive now, since it does not appear to be one!

Coq rejects the following with the error message `Error: Not an inductive product.`

:

```
Definition pstepf (e : expr) : option (event * expr) :=
match e with
| add (lit n1) (lit n2) => Some(empty, lit(n1 + n2))
| _ => None
end
.
Lemma equiv_pstep_pstepf {Hx : PrimStep} (e0 : expr) (a : event) (e1 : expr) :
e0 --[ a ]--> e1 <-> pstepf e0 = Some(a, e1).
Proof.
split.
- induction 1. (* Not an inductive product. *)
```

So, how can I possibly sidestep this issue? I'm aware that that typeclasses in Coq are some kind of fancier record, but I'm not sure how to "unpack" it.

Thanks in advance,

Matthis

your theorem statement is surprising; TLDR I suspect you should remove the `{Hx : PrimStep}`

assumption?

in fact, I don't understand how `{Hx : PrimStep}`

typechecks, but let's ignore that...

you have `e0 : expr`

: if `expr`

is the same type as you show, you probably intend to do a proof for a concrete language, so you don't need to abstract over which semantics to use?

OTOH, I presume the theorem is false for an arbitrary `PrimStep`

.

Thanks for your reply.

Paolo Giarrusso said:

OTOH, I presume the theorem is false for an arbitrary

`PrimStep`

.

gotcha. Of course, the theorem doesn't hold for arbitrary `PrimStep`

. :^)

My Coq knowledge seems to be too limited, the lemma statement doesn't typecheck without the `{Hx : PrimStep}`

and my best hope was that Coq would use `pstep e0 a e1`

for `e0 --[ a ]--> e1`

. Now I see that it doesn't, which makes sense. Whence, the error Coq gave also makes sense, since an arbitrary `PrimStep`

is not an inductive.

That being said, my intention is to use the previously defined inductive `pstep`

in the lemma statement, making use of the notation `_ --[ _ ]--> _`

.

Best regards,

Matthis

Once you fix that, the induction itself seems to work. Crucially, I declared `pstep`

to be an instance to make this work:

```
Inductive pstep : PrimStep expr event :=
| pstep_add : forall (n1 n2 : nat), (add (lit n1) (lit n2)) --[ empty ]--> (lit(n1 + n2))
.
Global Existing Instance pstep.
Definition pstepf (e : expr) : option (event * expr) :=
match e with
| add (lit n1) (lit n2) => Some(empty, lit(n1 + n2))
| _ => None
end
.
Lemma equiv_pstep_pstepf (e0 : expr) (a : event) (e1 : expr) :
e0 --[ a ]--> e1 <-> pstepf e0 = Some(a, e1).
Proof.
split.
- induction 1. (* works out *)
```

(I think I didn't change the earlier code)

whenever you use `pstep__class`

, Coq needs to find a typeclass instance to use — either because you abstract over one via `{Hx : PrimStep}`

, or because you declared one explicitly

and `Global Existing Instance pstep.`

declares `pstep`

to be an instance

Hey again and thanks for your additional reply!

Looks like I simply forgot to register it as an instance.... :see_no_evil:

Thanks, this solves my issues!

Matthis Kruse has marked this topic as resolved.

Last updated: Jan 29 2023 at 05:03 UTC