Equations taking a long time to type check mutually recursive functions

[JulesViennotFranca]

trafficstars

Lately, I have written a Coq project to verify a data structure using Equations.

This data structure is called catenable deques, a queue supporting push, pop, inject (push at the end), eject (pop at the end) and concatenation in constant time.

The types for the data structure are rather complex, and I need to define 4 mutually recursive types: stored_triple, body, packet and chain.

Next, I need to write some functions linking my different types to the sequence of elements they represent. I call these functions the model functions. When writing the model functions for stored_triple, body, packet and chain, Equations takes a really long time to type check them (approximatively 20 minutes).

Is there something I do wrong for Equations to take this much time or is there a specific explanation for this ?

Here is my code until the definition of the 4 mutually recursive model functions:

From Coq Require Import Program List.
Import ListNotations.
From Equations Require Import Equations.

(* +------------------------------------------------------------------------+ *)
(* |                                 Colors                                 | *)
(* +------------------------------------------------------------------------+ *)

(* Defining some hues. *)
Inductive green_hue  := SomeGreen  | NoGreen.
Inductive yellow_hue := SomeYellow | NoYellow.
Inductive orange_hue := SomeOrange | NoOrange.
Inductive red_hue    := SomeRed    | NoRed.

(* Deriving the [NoConfusion] trait needed by [Equations]. *)
Derive NoConfusion for green_hue.
Derive NoConfusion for yellow_hue.
Derive NoConfusion for orange_hue.
Derive NoConfusion for red_hue.

Module GYR.
  (* Defining colors type. *)
  Inductive color := Mix : green_hue -> yellow_hue -> red_hue -> color.

  Derive NoConfusion for color.

  (* Defining colors. *)
  Notation green := (Mix SomeGreen NoYellow NoRed).
  Notation yellow := (Mix NoGreen SomeYellow NoRed).
  Notation red := (Mix NoGreen NoYellow SomeRed).
  Notation uncolored := (Mix NoGreen NoYellow NoRed).
End GYR.

Module GYOR.
  (* Defining colors type. *)
  Inductive color :=
    Mix : green_hue -> yellow_hue -> orange_hue -> red_hue -> color.
  Derive NoConfusion for color.

  (* Defining colors. *)
  Notation green := (Mix SomeGreen NoYellow NoOrange NoRed).
  Notation yellow := (Mix NoGreen SomeYellow NoOrange NoRed).
  Notation orange := (Mix NoGreen NoYellow SomeOrange NoRed).
  Notation red := (Mix NoGreen NoYellow NoOrange SomeRed).
  Notation uncolored := (Mix NoGreen NoYellow NoOrange NoRed).
End GYOR.

(* +------------------------------------------------------------------------+ *)
(* | +--------------------------------------------------------------------+ | *)
(* | |                        Non-catenable deques                        | | *)
(* | +--------------------------------------------------------------------+ | *)
(* +------------------------------------------------------------------------+ *)

Module Deque.
  Import GYR.

