Упорядоченный seq в Coq/SSreflect

Question

В настоящее время я играю с красно-черными деревьями в Coq и хотел бы составить списки nat с заказом, так что они могут быть сохранены на красно-черном дереве с помощью MSetRBT модуль.

По этой причине я определил seq_lt как показано:

Fixpoint seq_lt (p q : seq nat) := match p, q with
  | _, [::] => false
  | [::], _ => true
  | h :: p', h' :: q' =>
    if h == h' then seq_lt p' q'
    else (h < h')
end.

Пока мне удалось показать:

Lemma lt_not_refl p : seq_lt p p = false.
Proof.
  elim: p => //= ? ?; by rewrite eq_refl.
Qed.

так же как

Lemma lt_not_eqseq : forall p q, seq_lt p q -> ~(eqseq p q).
Proof.
  rewrite /not. move => p q.
  case: p; case: q => //= a A a' A'.
  case: (boolP (a' == a)); last first.
  - move => ? ?; by rewrite andFb.
  - move => a'_eq_a A'_lt_A; rewrite andTb eqseqE; move/eqP => Heq.
    move: A'_lt_A; by rewrite Heq lt_not_refl.
Qed.

Однако я изо всех сил пытаюсь доказать следующее:

Lemma seq_lt_not_gt p q : ~~(seq_lt q p) -> (seq_lt p q) || (eqseq p q).
Proof.
  case: p; case: q => // a A a' A'.
  case: (boolP (a' < a)) => Haa'.
  - rewrite {1}/seq_lt.
    suff -> : (a' == a) = false by move/negP => ?.
    by apply: ltn_eqF.
  - rewrite -leqNgt leq_eqVlt in Haa'.
    move/orP: Haa'; case; last first.
    + move => a_lt_a' _; apply/orP; left; rewrite /seq_lt.
      have -> : (a == a') = false by apply: ltn_eqF. done.
    + (* What now? *)
Admitted.

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

Answer 1

Я не уверен, в чем ваша проблема с индукцией, но доказательство кажется простым:

Local Notation "x < y" := (seq_lt x y).
Lemma seq_lt_not_gt p q : ~~ (q < p) = (p < q) || (p == q).
Proof.
elim: p q => [|x p ihp] [|y q] //=; rewrite [y == x]eq_sym eqseq_cons.
by case: ifP => h_eq; [exact: ihp | rewrite orbF ltnNge leq_eqVlt h_eq negbK].
Qed.

Если вы собираетесь использовать заказы, я предлагаю вам использовать некоторые библиотеки, расширяющие ssreflect для этой цели; Кажется, я помню, что у Сирила Коэна была разработка на github. Обратите внимание, что леммы о заказах имеют немного другую форму в mathcomp (пример ltn_neqAle), так что вы также можете сделать:

Lemma lts_neqAltN p q : (q < p) = (q != p) && ~~ (p < q).
Proof.
elim: p q => [|x p ihp] [|y q] //=; rewrite eqseq_cons [y == x]eq_sym.
by case: ifP => h_eq; [apply: ihp | rewrite ltnNge leq_eqVlt h_eq].
Qed.

Это могло бы работать немного лучше для переписывания.

PS: Я предлагаю это доказательство для вашей второй леммы:

Lemma lt_not_eqseq p q : seq_lt p q -> p != q.
Proof. by apply: contraTneq => heq; rewrite heq lt_not_refl. Qed.