## Stream: Coq users

### Topic: simpl on own type

#### Dennis H (Feb 27 2023 at 10:50):

So I'm trying to do something similar to the natural numbers game in Lean, where after defining natural numbers, and proving some theorems about addition, they can turn their type `mynat` into a monoid by typing `instance : add_comm_monoid mynat := by structure_helper`. I am wondering if it is possible to do something similar in Coq, so that I can use the `simpl` tactic on my own type `mynats`.

#### Gaëtan Gilbert (Feb 27 2023 at 10:55):

AFAIK simpl in lean does rewriting using proved equalities
this is not what simpl in Coq does, simpl in Coq does computation with some heuristics to decide when to keep constants folded and when to refold fixpoints
it can be guided a little, eg https://coq.github.io/doc/master/refman/language/extensions/arguments-command.html#args-effect-on-unfolding but cannot be extended as each constant has only 1 definition

#### Gaëtan Gilbert (Feb 27 2023 at 10:56):

maybe https://coq.github.io/doc/master/refman/proofs/automatic-tactics/auto.html#coq:tacn.autorewrite is closer to lean's simpl but I'm not familar with autorewrite so I don't know how well it works

#### Dennis H (Feb 27 2023 at 11:11):

Hmmm, `autorewrite` seems promising, but it does not really seem to work well with commutativity, since it will always match the equality in expressions. Basically (without showing all the involved theorems, but the names kind of speak for themselves) I would like to do something like

``````Lemma assoc_add (a b c : mynat) : a + (b + c) = a + b + c.
Proof.
Qed.

Example simplify (a b c d e : mynat) : (((a+b)+c)+d)+e=(c+((b+e)+a))+d.
Proof.
(* basically I want this to solve it immediately *)
Abort.
``````

This way with `autorewrite` it does rewrite from `a + b + c + d + e = c + (b + e + a) + d` to `a + b + c + d + e = c + b + e + a + d` (basically it just removes the brackets), but the reordering does not happen yet, adding the commutativity theorems (`add_comm`) to the hint makes coqtop freeze cause it seems to just infinitely rewrite this.

#### Gaëtan Gilbert (Feb 27 2023 at 11:12):

maybe look into https://github.com/coq-community/aac-tactics/ ?

#### Dennis H (Feb 27 2023 at 12:58):

That seems to do kind of what I want, but looking around I did find this: https://www.dc.fi.udc.es/staff/freire/coqdoc/pauillac.inria.fr/coq/doc/nod9.htm which seems to imply something like this could be done natively (with `ring_simplify`)? I can't find much on `Add Semi Ring` though, looking through the source code of coq I found this https://github.com/coq/coq/blob/master/theories/setoid_ring/Ring_theory.v#L102, but I am not sure how to use this...

#### Gaëtan Gilbert (Feb 27 2023 at 13:04):

ring is for rings, so if you don't have a multiplication operator it's useless

#### Laurent Théry (Feb 27 2023 at 13:15):

if you have a monoid structure only, you can look at the section Monoid Expression Simplifier in CPDT

#### Michael Soegtrop (Feb 27 2023 at 13:53):

See the manual entry for Add Ring. You find several examples of this in the standard library. The tactic to use a ring declared this way is ring. The same exists for fields. For "lesser" algebraic structures the already mentioned aac-tactics are the method of choice. Another method might be to use trakt to convert your goals to something `lia` can understand.

#### Michael Soegtrop (Feb 27 2023 at 13:53):

You see there are plenty of choices - depending on what exactly you want to do.

#### Dennis H (Feb 27 2023 at 14:13):

Laurent Théry zei:

if you have a monoid structure only, you can look at the section Monoid Expression Simplifier in CPDT

Thanks for the suggestion! I tried it with this by adapting the proofs to not use `crush`, but sadly it only really works for resolving associativity, and not commutativity...

The example they give is ` Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d.`, but trying it with something like `Lemma test (a b c d e : mynat) : (((a+b)+c)+d)+e=(c+((b+e)+a))+d.` does not work for example.

#### Dennis H (Feb 27 2023 at 14:14):

