QinshiWang
commented
2 years ago I encountered this issue again recently and was able to figure out a small example.
Require Import Coq.Lists.List.
Require Import Hammer.Plugin.Hammer.
Import ListNotations.
Class ExternSem := {
extern_state : Type;
(* sauto works if removing this line. *)
AbsMet := extern_state -> extern_state -> Prop
}.
Section EXT.
Context {target : ExternSem}.
Definition EXT (a : list (extern_state -> Prop)) (es : extern_state) : Prop :=
fold_right and True (map (fun (ep : extern_state -> Prop) => (ep es)) a).
End EXT.
Section ExtExtract.
Context {target : ExternSem}.
Fixpoint remove_nth {A} (n : nat) (al : list A) {struct n} : list A :=
match n, al with
| O, a :: al => al
| S n', a :: al' => a :: remove_nth n' al'
| _, nil => nil
end.
Lemma test : forall n es,
EXT (remove_nth n []) es.
Proof.
(* sauto. *)
(* Anomaly "Unable to handle arbitrary u+k <= v constraints."
Please report at http://coq.inria.fr/bugs/. *)
(* Fail sauto. *)
(* Even this fails. *)
Abort.
End ExtExtract.
(* sauto works if a target is provided. *)
#[local] Instance target : ExternSem.
Admitted.
Lemma test : forall n es,
EXT (remove_nth n []) es.
Proof.
sauto.
Qed.There is no problem if EXT and test are in the same section.
Require Import Coq.Lists.List.
Require Import Hammer.Plugin.Hammer.
Import ListNotations.
Class ExternSem := {
extern_state : Type;
AbsMet := extern_state -> extern_state -> Prop
}.
Section ExtExtract.
Context {target : ExternSem}.
Definition EXT (a : list (extern_state -> Prop)) (es : extern_state) : Prop :=
fold_right and True (map (fun (ep : extern_state -> Prop) => (ep es)) a).
Fixpoint remove_nth {A} (n : nat) (al : list A) {struct n} : list A :=
match n, al with
| O, a :: al => al
| S n', a :: al' => a :: remove_nth n' al'
| _, nil => nil
end.
Lemma test : forall n es,
EXT (remove_nth n nil) es.
Proof.
sauto.
Qed.
End ExtExtract.
I encounter a strange problem. After a seemingly unrelated change, CoqHammer's
sautotactic does not work anymore in some goals, where it used to work. And it reportsIt seems that a certain proof searching step in
sautoproduces a universe constraint that Coq does not support. Coq only allows universe constraint in the form ofu+k <= vwherekis a constant. If this is the case, a possible fix is to locate what proof searching causes this constrain, and then either prevent this from happening or catch the exception and assume the proof searching step has failed.I have a relatively small example of the issue, but it's based on our project. I can try to make an independent example if it is helpful.