aac_rewrite not working with notations

[JulesViennotFranca]

I am writing a Coq project using AAC_tactics.

In my project, I use notation for some functions, and it breaks the aac_rewrite tactic.

To explain my problem, here is a simplified example:

(* Import useful packages *)
From Coq Require Import Program List Arith Lia.
Import ListNotations.
From Equations Require Import Equations.
From AAC_tactics Require Import AAC.
From AAC_tactics Require Import Instances.
Import Instances.Lists.

(* Type containing one element *)
Inductive singleton (A : Type) : Type :=
  | Single : A -> singleton A.
Arguments Single {A}.

(* Type containing two elements *)
Inductive doublon (A : Type) : Type :=
  | Double : A -> A -> doublon A.
Arguments Double {A}.

I want to define functions manipulating singletons and doublons while ensuring the total order of elements is preserved. To do so, I define functions using Equations returning the sequence associated to a singleton or a doublon:

Equations singleton_seq {A} : singleton A -> list A :=
singleton_seq (Single a) := [a].

Equations doublon_seq {A} : doublon A -> list A :=
doublon_seq (Double a b) := [a] ++ [b].

Next I can define my functions. First, I write small_rotation that takes a singleton and a doublon, and pops the first element of the doublon to push it on the singleton, returning a doublon and a singleton.

Notation "? x" := (exist _ x _) (at level 100).

Equations small_rotation {A} (s : singleton A) (d : doublon A) :
  { '(d', s') : doublon A * singleton A |
    singleton_seq s ++ doublon_seq d = doublon_seq d' ++ singleton_seq s' } :=
small_rotation (Single a) (Double b c) := ? (Double a b, Single c).

We use the "? x" notation to avoid writing the properties and let Equations try to prove them on its own. Here, Equations proves on its own the property singleton_seq s ++ doublon_seq d = doublon_seq d' ++ singleton_seq s', ensuring the order of elements is preserved.

Our next function is big_rotation, it does a same but takes a second singleton at the end. The function does nothing with this singleton but it forces us to use AAC_tactics.

Equations big_rotation {A} (s1 : singleton A) (d : doublon A) (s2 : singleton A) :
  { '(d', s1', s2') : doublon A * singleton A * singleton A |
    singleton_seq s1 ++ doublon_seq d ++ singleton_seq s2 =
      doublon_seq d' ++ singleton_seq s1' ++ singleton_seq s2' } :=
big_rotation s1 d s2 with small_rotation s1 d => {
  | exist _ (d', s1') H := ? (d', s1', s2) }.
Next Obligation.
  aac_rewrite H.
  aac_reflexivity.
Qed.

Because of the sequence of s2, Equations cannot rewrite H and therefore cannot prove the correctness of the function. We have to do it ourselves using aac_rewrite and aac_reflexivity.

However, in my project, the sequence functions are more complex for singletons and doublons to contain more specific types.

Definition concat_map_singleton_seq
  {T : Type -> Type}
  (f : forall A, T A -> list A)
  {A} (s : singleton (T A)) : list A :=
  match s with
  | Single a => f A a
  end.

Notation singleton_seq :=
  (concat_map_singleton_seq (T := fun A => A) (fun A a => [a])).

Definition concat_map_doublon_seq
  {T : Type -> Type}
  (f : forall A, T A -> list A)
  {A} (d : doublon (T A)) : list A :=
  match d with
  | Double a b => f A a ++ f A b
  end.

Notation doublon_seq :=
  (concat_map_doublon_seq (T := fun A => A) (fun A a => [a])).

Here, our previous singleton_seq and doublon_seq are just notations, being specific cases of the more general functions concat_map_singleton_seq and concat_map_doublon_seq.

small_rotation still works the same, is proved by Equations and does not require any changes. But when proving big_rotation, our previous proof doesn't work anymore. When trying to apply aac_rewrite H, an error is returned :
"Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/.".

The solution I found is to give name to every member of H, then aac_rewrite H works :

Equations big_rotation {A} (s1 : singleton A) (d : doublon A) (s2 : singleton A) : (* ... *).
Next Obligation.
  remember (singleton_seq s1) as s1_seq.
  remember (doublon_seq d) as d_seq.
  remember (doublon_seq d') as d'_seq.
  remember (singleton_seq s1') as s1'_seq.
  aac_rewrite H.
  aac_reflexivity.
Qed.

Is there a reason for this error ? I am doing something wrong ?

[palmskog]

@JulesViennotFranca this may be due to some interaction with Equations. But can you please post a self-contained minimal example that recreates the error on current AAC Tactics? For example you, could use the Fail command to highlight the error, as in:

(* ... *)
tactic1.
Fail my_tactic.
Abort.

[JulesViennotFranca]

Sure, in fact it fails when the aac_rewrite is placed before the remembers:

From Coq Require Import Program List.
Import ListNotations.
From Equations Require Import Equations.
From AAC_tactics Require Import AAC.
From AAC_tactics Require Import Instances.
Import Instances.Lists.

Inductive singleton (A : Type) : Type :=
  | Single : A -> singleton A.
Arguments Single {A}.

Inductive doublon (A : Type) : Type :=
  | Double : A -> A -> doublon A.
Arguments Double {A}.

Definition concat_map_singleton_seq
  {T : Type -> Type}
  (f : forall A, T A -> list A)
  {A} (s : singleton (T A)) : list A :=
  match s with
  | Single a => f A a
  end.

Notation singleton_seq :=
  (concat_map_singleton_seq (T := fun A => A) (fun A a => [a])).

Definition concat_map_doublon_seq
  {T : Type -> Type}
  (f : forall A, T A -> list A)
  {A} (d : doublon (T A)) : list A :=
  match d with
  | Double a b => f A a ++ f A b
  end.

Notation doublon_seq :=
  (concat_map_doublon_seq (T := fun A => A) (fun A a => [a])).

Notation "? x" := (exist _ x _) (at level 100).

Equations small_rotation {A} (s : singleton A) (d : doublon A) :
  { '(d', s') : doublon A * singleton A |
    singleton_seq s ++ doublon_seq d = doublon_seq d' ++ singleton_seq s' } :=
small_rotation (Single a) (Double b c) := ? (Double a b, Single c).

Equations big_rotation {A}
  (s1 : singleton A) (d : doublon A) (s2 : singleton A) :
  { '(d', s1', s2') : doublon A * singleton A * singleton A |
    singleton_seq s1 ++ doublon_seq d ++ singleton_seq s2 =
      doublon_seq d' ++ singleton_seq s1' ++ singleton_seq s2' } :=
big_rotation s1 d s2 with small_rotation s1 d => {
  | exist _ (d', s1') H := ? (d', s1', s2) }.
Next Obligation.
  Fail aac_rewrite H.
Abort.