Michael Soegtrop zei:

See the manual entry for Add Ring. You find several examples of this in the standard library. The tactic to use a ring declared this way is ring. The same exists for fields. For "lesser" algebraic structures the already mentioned aac-tactics are the method of choice. Another method might be to use trakt to convert your goals to something `lia` can understand.

Yeah after some fiddling and looking around I got `Add Ring` to work, but indeed I do not really want to have the multiplication structure in there. I added it with some axioms, perhaps I can kind of "hide" it by using some strange function name for the multiplication, and not adding an infix etc. I think I might go with that, just so that I don't have to load in the external libraries (I had some trouble setting those up anyway).

#### Michael Soegtrop (Feb 27 2023 at 14:17):

@Dennis H, yes wrangling all these libraries can be time consuming - the raison d'être of `<advertising>` Coq Platform `</advertising>`. Opam is of course also fine, if you already have it set up.

#### Michael Soegtrop (Feb 27 2023 at 14:19):

aac-tactics comes with a nice tutorial, btw.

#### Michael Soegtrop (Feb 27 2023 at 14:33):

One more thought on this: if you do anything serious with Coq, you anyway will need Coq libraries. So it is not a good start to try to avoid them.

#### Dennis H (Feb 27 2023 at 14:38):

Michael Soegtrop zei:

Dennis H, yes wrangling all these libraries can be time consuming - the raison d'être of `<advertising>` Coq Platform `</advertising>`. Opam is of course also fine, if you already have it set up.

Yeah, I was having some trouble with Opam, but my situation now is that I'm kind of learning Coq still, and later on I will be using UniMath (I am not sure if I will really need more libraries besides that), and what I'm currently working on I want to get working in a docker container running ubuntu, where I don't want to install too much extra, but the way I think I will end up doing it is in this (rather hacky) fashion:

``````Require Import Ring_theory.
Require Export Ring.

Module SemiRingFaking.
(* Some stuff to fake the `simpl` tactic to only affect
our own version of addition by defining some sort of fake
multiplication and a bunch of axioms to make the semi-ring
structure hold *)

Axiom _fake_mul : mynat -> mynat -> mynat.
Axiom _fake_one : mynat.

Axiom _fake_one_mul : forall a : mynat, _fake_mul _fake_one a = a.
Axiom _fake_zero_mul : forall a : mynat, _fake_mul 0 a = 0.
Axiom _fake_mul_comm : forall (a b: mynat), _fake_mul a b = _fake_mul b a.
Axiom _fake_mul_assoc : forall (a b c: mynat), _fake_mul a (_fake_mul b c) = _fake_mul (_fake_mul a b) c.
Axiom _fake_distr_mul : forall (a b c : mynat), _fake_mul (a + b) c = (_fake_mul a c) + (_fake_mul b c).

Lemma assoc_add (a b c : mynat) : a + (b + c) = (a + b) + c.
Proof.
Qed.

Definition mynat_semi_ring :=
mk_srt 0 _fake_one add _fake_mul (@eq _)
_fake_mul_assoc _fake_distr_mul.

End SemiRingFaking.

``````

Unless of course someone here has tips on how to do this in an easier or better way.

#### Michael Soegtrop (Feb 27 2023 at 14:55):

I would still recommend to install coq platform in your container and use aac-tactics. You can use extent "b" or "i" to install just coq (and cooqide for i). This will install opam (my scripts do a some sanity checks and should be bullet proof to quite some caliber). Then you can do `opam install coq-aac-tactics`. You can later install coq-unimath in the same way.

#### Michael Soegtrop (Feb 27 2023 at 14:55):

There is also a Coq Platform snap package btw. which installs in a few minutes in Ubuntu (download + extract time).

#### Paolo Giarrusso (Feb 27 2023 at 17:00):

Are aac-tactics and unimath compatible? I ask because unimath uses -noinit and -indices-matter

#### Gaëtan Gilbert (Feb 27 2023 at 17:05):

unimath using -indices-matter is a trick, they also use -type-in-type

Last updated: Jun 24 2024 at 00:02 UTC