dan/HITs-Examples
1
0
Fork 0
mirror of https://github.com/nmvdw/HITs-Examples synced 2025-11-03 07:03:51 +01:00
Code Issues Releases Wiki Activity

Add the difference operation

Browse Source
This commit is contained in:
Dan Frumin
2017-06-14 18:06:16 +02:00
parent 036d1599b2
commit 6971697c09
1 changed files with 9 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
FiniteSets/operations.v
View File

@@ -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).
Infix "⊆" := subset (at level 10, right associativity).