Add Tuple.map_Proper

1 files changed, 16 insertions, 0 deletions

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 7682c2d24..03cb4492b 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -845,5 +845,21 @@ Qed.
 Lemma to_list_repeat {A} (a:A) n : to_list _ (repeat a n) = List.repeat a n.
 Proof. induction n; [reflexivity|destruct n; simpl in *; congruence]. Qed.
 
+Global Instance map'_Proper {n A B} : Proper (pointwise_relation _ eq ==> eq ==> eq) (fun f => @map' A B f n) | 10.
+Proof.
+  induction n.
+  { compute; intros; subst; auto. }
+  { cbv [pointwise_relation Proper respectful] in *.
+    intros f g Hfg x y ?; subst y.
+    simpl; erewrite IHn by first [ eassumption | eauto ].
+    congruence. }
+Qed.
+
+Global Instance map_Proper {n A B} : Proper (pointwise_relation _ eq ==> eq ==> eq) (@map n A B) | 10.
+Proof.
+  destruct n; [ | apply map'_Proper ].
+  { repeat (intros [] || intro); auto. }
+Qed.
+
 Require Import Crypto.Util.ListUtil. (* To initialize [distr_length] database *)
 Hint Rewrite length_to_list' @length_to_list : distr_length.