1
$\begingroup$

I am trying to prove some theorems using sequent calculus, for some parts (e.g. cases with Exchange rule) I need a theorem like below

    Lemma exchg_partition: forall {X : Type} (D D' D1 D2 : list X) (a b : X),
D ++ a :: b :: D' = D1 ++ D2 ->
(
    ( D2 = D ++ a :: b :: D' /\ D1 = [])
    \/ (exists D3, D2 = D3 ++ a :: b :: D' /\ D = D1 ++ D3)
    \/ (D1 = D /\ D2 = a :: b :: D')
    \/ (D1 = D ++ [a]) /\ D2 = b :: D'
    \/ (D1 = D ++ [a; b] /\ D2 = D')
    \/ (exists D3, D1 = D ++ a :: b :: D3 /\ D' = D3 ++ D2)
    \/ (D1 = D ++ a :: b :: D' /\ D2 = [])
).

but I have no idea how to prove this, induction doesn't work since I clearly have to use induction on D1 or D2 and destructing hypothesis the first case is unprovable. I tried many things but I'm totally stuck in this.

$\endgroup$

2 Answers 2

3
$\begingroup$

Did you try a complete induction on list length ? More precisely prove forall n, if |D1|+|D2|<=n then forall D D', ...

See for instance https://stackoverflow.com/questions/45872719/how-to-do-induction-on-the-length-of-a-list-in-coq

You may also start with a proof of Levi's lemma (I'm not sure it has not been proved in Coq yet).

$\endgroup$
1
  • $\begingroup$ Thank you I guess this works. $\endgroup$ Jul 14, 2023 at 18:26
5
$\begingroup$

I apologize for a non-answer, but allow me to explain what I've learned from formalizing formal calculi. Unfortunately I do not have any ready-made examples of formalized calculu to show what I am preaching.

Formalization on paper is not the same thing as formalization in a proof assistant. In books it is acceptable to say that contexts (or both sides of $\vdash$ in a classical sequent calculus) are lists, subject to the exchange rule. This works only because such books get away with writing "$\ldots$" everywhere and claiming all sorts of obvious facts without actually proving them, such as the lemma you're trying to prove. Once you actually try to formalize formal logic, it bites back and wants to be done correctly.

I know of two approaches to dealing with contexts and structural rules. Both of them remove the strutural rules from the calculus, but differ in where they put them.

Use the correct mathematical structure

Before diving into formalization, we need to think carefully what the mathematical structure of contexts (or both sides of $\vdash$) actually is. If someone said "consider lists of elements, but you may exchange their order", the natural reply would be "so you mean multisets?". And if they threw in "you may also delete duplicates" then they are just talking about finite sets, but in a very clumsy way, because for some reason they want to work with a representation of finite sets in terms of lists.

This is precisely what traditional logic does with contexts. Lists are considered "more fundamental" and get used instead of multisets. But since we really want multisets, the sequent calculus (or whatever formal calculus we're dealing with) is rectified by introduction of rules of inference that explain what those lists really represent. This way, simple facts about multisets get all tangled up with actual content about the formal calculus. Worse, the trivialities feel important because we call them "structural", as if they were the bedrock of the calculus.

If my calculus has an exchange rule, I would first formalize the notion of finite decidable multisets (or sets if there is also contraction), thereby factoring out all trivial work regarding those. The more direct the formalization, the better. For example, I would seriously consider representing $\Gamma$ and $\Delta$ in a sequent $\Gamma \vdash \Delta$ as maps $\Gamma, \Delta : \mathsf{Formula} \to \mathbb{N}$ (multisets) or $\Gamma, \Delta : \mathsf{Formula} \to \mathsf{bool}$ (decidable sets). Yes, yes, this allows infinite contexts, but the simplicity of using a direct represenation of multisets is at least worth trying. We can always add the finiteness restriction later, if needed, and only where it matters.

The calculus itself should not have any "structural" rules, especially not any that can be applied at every step, as that pollutes inductive proofs. With some luck, someone else has already formalized multisets and proved all the silly lemmas – but even better, with the correct setup many silly lemmas become unnecessary.

Remove structural rules but show they're admissible

This option is often a good one. Often one can just drop the structural rules, and possibly make very minor modifications, and then show later that the structural rules are admissible.

For example, in natural deduction calculus one may have the weakening rule $$\frac{\Delta \vdash A}{\Gamma, \Delta, \Psi \vdash A}$$ together with the hypothesis rule $$\frac{\;}{A \vdash A}$$ One can drop the weakening rule and use the hypothesis rule $$\frac{A \in \Gamma}{\Gamma \vdash A}$$ which will work a lot better in formalization. (And also Frank Pfenning taught me that it will just be better all around.) The weakening rule becomes admissible, and so is does the exchange rule.

In case of a classical sequent calculus the situation may be similar, but I am not sure. I never thought about it carefully enough.

$\endgroup$
5
  • $\begingroup$ About multisets: Olivier Laurent makes a point of not using multisets in yalla because they lose computational content. For example, there should be two distinct derivations of A ⊗ A ⊢ A ⊗ A, which multisets conflate. However, I agree with non-answering this question, even though yalla shows that you can hack through with just lists, append, and the theory of permutations. $\endgroup$
    – James Wood
    Jul 13, 2023 at 15:48
  • 2
    $\begingroup$ Well, of course, there is not going to be a single answer to all variations. If one cares about the computational content, the game changes. The point of my non-answer was: don't be afraid to modify "standard" ways of doing things and adapt them to new situations. $\endgroup$ Jul 13, 2023 at 16:01
  • 2
    $\begingroup$ I would like to mention Russel O'Connor's goedel library, where the formaization of FOL and PA takes two steps. 1) Definition of an as simple as possible type of proof trees where contexts are lists 2) Using the conversion of a list to its set of elements, build a second system where contexts are sets. Once the deduction lemma is proven, a lot of natural deduction rules are derived. $\endgroup$ Jul 14, 2023 at 7:56
  • $\begingroup$ I just wanted to leave a comment regarding of how useful and important your answer was, using the methodology you suggested completely fixed all the issues I was having and I was able to prove the theorem I wanted in Coq. many thanks. $\endgroup$ Aug 18, 2023 at 11:37
  • $\begingroup$ I am glad I could help! Which approach did you take in the end? $\endgroup$ Aug 18, 2023 at 11:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.