|
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.
Next Obligation. apply remove_le. Defined.
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
