A test case that sfirstorder should solve

[QinshiWang]

I know that there may be no theoretical guarantee for sfirstorder, but it should solve this goal. I encounter this issue when proving a relation is transitive. Here are some minimal tests. Maybe it is worth adding them to the test suite. Test 1:

Require Import Hammer.Plugin.Hammer.

Axiom ident : Type.
Axiom state : Type.
Axiom val : Type.
Axiom get : ident -> state -> val.

Definition cond (p : ident) : bool :=
  true.

Goal forall st1 st2 st3,
  (forall q : ident, is_true (cond q) -> get q st1 = get q st2) ->
  (forall q : ident, is_true (cond q) -> get q st2 = get q st3) ->
  (forall q : ident, is_true (cond q) -> get q st1 = get q st3).
Proof.
  intros. Fail sfirstorder.
Abort.

Test 2:

Require Import Hammer.Plugin.Hammer.

Axiom ident : Type.
Axiom state : Type.
Axiom val : Type.
Axiom get : ident -> state -> val.

Definition cond (p : ident) : bool :=
  true.

Goal forall st1 st2 st3,
  (forall q : ident, is_true (negb (cond q)) -> get q st1 = get q st2) ->
  (forall q : ident, is_true (negb (cond q)) -> get q st2 = get q st3) ->
  (forall q : ident, is_true (negb (cond q)) -> get q st1 = get q st3).
Proof.
  intros. sfirstorder.
Abort.

Test 3:

Require Import Hammer.Plugin.Hammer.

Axiom ident : Type.
Axiom state : Type.
Axiom val : Type.
Axiom get : ident -> state -> val.

Axiom cond : ident -> bool.

Goal forall st1 st2 st3,
  (forall q : ident, is_true (cond q) -> get q st1 = get q st2) ->
  (forall q : ident, is_true (cond q) -> get q st2 = get q st3) ->
  (forall q : ident, is_true (cond q) -> get q st1 = get q st3).
Proof.
  intros. sfirstorder.
Abort.

Test 4:

Require Import Hammer.Plugin.Hammer.

Axiom ident : Type.
Axiom state : Type.
Axiom val : Type.
Axiom get : ident -> state -> val.

Definition cond (p : ident) : Prop :=
  True.

Goal forall st1 st2 st3,
  (forall q : ident, cond q -> get q st1 = get q st2) ->
  (forall q : ident, cond q -> get q st2 = get q st3) ->
  (forall q : ident, cond q -> get q st1 = get q st3).
Proof.
  intros. Fail sfirstorder.
Abort.

We can see that sfirstorder solves Tests 2&3 but not Test 1&4 for no obvious reason.

[QinshiWang]

CoqHammer version (from OPAM):

coq-hammer.8.13.dev 8.13.dev    pinned to version 8.13.dev at git+https://github.com/lukaszcz/coqhammer.git#v1.3.1-coq8.13

[lukaszcz]

Thank you for the report, but this is not an issue with CoqHammer per se.

sfirstorder is just a wrapper around firstorder and congruence, for the above tests roughly equivalent to simpl in *; firstorder congruence. The latter combination can solve Tests 2&3, but fails on 1&4. It solves Test 2 only because you get is_true false in the context after simpl in *. It seems firstorder has a problem with definitions. This issue should be directed to the authors of this tactic, or maybe submitted to the Coq developers since firstorder and congruence are part of standard Coq.