Канонический способ получить более конкретную лемму

Question

Скажем, у меня есть лемма mylem: foo ?a = bar ?a, и мне нужно применить ее к цели, которая имеет два вхождения foo, например. baz (foo (f p q)) (foo (g r s)), но только в одном из этих положений. Я знаю два способа сделать это, не выписывая все p, q ..., которые могут быть сложными выражениями.

• Используя apply (subst mylem), за которым следует соответствующий номер (здесь, ноль или один) из back команд.
• Использование apply (subst mylem[where a = 'foo x y', standard]), где x и y - это несвязанные имена.

Использование subst здесь только для демонстрации; Я действительно хочу изменить лемму, например. использовать его с rule, когда есть несколько возможных совпадений, которые я бы хотел устранить так.

Оба подхода выглядят как плохой стиль для меня. Есть ли лучший способ достичь этого?

Answer 1

Вы можете сказать, subst появление которых он должен заменить: subst (i) mylem разворачивает mylem на -м возникновения согласования с i. Это сэкономит вам шаги back. Вы также можете перечислить несколько позиций, как в subst (1 2) mylem. Если вы хотите развернуть mylem в помещениях, используйте subst (asm) (1 2) mylem.

В общем, я не знаю, как добиться того, чего вы хотите в сценарии apply. На уровне теории, вы можете использовать lemmas с пунктом for обобщать над локально введенные переменные:

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

Внутри структурированном доказательства, вы можете сделать это в явном виде, как это:

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