The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

You are right, Jason. I managed to achieve what I was looking for [1]. 

Coq developers: is there something changed with Coq 8.16 evaluation mechanism? It’s surprising that  I can evaluate this _expression_ [2], even though there are (opaque?) proof terms inside groupBy function. I remember, if my memory serves me correctly,  in the past  that I never managed to evaluate any _expression_ that involved well founded induction. 

Best, 

Mukesh 

[1 https://gist.github.com/mukeshtiwari/aaecb848a31c7df7c09d47139122a698

[2]https://gist.github.com/mukeshtiwari/aaecb848a31c7df7c09d47139122a698#file-groupby-v-L129

On Fri, 23 Dec 2022 at 10:17, Jason Hu <fdhzs2010 AT hotmail.com> wrote:

Hi Mukesh,

 

My immediate feeling is that the In predicate is not necessary. In fact, `(ys, zs) = go z xs -> Permutation (ys ++ zs) xs` should hold universally regardless of what z is. I only suppose there is a lemma which states that

 

If Permutation (ys ++ zs) xs, then Permutation (x :: ys ++ zs) (x :: xs) /\ Permutation (ys ++ x :: zs) (x :: xs)

 

Did you try this path? I suppose to prove the second part of the conjunction you need to do another induction.

 

Thanks,

Jason

 

From: mukesh tiwari
Sent: Thursday, December 22, 2022 6:09 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof about permutation

 

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