search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 231 forks source link

Some basic simplification rules for reals #3305

Closed mtzguido closed 3 months ago

mtzguido commented 4 months ago

There are no primops or simplification rules for reals, which means 1.0R >. 0.0R goes to SMT.

I'm marking this as a draft since it's really some special casing to check for common VCs in Pulse. I could write something more general.. it's just slightly annoying as we have to work with the string representations and make sure we check for canonicity (1.0R vs 01.00R, etc). I wonder if, instead, we should write a library of rational numbers.

mtzguido commented 3 months ago

This is definitely incomplete, but already useful, so I'll merge it.