From 4d7b3d1ed5e8d894e4bb9c1502d8b4432cdbe7af Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Nov 2017 16:23:24 -0500 Subject: Add fieldwise_Proper --- src/Util/Tuple.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 10f431990..b0904f09d 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -1042,3 +1042,20 @@ Proof. destruct n; intros; [ | apply map'_Proper ]. { repeat (intros [] || intro); auto. } Qed. + +Global Instance fieldwise'_Proper + : forall {n A B}, Proper (pointwise_relation _ (pointwise_relation _ impl) ==> eq ==> eq ==> impl) (@fieldwise' A B n) | 10. +Proof. + induction n as [|n IHn]; intros. + { compute; intros; subst; auto. } + { cbv [pointwise_relation Proper respectful impl] in *. + intros f g Hfg x y ? x' y' ? H'; subst y y'. + simpl in *; destruct H'; eauto. } +Qed. + +Global Instance fieldwise_Proper + : forall {n A B}, Proper (pointwise_relation _ (pointwise_relation _ impl) ==> eq ==> eq ==> impl) (@fieldwise A B n) | 10. +Proof. + destruct n; intros; [ | apply fieldwise'_Proper ]. + compute; trivial. +Qed. -- cgit v1.2.3