From c9f4cf296671baf01f3f08d2e027b415ef014059 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 23 Oct 2018 21:59:09 -0400 Subject: Add some equality lemmas about Positive{Map,Set} --- src/Util/FMapPositive/Equality.v | 28 ++++++++++++++++++++++++++++ src/Util/MSetPositive/Equality.v | 15 +++++++++++++++ 2 files changed, 43 insertions(+) create mode 100644 src/Util/FMapPositive/Equality.v create mode 100644 src/Util/MSetPositive/Equality.v (limited to 'src/Util') 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. -- cgit v1.2.3