The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Hi Eddy

As Pierre wrote, Trakt is able to do what you want. You can find 
examples here: 
https://github.com/ecranceMERCE/trakt/blob/master/example/Example.v#L303

The documentation is available here: https://ecrancemerce.github.io/trakt/#/

Best
Chantal



Le 14/10/2022 à 01:46, Eddy Westbrook a écrit :
> Mukesh and Pierre,
>
> It’s ironic that you would say that, because we actually go the other 
> direction, and only translate to Coq when we can’t just solve something with 
> SMT. Unfortunately, while SMT is good at proving properties of concrete sizes 
> of bitvectors, it is not good at proving properties for all sizes of 
> bitvector.
>
> Back to my original question: is it maybe the case that Add Zify is just a 
> thin wrapper around adding some hints to a particular database? If so, could 
> I add them in a way that generalizes over the width value?
>
> -Eddy
>
> > On Oct 13, 2022, at 2:07 PM, Pierre Vial <pvial2401 AT gmail.com> wrote:
> >
> >
> >
> > Le jeu. 13 oct. 2022 à 22:46, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com 
> > <mailto:mukeshtiwari.iiitm AT gmail.com>> a écrit :
> > This is not an answer to your question, but have you seen  SMTCoq [1, 2]. I 
> > haven’t used it in my projects but SMT solvers are good with length indexed 
> > vectors so most of your problems can be solved (but I could be wrong).
> >
> > [1] https://smtcoq.github.io/ <https://smtcoq.github.io/>
> > [2] https://github.com/smtcoq/sniper <https://github.com/smtcoq/sniper>
> >
> > I have a type function bitvector : nat -> Set that constructs the type of 
> > bitvectors (binary numbers) of a given bit width. Is it possible to get the zify 
> > tactic to support the class of types bitvector w for all w? The existing Add 
> > Zify commands seem to only work for a specific type.
> >
> >
> > Mukesh is right, Sniper not only features SMTsolving, but also Trakt which  
> > allows you to quickly implement an equivalent of zify w.r.t any integer type 
> > you want.
> > You will find examples on the sniper repository but also there  ( 
> > https://github.com/ecranceMERCE/trakt <https://github.com/ecranceMERCE/trakt> 
> > ) and I think Enzo Crance will be happy to answer any question you have on Zulip.
> >
> > --
> > Pierre