Just like on pen and paper: pick a fresh x!

Check out HasFresh at api.cslib.io/docs/Cslib/F...

#FormalMethods #FORM

6/6

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.

5/

This way, you can make reusable definitions that work for any type x might have, instead of hardcoding your model on something ad hoc.

4/

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.

3/

I myself must've seen this pattern hundreds of times in compilers, process models, and semantics – to mention a few.

We offer a library-level solution in #CSLib through the 'HasFresh' typeclass.

2/

🔦 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.

1/

If you’re curious about its progress, the contributions we seek, or the open challenges we’re discussing, watch this space. I’ll start sharing updates about these topics soon.

#FormalMethods #FORM

🚀 CSLib is Growing – Follow Its Journey!

The #Lean Computer Science Library (#CSLib) – a global effort to build reusable infrastructure for formal methods in AI-ready computer programming and research – is gaining momentum (>100 forks, >400 PRs, and nearly 500 stars on GitHub).

(1/2)