aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4725.v
blob: fd5e0fb60d48c5e48b06c1eb976b658cad4840c5 (plain)
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
Require Import EquivDec Equivalence List Program.
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.

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.