Stream: Coq users

Topic: simpl on own type


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Feb 27 2023 at 11:12):

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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Feb 27 2023 at 13:53):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Feb 27 2023 at 14:19):

aac-tactics comes with a nice tutorial, btw.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Feb 27 2023 at 17:00):

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

view this post on Zulip 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