The Coq mailing list

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

Hi Agnoshom, 

I don’t access to my computer right now, so I can’t produce any Coq code which solves the problem, but I would suggest you to do a google search “convoy patterns Coq” and have a look at the Adam Chlipala’s book [1] (go for PDF version) 

  

I am giving a shot to write your function (but it may not typecheck because I am writing it on my phone) 

Theorem rorate: forall (f r s : list A), length r =  1 + length l -> list A. 

induction f. 

+ (* f is empty and you need to do more destructs on r and s*) 

+ (* inductive case and maybe again destructs on r and s *) 

Defined.  

I think that it’s easier to write program in proof mode, but convoy patterns are fun. Hope it helps. 

-Mukesh 

[1] 

http://adam.chlipala.net/cpdt/html/MoreDep.html

On Sat, 14 Mar 2020 at 10:03 am, Agnishom Chattopadhyay <agnishom AT cmi.ac.in> wrote:

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