diff options
author | Jason Gross <jgross@mit.edu> | 2019-03-07 17:29:48 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-03-07 17:29:48 -0500 |
commit | f5da3b5f4129e53d1b6f86c5942eab83b8af704f (patch) | |
tree | b440cc14d70dab9ec35152f20ab3914b0aa5a7e8 | |
parent | 8c8da234153c447b8bebc74865f9016b46322314 (diff) |
Add some Proper lemmas to ListUtil
-rw-r--r-- | src/Util/ListUtil.v | 21 |
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. |