Как уничтожить список в Coq (ноль или нет ноль)

Question

Я хочу уничтожить свой объект списка типов в двух случаях, таких как:

H: lst = nil.
H: lst <> nil

Answer 1

Если вы используете destruct lst as [ | fst_elnt lst_tl] eqn:H, вы получите две цели, в первой цели у вас есть нужная вам гипотеза.

H : lst = nil

Во второй цели у вас есть гипотеза в форме

H : lst = fst_elnt :: lst_tl

Это не то, что вы ожидаете от H, это на самом деле сильнее. Чтобы получить H с ожидаемым оператором, вы можете набрать следующее:

rename H into H'.  (* to free the name H *)
assert (H : lst <> nil).
   rewrite H'; discriminate.

discriminate - это основа c tacti c, которая выражает тот факт, что два разных конструктора типа данных не могут вернуть равные значения.

Answer 2

Один из возможных шаблонов для вашего пользовательского анализа случаев - предоставить пользовательскую лемму анализа случаев, шаблон выглядит следующим образом:

From Coq Require Import List.
Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive list_spec A : list A -> Type :=
  | Nil_case : forall x, x = [] -> list_spec x
  | Cons_case : forall x, x <> [] -> list_spec x.

Lemma listP A (l : list A) : list_spec l.
Proof. now case l; constructor. Qed.

Lemma foo A (l : list A) : False.
Proof.
case (listP l); intros x Hx.

Тогда вы получите правильную гипотезу в своем контексте. Использование destruct вместо case очистит оставшиеся ложные l.

Обратите внимание, что ssreflect case tacti c включает специальную поддержку для этого вида лемм анализа случаев, вы обычно делаю case: l / listP.