The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sun, Nov 28, 2021 at 10:18 PM Ian Shillito <Ian.Shillito AT anu.edu.au> wrote:
> Pascal: I intend to use this order to prove the termination of a proof 
> search procedure for a sequent calculus.

If that's the use case, then I have something vaguely similar already
implemented (in a past version of Coq, but hopefully not too much
needs to be updated):
https://github.com/dschepler/coq-sequent-calculus/blob/master/LJTStar.v
.  There, I have a function context_cost that takes in a list of
propositions, and returns a list of counts of how many propositions
there are of each cost (calculated using prop_cost, result list
starting at cost 0 and going up to the maximum cost).  Then, I have a
relation context_cost_lt which is reverse lexicographic order on that
list of counts, and a proposition context_cost_lt_wf which shows that
relation is well-founded.  (And then, I have a series of propositions
that each manipulation in the LJT* search procedure strictly reduces
the context cost.  I never actually got around to implementing the
full search procedure and using those propositions to show it
terminates, though.)
-- 
Daniel Schepler