coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Getting lra to work with canonical rationals

From: Théo Zimmermann <theo AT irif.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Getting lra to work with canonical rationals
Date: Fri, 9 Oct 2020 12:17:28 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
Ironport-phdr: 9a23:8k6MOxJ4GVjSoPjWStmcpTZWNBhigK39O0sv0rFitYgeIv3xwZ3uMQTl6Ol3ixeRBMOHsq0C1rOd6f6ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalyIRmrogndqMgbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2UxLjljsJOCAl/2HWksxwjbxUoBS9pxxk3oXYZJiZOOdicq/BeN8XQ3dKUMRMWCxbGo6zYIUPAOgBM+hWrIfzukUAogexCwS3GOPv0yVFimPq0aEm0eksFxzN0gw6H9IJtXTZtMv7NKcIVuCy1KbHzjTDb/ZT2Tjj8ojIdwouofeKXbltdsfR1UkvGB3CjliLqIzlJTKV1uoXv2iV9eptTOSigHMopA9tuDag3NssipXXiYIPzFDJ7Tl0zYUrKNGmVUN1YcOoHIdQuS+aKoZ7XsMvTmJntiokzrALvZC2cDQKxZoo2RLSa/6Kf5SU7x/sV+ucLyp1iG9jdbmiiRiy9k2gxff9VsmyyFtKoStFksXMtnAQzBPf8NSISvx4/kqnxD2B1BjT5/lZLU0wmqfXMYAtz74/m5YJsEnPAzX6lFj4gaKVbkko5PSk5uD9brjlppKQLZJ4hwD8P6g0lcGyAeI1ORUUUWeB4+Szzrjj8FX5QLpUiv02lbHUsJPdJcQBoa65BxFa0pg55xaiCTem0coYkWAfLF1fYhKHjpPpNlPULPD2F/ezm1WskDF1yPDaJrDtH5HAI3fZnLv/fbtw5FRQxQsuwdxF+p5ZBLIMLOr2WkDrtdzYChE5Mxazw+biENh9yoMeVnyIAqKCMaPSq16I5uw1L+mCfo8ZoCz9JOQ95/7ykX85nkcQcrWu3ZsOcXy3AvBmI1iCbnf3mdcAEWIKvhIkQ+DwiV2CVyRTZ3eoUK4m6DE7EtHuMYCWbYe0yJeFwS3zSpZRfyVNDk2GOXbubYSNHfkWPnG8OMhkxwAE1L+WeY4k0By0sQb8zfIzMurZ/QUZr5PtktZvsb6A3Sou/CB5WpzOm1qGSHt5yyZRH2dvgfJP5Hdlw1LG6pBWxvxVEdsJu6FKVR09MZPCifF8Cs63Qgvbf8zWDli8EI3/XWMBC+kpytpLWH5TXs24h0GR3jCrDfkbje7TXc1mwufnx3H0Yv1F5TPD3aglgUMhR5odNHeniOhx7VqKCg==

Hi Raphaël,

Have you used the transfer library recently? I haven't maintained it,
so I'm afraid it's probably not very useful anymore.

OTOH, CoqEAL has seen significant progress and several releases
recently. Given that the ideas on which it is based are essentially
the same (my own library was strongly inspired by the CoqEAL paper),
it might be useful in this case as well. I say "might" because the
documented use cases are not exactly the same and I haven't used it
myself. Cyril might be able to say more.

Théo

Le ven. 9 oct. 2020 à 11:15, Raphaël Cauderlier
<raphael.cauderlier AT nomadic-labs.com> a écrit :
>
> This library might help: https://github.com/Zimmi48/transfer
>
> > This library helps you working seamlessly with several representations
> > for the same objects, switching from one to another when doing proofs and
> > easily transferring theorems across representations.
> --
> Raphaël Cauderlier

[Coq-Club] Getting lra to work with canonical rationals, Elias Castegren, 10/08/2020
- Re: [Coq-Club] Getting lra to work with canonical rationals, Frédéric Besson, 10/08/2020
  - Re: [Coq-Club] Getting lra to work with canonical rationals, Tej Chajed, 10/08/2020
    - Re: [Coq-Club] Getting lra to work with canonical rationals, Raphaël Cauderlier, 10/09/2020
      - Re: [Coq-Club] Getting lra to work with canonical rationals, Théo Zimmermann, 10/09/2020
        
        Re: [Coq-Club] Getting lra to work with canonical rationals, Raphaël Cauderlier, 10/09/2020