aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-07 17:29:48 -0500
committerGravatar Jason Gross <jgross@mit.edu>2019-03-07 17:29:48 -0500
commitf5da3b5f4129e53d1b6f86c5942eab83b8af704f (patch)
treeb440cc14d70dab9ec35152f20ab3914b0aa5a7e8 /src/Util
parent8c8da234153c447b8bebc74865f9016b46322314 (diff)
Add some Proper lemmas to ListUtil
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/ListUtil.v21
1 files changed, 19 insertions, 2 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 803dca784..685c132b1 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -24,17 +24,34 @@ Definition list_case
| cons x xs => C x xs
end.
+Global Instance list_rect_Proper_dep_gen {A P} (RP : forall x : list A, P x -> P x -> Prop)
+ : Proper (RP nil ==> forall_relation (fun x => forall_relation (fun xs => RP xs ==> RP (cons x xs))) ==> forall_relation RP) (@list_rect A P) | 10.
+Proof.
+ cbv [forall_relation respectful]; intros N N' HN C C' HC ls.
+ induction ls as [|l ls IHls]; cbn [list_rect];
+ repeat first [ apply IHls | apply HC | apply HN | progress intros | reflexivity ].
+Qed.
Global Instance list_rect_Proper_dep {A P} : Proper (eq ==> forall_relation (fun _ => forall_relation (fun _ => forall_relation (fun _ => eq))) ==> forall_relation (fun _ => eq)) (@list_rect A P) | 1.
Proof.
- cbv [forall_relation]; intros N N' ? C C' HC ls; subst N'; revert N.
- induction ls as [|l ls IHls]; cbn [list_rect]; intro; rewrite ?IHls, ?HC; reflexivity.
+ cbv [forall_relation respectful Proper]; intros; eapply (@list_rect_Proper_dep_gen A P (fun _ => eq)); cbv [forall_relation respectful]; intros; subst; eauto.
+Qed.
+Global Instance list_rect_arrow_Proper_dep {A P Q} : Proper ((eq ==> eq) ==> forall_relation (fun _ => forall_relation (fun _ => (eq ==> eq) ==> (eq ==> eq))) ==> forall_relation (fun _ => eq ==> eq)) (@list_rect A (fun x => P x -> Q x)) | 10.
+Proof.
+ cbv [forall_relation respectful Proper]; intros; eapply (@list_rect_Proper_dep_gen A (fun x => P x -> Q x) (fun _ => eq ==> eq)%signature); intros; subst; eauto.
Qed.
Global Instance list_case_Proper_dep {A P} : Proper (eq ==> forall_relation (fun _ => forall_relation (fun _ => eq)) ==> forall_relation (fun _ => eq)) (@list_case A P) | 1.
Proof.
cbv [forall_relation]; intros N N' ? C C' HC ls; subst N'; revert N; destruct ls; eauto.
Qed.
+Global Instance list_rect_Proper_gen {A P} R
+ : Proper (R ==> (eq ==> eq ==> R ==> R) ==> eq ==> R) (@list_rect A (fun _ => P)) | 10.
+Proof. repeat intro; subst; apply (@list_rect_Proper_dep_gen A (fun _ => P) (fun _ => R)); cbv [forall_relation respectful] in *; eauto. Qed.
Global Instance list_rect_Proper {A P} : Proper (eq ==> pointwise_relation _ (pointwise_relation _ (pointwise_relation _ eq)) ==> eq ==> eq) (@list_rect A (fun _ => P)).
Proof. repeat intro; subst; apply (@list_rect_Proper_dep A (fun _ => P)); eauto. Qed.
+Global Instance list_rect_arrow_Proper {A P Q}
+ : Proper ((eq ==> eq) ==> (eq ==> eq ==> (eq ==> eq) ==> eq ==> eq) ==> eq ==> eq ==> eq)
+ (@list_rect A (fun _ => P -> Q)) | 10.
+Proof. eapply list_rect_Proper_gen. Qed.
Global Instance list_case_Proper {A P} : Proper (eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq) (@list_case A (fun _ => P)).
Proof. repeat intro; subst; apply (@list_case_Proper_dep A (fun _ => P)); eauto. Qed.