The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

The problem you face is that "match" only operates on the conclusion of a goal,

not on the hypotheses, hence H in your case. This is a way to proceed:

Require Import List Arith Lia.

Section rotate.

Variable A : Type.

Fixpoint rotate (f r s : list A)
    (H : length r = length f + 1) : list A.
    revert H.
    refine
      (match f, r, s with
       | nil, nil, _ => _
       | nil, (y :: nil), a => fun H => y :: a
       | nil, (y :: _), a => _
       | (x :: xs), nil, a => _
       | (x :: xs), (y :: ys), a => fun H => x :: (rotate xs ys (y::a) _ )
       end); simpl in *; try discriminate; lia.
Defined.

End rotate.

Best,

Dominique
   

---

De: "Agnishom Chattopadhyay" <agnishom AT cmi.ac.in>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Samedi 14 Mars 2020 00:02:38
Objet: Re: [Coq-Club] How do I manage data structures with invariants in Coq?

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