Как найти разницу между двумя списками в coq

Question

У меня есть два списка в coq. Я хочу найти разницу между этими двумя списками. Пожалуйста, помогите мне написать код в coq

Answer 1

То, что вы ищете, это не разница между двумя списками, а их пересечение. Вы можете запрограммировать эту функцию, повторно используя части стандартной библиотеки.

Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.

Definition intersection (l1 l2 : list nat) : list nat :=
  List.filter (fun n => List.existsb (Nat.eqb n) l2) l1.

Lemma intersectionP l1 l2 n : In n (intersection l1 l2) <-> In n l1 /\ In n l2.
Proof.
unfold intersection.
rewrite filter_In, existsb_exists; split.
- intros [H1 [m [H2 e]]]; split; trivial.
  rewrite Nat.eqb_eq in e; congruence.
- intros [H1 H2]; split; trivial.
  now exists n; split; trivial; rewrite Nat.eqb_refl.
Qed.

Answer 2

Как говорит Артур, существует множество версий различий. Если вы имеете в виду вычитание, здесь есть два подхода:

Variable (T: eqType).

Definition dlist1 (l1 l2 : seq T) :=
  foldr (fun x l => if x \in l2 then l else [:: x & l]) [::] l1.

Definition dlist2 (l1 l2 : seq T) :=
  foldl (fun l x => filter (predC1 x) l) l1 l2.

YMMV. Доказательства:

Lemma dlist2_nil l2 : dlist2 [::] l2 = [::].
Proof. by elim: l2. Qed.

Lemma dlist2_cons x1 l1 l2 :
  dlist2 (x1 :: l1) l2 =
  if x1 \in l2 then dlist2 l1 l2 else [:: x1 & dlist2 l1 l2].
Proof. by elim: l2 l1 => //= x2 l2 ih2 l1; rewrite inE; case: eqP => /=. Qed.

Lemma dlistP l1 l2 : dlist1 l1 l2 = dlist2 l1 l2.
Proof.
by elim: l1 l2 => [|x1 l1 ih1] /= l2; rewrite ?dlist2_nil // dlist2_cons ih1.
Qed.