1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
From Stdlib Require Import EquivDec Equivalence List Program.
From Stdlib Require Import Relation_Definitions.
Import ListNotations.
Generalizable All Variables.
Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V
:=
match l with
| nil => nil
| y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl)
end.
Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV :
@EqDec V eqV equivV} (xs : list V) (x : V) :
length (removeV x xs) < length (x :: xs).
Proof. Admitted.
(* Function version *)
Set Printing Universes.
From Stdlib Require Import Recdef.
Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV :
@EqDec V eqV equivV} (l : list V) { measure length l} :=
match l with
| nil => nil
| x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs)
end.
Proof. intros. apply remove_le. Qed.
(* Program version *)
Program Fixpoint nubV' `{eqDecV : @EqDec V eqV equivV} (l : list V)
{ measure (@length V l) lt } :=
match l with
| nil => nil
| x::xs => x :: @nubV' V eqV equivV eqDecV (removeV x xs) _
end.
Next Obligation. apply remove_le. Defined.
|
