🔦 CSLib feature spotlight: fresh values. A great example of theory meeting practice.
In many explanations of programs and proofs in computer science, you might find sentences like:
- 'Pick a fresh value x not in the set'
- 'For a fresh x'
- 'Where x is a fresh name not in the program P'
etc.
I myself must've seen this pattern hundreds of times in compilers, process models, and semantics – to mention a few.
1/
We offer a library-level solution in #CSLib through the 'HasFresh' typeclass. Whatever the type of x is, you just need to convince #Lean that there's a 'fresh' value generator and you're good to go with your proofs. For many types (like natural numbers), we've even already convinced Lean for you.
This way, you can make reusable definitions that work for any type x might have, instead of hardcoding your model on something ad hoc.
2/
Generality brings further utility. Based on HasFresh, CSLib's free_union tactic will automatically look at your context for you and try to collect all current values into a finite set. You can then use HasFresh's API to get a fresh value that is different from all those in your context.
Just like on pen and paper: pick a fresh x!
Check out HasFresh at https://api.cslib.io/docs/Cslib/Foundations/Data/HasFresh.html
3/3
Fabrizio Montesi ⬣ A➔B