Clever Geek Handbook

Coq: why do I need to manually expand the value even if it has "Hint Unfold" on it?

I came up with the following toy proof script:

Inductive myType : Type :=
| c : unit -> myType.

Inductive myProp : myType -> Type :=
| d : forall t, myProp (c t).
Hint Constructors myProp.

Definition myValue : myType := c tt.
Hint Unfold myValue.

Example test: myProp myValue.
Proof.
  auto 1000. (* does nothing *)
  unfold myValue.
  trivial.
Qed.

Why do I need to manually deploy myValue

here? Should a tooltip be displayed?

+3


source to share


2 answers


This is because (see refman )

This [ Hint Unfold <qualid>

] adds a tactic unfold qualid

to the tooltip list, which will only be used when the head target constant is an identifier.

And the target myProp myValue

is myProp

in the position of the head, not myValue

.

There are several ways to deal with this:

Hint Extern 4 => constructor.   (* change 4 with a cost of your choice *)


or

Hint Extern 4 => unfold myValue.

or even

Hint Extern 1 =>
  match goal with
  | [ |- context [myValue]] => unfold myValue
  end.
+4


source


@AntonTrunov correctly explains why Hint Unfold

not used here. There is an alternative Hint Transparent

that makes the application modulo delta for some specific constants. trivial

and , but supported , as you can see in the following: auto

eauto 



Inductive myType : Type :=
| c : unit -> myType.

Inductive myProp : myType -> Type :=
| d : forall t, myProp (c t).
Hint Constructors myProp.

Definition myValue : myType := c tt.
Hint Transparent myValue.

Example test: myProp myValue.
Proof.
  eauto.
Qed.
+3


source






More articles:


All Articles