The Coq mailing list

[Frederik Krogsdal Jacobsen <fkjac AT dtu.dk>]

Dear Raj,

A few months ago I also spent some time thinking about how to represent a sequent calculus and a prover for it using the existing multiset package (MSets) so that I could "easily" prove soundness and completeness of the calculus and prover.

I am not a Coq expert (I usually work in Isabelle), so I'm sure my formalization can be improved significantly, but maybe seeing it could at least be helpful for getting a taste of some possibilities.

My lightly commented development is available here:
https://github.com/fkj/coq-microprover

I should note that my approach is heavily inspired by similar developments in Isabelle and Agda by J. Villadsen and A.H. From.

Cheers,
Frederik

On 23/12/2022 10:16, Dominique Larchey-Wendling wrote:

Dear Raj and Mukesh,

Indeed finite multisets (or finite sets) can be a pain in Coq because they are not

inductive types: they are quotient types. Here I discuss two opposed approaches:

1) trying to build the quotient type. In Coq this usually requires being able to 

   compute a witness for an equivalence class (eg a normal form) and a Boolean

   test for normal forms.

   For multisets, the least assumptions that I know of are of a type X with 

   a (computably) decidable total order (DTO) over it, ie 

   - an irreflexive and transitive relation R : X -> X -> Prop

   - together with Rdec : forall x y : X, { R x y } + { x = y } + { R y x }

   Then the type of finite multisets can be implemented as 

             

             { l : list X | is_ordered R_dec l = true } 

             

   where is_ordered R_dec : list X -> bool is a Boolean checker for orderedness. 

   The Boolean output ensures that (is_ordered R_dec l = true) has a unique proof

   (see EqDep_dec).

2) The second approach (that I prefer, see below) is working with lists, up to 

   permutations.

   

    a) It can be lightly automated but with no assumptions using Setoid rewriting,

       declaring (@Permutation X) as a "Parametric Morphism".

       

    b) It can be heavily automated assuming a computably decidable equality over X

       (which is a bit weaker than a DTO as above).

       The idea is: in that case, two list are permutable iff the number of 

       occurrences of each value x:X matches for the two lists. Then, one projects 

       permutation identities onto equalities between number of occurrences (in nat) 

       and then call tools like autorewrite/lia to solve arithmetic equations. 

       See the following gist to get an idea of what can be done

       https://gist.github.com/DmxLarchey/17e0a90d558313b98cc30617b5a67086

       

       For instance, the following statement can be proved automatically:

       

                l++[x] ~p x::u -> k ~p rev v -> k++u ~p v++l

Certainly, to manipulate sequents, it is not a problem to assume decidability of

equality for logical formulas and then 2b) can be a good solution which I encourage

you to look at.

However, when writing libraries, assuming decidable equality might be too

heavy and then Setoid rewriting is a better choice, but with much more

rewriting work.

The first reason I do not like building quotient types like 1) is that you 

still need to manipulate proofs that lists are ordered, so not much is gained 

compared to 2a).

The second reason is that the quotient type of multisets cannot be nested

within trees to build for instance unordered finitely branching trees. Trying

to build that type is already a painful exercise. The way I know of is to

define a (DTO) over ordered finitely branching trees and select those which

are recursively totally ordered.

Raj, for an easy start, I recommend 2b as described in the gist.

Best,

Dominique

---

De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
À: "Rajeev Gore" <rajeev.gore AT iinet.com.au>
Cc: "coq-club" <coq-club AT inria.fr>
Envoyé: Vendredi 23 Décembre 2022 07:00:51
Objet: Re: [Coq-Club] Proof about permutation

On Fri, 23 Dec 2022 at 16:55, Rajeev Gore <rajeev.gore AT iinet.com.au> wrote:

Hi Mukesh,

> I don’t much about sequent calculus (even though I was a part of ANU
> logic group for a long time :)),

Shame on you :)

I deserve that :) 

> but my use case is to deal with an equality (equal_finite_sets) in a sane
> (* multiset represented by list *)
> Definition finite_set {A : Type) := list A.
>
> (* two multisets are equal *)
> Definition equal_finite_set {A : Type) (xs ys  : @finite_set A) : Prop :=
>    forall x, In x xs <-> In x ys.
> etc

But there is already a multiset package in Coq, so why redefine it?

Because I am working on a existing project (not open sourced yet) and it has its own multiset library.

I am trying to wrap my head around the existing multiset package in Coq,
and in particular, how to use it to define sequents built from multisets
in a way that is comprehensible to a proof-theorist (not a Coq expert).

I believe Dominique is an expert, that I am aware of, about the proof theory and Coq so probably he will have more to say.

Best,

Mukesh

raj