From 6971697c09e6720b8943865d80673a4b0a5083a6 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 14 Jun 2017 18:06:16 +0200 Subject: [PATCH] Add the difference operation --- FiniteSets/operations.v | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/FiniteSets/operations.v b/FiniteSets/operations.v index 5299d39..9f46115 100644 --- a/FiniteSets/operations.v +++ b/FiniteSets/operations.v @@ -16,7 +16,11 @@ hrecursion. - intros x y. compute. destruct x, y; reflexivity. - intros x. compute. reflexivity. - intros x. compute. destruct x; reflexivity. -- intros a'. compute. destruct (A_deceq a a'); reflexivity. +- intros a'. simpl. + destruct (match dec (a = a') with + | inl _ => true + | inr _ => false + end); compute; reflexivity. Defined. @@ -46,6 +50,9 @@ intros X Y. apply (comprehension (fun (a : A) => isIn a X) Y). Defined. +Definition difference : + FSet A -> FSet A -> FSet A := fun X Y => + comprehension (fun a => negb (isIn a X)) Y. Definition subset : FSet A -> FSet A -> Bool. @@ -65,4 +72,4 @@ Defined. End operations. Infix "∈" := isIn (at level 9, right associativity). -Infix "⊆" := subset (at level 10, right associativity). \ No newline at end of file +Infix "⊆" := subset (at level 10, right associativity).