You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
From Coq Require Import StrictProp.
From Hammer Require Import Tactics Hammer.
Fixpoint s_eq_nat (n m : nat): SProp :=
match n with
| O => match m with
| O => sUnit
| _ => sEmpty
end
| S n' => match m with
| O => sEmpty
| S m' => s_eq_nat n' m'
end
end.
Record sreflect (A : SProp) (B : Prop) := {
sprop_to_prop : A -> B;
prop_to_sprop : B -> A
}.
Theorem sreflect_eq_nat : forall n m, sreflect (s_eq_nat n m) (eq n m).
Proof.
intros n m.
split.
{ hammer. }
When the hammer tactic executes it yields the following anomaly:
"File "kernel/inductive.ml", line 124, characters 19-25: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
I guess this is a Coq bug and not a Coqhammer bug but I thought that you might be better equipped to figure out where the anomaly is coming from.
Coqc version:
The Coq Proof Assistant, version 8.17.0
compiled with OCaml 5.0.0
The text was updated successfully, but these errors were encountered:
I have experienced a similar issue but haven't found a way to produce a minimal example.
I always use sauto instead of hammer and sauto usually gives me the same error when the goal is not in SProp but the proof needs to use some SProp in the context to derive a contradiction. A manual proof usually requires some juggling to ensure the SProp hypotheses are destructed only when the goal is of sort SProp. My guess is that CoqHammer is not yet able to handle this type of scenario properly.
SProp has not been tested too well - it was introduced after the creation of CoqHammer. It might be a CoqHammer bug in that it might use the Coq API in some unexpected way.
I have the following anomaly:
When the
hammer
tactic executes it yields the following anomaly:I guess this is a Coq bug and not a Coqhammer bug but I thought that you might be better equipped to figure out where the anomaly is coming from.
Coqc version:
The Coq Proof Assistant, version 8.17.0
compiled with OCaml 5.0.0
The text was updated successfully, but these errors were encountered: