The Coq mailing list

[Agnishom Chattopadhyay <agnishom AT cmi.ac.in>]

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