Méthode canonique pour obtenir un lemme plus spécifique

Question

Disons que j'ai un lemme mylem: foo ?a = bar ?a, et je dois l'appliquer sur un objectif qui a deux occurrences de foo, par ex. baz (foo (f p q)) (foo (g r s)), mais seulement à l'une de ces positions. Je connais deux façons de le faire sans avoir à écrire tous les p, q ..., qui peuvent être des expressions complexes.

• Utilisation apply (subst mylem) suivie d'un nombre approprié (ici, zéro ou un) de back commandes.
• En utilisant apply (subst mylem[where a = 'foo x y', standard]), où x et y sont des noms non liés.

L'utilisation de subst ici est juste pour la démonstration; Je veux vraiment modifier le lemme, par ex. pour l'utiliser avec rule quand il y a plusieurs correspondances possibles que je voudrais désambiguïser de cette façon.

Les deux approches ressemblent à un mauvais style pour moi. Y a-t-il une meilleure façon d'y parvenir?

Answer 1

Vous pouvez indiquer subst l'occurrence à remplacer: subst (i) mylem se déroule mylem lors de l'occurrence correspondante i. Cela vous évite les étapes back. Vous pouvez également répertorier plusieurs positions comme dans subst (1 2) mylem. Si vous souhaitez déplier mylem dans les locaux, utilisez subst (asm) (1 2) mylem.

En général, je ne connais pas un moyen d'obtenir ce que vous voulez dans un script apply. vous pouvez le faire explicitement comme ce

lemmas mylem' = mylem[where a="f x y"] for x y 

l'intérieur d'une preuve structurée,::

{ fix x y note mylem[where a="f x y"] } 
note mylem' = this