Есть ли соглашение о порядке применения тактики / подсказок ssreflect?

Я пытаюсь понять, как комбинированные тактики ssreflect должны быть «декомпозированы» (или как они складываются в первую очередь). Одна из моих проблем - понять порядок и ассоциативность татикалов.

Иногда мне кажется, что порядок идет справа налево. Например

apply : AiB.

кажется эквивалентным

move : AiB; apply.

Игнорируя бездействие move, мы как бы применяем функции к AiB по порядку, а apply : AiB. можно рассматривать как apply (: AiB).. То есть мы сначала перемещаем AiB в цель, а затем вызываем apply для цели с AiB в ней.

Однако в других случаях меня сбивают с толку:

case: (EM (P y)) => // notPy.

Согласно учебнику, здесь проводится анализ случая на (EM (P y)) , а затем // пытается решить тривиальные подзадачи. Потом?? move => ввести остальные в контекст? Какой здесь порядок действий?

Пусть EM_ будет (EM (P y)), это (move=> notPy (// ( case (:EM_) ) ) ) ?? Правильно ли я прочитал, каков «правильный порядок» применения тактики?

Порядок искажен рядом с notPy и в целом непоследователен. Есть ли способ записать указанное выше справа налево в допустимом ssreflect?


coq ssreflect coq-tactic
person tinlyx    schedule 30.12.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Я советую вам прочитать руководство, чтобы получить более подробную информацию. https://hal.inria.fr/inria-00258384

В вашем примере вспомните, что ход всегда запрещен, поэтому он «плавится». Таким образом, с двоеточием он сливается слева.

move: H; case <=> case: H

а с => сливается справа:

case: H; move => U <=> case: H => U.

Таким образом, для вашего конкретного примера,

case: (EM (P y)) => // notPy.

можно рассматривать как

move: (EM (P y)); case; move=> // notPy.

С Уважением!

person ejgallego    schedule 28.01.2016