Сопоставление с образцом гипотеза, полученная из сопоставления с образцом по цели - PullRequest
Новая
       68

Сопоставление с образцом гипотеза, полученная из сопоставления с образцом по цели

0 голосов
/ 22 октября 2018

Рассмотрим следующую ситуацию: 

Definition done {T : Type} (x : T) := True.

Goal Test.
  pose 1 as n.
  assert (done n) by constructor.
  Fail ltac:(
    match goal with 
    | [ H : done _ |- _ ] => fail
    | [ H : _ |- _ ] =>
      match goal with
      | [ _: done H |- _ ] => idtac "H == n"
      | [ _: done n |- _ ] => idtac "H != n"; fail 2
      end
    end
  ).
Abort.

Это печатает H != n.Я нахожу это очень удивительным, поскольку единственная гипотеза в области действия - это n и done n - и done n уже отправлено первой ветвью совпадения верхнего уровня.

Как я могусопоставить done n без явной ссылки на n, как в первой ветви второго совпадения?

1 Ответ

0 голосов
/ 25 октября 2018

Я думаю, вы смущены тем, как работает match.Первая ветвь сопоставления сопоставляется с каждой гипотезой, и если она всегда терпит неудачу, проверяется вторая ветвь и так далее.В вашем примере первая ветвь соответствует гипотезе H, но выполнение соответствующей тактики (fail) завершается неудачей, поэтому пробуется вторая ветвь, которая также соответствует гипотезе H.

На самом деле,первая ветвь внешнего match, кажется, делает то, что вы хотите (то есть соответствует гипотезе вида done _), поэтому я действительно не понимаю точку вашего внутреннего match.

Длянапример, 

match goal with 
| [ H' : done _ |- _ ] => idtac H'
end.

печатает H, показывая, что правильная гипотеза совпадает.

Обратите внимание, что вам не нужно выражение ltac:(), чтобы использовать Fail в тактике,Например, Fail fail. работает.

...