Repository navigation
Conversation
thomaskwaring
left a comment
thomaskwaring
left a comment
There was a problem hiding this comment.
first pass — in general there seems to be a lot of back-and-forth between multisets and lists, do you think there's any way to avoid this? say by having a more "computational" inference system using lists, then only converting at the end
| @Proof.IsCutFree Atom ((!a) ::ₘ Γ) (Proof.bang (a := a) (Γ := Γ) hΓ p) := hp | ||
|
|
||
| /-- Recursor for cut-free proofs: never sees the `cut` case. -/ | ||
| @[induction_eliminator, cases_eliminator, elab_as_elim] |
There was a problem hiding this comment.
i think we should consider the alternate design where CF.Proof is it's own inductive type, and the generated recursor for that type replaces this def — that would make the above isCutFree_* obsolete, same with the below CF.Proof.*. The tradeoff is that the coercion to ordinary proofs is no longer immediate, but i think that's easier to handle.
There was a problem hiding this comment.
My long-term intention is to make a metaprogram (or at least something that makes this easy) for this kind of stuff, so I'd like to keep this as a use case, is that ok?
thomaskwaring
left a comment
thomaskwaring
left a comment
There was a problem hiding this comment.
first pass — in general there seems to be a lot of back-and-forth between multisets and lists, do you think there's any way to avoid this? say by having a more "computational" inference system using lists, then only converting at the end
0bb10ce to
e74826e
Compare
|
@thomaskwaring, I'm still thinking about the PSigma comment, but the rest is done. Thank you for the detailed read. Any new thoughts? |
Adds a cut elimination procedure for CLL. The definition requires a list representation of the sequent (since that's a multiset) for computability reasons. The PR also adds a multiset grind set for multiset rewritings, which has been very useful to formulate a series of utility lemmas for improving the efficiency of several pieces of the cut elimination/admissibility proofs.
AI disclosure and discussion:
This PR is also an AI-assisted formalisation milestone. Cut elimination is a very tedious proofs with lots of cases, rewritings, and nontrivial termination arguments. I've used cut elimination as a test for AI agents for a while, and until recently they failed badly. The same AI agents now managed to formulate appropriate induction principles and carry out the proof. I've reviewed the most important pieces and refactored/polished a lot of the code.
It seems that one of the biggest difference makers has been that the repository has grown enough to give useful context. In particular all the developments about logic, the various READMEs, and the introduction of the
modalgrind set seem to have been important to 'inspire' the AI on how to work. I suspect CSLib is starting to make a difference in AI performance.Depends on #941 and #938.