Coq cannot `simple apply reflexivity` in custom tactic

Question

The fast reflexivity tactic shown below is very interesting. It exposes some of the unification machinery by disabling it.

I'm planning on going back and using it in the first part of Software Foundations in place of reflexivity to get a feel for when I'm relying on unification to close a goal.

(* reflexivity without unification, taken from coq stdpp *)
Ltac fast_reflexivity :=
  match goal with
  | |- _ ?x ?x => solve [simple apply reflexivity]
  end.                                                                                                                                                                                    

I learned about the stdpp library from this answer which links to the source on gitlab.

Here is the beginning of the tactic I am interested in.

A casual examination of the definition of the tactic suggests that it doesn't have any dependencies or depend on any non-default Coq settings.

However, if I try to compile it by itself I get the following error:

$ coqc fast_reflexivity.v 
File "./fast_reflexivity.v", line 4, characters 38-49:
Error: The reference reflexivity was not found in the current environment.

This error is confusing, the tactic reflexivity is definitely in scope by default.

The Coq program below compiles without issue.

Inductive bool :=
  | true
  | false
.

Theorem foo : true = true.
Proof.
  reflexivity.
Qed.

Although, interestingly, the program below also fails because it can't find reflexivity.

Inductive bool :=
  | true
  | false
.

Theorem foo : true = true.
Proof.
  simple apply reflexivity.
Qed.

I have two questions:

1. Why can't Coq see reflexivity?
2. Is there a way to write the fast_reflexivity tactic so that it will work in a vanilla Coq environment?

Answer 1

You are missing the following import:

From Coq Require Import Classes.RelationClasses.

You can realize that by clicking on reflexivity in your first link, or asking Locate reflexivity. in the context of the stdpp file above.

This particular reflexivity is a term (contrast with the reflexivity tactic, which is part of the Coq prelude), which might be what confused you? The way to parse the simple apply reflexivity tactic is that simple apply is a general tactic, with simple apply foo instructs Coq to apply lemma foo without resorting to unification, and this is applied to the particular reflexivity lemma from RelationClasses.