coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Samuel Gruetter <gruetter AT mit.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] morphism option of ring tactic
- Date: Fri, 10 Aug 2018 13:16:14 +0000
- Accept-language: en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gruetter AT mit.edu; spf=Pass smtp.mailfrom=gruetter AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-1.mit.edu
- Ironport-phdr: 9a23:TxRzeRb4HLWONouMkQU8pUL/LSx+4OfEezUN459isYplN5qZr8y+bnLW6fgltlLVR4KTs6sC17KI9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa8bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrhKvpRN/wpLbbo6aO/dlYqPSZskXSXZdUspNVSFMBJ63YYsVD+oGOOZVt5TzqEELrRujGwasAP7kxD5Shn/rw6I6z/ghHh/c3Ac9GN8Ov27UrMjrO6cOTeC60rPIwC7Gb/NXxTfx8pbHfQ08ofyVW797bMTfyU4qFwzfj1WQr5ToPzyU1uQRs2ib8vFvWfizhG4grgF8pCWkyMQ0ioTRm44YyUrI+CFjzIorJdC0UlN3bcC8HJZSuSyWLZZ6Tt8+T21ypSo3yLwLtYSlcCQW0Jgr2h/SZvidf4SW4h/uW/ydLSpiiH54Zr6zmxC/+lW6xOLmTMm7ylNKozJFktbSsnAN0ATe5dWCSvp850uh3CyA1wHX6uFfP087ibPXK4U9zbEqkJoTt1rMHjXvlEnrlqOWc0Qk+vSy5+v5f7rmu4eQN45yig7gLqQjgtGzDOciPgUKRWSX5+Sx2Kf+8UHnWLlKi+c5kqjdsJDUP8Qboau5Dhda0oY59hawESum0MgGknkdN19FfROHj5TzN17QPf/4EO+zg06wnzdz2/DGIrrhD43RIXjEibftZKpy60pByAUo1t1f/JJVCrQZIP3pQEPxtdrYDgU4MwOu2ernBs99hcsiXjfFCaiAdajWrFWg5+Q1IuDKapVf8GL2LOFg7Przh1c4n0UcdO+nx81ERmq/G6FdKkCEbH6krc0cHHsWsxB2GOPwlVCeTTNJT3OzQ+Qx6ixtW9HuNpvKWo342O/J5yy8BJADPjkXWGDJKm/hcsC/Y9lJbSuTJsF7lTlVB72gV8ks2Qz87VammYoiFfLd/2gjjbymzMJ8tr/WlA10+DBpXZzEjjO9Clpsl2ZNfAcYmaBypUsmkwWP1Lo9hvVZEcde7LZSWQ48M5PGirU8DtHuHA/NY4XRRQ==
> 1.) There is an (undocumented) tactic called "is_constructor". This might
> simplify your checks. There is also a tactic to check for ground terms in
> the pipeline. Search for "is_" in
> https://github.com/coq/coq/blob/master/plugins/ltac/extratactics.ml4 for
> other undocumented term classification tactics (I have it on my to do list
> to write the documentation).
>
Turns out the library already has an Ltac isZcst:
https://github.com/coq/coq/blob/629fbc743f8b5e7623a6834f19885b2e379cb782/plugins/setoid_ring/InitialRing.v#L883
> 2.) In case you are working on large terms, it might be worthwhile to do a
> performance comparison of autorewrite vs. repeat rewrite vs. rewrite_strat
> vs. match context + rewrite. A usage of rewrite_strat for your case would
> look as below, but there are quite a few options one can try:
>
> [rewrite_strat (bottomup terms ZToReg_morphism.(morph_add)
> ZToReg_morphism.(morph_sub) ZToReg_morphism.(morph_mul))]
>
> In case you look into this, I would be interested in the results. I did
> test this in the past, but I had only rater modest term sizes where it did
> not make much of a difference and didn't bother to create large artificial
> terms. For large term sizes, timing might be substantially different.
>
For ring preprocessing, I didn't have any large terms so far, but I did for
expressions involving Z.testbit. There, switching from "repeat rewrite" to
rewrite_strat yielded a ~10x speedup:
https://github.com/mit-plv/riscv-coq/commit/4d83bc164c
- [Coq-Club] morphism option of ring tactic, Samuel Gruetter, 08/06/2018
- RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/07/2018
- RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/07/2018
- Re: [Coq-Club] morphism option of ring tactic, Samuel Gruetter, 08/08/2018
- RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/08/2018
- Re: [Coq-Club] morphism option of ring tactic, Samuel Gruetter, 08/10/2018
- RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/08/2018
- Re: [Coq-Club] morphism option of ring tactic, Samuel Gruetter, 08/08/2018
- RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/07/2018
- RE: [Coq-Club] morphism option of ring tactic, Soegtrop, Michael, 08/07/2018
Archive powered by MHonArc 2.6.18.