Tactic to partially compute goal in Coq

1
votes

I have goal 

quad X Y

, but I don't remember definition of "quad" and I don't want to start searching of its definition.

Is there a tactic that allow me rapidly substitute quad with its definition?

 Record quad (X Y:Type):= { x:X; y:Y}.

Or I have to remember and use 

refine (@Build_quad _ _).

?

1
coqcoq-tactic
constructor should work is most cases. You may also find Hint Constructors useful. – ejgallego
Btw, search in this case is not necessary, but it's rather simple: Print quad. will give you the desired information. If you're using ProofGeneral, you need to move the cursor (point) over the entity of interest and hit C-c C-a C-p and Enter. – Anton Trunov

1 Answers

3
votes

Your slightly mistaken, Build_quad is not the definition of quad, it is its constructor. It creates terms of type quad. As @ejgallego said, you should use the constructor tactic in this situation.

Your goal wants you to provide a term of type quad X Y, and the only way to build such a term from scratch is to use the constructor Build_quad of type forall X Y: Type, X -> Y -> quad X Y.