(* +------------------------------------------------------------------------+ *)
(* |                                 Types                                  | *)
(* +------------------------------------------------------------------------+ *)

  (* A type for products. *)
  Inductive prodN (A : Type) : nat -> Type :=
    | prodZ : A -> prodN A 0
    | prodS {n : nat} : prodN A n -> prodN A n -> prodN A (S n).
  Arguments prodZ {A}.
  Arguments prodS {A n}.

  (* A type for buffers. *)
  Inductive buffer (A : Type) (lvl : nat) : nat -> color -> Type :=
    | B0         : buffer A lvl 0 red
    | B1 {y r}   : prodN A lvl -> buffer A lvl 1 (Mix NoGreen y r)
    | B2 {g y r} : prodN A lvl -> prodN A lvl -> buffer A lvl 2 (Mix g y r)
    | B3 {g y r} : prodN A lvl -> prodN A lvl -> prodN A lvl ->
                  buffer A lvl 3 (Mix g y r)
    | B4 {y r}   : prodN A lvl -> prodN A lvl -> prodN A lvl ->
                  prodN A lvl -> buffer A lvl 4 (Mix NoGreen y r)
    | B5         : prodN A lvl -> prodN A lvl -> prodN A lvl ->
                  prodN A lvl -> prodN A lvl -> buffer A lvl 5 red.
  Arguments B0 {A lvl}.
  Arguments B1 {A lvl y r}.
  Arguments B2 {A lvl g y r}.
  Arguments B3 {A lvl g y r}.
  Arguments B4 {A lvl y r}.
  Arguments B5 {A lvl}.

  (* A type for packets. *)
  Inductive packet (A : Type) (lvl : nat) : nat -> nat -> nat -> color -> Type :=
    | Hole {size : nat} : packet A lvl lvl size size uncolored
    | Packet {clvl psize pktsize csize ssize C y} :
        buffer A lvl psize C ->
        packet A (S lvl) clvl pktsize csize (Mix NoGreen y NoRed) ->
        buffer A lvl ssize C ->
        packet A lvl clvl (psize + pktsize + pktsize + ssize) csize C.
  Arguments Hole {A lvl size}.
  Arguments Packet {A lvl clvl psize pktsize csize ssize C y}.

  (* A type for the regularity relation. *)
  Inductive regularity : color -> color -> Type :=
    | G {g r} : regularity green  (Mix g NoYellow r)
    | Y       : regularity yellow green
    | R       : regularity red    green.

  (* A type for chains. *)
  Inductive chain (A : Type) (lvl : nat) : nat -> color -> Type :=
    | Ending {size : nat} {C : color} :
        buffer A lvl size C ->
        chain A lvl size green
    | Chain {clvl size csize : nat} {C1 C2 : color} :
        regularity C1 C2 ->
        packet A lvl clvl size csize C1 ->
        chain A clvl csize C2 ->
        chain A lvl size C1.
  Arguments Ending {A lvl size C}.
  Arguments Chain {A lvl clvl size csize C1 C2}.

  (* A type for deque. *)
  Inductive t (A : Type) (size : nat) : Type :=
    | T {g y} : chain A 0 size (Mix g y NoRed) -> t A size.
  Arguments T {A size g y}.

