Add some equality lemmas about Positive{Map,Set}

2 files changed, 43 insertions, 0 deletions

diff --git a/src/Util/FMapPositive/Equality.v b/src/Util/FMapPositive/Equality.v
new file mode 100644
index 000000000..aacd06a58
--- /dev/null
+++ b/src/Util/FMapPositive/Equality.v
@@ -0,0 +1,28 @@
+Require Import Coq.FSets.FMapPositive.
+Require Import Crypto.Util.Bool.Equality.
+Require Import Crypto.Util.Decidable.
+
+Module PositiveMap.
+  Scheme Induction for PositiveMap.tree Sort Type.
+  Scheme Induction for PositiveMap.tree Sort Set.
+  Scheme Induction for PositiveMap.tree Sort Prop.
+  Scheme Equality for PositiveMap.tree.
+
+  Notation t_beq := tree_beq.
+  Notation t_eq_dec := tree_eq_dec.
+  Notation internal_t_dec_bl := internal_tree_dec_bl.
+  Notation internal_t_dec_lb := internal_tree_dec_lb.
+
+  Lemma tree_eq_dec' {A} (A_dec : forall x y : A, {x = y} + {x <> y})
+    : forall x y : PositiveMap.tree A, {x = y} + {x <> y}.
+  Proof.
+    intros; do 2 decide equality.
+  Qed.
+
+  Global Instance tree_dec_eq {A} {A_dec : DecidableRel (@eq A)}
+    : DecidableRel (@eq (PositiveMap.tree A))
+    := @tree_eq_dec' A A_dec.
+  Global Instance t_dec_eq {A} {A_dec : DecidableRel (@eq A)}
+    : DecidableRel (@eq (PositiveMap.t A))
+    := @tree_eq_dec' A A_dec.
+End PositiveMap.
diff --git a/src/Util/MSetPositive/Equality.v b/src/Util/MSetPositive/Equality.v
new file mode 100644
index 000000000..4a5872a5e
--- /dev/null
+++ b/src/Util/MSetPositive/Equality.v
@@ -0,0 +1,15 @@
+Require Import Coq.MSets.MSetPositive.
+Require Import Crypto.Util.Bool.Equality.
+Require Import Crypto.Util.Decidable.
+
+Module PositiveSet.
+  Scheme Equality for PositiveSet.tree.
+
+  Notation t_beq := tree_beq.
+  Notation t_eq_dec := tree_eq_dec.
+  Notation internal_t_dec_bl := internal_tree_dec_bl.
+  Notation internal_t_dec_lb := internal_tree_dec_lb.
+
+  Global Instance tree_dec_eq : DecidableRel (@eq PositiveSet.tree) := tree_eq_dec.
+  Global Instance t_dec_eq : DecidableRel (@eq PositiveSet.t) := t_eq_dec.
+End PositiveSet.