Je butTactic pour calculer partiellement but en Coq
quad X Y
, mais je ne me souviens pas de définition « quad » et je ne veux pas commencer à chercher de sa définition.
Y a-t-il une tactique qui me permette de substituer rapidement le quad avec sa définition?
Record quad (X Y:Type):= { x:X; y:Y}.
Ou je dois me rappeler et utiliser
refine (@Build_quad _ _).
?
Votre légèrement erroné, Build_quad n'est pas la définition de quad, c'est son constructeur. Il crée des termes de type quad. Comme l'a dit @ejgallego, vous devriez utiliser la tactique constructor dans cette situation. Votre but veut que vous fournissiez un terme de type quad X Y, et la seule façon de construire un tel terme de toutes pièces est d'utiliser le constructeur Build_quad de type forall X Y: Type, X -> Y -> quad X Y.
Par souci d'exhaustivité: une méthode moins automatisée consisterait à 'appliquer Build_quad.' au lieu d'utiliser' constructor.' –
Habituellement j'utilise 'split' pour les enregistrements. – eponier
'constructor' devrait fonctionner dans la plupart des cas. Vous pouvez également trouver des 'Constructeurs de conseil 'utiles. – ejgallego
Btw, la recherche dans ce cas n'est pas nécessaire, mais c'est plutôt simple: 'Imprimer quad.' vous donnera l'information désirée. Si vous utilisez ProofGeneral, vous devez déplacer le curseur (point) sur l'entité qui vous intéresse et appuyer sur 'C-c C-a C-p' et' Enter'. –