diff options
-rw-r--r-- | src/Util/ListUtil.v | 37 | ||||
-rw-r--r-- | src/Util/NatUtil.v | 9 |
2 files changed, 40 insertions, 6 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 3e0313800..390f75cd7 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -24,16 +24,19 @@ Definition list_case | cons x xs => C x xs end. -Global Instance list_rect_Proper A P : Proper (eq ==> pointwise_relation _ (pointwise_relation _ (pointwise_relation _ eq)) ==> eq ==> eq) (@list_rect A (fun _ => P)). +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. - intros N N' HN C C' HC xs ys Hxs; subst N' ys. - induction xs; cbn; trivial; rewrite IHxs; apply HC. + 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. Qed. -Global Instance list_case_Proper A P : Proper (eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq) (@list_case A (fun _ => P)). +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 [pointwise_relation respectful]. - intros N N' HN C C' HC xs ys Hxs; subst N' ys; destruct xs; cbn; auto. + cbv [forall_relation]; intros N N' ? C C' HC ls; subst N'; revert N; destruct ls; 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_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. Create HintDb distr_length discriminated. Create HintDb simpl_set_nth discriminated. @@ -512,6 +515,9 @@ Global Instance update_nth_Proper {T} : Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@update_nth T). Proof. repeat intro; subst; apply update_nth_ext; trivial. Qed. +Global Instance update_nth_Proper_eq {A} : Proper (eq ==> (eq ==> eq) ==> eq ==> eq) (@update_nth A) | 1. +Proof. repeat intro; subst; apply update_nth_Proper; repeat intro; eauto. Qed. + Lemma update_nth_id_eq_specific {T} f n : forall (xs : list T) (H : forall x, nth_error xs n = Some x -> f x = x), update_nth n f xs = xs. @@ -1954,6 +1960,25 @@ Proof. induction xs; cbn in *; [ reflexivity | rewrite IHxs; f_equal ]; intros; Global Instance flat_map_Proper A B : Proper (pointwise_relation _ eq ==> eq ==> eq) (@flat_map A B). Proof. repeat intro; subst; apply flat_map_ext; auto. Qed. +Global Instance map_Proper_eq {A B} : Proper ((eq ==> eq) ==> eq ==> eq) (@List.map A B) | 1. +Proof. repeat intro; subst; apply pointwise_map; repeat intro; eauto. Qed. +Global Instance flat_map_Proper_eq {A B} : Proper ((eq ==> eq) ==> eq ==> eq) (@List.flat_map A B) | 1. +Proof. repeat intro; subst; apply flat_map_Proper; repeat intro; eauto. Qed. +Global Instance partition_Proper {A} : Proper (pointwise_relation _ eq ==> eq ==> eq) (@List.partition A). +Proof. + cbv [pointwise_relation]; intros f g Hfg ls ls' ?; subst ls'. + induction ls as [|l ls IHls]; cbn [partition]; rewrite ?IHls, ?Hfg; reflexivity. +Qed. +Global Instance partition_Proper_eq {A} : Proper ((eq ==> eq) ==> eq ==> eq) (@List.partition A) | 1. +Proof. repeat intro; subst; apply partition_Proper; repeat intro; eauto. Qed. +Global Instance fold_right_Proper {A B} : Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@fold_right A B) | 1. +Proof. + cbv [pointwise_relation]; intros f g Hfg x y ? ls ls' ?; subst y ls'; revert x. + induction ls as [|l ls IHls]; cbn [fold_right]; intro; rewrite ?IHls, ?Hfg; reflexivity. +Qed. +Global Instance fold_right_Proper_eq {A B} : Proper ((eq ==> eq ==> eq) ==> eq ==> eq ==> eq) (@fold_right A B) | 1. +Proof. cbv [respectful]; repeat intro; subst; apply fold_right_Proper; repeat intro; eauto. Qed. + Lemma partition_map A B (f : B -> bool) (g : A -> B) xs : partition f (map g xs) = (map g (fst (partition (fun x => f (g x)) xs)), map g (snd (partition (fun x => f (g x)) xs))). diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 08fd8a92a..cf09b33d2 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,5 +1,6 @@ Require Coq.Logic.Eqdep_dec. Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. +Require Import Coq.Classes.Morphisms. Require Import Coq.micromega.Lia. Import Nat. @@ -59,6 +60,14 @@ Tactic Notation "omega" := coq_omega. Tactic Notation "omega" "*" := omega_with_min_max_case. Tactic Notation "omega" "**" := omega_with_min_max. +Global Instance nat_rect_Proper {P} : Proper (Logic.eq ==> forall_relation (fun _ => forall_relation (fun _ => Logic.eq)) ==> forall_relation (fun _ => Logic.eq)) (@nat_rect P). +Proof. + cbv [forall_relation]; intros O_case O_case' ? S_case S_case' HS n; subst O_case'; revert O_case. + induction n as [|n IHn]; cbn [nat_rect]; intro; rewrite ?IHn, ?HS; reflexivity. +Qed. +Global Instance nat_rect_Proper_nondep {P} : Proper (Logic.eq ==> pointwise_relation _ (pointwise_relation _ Logic.eq) ==> Logic.eq ==> Logic.eq) (@nat_rect (fun _ => P)). +Proof. repeat intro; subst; apply (@nat_rect_Proper (fun _ => P)); eauto. Qed. + Lemma nat_eq_dec_S x y : match nat_eq_dec (S x) (S y), nat_eq_dec x y with | left pfS, left pf => pfS = f_equal S pf |