Coq - недокументированная ошибка при индукции с eqn:

Используя Coq 8.4pl3, я получаю сообщение об ошибке при индукции с вариантом eqn:, который не указан в разделе индукции в справочном руководстве.

(* Export below requires Software Foundations 4.0. *)
Require Export Logic.

Inductive disjoint (X : Type) (l1 l2 : list X) : Prop :=
  | nil1 : l1 = [] -> disjoint X l1 l2
  | nil2 : l2 = [] -> disjoint X l1 l2
  | bothCons : forall x:X, 
                 In x l1 -> 
                   not (In x l2) -> 
                     disjoint X l1 l2.

Fixpoint head (X : Type) (l : list X) : option X :=
  match l with
  | [] => None
  | h :: t => Some h
  end.

Fixpoint tail (X : Type) (l : list X) : list X :=
  match l with
  | [] => []
  | h :: t => t
  end.

Inductive NoDup (X : Type) (l : list X) : Prop :=
  | ndNil : l = [] -> NoDup X l
  | ndSingle : forall x:X, l = [x] -> NoDup X l
  | ndCons : forall x:X, head X l = Some x ->
               not (In x (tail X l)) /\ NoDup X (tail X l) -> 
                 NoDup X l.

Theorem disjoint__app_NoDup : 
      forall (X : Type) (l1 l2 : list X),
        disjoint X l1 l2 /\ NoDup X l1 /\ NoDup X l2 ->
          NoDup X (l1 ++ l2).
Proof.
      intros. induction H eqn:caseEqn.

Если я заменю последний шаг просто «индукцией H», я не получу ошибки, но с указанным выше аргументом eqn: я получу ошибку:

Ошибка: в заключении используется a.

(Раньше в формулировке теоремы отсутствовало условие, и вместо этого в той же ошибке указывался идентификатор d.)

Ссылки на ручные списки "используется в заключении" как ошибка из-за использования assert. Это имеет какой-то смысл, что за кулисами eqn: может генерировать утверждения, но у меня нет идентификатора a, видимого в контексте, и я не вижу, что Coq пытается автоматически с этим справиться.

Пытался заменить начало доказательства на

  intros. remember H. induction H.

Теперь попытка выполнить индукцию дает ту же ошибку, что и раньше, только с H вместо a. (Когда в теореме отсутствовало дополнительное условие, Coq также явно добавил d в контекст, что идентично гипотезе H.)

Как я могу здесь двигаться дальше? Я стараюсь не терять информацию из контекста.


coq coq-tactic
person Christopher Brinkley    schedule 31.08.2016    source источник
comment
Было бы очень полезно MCVE со всем импортом. Например. в стандартной библиотеке нет disjoint (все строчные).   -  person Anton Trunov    schedule 01.09.2016
comment
Как бы то ни было, ваша теорема, вероятно, неверна. Списки [1;1] и [2;2] не пересекаются, но [1;1]++[2;2] содержат дубликаты. Возможно, вам также следует потребовать NoDup l1 /\ NoDup l2.   -  person larsr    schedule 01.09.2016
comment
(1) Проблема здесь в определении disjoint - оно на самом деле не индуктивное, поскольку его конструкторы не включают disjoint в качестве предпосылок, а только в качестве выводов. Таким образом, induction H eqn:caseEqn. можно заменить на destruct H eqn:caseEqn. (2) Кроме того, конструктор bothCons на самом деле является определением всей концепции disjoint, мы можем вывести из него nil1 и nil2, так что вы можете определить disjoint следующим образом: Definition disjoint {X : Type} (l1 l2 : list X) : Prop := forall x:X, In x l1 -> ~ (In x l2).   -  person Anton Trunov    schedule 02.09.2016
comment
Также я предлагаю вам взглянуть на определение NoDup в стандартная библиотека.   -  person Anton Trunov    schedule 02.09.2016
comment
Антон, спасибо за образование. Возможно, я здесь очень наивен, но я подумал, что если средство проверки типов Coq принимает индуктивное определение, оно должно быть правильно сформировано?   -  person Christopher Brinkley    schedule 02.09.2016
comment
(1) Действительно, он составлен правильно, и вы можете доказать свою теорему, используя его, но первые два конструктора избыточны - они не независимы от третьего, и такая независимость - то, к чему вы обычно стремитесь, более того, она не генерирует полезный принцип индукции. Если вы попробуете мое определение (или что-то подобное), вы можете использовать индукцию по списку.   -  person Anton Trunov    schedule 03.09.2016
comment
(2) Другой подход будет примерно таким: Inductive disjoint_i {X : Type} : list X -> list X -> Prop := dnil : forall l2, disjoint_i [] l2 | dcons : forall l1 l2 x, ~ (In x l2) -> disjoint_i l1 l2 -> disjoint_i (x::l1) l2. Это действительно индуктивное определение с независимыми случаями, и можно доказать, что оно эквивалентно неиндуктивному определению, которое я дал ранее. Возможно, его не очень удобно использовать при любых обстоятельствах из-за отсутствия симметрии, но я считаю, что его можно исправить.   -  person Anton Trunov    schedule 03.09.2016

Ответы (1)


arrow_upward
0
arrow_downward

Это незначительная ошибка; Я сообщил об этом. Однако то, что вы здесь пытаетесь сделать, не имеет особого смысла. Обратите внимание, что вы вызываете induction в соединении (/\) и просите Coq оставить вам уравнение, в котором говорится, что исходная гипотеза равна объединению двух сгенерированных доказательств. Здесь есть две проблемы:

  1. Ваша гипотеза нигде не используется зависимым образом, поэтому вам не нужно ее запоминать.
  2. Ваша гипотеза не рекурсивна, поэтому вы могли бы с таким же успехом использовать destruct H, а не induction H.

Что касается сообщения об ошибке, оно станет немного более ясным, если вы заметите, что замена /\ на * заставляет induction H eqn:caseEqn пройти и разбивает вашу гипотезу на две части с именами a и b. Фактическая проблема заключается в том, что термин доказательства, созданный induction H eqn:..., неверно типизирован, когда тип H - Prop, потому что вы не можете исключить Prop для получения информации. Я подозреваю, что код просто пытается что-то сделать с a, который он создает определенным образом, и предполагает, что любой отказ сделать это должен быть потому, что a используется в заключении, а не потому, что созданный им доказательный термин был плохим. -формированный.

person Jason Gross    schedule 28.02.2018