Рекомендации по эффективному использованию базы данных подсказок Coq

«Вопрос, который вы задаете, кажется субъективным и, скорее всего, будет закрыт».

Ну, я это знаю, но все же кажется, что стоит спросить здесь.

Мне много раз говорили, что я должен использовать базу данных подсказок и авто, потому что это лучшая вещь на свете и все такое. Однако несколько раз, когда я пытался использовать это, меня крайне раздражали тривиальные детали. Вот одна вещь, которая постоянно происходит.

Section Annoying.

Variable T : Type.
Variable P : T -> Prop.

Axiom notP : forall x, ~ P x.
Hint Resolve notP.

Goal forall (x : T), P x -> False.
intros x.
auto. (* nothing... *)
replace (P x -> False) with (~ P x) by reflexivity.
(* fold not. does not work, don't know why either but that is not the point here... *)
auto.
Qed.

End Annoying.

Поэтому мой вопрос: как люди пользуются базой данных подсказок и не натыкаются на такие неприятности. Существуют ли хорошие эмпирические правила для эффективной базы данных подсказок?


coq
person Ptival    schedule 09.01.2013    source источник

Ответы (1)


arrow_upward
3
arrow_downward

auto работает, применяя немодифицированные теоремы к целям. Он ищет, какие теоремы применить, путем синтаксического наблюдения за их формой. Таким образом, ваша теорема notP будет применяться только к целям вида

~ P ...

Цель формы P x -> False синтаксически не находится в этой форме. На самом деле автотактика работает следующим образом: сначала как можно больше используйте вступления, а затем пытайтесь применять теоремы. Таким образом, ваша цель превращается в

H : P x
=========
 False

а затем пытается применить теоремы, которые могут оказаться ложными. К сожалению, он пытается применять только те теоремы, для которых не требуется угадывать конкретизацию (теоремы, которые можно использовать с тактикой, применяются и не требуют расширения «с»). Таким образом, теорема с утверждением в форме «для всех a, P a -> False» никогда не будет использоваться auto, потому что apply будет жаловаться на то, что он знает, как создать экземпляр a.

Таким образом, хорошие доказательства-кандидаты для авто - это доказательства, которые вы можете сделать, используя только вводные и применяя, без экземпляра развертывания или применения ... с и без ручного применения теорем к аргументам, и где на каждом шаге самая правая формула ( в конце стрелок) теоремы использует предикат в качестве предиката, фигурирующего в заключении цели.

Ваш раздражающий пример работает, потому что цель в какой-то момент основной формулы - "~ P x", поэтому основной символ - нет, а auto имеет лемму notP в своей таблице для этого основного символа.

Вот пример, который хорошо работает:

Variable my_le : nat -> nat -> Prop.

Hypotheses my_le_n : forall x, my_le x x.

Hypothesis my_le_S : forall x y, my_le x y -> my_le x (S y).

Hint Resolve my_le_n my_le_S.

Lemma toto : my_le 10 14.
Proof.
auto.
Qed.

После команды Hint в таблице auto есть две леммы «my_le_n» и «my_le_S», которые будут использоваться, когда основным символом цели является my_le. Глядя на "my_le 10 14", он по очереди проверяет эти две леммы. Первый терпит неудачу, но второй применяется и создает новую цель «my_le 10 13», это можно повторить несколько раз, пока auto не удастся применить «my_le_n». Таким образом, auto исследует дерево возможностей, где ветвление возникает из-за того, что может быть несколько теорем, применимых для данной цели. Кроме того, длина ветвей ограничена 5, так что my_le 10 15 не будет решаться автоматически. Вы можете изменить длину ветвей, указав числовой аргумент для auto. поэтому «auto 20» решит «my_le 10 15» и другие подобные случаи.

person Yves    schedule 11.01.2013
comment
Я приму это как ответ, даже если бы я знал большую часть этого. Мне просто интересно, расширили ли люди определения not в леммах, которые попадут в hintdb, чтобы они работали всякий раз, когда какая-то тактика превращала nots в -> Falses... Думаю, нет, так что это немного раздражает. - person Ptival; 21.01.2013