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.
| variable {Atom : Type u} {a b : Proposition Atom} {Γ Δ Θ : Sequent Atom} | ||
|
|
||
| /-- Derive `BEq` from `DecidableEq` for proposition comparison. -/ | ||
| local instance [DecidableEq Atom] : BEq (Proposition Atom) := instBEqOfDecidableEq |
There was a problem hiding this comment.
you can omit this if you also delete the deriving BEq from CLL.Proposition, which i think is better (when would we have BEq but not DecidableEq which implies it)
| /-- Derive `BEq` from `DecidableEq` for proposition comparison. -/ | ||
| local instance [DecidableEq Atom] : BEq (Proposition Atom) := instBEqOfDecidableEq | ||
|
|
||
| namespace Sequent |
There was a problem hiding this comment.
i think these whole section should be moved into another file (it has nothing to do with cut elimination) or deleted entirely in favour of grind [multiset] wherever its needed. maybe you haven't done the latter for performance reasons? another option would be to have these as multiset lemmas, bc Sequent is an abbrev, in which case they can be used elsewhere.
| grind only [multiset] | ||
|
|
||
| /-- Commute a cut through the left premise of tensor. -/ | ||
| theorem tensor_add_left {Λ R T : Sequent Atom} |
There was a problem hiding this comment.
this (and the subsequent) has nothing to do with tensor
|
|
||
| /-- Checking a list context agrees with checking its multiset coercion. -/ | ||
| @[simp, scoped grind =] | ||
| theorem allQuest_coe (Γ : List (Proposition Atom)) : allQuest (Γ : Sequent Atom) = Γ.allQuest := |
There was a problem hiding this comment.
these allQuest lemmas should be moved
| def Proof.cutStep [DecidableEq Atom] | ||
| {a : Proposition Atom} (notQuest : ∀ b, a ≠ ʔb) | ||
| {Θ : Sequent Atom} (r : Proof Θ) (hr : r.IsCutFree) : | ||
| ∀ {Γ Δ : List (Proposition Atom)}, |
There was a problem hiding this comment.
hypotheses that are introduced straight away should go on the left of the colon
|
|
||
| /-- Explicit structural rank for propositions, used to drive computable strong recursion. | ||
| Every connective adds 1 plus the ranks of its subpropositions. -/ | ||
| def Proposition.rank : Proposition Atom → ℕ |
There was a problem hiding this comment.
this should be defined in Basic, and CutAdmissibleBelow should be defined in terms of it from the start
| have go : ∀ n : ℕ, ∀ {b : Proposition Atom}, | ||
| b.rank = n → CutAdmissibleAt b := by | ||
| intro n | ||
| induction n using Nat.strongRec with | ind n ih => ?_ | ||
| intro b hb | ||
| apply Proof.cutAdmOfSmaller | ||
| intro c hc | ||
| have hcrank : c.rank < n := by grind only [Proposition.rank_eq_sizeOf] | ||
| intro _ _ pc qc | ||
| exact (ih c.rank hcrank (b := c) rfl) pc qc | ||
| exact go a.rank (b := a) rfl p q |
There was a problem hiding this comment.
| have go : ∀ n : ℕ, ∀ {b : Proposition Atom}, | |
| b.rank = n → CutAdmissibleAt b := by | |
| intro n | |
| induction n using Nat.strongRec with | ind n ih => ?_ | |
| intro b hb | |
| apply Proof.cutAdmOfSmaller | |
| intro c hc | |
| have hcrank : c.rank < n := by grind only [Proposition.rank_eq_sizeOf] | |
| intro _ _ pc qc | |
| exact (ih c.rank hcrank (b := c) rfl) pc qc | |
| exact go a.rank (b := a) rfl p q | |
| suffices CutAdmissibleAt a from this p q | |
| clear p q Γ Δ | |
| induction hn : a.rank using Nat.strongRec generalizing a with | ind n ih => | |
| refine Proof.cutAdmOfSmaller ?_ | |
| intro c hc | |
| have hcrank : c.rank < n := by grind only [Proposition.rank_eq_sizeOf] | |
| exact @ih c.rank hcrank c rfl |
this should maybe be stated as CutAdmissibleAt a, and will be simpler once we use rank throughout
| let t' := Proof.cutElimAux t (c⫠ :: R) (by grind only [multiset]) | ||
| exact (Proof.cutAdm (a := c) (Γ := Λ) (Δ := R) s' t').rwConclusion | ||
| (by grind only [multiset]) | ||
| termination_by structural r |
There was a problem hiding this comment.
| termination_by structural r |
automatic
|
|
||
| /-- Cut elimination: given a proof `p` in CLL of a sequent for which there is a list representation | ||
| `Γ`, produces a cut-free proof of the same sequent. -/ | ||
| def Proof.cutElim [DecidableEq Atom] {Γ : List (Proposition Atom)} |
There was a problem hiding this comment.
there should be a public-facing theorem which is stated for Sequent rather than List
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
2 participants
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.