Автоматически выбирать предположение из местного контекста

У меня есть тестовый скрипт с разделом, который выглядит так:

  - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.
  - destruct (IHx1 _ _ H6). congruence.
  - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.
  - destruct (IHx1 _ _ H6). congruence.
  - destruct (IHx  _ _ H2). congruence.
  - destruct (IHx  _ _ H5). congruence.
  - destruct (IHx  _ _ H2). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H7). congruence.
  - destruct (IHx  _ _ H4). congruence.
  - destruct (IHx1 _ _ H8). congruence.
  - destruct (IHx1 _ _ H5). subst. destruct (IHx2 _ _ H9).

Кажется, что это был бы кандидат на использование ; для чистого решения, к сожалению, гипотезы повсюду. Как я могу свернуть различные поддоказательства вместе?


coq coq-tactic
person Carl Patenaude Poulin    schedule 27.05.2017    source источник
comment
Пожалуйста, не размещайте полные решения упражнений в SF в Интернете!   -  person Zimm i48    schedule 28.05.2017
comment
Разве вы не видели единственное, что выделено красным во введении? ?   -  person Zimm i48    schedule 28.05.2017
comment
Я прошу прощения! Я отредактирую свое решение, как только на него будет ответ. Я бы удалил его сейчас, но у меня нет другой столь же хорошей демонстрации проблемы, которую я пытаюсь продемонстрировать.   -  person Carl Patenaude Poulin    schedule 28.05.2017
comment
Я думаю, вам следует хотя бы отредактировать имена, чтобы это решение было трудно найти в Google.   -  person Anton Trunov    schedule 29.05.2017
comment
Я удалил информацию, которая идентифицировала вопрос. Извините за отсутствие осторожности :o   -  person Carl Patenaude Poulin    schedule 31.05.2017

Ответы (1)


arrow_upward
2
arrow_downward

Случаи, когда у нас есть только одна гипотеза индукции, могут быть решены с помощью следующего фрагмента Ltac (см. руководство, глава 9):

match goal with
  IH : forall st2 s2, ?c / ?st \\ s2 / st2 -> _,
  H : ?c / ?st \\ _ / _
  |- _ => now destruct (IH  _ _ H)
end

Где переменные с префиксом вопросительных знаков, например. ?c, ?st и т. д. — метапеременные, соответствующие шаблону, запятые разделяют гипотезы, а символ турникета (|-) отделяет гипотезы от цели. Здесь мы ищем индукционную гипотезу IH и совместимую гипотезу H, чтобы мы могли применить IH к H. Часть ?c / ?st обеспечивает совместимость IH и H.

Аналогично решаются подцели с двумя гипотезами индукции:

match goal with
  IH1 : forall st2 s2, ?c1 / ?st \\ s2 / st2 -> _,
  IH2 : forall st2 s2, ?c2 / _ \\ s2 / st2 -> _,
  H1 : ?c1 / ?st \\ _ / ?st'',
  H2 : ?c2 / ?st'' \\ _ / st2
  |- _ => now destruct (IH1  _ _ H1); subst; destruct (IH2 _ _ H2)
end

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

Ltac solve1 :=
  try match goal with
        IH : forall st2 s2, ?c / ?st || s2 / st2 -> _,
        H : ?c / ?st || _ / _
        |- _ => now destruct (IH  _ _ H)
      end.
person Anton Trunov    schedule 29.05.2017