diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-30 21:27:40 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-30 21:27:40 -0400 |
| commit | ce35e72e6771b9bb50775467008a4720f1a65eaa (patch) | |
| tree | 962caf6d78ef0181674cf6772650b3dc7cc9d718 /src/Util/NatUtil.v | |
| parent | feccf58999d715c7bc6d56c392985a67d3aa8dd1 (diff) | |
Add nat_rect_Proper_nondep_gen
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index cf09b33d2..865dc08f0 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -68,6 +68,12 @@ 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. +Global Instance nat_rect_Proper_nondep_gen {P} (R : relation P) : Proper (R ==> (eq ==> R ==> R) ==> Logic.eq ==> R) (@nat_rect (fun _ => P)) | 100. +Proof. + cbv [forall_relation respectful]; intros O_case O_case' HO S_case S_case' HS n n' ?; subst n'; revert O_case O_case' HO. + induction n as [|n IHn]; cbn [nat_rect]; intros; rewrite ?IHn, ?HS; auto. +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 |