(* +------------------------------------------------------------------------+ *)
(* |                                 Models                                 | *)
(* +------------------------------------------------------------------------+ *)

  (* In the following, [concat_map_***_seq] functions assume the structure
    contains elements of type [T A lvl] where [T : Type -> nat -> Type],
    [A : Type] and [lvl : nat].

    These functions are needed for the implementation of catenable deques. In
    this implementation, non-catenable deques contain elements of type
    [T A lvl] where [T] is instanciated with [stored_triple].

    Such functions compute the sequence associated to a structure, then perform a map on them using the model functions [f] of the type [T], and finally concatenate the resulting sequence to obtain a term of type [list A]. *)

  (* Sequence + map + concat for products. *)
  Definition concat_map_prodN_seq
    {T : Type -> nat -> Type}
    (f : forall A lvl, T A lvl -> list A)
    {A lvlt lvl} : prodN (T A lvlt) lvl -> list A :=
    let fix local {lvl} (p : prodN (T A lvlt) lvl) : list A :=
      match p with
      | prodZ ta => f A lvlt ta
      | prodS p1 p2 => local p1 ++ local p2
      end
    in local.

  (* Sequence + map + concat for buffers. *)
  Definition concat_map_buffer_seq
    {T : Type -> nat -> Type}
    (f : forall A lvl, T A lvl -> list A)
    {A lvlt lvl size C} (b : buffer (T A lvlt) lvl size C) : list A :=
    match b with
    | B0 => []
    | (B1 a) => concat_map_prodN_seq f a
    | (B2 a b) => concat_map_prodN_seq f a ++ concat_map_prodN_seq f b
    | (B3 a b c) => concat_map_prodN_seq f a ++ concat_map_prodN_seq f b ++
                    concat_map_prodN_seq f c
    | (B4 a b c d) => concat_map_prodN_seq f a ++ concat_map_prodN_seq f b ++
                      concat_map_prodN_seq f c ++ concat_map_prodN_seq f d
    | (B5 a b c d e) => concat_map_prodN_seq f a ++ concat_map_prodN_seq f b ++
                        concat_map_prodN_seq f c ++ concat_map_prodN_seq f d ++
                        concat_map_prodN_seq f e
    end.

  (* Sequence + map + concat for packets. *)
  Definition concat_map_packet_seq
    {T : Type -> nat -> Type}
    (f : forall A lvl, T A lvl -> list A)
    {A lvlt lvl clvl pktsize csize C} :
    packet (T A lvlt) lvl clvl pktsize csize C -> list A -> list A :=
    let fix local {lvl clvl pktsize csize C}
      (pkt : packet (T A lvlt) lvl clvl pktsize csize C) (l : list A) : list A :=
      match pkt with
      | Hole => l
      | Packet p pkt s => concat_map_buffer_seq f p ++
                          local pkt l ++
                          concat_map_buffer_seq f s
      end
    in local.

  (* Sequence + map + concat for chains. *)
  Definition concat_map_chain_seq
    {T : Type -> nat -> Type}
    (f : forall A lvl, T A lvl -> list A)
    {A lvlt lvl size C} : chain (T A lvlt) lvl size C -> list A :=
    let fix local {lvl size C} (c : chain (T A lvlt) lvl size C) : list A :=
      match c with
      | Ending b => concat_map_buffer_seq f b
      | Chain _ pkt c => concat_map_packet_seq f pkt (local c)
      end
    in local.

  (* Sequence + map + concat for deques. *)
  Definition concat_map_seq
    {T : Type -> nat -> Type}
    (f : forall A lvl, T A lvl -> list A)
    {A lvlt size} (d : t (T A lvlt) size) : list A :=
    match d with
    | T c => concat_map_chain_seq f c
    end.

End Deque.

(* +------------------------------------------------------------------------+ *)
(* | +--------------------------------------------------------------------+ | *)
(* | |                          Catenable deques                          | | *)
(* | +--------------------------------------------------------------------+ | *)
(* +------------------------------------------------------------------------+ *)

Import GYOR.

(* +------------------------------------------------------------------------+ *)
(* |                                 Types                                  | *)
(* +------------------------------------------------------------------------+ *)

(* Type for node kinds. *)
Inductive nkind : Type := only | left | right.

(* Notations for chain kind. *)
Notation ckind := nat.
Notation empty  := 0.
Notation single := 1.
Notation pair   := 2.

Derive NoConfusion for nkind.

(* Types for general prefix and suffix, they are simply aliases for Deque.t. *)
Definition prefix' := Deque.t.
Definition suffix' := Deque.t.

(* A type for the coloring of a node. *)
Inductive coloring : nat -> nat -> nat -> color -> Type :=
  | Gc {qp qs nc : nat} : coloring (3 + qp) (3 + qs) (S nc) green
  | Yc {qp qs nc : nat} : coloring (2 + qp) (2 + qs) (S nc) yellow
  | Oc {qp qs nc : nat} : coloring (1 + qp) (1 + qs) (S nc) orange
  | Rc {qp qs nc : nat} : coloring (0 + qp) (0 + qs) (S nc) red
  | Ec {qp qs : nat}    : coloring (0 + qp) (0 + qs)    0   green.

