The Coq mailing list

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

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