How to define an automatically unfoldable definition

Question

I sometimes want to define some shortcut for existing functions like in the following example:

Parameter T : Set.
Parameter zero one : T.
Parameter f : T -> T -> option T.
Hypothesis f_unit : forall t, f zero t = None.Interpreting this declaration as if a global
declaration prefixed by "Local", i.e. as a global
declaration which shall not be available without
qualification when imported. [local-declaration,scope]

Definition g (t : T) := f t one.

However, this definition seems to be abstract since I cannot use theorems about f on instances of g without first unfolding:

Goal g zero = None.g zero = None
  unfold g.f zero one = None rewrite f_unit.None = None reflexivity.
Qed.

Is there a way to mark definitions as automatically unfoldable?

A: Yes, I would like not to have to manually unfold.

A: You could allow simpl to expand the definition of g by declaring Arguments g t /.

A: Or define g as a "parsing-only" shorthand notation instead of a function. Something like: Notation "'g' t" := (f t one) (at level 0, parsing only).

A: Or Hint Unfold g. and then use autounfold tactic in the proof.

A: Also, ssreflect can do it with with context patterns: Require Import ssreflect. then your goal can be proved by by rewrite [g _]f_unit.. This [g _] pattern makes rewrite to unfold the definition of g.

Answer

There are a couple of ways to accomplish what you ask, and here is an explanation of the ones I know:

Use an abbreviation. To quote the reference manual:

An abbreviation is a name, possibly applied to arguments, that denotes a (presumably) more complex expression.

[...]

Abbreviations are bound to an absolute name as an ordinary definition is, and they can be referred by qualified names too.

Abbreviations are syntactic in the sense that they are bound to expressions which are not typed at the time of the definition of the abbreviation but at the time it is used.

In your case, this would be
```
Notation g t := (f t one).
```
This is much like Daniel Schepler's suggestion of a Notation, except that it does not reserve g as a global keyword.

Use setoid_rewrite. Coq's setoid_rewrite tactic is similar to rewrite, except that it looks for occurrences modulo δ (unfolding), can rewrite under binders, and a few other minor things.

For your example, this is:
```
Require Import Coq.Setoids.Setoid.
Goal g zero = None.g zero = None
Proof.g zero = None
  setoid_rewrite f_unit.None = None reflexivity.
Qed.
```

In some cases, you can use Set Keyed Unification and Declare Equivalent Keys, though this does not work in your case (I've opened an issue on GitHub here. This tells rewrite to "unfold" one head constant to another, though it apparently isn't quite good enough to handle your case. There's a bit of documentation on the relevant commit message, and an open issue to add proper documentation.

Here is an example this is useful:

Parameter T : Set.
Parameter zero one: T.
Parameter f : T -> T -> option T.
Hypothesis f_unit : forall t, f zero t = None.Interpreting this declaration as if a global
declaration prefixed by "Local", i.e. as a global
declaration which shall not be available without
qualification when imported. [local-declaration,scope]

Definition g := f zero zero.

Set Keyed Unification.
Goal g = None.g = None
Proof.g = None
  rewrite f_unit.Found no subterm matching "f zero ?M160" in the current goal.
g = None
  Declare Equivalent Keys g f.g = None
  rewrite f_unit.None = None reflexivity.
Qed.