Coq: Как добавить содержательные подсказки?

Я новичок в Coq и, возможно, делаю совершенно неправильный путь. Мне кажется, что мне нужно выбирать между написанием аксиом / теорем, которые хорошо читаются человеком, и аксиомами / теоремами, которые полезны в качестве подсказок, поскольку в удобочитаемой форме они слишком "скрывают" синтаксис, и автоматическая тактика дает сбой. использовать их. Я хочу знать, есть ли способ насладиться лучшим из обоих миров.

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

В качестве обучающего упражнения я пытаюсь изучить теорию групп. Вот мои определения:

Variable G: Set.
Variable op: G -> G -> G.
Variable inv: G -> G.
Variable e:G.
Infix "+" := op.
Notation "- x" := (inv x).

Definition identity x := forall a:G, a + x = a /\ x + a = a.

Definition associative_law := forall a b c:G, a + (b + c) = (a + b) + c.
Definition identity_law := identity e.
Definition inverse_law := forall a:G, a + (-a ) = e /\ -a + a = e.
Definition group_laws:= associative_law /\ identity_law /\ inverse_law.
Axiom group_laws_hold: group_laws.

Я попытался сделать все доступным для чтения (по крайней мере, для меня). Таким образом, аксиома, гласящая, что e есть идентичность, «спрятана» за двумя уровнями абстракции: «group_laws» и «identity».

Я также могу написать эту аксиому (ну, одна половина мне понадобится) напрямую:

 Axiom identity_law_holds: forall a:G, a + e = a.

Теперь возьмем нашу групповую аксиому как подсказку:

Hint Resolve group_laws_hold.

Теперь я пытаюсь доказать простое утверждение о группах - идентичность уникальна:

Theorem identity_is_unique: forall x:G, identity x -> x = e.
Proof.
intros.
transitivity (op x e).
symmetry.

Все идет нормально. Теперь моя текущая цель - «x + e = x». Если я сделаю сейчас

apply group_laws_hold.

Эта цель будет решена. Однако выполнение «auto» ничего не дает, вероятно, поскольку Coq не может распознать, что «group_laws_hold» имеет отношение к «x + e = x» из-за того, что «group_laws_hold» не имеет того же синтаксиса, что и «x + e. = х ".

Однако, если я добавлю подсказку

Hint Resolve identity_law_holds.

Тогда "авто", конечно, будет работать. Но если я немного изменю "identity_law_holds" на что-то более общее (и более правильное)

 Axiom identity_law_holds: forall a:G, a + e = a /\ e + a = a.

Тогда "авто" снова выйдет из строя.

Итак, мой вопрос: есть ли способ исправить мой код так, чтобы "auto" работал, но с более общими подсказками, чем мой "Axiom identity_law_holds: forall a: G, a + e = a"?


coq
person Gadi A    schedule 23.12.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

eauto может выполнять некоторую нормализацию. Чего eauto не может сделать, так это индукции, потому что вывод принципов индукции, подобных and_ind, настолько общий, что замедлит eauto почти до полной остановки. Во всяком случае, eauto использует intros перед использованием eapply, когда часто необходимо провести индукцию, прежде чем что-либо вводить.

Вам нужно будет составить свои собственные менее общие прогнозы.

Lemma l1 : group_laws -> identity_law.
Proof. intros [? [? ?]]. eauto. Qed.

Lemma l2 : identity_law -> identity e.
Proof. eauto. Qed.

Lemma l3 : forall x, identity x -> forall a, a + x = a.
Proof. intros. einduction H. eauto. Qed.

Lemma l4 : forall x, identity x -> forall a, x + a = a.
Proof. intros. einduction H. eauto. Qed.

Hint Resolve eq_sym eq_trans group_laws_hold l1 l2 l3 l4.

Theorem identity_is_unique: forall x, identity x -> x = e.
Proof. info_eauto 7. Qed.

Но вы можете заставить eauto использовать and_ind.

Hint Extern 1 => eapply and_ind.
person Community    schedule 24.12.2013