dan
/
HITs-Examples
mirror of https://github.com/nmvdw/HITs-Examples
1
0
Fork 0
Code Issues Releases Wiki Activity

Decidable equality on FSets

This commit is contained in:
Dan Frumin 2017-06-21 11:22:56 +02:00
parent 1a3bb2cb5a
commit ab48ab4a75
1 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
FiniteSets/Ext.v
View File

@ -191,4 +191,16 @@ Proof.
apply H2.
Defined.
(* With extensionality we can prove decidable equality *)
Instance fsets_dec_eq `{Funext} : DecidablePaths (FSet A).
Proof.
intros X Y.
apply (decidable_equiv ((subset Y X = true) * (subset X Y = true)) (eq_subset X Y)^-1). (* TODO: this is so slow?*)
destruct (Y ⊆ X), (X ⊆ Y).
- left. refine (idpath, idpath).
- right. refine (false_ne_true o snd).
- right. refine (false_ne_true o fst).
- right. refine (false_ne_true o fst).
Defined.
End ext.