1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
From Corelib Require Import ssreflect ssrbool.
From Corelib Require Import ListDef.
Fixpoint contains {X: Type} (eqt: X -> X -> bool) (l: list X) (x: X): bool := true.
Fixpoint deduplicate {X: Type} (eqt: X -> X -> bool) (l: list X): list X := match l with
| nil => nil
| x :: xs => let deduplicatedRest := deduplicate eqt xs in
if (contains eqt deduplicatedRest x) then deduplicatedRest
else x :: deduplicatedRest
end.
Theorem deduplicate_idempotent: forall {X: Type} (eqt: X -> X -> bool) (l: list X), deduplicate eqt (deduplicate eqt l) = deduplicate eqt l.
Proof.
move => ? eqt.
elim => [|x xs IHxs] => //.
simpl.
case H: eqt.
Abort.
|
