How to formalize substructures (subrings, subspaces etc.) in Coq?

Using Coq
1

For example, let’s take very simple structure.

Structure smth A := {
op: A -> A -> A;
op_comm: forall x y, op x y = op y x
}.

How to make/model “subsmth”? Or maybe work around somehow?

2

This is what I got. Let’s hope I didn’t mess anything up in such short code.

Structure smth A := {
  op: A -> A -> A;
  _: forall x y, op x y = op y x
}.
Definition injective A B (f: A -> B) := forall x y, f x = f y -> x = y.
Definition subsmth A B (sA: smth A) (sB: smth B): Prop :=
  exists (f: A -> B), injective f /\ forall x y, f (op sA x y) = op sB (f x) (f y).
1 Like