diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-09 16:23:24 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-09 16:23:24 -0500 |
| commit | 4d7b3d1ed5e8d894e4bb9c1502d8b4432cdbe7af (patch) | |
| tree | 8056ba848ced0915152fb7413e1fcb6935e6070f /src/Util/Tuple.v | |
| parent | 818788035fb8130dca0aaf6a2ef78678ec437245 (diff) | |
Add fieldwise_Proper
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 17 |
1 files changed, 17 insertions, 0 deletions
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. |