Coq examples of cut elimination in sequent calculi?

Using Coq
1

I am trying to prove a cut-elimination result for a sequent calculus in Coq. I have a derivation of A \vdash B and a derivation of B \vdash C, and I build a derivation of A \vdash C. (My actual sequent calculus is more complex than that, but this is the idea.)

Do you have examples of such cut-elimination proofs already done in this style? I found that doing it in Coq is harder than I thought (details below), and I would have liked to find inspiration in previous developments, but googling for “Coq sequent cut-elimination” does not list an example that I could follow, and in fact it contains more examples of “semantic” cut-elimination arguments than of the usual syntactic approach that I am trying to formalize here.

The examples I found:

  • propcalc, for classical propositional logic, does a strong induction on the size of formulas (rather than the size of derivations as one might expect) as the termination measure
  • yalla, for linear logic, does a strong induction on the size of both the derivations and the cut formula.

Details

The problem is that this is not obviously a structural induction: there are “principal cases” where both derivations decrease, then there are “commutation” cases where only one of the two derivations decreases (sometime the first one, sometimes the second). So we need to use a measure or well-founded induction.

Furthermore, there is a bit of dependent pattern-matching involved: when you inspect the proof of A \vdash B, you learn about the shape of A and B. For this reason, I have been using Equations, but Equations does not seem to scale to the sequent calculus I am using (Equations Derive NoConfusion for derivation does not appear to terminate.)

I was looking for solutions where I can write the cut-elimination proof as a program, and I find myself in a bit of a bind:

  • Program Fixpoint is good at dealing with measures, but wants me to do dependent pattern-matching by hand which is proving (in this case; there is a lot of indexing going on in my derivations) above my expertise level, and results in very noisy code.
  • Equations demands well-formed induction, not measures, and seems to struggle in more complex cases.

(For the time being I think that I will revert to the Proof…End mode to write this.)

2

Some results about cut elimination are also covered in the Coq Library of First-Order Logic, at least here, but this one is by going through Kripke semantics. The corresponding paper should be https://doi.org/10.1093/logcom/exaa073, but I don’t think there is too much discussion about this.

Regarding Equations, you can simulate measures by doing by wf (measure x) lt where x : X is the argument to apply the measure to and measure : X -> nat.

3

Thanks!

While I am at it, let me dump here some minor notes on remark I had while looking for this stuff. (With time and motivation I could turn them into small contributions to documentation, but for now just dumping here.)

  • It would be useful if the reference manual contained small examples of using {wf ...} and {measure ...}. For now it only gives the formal syntax (and examples using {struct ..}), which raises the barrier to use them. (I learned more from this StackOverflow discussion than from the manual, which suggests that the manual can improve.) For example, if I understand correctly, Function and Program Fixpoint expect slightly different {measure ...} syntaxes, examples would make this clear.
  • the Equations documentation is full of broken URLs ( Many links broken on http://mattam82.github.io/Coq-Equations/ · Issue #571 · mattam82/Coq-Equations · GitHub ). I needs maintenance, which suggests that it would benefit from being included in the reference manual, as Function and Program are.