Open JulesViennotFranca opened 1 month ago
@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.
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.
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:
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: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.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 propertysingleton_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 useAAC_tactics
.Because of the sequence of
s2
,Equations
cannot rewriteH
and therefore cannot prove the correctness of the function. We have to do it ourselves usingaac_rewrite
andaac_reflexivity
.However, in my project, the sequence functions are more complex for singletons and doublons to contain more specific types.
Here, our previous
singleton_seq
anddoublon_seq
are just notations, being specific cases of the more general functionsconcat_map_singleton_seq
andconcat_map_doublon_seq
.small_rotation
still works the same, is proved byEquations
and does not require any changes. But when provingbig_rotation
, our previous proof doesn't work anymore. When trying to applyaac_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
, thenaac_rewrite H
works :Is there a reason for this error ? I am doing something wrong ?