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
.
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
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
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.
now rewrite add_assoc.
Qed.
Global Hint Rewrite assoc_add zero_add add_zero add_succ succ_add: addition.
Example simplify (a b c d e : mynat) : (((a+b)+c)+d)+e=(c+((b+e)+a))+d.
Proof.
autorewrite with addition.
(* 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.
maybe look into https://github.com/coq-community/aac-tactics/ ?
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...
ring is for rings, so if you don't have a multiplication operator it's useless
if you have a monoid structure only, you can look at the section Monoid Expression Simplifier in CPDT
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.
You see there are plenty of choices - depending on what exactly you want to do.
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.
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).
@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.
aac-tactics comes with a nice tutorial, btw.
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.
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.
rewrite add_assoc; easy.
Qed.
Definition mynat_semi_ring :=
mk_srt 0 _fake_one add _fake_mul (@eq _)
zero_add add_comm assoc_add _fake_one_mul _fake_zero_mul _fake_mul_comm
_fake_mul_assoc _fake_distr_mul.
End SemiRingFaking.
Add Ring mynat_ring : SemiRingFaking.mynat_semi_ring.
Unless of course someone here has tips on how to do this in an easier or better way.
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.
There is also a Coq Platform snap package btw. which installs in a few minutes in Ubuntu (download + extract time).
Are aac-tactics and unimath compatible? I ask because unimath uses -noinit and -indices-matter
unimath using -indices-matter is a trick, they also use -type-in-type
Last updated: Oct 13 2024 at 01:02 UTC