(* A type for nodes, i.e. pairs made of a prefix and a suffix. *)
Inductive node' (A : Type) : nat -> nkind -> color -> Type :=
  | Only_end {q  : nat} : prefix' A (S q) -> node' A 0 only green
  | Only {qp qs nc : nat} {C : color} :
    coloring qp qs (S nc) C -> prefix' A (5 + qp) -> suffix' A (5 + qs) ->
    node' A (S nc) only C
  | Left {qp qs nc : nat} {C : color} :
    coloring qp qs nc C -> prefix' A (5 + qp) -> suffix' A 2 ->
    node' A nc left C
  | Right {qp qs nc : nat} {C : color} :
    coloring qp qs nc C -> prefix' A 2 -> suffix' A (5 + qs) ->
    node' A nc right C.
Arguments Only_end {A q}.
Arguments Only {A qp qs nc C}.
Arguments Left {A qp qs nc C}.
Arguments Right {A qp qs nc C}.

(* A type for the regularity relation. *)
Inductive regularity :
  color -> color -> ckind -> color -> color -> Type :=
 | G {ck Cl Cr} : regularity green  green ck     Cl    Cr
 | Y {ck Cl Cr} : regularity yellow Cl    (S ck) Cl    Cr
 | OS {C}       : regularity orange C     single C     C
 | OP {Cr}      : regularity orange Cr    pair   green Cr
 | R {ck}       : regularity red    red   (S ck) green green.

(* A type for stored triples. *)
Inductive stored_triple (A : Type) : nat -> Type :=
  | Ground : A -> stored_triple A 0
  | Small {lvl q : nat} :
    suffix' (stored_triple A lvl) (3 + q) ->
    stored_triple A (S lvl)
  | Big {lvl qp qs : nat} {ck : ckind} {Cl Cr : color} :
    prefix' (stored_triple A lvl) (3 + qp) ->
    chain A (S lvl) ck only Cl Cr ->
    suffix' (stored_triple A lvl) (3 + qs) ->
    stored_triple A (S lvl)

(* A type for bodies, i.e. lists of yellow and orange nodes. *)
with body (A : Type) : nat -> nat -> nkind -> nkind -> Type :=
  | Hole {lvl : nat} {k : nkind} : body A lvl lvl k k
  | Single_child {hlvl tlvl : nat} {hk tk : nkind} {y o}:
    node' (stored_triple A hlvl) 1 hk (Mix NoGreen y o NoRed) ->
    body A (S hlvl) tlvl only tk ->
    body A hlvl tlvl hk tk
  | Pair_yellow {hlvl tlvl : nat} {hk tk : nkind} {C : color} :
    node' (stored_triple A hlvl) 2 hk yellow ->
    body A (S hlvl) tlvl left tk ->
    chain A (S hlvl) single right C C ->
    body A hlvl tlvl hk tk
  | Pair_orange {hlvl tlvl : nat} {hk tk : nkind} :
    node' (stored_triple A hlvl) 2 hk orange ->
    chain A (S hlvl) single left green green ->
    body A (S hlvl) tlvl right tk ->
    body A hlvl tlvl hk tk

(* A type for packets, a body and a following node, the tail. *)
with packet (A : Type) : nat -> nat -> nat -> nkind -> color -> Type :=
  | Packet {hlvl tlvl nc : nat} {hk tk : nkind} {g r} :
    body A hlvl tlvl hk tk ->
    node' (stored_triple A tlvl) nc tk (Mix g NoYellow NoOrange r) ->
    packet A hlvl tlvl nc hk (Mix g NoYellow NoOrange r)

(* A type for chains. *)
with chain (A : Type) : nat -> ckind -> nkind -> color -> color -> Type :=
  | Empty {lvl : nat} : chain A lvl empty only green green
  | Single {hlvl tlvl : nat} {ck : ckind} {nk : nkind} {C Cl Cr : color} :
    regularity C C ck Cl Cr ->
    packet A hlvl tlvl ck nk C ->
    chain A (S tlvl) ck only Cl Cr ->
    chain A hlvl single nk C C
  | Pair {lvl : nat} {Cl Cr : color} :
    chain A lvl single left Cl Cl ->
    chain A lvl single right Cr Cr ->
    chain A lvl pair only Cl Cr.

