Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How do I manage data structures with invariants in Coq?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How do I manage data structures with invariants in Coq?


Chronological Thread 
  • From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] How do I manage data structures with invariants in Coq?
  • Date: Fri, 13 Mar 2020 18:02:38 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
  • Ironport-phdr: 9a23:NzcTmxAeR33PO1BMi1OiUyQJP3N1i/DPJgcQr6AfoPdwSP39o8bcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHERLmcAFxO+7dG4jIjs3x2frh1YfUZlBhizy8erN1KV2drQzNqs4OiIdiO68ggk/ArX1JYORRwEtjIFPVlh2658Hmr80ryDhZp/90r50Iaq79ZaltFeUJXgRjCHg84YjQjTeGSAKO4nUGVWBPy0hDBgmD5Rq8X5Gj63Kn5No44zGTOIjNdZ5xWTmm6P41GhrhiSNBPDs4tmjczM123voC/ECR4idnyouRW7m7ceJkd/qEL9gfRCxIVYBQUX4ZDw==

In a similar spirit, I am trying to define a function rotate (f r s : list A) (H : length r = 1 + length f ) : list A

To do this, I am doing the following:

Fixpoint rotate (f r s : list A)
    (H : length r = length f + 1) : list A.
    refine
      (match f, r, s with
       | [], [], _ => _
       | [], (y :: []), a => y :: a
       | [], (y :: _), a => _
       | (x :: xs), [], a => _
       | (x :: xs), (y :: ys), a => x :: (rotate xs ys (y::a) _ )
       end).

Here, the first three _ on the right is some kind of contradiction. The fourth _ is a proof that the condition for evaluating the function is satisfied.

However, I do not seem to be able to complete this proof. For example, when I try to prove the first case, the fact that f and r are empty lists seem to be lost.

Any help would be appreciated.

--Agnishom


On Tue, Mar 10, 2020 at 6:06 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:
Hi Agnishom,

You can write your Definition in proof mode. I have wrapped your
definition (Gallina term?) in refine tactic, and you can discharge
your proof in tactic mode. Hope it helps.


 Definition snoc (q : queue) (x: A) : queue.
    refine (
      let ans := exec (front q) (x :: rear q) (silly q) in
      let s := snd ans in
      let f := fst (fst ans) in
      let r := snd (fst ans) in
      let inv' := (exec_preserves_invariant q f r s x _)
      in Build_queue f r s inv').
     (* Write your tactic here to discharge the rest of the proof *)

 A : Type
  q : queue
  x : A
  ans := exec (front q) (x :: rear q) (silly q) : list A * list A * list A
  s := snd ans : list A
  f := fst (fst ans) : list A
  r := snd (fst ans) : list A
  ============================
  (f, r, s) = exec (front q) (x :: rear q) (silly q)

Best,
Mukesh

On Wed, Mar 11, 2020 at 9:26 AM Agnishom Chattopadhyay
<agnishom AT cmi.ac.in> wrote:
>
> I am trying to implement a functional queue in Coq. My idea is to add the proof of the invariant as a part of the type. Like this:
>
> Require Import Coq.Lists.List.
> Import ListNotations.
> Require Import Lia.
>
> Section Queue.
>
>   Variable A : Type.
>
>   Record queue :=
>     {
>       front : list A;
>       rear : list A;
>       silly : list A;
>       invariant : length front - length rear = length silly
>     }.
>
>   Definition empty : queue := Build_queue [] [] [] (eq_refl).
>
>   Definition isEmpty (q : queue) : bool :=
>     match (front q) with
>     | [] => true
>     | _ => false
>     end.
>
>   Fixpoint rotate (f : list A) (r : list A) (s : list A) : list A :=
>     match f, r, s with
>     | [], (y :: _),  a => y :: a
>     | (x :: xs), (y :: ys), a => x :: (rotate xs ys (y::a))
>     | _, _, _ => []
>     end.
>
>   Fixpoint exec (f : list A) (r : list A) (s : list A) : list A * list A * list AUTO :=
>     match f, r, s with
>     | _, _, (x :: xs) => (f, r, xs)
>     | _, _, [] => let f' := rotate f r [] in (f', [], f')
>     end.
>
> The following Lemma is to support the next definition
>
>   Lemma exec_preserves_invariant : forall (q : queue),
>       forall f r s x ,
>         (f, r, s) = exec (front q) (x :: rear q) (silly q)
>          -> length f - length r = length s.
>   Proof.
>     intros.
>     pose proof (invariant q).
>     destruct (front q); destruct (silly q).
>     - simpl in H. inversion H. simpl. lia.
>     - inversion H0.
>     - simpl in H. inversion H. simpl. lia.
>     - simpl in H. inversion H. simpl.
>       replace (length (a :: l)) with (S (length l)) in H0 by reflexivity.
>       replace (length (a0 :: l0)) with (S (length l0)) in H0 by reflexivity.
>       lia.
>   Qed.
>
> However, I cannot figure out what would be the correct way to replace the underscore below.
>
>   Definition snoc (q : queue) (x: A) : queue :=
>     let ans := exec (front q) (x :: rear q) (silly q) in
>     let s := snd ans in
>     let f := fst (fst ans) in
>     let r := snd (fst ans) in
>     let inv' := (exec_preserves_invariant q f r s x _)
>     in
>     Build_queue f r s inv '.
>
> What is the correct way to define the invariant preserving functions such as snoc?
>
> In some languages like Lean, I have noticed that any term can be replaced by a tactic that synthesizes a similar term. So, in such a context, I could have replaced the underscore by a proof using tactics.
>
> --Agnishom



Archive powered by MHonArc 2.6.18.

Top of Page