Применение тактики после epose или eset - PullRequest
Новая
       11

Применение тактики после epose или eset

0 голосов
/ 22 января 2019

Я хочу сделать тактику вроде 

let x := fresh in
epose (x := _);
forward_call x.

forward_call - это тактика обработки вызова функции в VST . Я нахожу, что если я сделаю epose _; forward_call x (если x - это имя по epose), то оно тоже перейдет в конечный цикл. Но это работает, если я делаю epose _. forward_call x., тогда это работает. То же самое произойдет, если я использую eset вместо epose. Я не понимаю, почему использование точки с запятой для соединения двух тактик отличается от использования двух команд, разделенных точкой, когда первая тактика генерирует только одну цель. Знаете ли вы разницу между этими двумя?

Я обнаружил, что epose (_); show_hyps. дает y := ?y : ?T, а epose (_). show_hyps. дает y := ?Goal0 : ?Goal. Может быть, это говорит о некоторой разнице.

Я не нашел простой пример для этой проблемы. Я пробовал простые случаи, как показано ниже, и нет разницы между использованием точки и точки с запятой. 

Require Import Coq.omega.Omega.
Require Import Coq.Program.Tactics.

Open Scope Z_scope.

Goal exists x, x = 2.
epose (y := _). refine (ex_intro _ y _); subst y.
reflexivity.
...