I currently have a predicate representing sequent calculus derivations i.e. `seq: list form -> form -> Prop`

(where form is the inductive type of propositional formulas).

When seq is defined this way, after proving a lemma about invariance under permutation equivalence I can register a proper instance

`Proper (@Permutation form) ==> eq ==> imp`

to allow rewriting under equal Permutations (i.e if I have` seq A s`

as a hypothesis and know `Permutation A B`

, I can rewrite this to `seq B s`

).

Is rewriting possible, when I change the the type of seq to ` list form -> form -> Type`

?

It should be possible, in theory, using the module CMorphisms instead of Morphisms, but I don't have any first hand experience with that module.

Baring a few bugs (with open PRs about them, that should make it to the next version), indeed you should just be able to use `CMorphisms.Proper`

instead of `Morphisms.Proper`

to get the same support in generalized rewriting

There are indeed some troubles with such a move to `Type`

: issue #7675

If you are interested in manipulating proofs, you could have to move from `Permutation`

to `Permutation_Type`

at some point. I have been playing quite a lot with this kind of representation of the sequent calculus for the Yalla library if you want to see more.

I tried working with CMorphisms.Proper (and CMorphisms.Equivalence, etc) instead of the Prop versions, and while it seems to mostly work there are some problems that I encountered (universe issues as the ones linked by Olivier).

If I may ask you, why do you want to put your sequent calculus derivations in a Type?

Yes, hopefully I can get some of the obvious bugs fixed in 8.14 (working on it)

Dan Frumin said:

If I may ask you, why do you want to put your sequent calculus derivations in a Type?

The way I understand things is: defining it in `Prop`

is defining a provability predicate, defining it in `Type`

is defining a type of proofs. So If you want to do proof transformations and/or extract information from proofs (typically in the spirit of the Curry-Howard correspondence or for computing the interpretation of a proof in a denotational model), you need them to be in `Type`

. A more direct example is being able to define the size of a proof as a function of type `forall l A, seq_proof l A -> nat`

where `seq_proof : list form -> form -> Type`

(`Prop`

would not do the job here).

Indeed, for general proof-relevant proof transformation there doesn't seem to be options other than putting the thing into a `Type`

.

If you need proof size specifically, I found it easier to annotate the sequent calculus with the proof height (bounds), e.g.

`seq_proof : nat -> list form -> form -> Prop`

.

At least that is what I ended up doing for my formalization.

Indexing has the advantage that you don't need to do proof-relevant inversions indeed. But then you're really working with type $\sum n : nat, seq_proof n ...$

Matthieu Sozeau said:

Indexing has the advantage that you don't need to do proof-relevant inversions indeed. But then you're really working with type $\sum n : nat, seq_proof n ...$

Yes, in my development I have to data-types `seq_proof`

and `seq_proof_height`

, and relate them using the sigma type as you mentioned.

Working with the instrumented type is still annoying

I've been thinking a bit about this --- and this is far from a profound observation --- but I guess it's also possible to describe the proof height as a relation: `proof_height : forall Gamma A (pf : seq_proof Gamma A), nat -> Prop`

and use that for your induction purposes.

Last updated: Feb 09 2023 at 00:03 UTC