Arguments Ground {A}.
Arguments Small {A lvl q}.
Arguments Big {A lvl qp qs ck Cl Cr}.

Arguments Hole {A lvl k}.
Arguments Single_child {A hlvl tlvl hk tk y o}.
Arguments Pair_yellow {A hlvl tlvl hk tk C}.
Arguments Pair_orange {A hlvl tlvl hk tk}.

Arguments Packet {A hlvl tlvl nc hk tk g r}.

Arguments Empty {A lvl}.
Arguments Single {A hlvl tlvl ck nk C Cl Cr}.
Arguments Pair {A lvl Cl Cr}.

(* Prefixes, suffixes and nodes are only used with [stored_triple A lvl] inside
   of them. *)

Definition prefix (A : Type) (lvl : nat) := prefix' (stored_triple A lvl).
Definition suffix (A : Type) (lvl : nat) := suffix' (stored_triple A lvl).

Definition node (A : Type) (lvl : nat) := node' (stored_triple A lvl).

(* A type for catenable deques. *)
Inductive cadeque : Type -> Type :=
  | T {A : Type} {ck : ckind} : chain A 0 ck only green green -> cadeque A.

(* +------------------------------------------------------------------------+ *)
(* |                                 Models                                 | *)
(* +------------------------------------------------------------------------+ *)

(* Sequence + map + concat for nodes. *)
Definition concat_map_node'_seq
  {T : Type -> nat -> Type}
  (f : forall A lvl, T A lvl -> list A)
  {A lvlt nc nk C} (n : node' (T A lvlt) nc nk C) (l : list A) : list A :=
  match n with
  | Only_end p => Deque.concat_map_seq f p
  | Only  _ p s => Deque.concat_map_seq f p ++ l ++ Deque.concat_map_seq f s
  | Left  _ p s => Deque.concat_map_seq f p ++ l ++ Deque.concat_map_seq f s
  | Right _ p s => Deque.concat_map_seq f p ++ l ++ Deque.concat_map_seq f s
  end.

(* Returns the sequence associated to a stored triple. *)
Equations stored_triple_seq A lvl
  (st : stored_triple A lvl) : list A by struct st :=
stored_triple_seq A lvl (Ground a) := [a];
stored_triple_seq A lvl (Small s) := Deque.concat_map_seq stored_triple_seq s;
stored_triple_seq A lvl (Big p child s) :=
  Deque.concat_map_seq stored_triple_seq p ++
  chain_seq child ++
  Deque.concat_map_seq stored_triple_seq s

(* Returns the sequence associated to a body. *)
with body_seq {A hlvl tlvl hk tk}
  (b : body A hlvl tlvl hk tk) : list A -> list A by struct b :=
body_seq Hole l := l;
body_seq (Single_child hd b) l :=
  concat_map_node'_seq stored_triple_seq hd (body_seq b l);
body_seq (Pair_yellow hd b cr) l :=
  concat_map_node'_seq stored_triple_seq hd (body_seq b l ++ chain_seq cr);
body_seq (Pair_orange hd cl b) l :=
  concat_map_node'_seq stored_triple_seq hd (chain_seq cl ++ body_seq b l)

(* Returns the sequence associated to a packet. *)
with packet_seq {A hlvl tlvl nc nk C} :
  packet A hlvl tlvl nc nk C -> list A -> list A :=
packet_seq (Packet b tl) l :=
  body_seq b (concat_map_node'_seq stored_triple_seq tl l)

(* Returns the sequence associated to a chain. *)
with chain_seq {A lvl ck nk Cl Cr}
  (c : chain A lvl ck nk Cl Cr) : list A by struct c :=
chain_seq Empty := [];
chain_seq (Single _ pkt rest) := packet_seq pkt (chain_seq rest);
chain_seq (Pair cl cr) := chain_seq cl ++ chain_seq cr.