search

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
https://math-classes.github.io
MIT License
162 stars 43 forks source link

added group tactic and automated some proofs in groups.v #100

Closed mdgeorge4153 closed 3 years ago

mdgeorge4153 commented 3 years ago

I created a group_simplify tactic that simplifies group expressions by first pushing group morphisms and negations all the way down to the leaves, and then cancels out multiple negations, inverses, and mon_unit. I used this tactic to simplify and automate the proofs of several lemmas in groups.v.

This is my first serious attempt at writing new proof automation, so feedback would be appreciated.

spitters commented 3 years ago

Thanks. Looks good.

mdgeorge4153 commented 3 years ago

I updated the group tactic to use easy instead of firstorder, and updated the proofs as necessary.

spitters commented 3 years ago

LGTM. Shall I merge?

mdgeorge4153 commented 3 years ago

I think so!

From: Bas Spitters @.> Sent: Thursday, June 10, 2021 3:37:50 AM To: coq-community/math-classes @.> Cc: Michael David George @.>; Author @.> Subject: Re: [coq-community/math-classes] added group tactic and automated some proofs in groups.v (#100)

LGTM. Shall I merge?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://github.com/coq-community/math-classes/pull/100#issuecomment-858389338, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAJ2CMOBFAWIRRTO4IDE2TLTSBTU5ANCNFSM46BTNFDQ.