Christian Hagemeier (May 19 2021 at 10:38): Christian Hagemeier (May 19 2021 at 10:38):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?
Kenji Maillard (May 19 2021 at 11:19):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.
Matthieu Sozeau (May 21 2021 at 11:27):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
Olivier Laurent (May 21 2021 at 12:05):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.
Dan Frumin (Jun 17 2021 at 08:23):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?
Matthieu Sozeau (Jun 17 2021 at 12:37):Yes, hopefully I can get some of the obvious bugs fixed in 8.14 (working on it)
Olivier Laurent (Jun 17 2021 at 12:55):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).
Dan Frumin (Jun 21 2021 at 09:45):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.
Matthieu Sozeau (Jun 21 2021 at 09:56):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 ...$
Dan Frumin (Jun 21 2021 at 10:51):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
Dan Frumin (Jun 21 2021 at 10:54):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: Oct 05 2023 at 02:01 UTC