From f5da3b5f4129e53d1b6f86c5942eab83b8af704f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Mar 2019 17:29:48 -0500 Subject: Add some Proper lemmas to ListUtil --- src/Util/ListUtil.v | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'src/Util') 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. -- cgit v1.2.3