Bug with Strictprop?

[patrick-nicodemus]

I have the following anomaly:

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

[yiyunliu]

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.

[lukaszcz]

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.