Dennis H (Feb 27 2023 at 10:50): 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.
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.
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
liacan 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.
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.
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: Apr 18 2024 at 21:01 UTC