Coq индуктивные рассуждения о ACSL индуктивных предикатов?

Можно ли использовать индукцию для индуктивных предикатов, определенных в ACSL?

Рассмотрим следующий пример из руководства ACSL:

struct List {
    int value;
    struct List* next;
};
/*@ inductive reachable{L}(struct List* root, struct List* to) {
  @   case empty{L}: \forall struct List* l; reachable(l, l);
  @   case non_empty{L}: \forall struct List *l1,*l2;
  @     \valid(l1) && reachable(l1->next, l2) ==> reachable(l1, l2);
  @ }
*/

Я пытаюсь доказать следующую лемму:

/*@ lemma next_null_reachable: \forall struct List* l;
  @   \valid(l) && reachable(l, \null) ==> reachable(l->next, \null);
*/

Alt-Ergo терпит неудачу здесь, поэтому я прибегаю к ручным рассуждениям Coq:

Goal
  forall (t : array Z),
  forall (t_1 : farray addr addr),
  forall (a : addr),
  ((valid_rw t a 2%Z)) ->
  ((P_reachable t t_1 a (null))) ->
  ((P_reachable t t_1 (t_1.[ (shiftfield_F_List_next a) ]) (null))).

Но когда я Search P_reachableЯ нахожу только две сгенерированные аксиомы:

Q_non_empty:
  forall (t : array int) (t_1 : farray addr addr) (a_1 a : addr),
  valid_rw t a_1 2 ->
  P_reachable t t_1 (t_1 .[ shiftfield_F_List_next a_1]) a ->
  P_reachable t t_1 a_1 a
Q_empty:
  forall (t : array int) (t_1 : farray addr addr) (a : addr),
  P_reachable t t_1 a a

И нет принципа индукции. Поэтому я не могу подать заявку induction P_reachable или же destruct P_reachable,

Я использую плагин WP frama-c Версия Sodium-20150201.

Чтобы воспроизвести, вы могли бы запустить frama-c -wp -wp-rte -wp-prover coqide file.c, где file.c содержит List а также reachable определения и тому next_null_reachable Лемма.

Источник

2 ответа

Решение

Исходя из формы ваших целей, я предполагаю, что вы используете плагин WP. Действительно, он не дает лемму, указывающую, что reachable наименьший предикат, подтверждающий два случая empty а также non_emptyЭто означает, что вы не можете использовать индукцию.

Если я правильно помню, добавление такой аксиомы могло бы сбить с толку доказателей теорем первого порядка (которые бы неоднократно создавали примеры reachable через empty или же non_empty и уничтожить их по принципу индукции). Тем не менее, вывод Coq WP вполне может обеспечить полный перевод.

Обходной путь должен обеспечить соответствующий набор специализированных лемм (которые не могут быть доказаны через WP) вместо принципа индукции. См. Например binary_search_proved.c в этом архиве.

Источник

Я никогда не использовал Alt-Ergo, но кажется, что они не создают реальное индуктивное суждение, а скорее аксиоматизируют их. Так что вы не можете сделать induction но вы можете использовать основные блоки, которые они предоставляют (Q_empty ваш конструктор по умолчанию и Q_non_empty ваш индуктивный конструктор), чтобы выполнить доказательство.

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

Источник
Другие вопросы по тегам