diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-26 11:59:14 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-26 11:59:14 -0400 |
| commit | 9be3994372659801306a848dc2ef419f04a5823a (patch) | |
| tree | 2ea2c25afa2e4859d3372263c0efc515f8e7f12f /src/Util/NatUtil.v | |
| parent | 0d9c835ea2b3d8c1931ee6b017c02cb6301484ee (diff) | |
Add more proper instances
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 9 |
1 files changed, 9 insertions, 0 deletions
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 |