coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How do I add simple first-order equalities in a typeclass to a rewrite database?

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] How do I add simple first-order equalities in a typeclass to a rewrite database?
Date: Tue, 19 May 2020 11:29:59 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:qlnaAx28/rMl1VtfsmDT+DRfVm0co7zxezQtwd8ZseIUL/ad9pjvdHbS+e9qxAeQG9mCtrQd07Wd4vCocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTqwbalvIBmqrwjduc0bjIh/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6JVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOtEoIn9oVoOrQC+BQmrAePk1yFFhn/s0q0mz+QhFhnG0xY9ENIOsHXbttX0P7oVXO+vw6nIyzTDb+hW2Tf67YjFaQwuofSNXb5qa8Xe1VMjFwLDjliJr4HuIjya2PgXvWeB8+pgSfygi3QhqwxprDaj2Nogh4bVi44JxV7J6zh1zok6KNGkTEN2Yd6pHIVNui2EK4d7XscvTW9qtSs01rALup22cDULxZklyRPSb/qKeJWL7BL7TOudPCp0iXJ/dL6hiBu/8lKsxvPhWsWuzVpHrTZJnsHSunwR0xHf8MuKR/tn8ku82DuC1hrf5vxGLE06k6fQNoQvzaQqlpUJtETOBi/2l1vyjK+Rbkgk//Kn6+XjYrn8upCcMo50hhvkPasygMC/AOI4PhAPX2id5+u8yKXu8VDkTLhKlPE6jKbUvZPAKcgFu6K1GRJZ34U/5xqnCjepytUYnX0JLFJffxKHipDkNEvBIPD+DPe/mFSskDBux/3dIrLhB5TNImLZn7j9Z7p96khcxBIpzd9D/5JUFq0BIPXrV0Dts9zYFwY1PBCww+b6E9pwzZgeWGKKAq+BKqzeq16I5uQ1I+mNfoAZojj9K+J2r8Lp2HQ+gBoWebSj9ZoRcnGxWPp8cGuDZn+5q9gHEHwKuQ92Z+zjlEGFSTdfZ2e7Tupo7z49CZmmCoLrTYWsxrWKmia9SM4FLltaA0yBRC+7P76PXO0BPXrLf51R1wccXL3kcLcPkBGjsAijlehiJ+vQvCYdtNTq35504b+LzEBgxXlPF82Yllq1YSRxl2IMSSUx2fkm80d4yxGK2u55ha4BTIAB17ZySg4/cKXk4aliEdmrA1DKe9bPQV3gQ9P0WTw=

Hi;

I have a couple of typeclasses like this:

Class Lattice A :=
{
join : A -> A -> A;
meet : A -> A -> A;
join_comm : forall x y, join x y = join y x;
meet_comm : forall x y, meet x y = meet y x;
join_assoc : forall x y z, join (join x y) z = join x (join y z);
meet_assoc : forall x y z, meet (meet x y) z = meet x (meet y z);
absorb1 : forall x y, join x (meet x y) = x;
absorb2 : forall x y, meet x (join x y) = x;
}.

Infix "⊓" := meet (at level 85, right associativity).
Infix "⊔" := join (at level 80, right associativity).

Generalizable All Variables.

Class BoundedLattice A `{Lattice A}:=
{
bottom : A;
top : A;
join_bottom_r : forall x, (x ⊔ bottom) = x;
meet_top_r : forall x, (x ⊓ top) = x;
}.

Lemma join_bottom_l `{BoundedLattice} : forall x, (bottom ⊔ x) = x.
Proof.
intros. rewrite join_comm. now rewrite join_bottom_r.
Qed.

I'd like to be able to replace the last proof with `autorewrite with ...`. How do I add the equalities I have to a Rewrite Hint Database? Saying `Hint Rewrite join_comm`, for example, did not work.

--Agnishom

[Coq-Club] How do I add simple first-order equalities in a typeclass to a rewrite database?, Agnishom Chattopadhyay, 05/19/2020