Использование тактики "зависимой индукции" для сохранения информации во время индукции

Я только что столкнулся с проблемой, когда Coq induction отбрасывает информацию о сконструированных терминах при чтении доказательства из здесь.

Авторы использовали что-то вроде:

remember (WHILE b DO c END) as cw eqn:Heqcw.

переписать гипотезу H перед фактической индукцией induction H. Мне действительно не нравится идея вводить тривиальное равенство, потому что это похоже на черную магию.

Некоторый поиск здесь, в SO, показывает, что на самом деле трюк remember необходим. Однако один ответ, здесь, указывает на то, что новый dependent induction можно использовать, чтобы избежать уловки remember. Это хорошо, но сама dependent induction теперь кажется немного волшебной.

Мне трудно понять, как работает dependent induction. В документации приведен пример, в котором требуется dependent induction:

Lemma le_minus : forall n:nat, n < 1 -> n = 0.

Я могу проверить, как induction выходит из строя и dependent induction работает в этом случае. Но я не могу использовать трюк remember, чтобы воспроизвести результат dependent induction.

До сих пор я пытался имитировать трюк remember:

Require Import Coq.Program.Equality.

Lemma le_minus : forall n:nat, n < 1 -> n = 0.
intros n H. (* dependent induction H works*) 
remember (n < 1) as H0. induction H.

Но это не работает. Кто-нибудь может объяснить, как dependent induction здесь работает с точки зрения remember-ing?


induction coq coq-tactic
person tinlyx    schedule 04.12.2015    source источник
comment
Как указано в документации, зависимая индукция определяется в Coq.Program.Equality. Вы можете покопаться в нервах, чтобы увидеть, как он работает.   -  person gallais    schedule 04.12.2015

Ответы (1)


arrow_upward
1
arrow_downward

Ты можешь сделать

Require Import Coq.Program.Equality.

Lemma le_minus : forall n:nat, n < 1 -> n = 0.
Proof.
intros n H.
remember 1 as m in H. induction H.
- inversion Heqm. reflexivity.
- inversion Heqm. subst m.
  inversion H.
Qed.

Как указано здесь, проблема в том, что Coq не может отслеживать форму терминов, которые появляются в типе того, что вы делаем индукцию по. Другими словами, выполнение индукции по отношению «меньше чем» указывает Coq попытаться доказать что-то относительно общей верхней границы, в отличие от конкретной, которую вы рассматриваете (1).

Обратите внимание, что всегда можно доказать такие цели без remember или dependent induction, немного обобщив свой результат:

Lemma le_minus_aux :
  forall n m, n < m ->
    match m with
    | 1 => n = 0
    | _ => True
    end.
Proof.
intros n m H. destruct H.
- destruct n; trivial.
- destruct H; trivial.
Qed.

Lemma le_minus : forall n, n < 1 -> n = 0.
Proof.
intros n H.
apply (le_minus_aux n 1 H).
Qed.
person Arthur Azevedo De Amorim    schedule 04.12.2015