feat: add linear logic tests/benchmark #302
Conversation
There was a problem hiding this comment.
Pull request overview
This PR introduces a comprehensive test suite for the Classical Linear Logic (CLL) implementation in CSLib. The tests serve both as verification of the implementation and as pedagogical examples demonstrating the syntax and semantics of linear logic. The PR includes a proof of a linear logic theorem from the ILLTP (Intuitionistic Linear Logic Theorem Prover) library, specifically Example 37 from Figure 5 of the referenced paper.
Changes:
- Added extensive tests for CLL covering proposition construction, duality, proofs, equivalences, inversions, and classifications
- Included a concrete proof example from academic literature (arxiv.org/abs/1904.06850) demonstrating linear implication
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| I use `Proposition Nat` as the concrete instantiation for atoms. | ||
| -/ | ||
|
|
||
| open Cslib.CLL |
There was a problem hiding this comment.
The test file is missing the namespace CslibTests wrapper that is used consistently in other test files (see CslibTests/CCS.lean, CslibTests/Bisimulation.lean, CslibTests/LTS.lean, CslibTests/LambdaCalculus.lean, CslibTests/DFA.lean, CslibTests/FreeMonad.lean). The file should be wrapped in namespace CslibTests ... end CslibTests to follow the established convention.
CslibTests/CLL.lean
Outdated
| !(A ⊸ B) ⊸ B = (!(A ⊸ B))⫠ ⅋ B = ʔ(A ⊗ B⫠) ⅋ B | ||
| !A ⊸ B = (!A)⫠ ⅋ B = ʔA⫠ ⅋ B | ||
| B ⊸ (!A ⊸ B) = B⫠ ⅋ (ʔA⫠ ⅋ B) -/ | ||
| --/ |
There was a problem hiding this comment.
There is a spurious comment marker --/ on line 225 that should be removed. The doc comment starting at line 209 already closes with -/ on line 224, making this extra marker unnecessary and potentially confusing.
| --/ |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
I think it is a good general idea to have these sorts of examples as a sanity check that we've correctly defined various logics and languages.
(Leaving approval to Fabrizio since he wrote this module)
| B ⊸ (!A ⊸ B) = B⫠ ⅋ (ʔA⫠ ⅋ B) | ||
| -/ | ||
| example : ⇓({b⫠, (!(a ⊸ b) ⊸ b) ⊗ (b ⊸ (!a ⊸ b))} : Sequent Nat) := by | ||
| apply Proof.rwConclusion (Multiset.pair_comm ..) |
There was a problem hiding this comment.
We try to follow the convention of not constructing data (non-propositions) with tactics, though it is very awkward for linear logic.
There was a problem hiding this comment.
Hi @chenson2018, I thought about that. The first version of the proof was a term-based proof. But the bottom-up approach to the tactics - at least in the case of LL - makes the proof much clearer. But I am open to respecting any decision.
There was a problem hiding this comment.
I completely agree that it is natural to write this way. I'm fine with leaving it this way for a test file. If it breaks for whatever reason, this is also interesting information and easily fixed.
For all logics that are likely to be implemented, it would be interesting to have a test suite that not only demonstrates how the definitions of syntax and semantics work, but also serves a didactic purpose through concrete instantiations of the logic. In this PR, I suggest some initial tests for the linear logic already implemented in CSLib. In addition to tests for syntax and trivial equivalences, I present a proof of a linear logic theorem that I picked at random from https://arxiv.org/abs/1904.06850. From this PR onward, we can think about more systematic methods for constructing proof benchmarks. ``` @Article{Olarte_2019, title={The ILLTP Library for Intuitionistic Linear Logic}, volume={292}, ISSN={2075-2180}, url={http://dx.doi.org/10.4204/EPTCS.292.7}, DOI={10.4204/eptcs.292.7}, journal={Electronic Proceedings in Theoretical Computer Science}, publisher={Open Publishing Association}, author={Olarte, Carlos and de Paiva, Valeria and Pimentel, Elaine and Reis, Giselle}, year={2019}, month=apr, pages={118–132}} ```
For all logics that are likely to be implemented, it would be interesting to have a test suite that not only demonstrates how the definitions of syntax and semantics work, but also serves a didactic purpose through concrete instantiations of the logic. In this PR, I suggest some initial tests for the linear logic already implemented in CSLib. In addition to tests for syntax and trivial equivalences, I present a proof of a linear logic theorem that I picked at random from https://arxiv.org/abs/1904.06850. From this PR onward, we can think about more systematic methods for constructing proof benchmarks. ``` @Article{Olarte_2019, title={The ILLTP Library for Intuitionistic Linear Logic}, volume={292}, ISSN={2075-2180}, url={http://dx.doi.org/10.4204/EPTCS.292.7}, DOI={10.4204/eptcs.292.7}, journal={Electronic Proceedings in Theoretical Computer Science}, publisher={Open Publishing Association}, author={Olarte, Carlos and de Paiva, Valeria and Pimentel, Elaine and Reis, Giselle}, year={2019}, month=apr, pages={118–132}} ```
3 participants
For all logics that are likely to be implemented, it would be interesting to have a test suite that not only demonstrates how the definitions of syntax and semantics work, but also serves a didactic purpose through concrete instantiations of the logic.
In this PR, I suggest some initial tests for the linear logic already implemented in CSLib. In addition to tests for syntax and trivial equivalences, I present a proof of a linear logic theorem that I picked at random from https://arxiv.org/abs/1904.06850. From this PR onward, we can think about more systematic methods for constructing proof benchmarks.