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

Question

Используя 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» для последнего шага, я не получаю сообщение об ошибке, но с указанным выше уравнением: аргумент, я получаю ошибку:

Error: a is used in conclusion.

(Ранее было условие отсутствует в формулировке теоремы, и та же ошибка, перечисленные в идентификатор д вместо.)

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

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

intros. remember H. induction H. 

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

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

Answer 1

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

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

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