Stream: Coq users

Topic: ✔ "Overloading" notation of inductives using typeclasses

Matthis Kruse (Sep 07 2022 at 17:14):

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

Paolo Giarrusso (Sep 07 2022 at 17:36):

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

Paolo Giarrusso (Sep 07 2022 at 17:38):

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?

Paolo Giarrusso (Sep 07 2022 at 17:39):

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

Matthis Kruse (Sep 07 2022 at 17:45):

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

Paolo Giarrusso (Sep 07 2022 at 17:45):

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

Paolo Giarrusso (Sep 07 2022 at 17:45):

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

Paolo Giarrusso (Sep 07 2022 at 17:47):

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

Paolo Giarrusso (Sep 07 2022 at 17:47):

and Global Existing Instance pstep. declares pstep to be an instance

Matthis Kruse (Sep 07 2022 at 17:48):

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!

Notification Bot (Sep 07 2022 at 17:48):

Matthis Kruse has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC