The Coq mailing list

[Rajeev Gore <rajeev.gore AT iinet.com.au>]

Hi all,

apologies if this is a dumb question, but I am a Coq newbie so be gentle
please:)

> I am trying to write a function that traverse the list and groups the
> similar elements. For example, if I have a list [3; 1; 1; 3; 5; 1] then
> I want it to arranged [[3; 3]; [1;1;1]; [5]],

I have been trying to think of a way to implement a sequent calculus in
Coq using multisets rather than lists because, then, exchange comes for
free.

One of the things that crossed my mind was a function that did exactly
what Mukesh asks about above since [[3; 3]; [1;1;1]; [5]] to my mind is
just the multiset consisting of two-3s, three-2s and one-5.

So, suppose that the Gamma (LHS) part of my sequent consisted of the
list of "formulae" [3; 1; 1; 3; 5; 1] then its multiset representation
would something like [[3; 3]; [1;1;1]; [5]].

Am I just being dumb?

Is there a "natural" way to encode sequents which are lists of formulae
so that Coq thinks of them as multisets?

thanks,
raj

mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> writes:

> Hi Dominique, 
>
> I am trying to write a function that traverse the list and groups the 
> similar elements. For example,  if I have a list [3; 1; 1; 3; 5; 1] then I 
> want it to arranged [[3; 3]; [1;1;1]; [5]],
> and go is a helper function that is called by a top level function with R 
> instantiated with boolean equality of natural numbers (Nat.eqb).  But your 
> speculation is right because if R
> is instantiated with Nat.ltb then it can be a part of quicksort.
>
> Best, 
> Mukesh 
>
> On Fri, 23 Dec 2022 at 03:48, Dominique Larchey-Wendling 
> <dominique.larchey-wendling AT loria.fr> wrote:
>
>  Hi Mukesh,
>
>  This looks like part of quicksort. Is this your target?
>
>  Best,
>
>  Dominique
>
>  ----- Mail original -----
>  > De: "mukesh tiwari" <mukeshtiwari.iiitm AT gmail.com>
>  > À: "coq-club" <coq-club AT inria.fr>
>  > Envoyé: Jeudi 22 Décembre 2022 11:55:38
>  > Objet: [Coq-Club] Proof about permutation
>
>  > Hi everyone,
>  > 
>  > How can I prove the theorem, go_app, shown below? I find it slightly
>  > amusing that in the base there is not enough information that I can
>  > use to discharge it.  You can see the complete source code [1] (I
>  > manage to prove this theorem for a simplified definition of go using
>  > filter [2])
>  > 
>  > Fixpoint go (z : A) (xs : list A) : list A * list A :=
>  >    match xs with
>  >    | [] => ([], [])
>  >    | (x :: xs) =>
>  >      match go z xs with
>  >      | (ys, zs) =>
>  >        match R x z with
>  >        | true => (x :: ys, zs)
>  >        | _ => (ys, x :: zs)
>  >        end
>  >      end
>  >    end.
>  > 
>  > 
>  > Theorem go_app :
>  >    ∀ (xs ys zs : list A) (z : A),
>  >    In z xs ->
>  >    (ys, zs) = go z xs -> Permutation (ys ++ zs) xs.
>  >  Proof.
>  >    refine(fix Fn xs {struct xs} :=
>  >      match xs as xsp return xs = xsp -> _
>  >      with
>  >      | [] => fun Ha => _
>  >      | xh :: xst => fun Ha => _
>  >      end eq_refl);
>  >      simpl;
>  >      intros ? ? ? Hb Hc.
>  >    +
>  >      refine(match Hb with end).
>  >    +
>  >      refine(match Hb with
>  >        | or_introl Hap => _
>  >        | or_intror Hap => _
>  >        end).
>  >      ++
>  >        rewrite Hap in Hc.
>  >        rewrite R_refl in Hc.
>  >        (* There is no information in the context that
>  >          connects xst to xsh and ysh *)
>  >        destruct (go z xst) as (xsh, ysh) eqn:He.
>  >        inversion Hc; subst; clear Hc; simpl.
>  >        constructor.
>  >        (* Now I am stuck! Because this is what
>  >          I am trying to discharge so I am chasing my tail?
>  >        *)
>  >        admit.
>  >      ++
>  >        destruct (R xh z) eqn:Hd.
>  >        +++
>  >          destruct (go z xst) as (xsh, ysh) eqn:He.
>  >          inversion Hc; subst; clear Hc; simpl.
>  >          constructor.
>  >          eapply Fn;
>  >          [exact Hap | eapply eq_sym; exact He].
>  >        +++
>  >          destruct (go z xst) as (xsh, ysh) eqn:He.
>  >          inversion Hc; subst; clear Hc; simpl.
>  >          eapply Permutation_sym, Permutation_cons_app,
>  >            Permutation_sym.
>  >          eapply Fn;
>  >          [exact Hap | eapply eq_sym; exact He].
>  >    Admitted.
>  > 
>  > 
>  > Best,
>  > Mukesh
>  > 
>  > [1] https://gist.github.com/mukeshtiwari/55439c129b35071585e05c9847a96c59
>  > [2]
>  > 
> https://gist.github.com/mukeshtiwari/55439c129b35071585e05c9847a96c59#file-constant_space-v-L17