diff options
author | Jason Gross <jagro@google.com> | 2018-08-13 23:58:49 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-08-15 22:09:50 -0400 |
commit | 8926b3f6b2aa1fe0f8d3f65f1966f60402cad4b9 (patch) | |
tree | b4f92732531a3aab686f2e4a5a9f98d4264e61b0 /src/Util/ZRange/Operations.v | |
parent | f4d27f9218990b904da65ec4e87ed5d84358ce65 (diff) |
Prove monotonicity properties about zrange
Diffstat (limited to 'src/Util/ZRange/Operations.v')
-rw-r--r-- | src/Util/ZRange/Operations.v | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 32af62ee5..c8db4adf0 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -72,6 +72,55 @@ Module ZRange. Definition constant (v : Z) : zrange := r[v ~> v]. + Fixpoint nary_T (A B : Type) (n : nat) := + match n with + | O => B + | S n => A -> nary_T A B n + end. + + Fixpoint under_args {A B B'} (F : B -> B') {n : nat} : nary_T A B n -> nary_T A B' n + := match n with + | O => F + | S n => fun f x => @under_args A B B' F n (f x) + end. + + Fixpoint under_args2 {A B B' B''} (F : B -> B' -> B'') {n : nat} : nary_T A B n -> nary_T A B' n -> nary_T A B'' n + := match n with + | O => F + | S n => fun f g x => @under_args2 A B B' B'' F n (f x) (g x) + end. + + Definition apply_to_range_under_args {A} {n} (f : Z -> nary_T A zrange n) (v : zrange) : nary_T A zrange n + := let (l, u) := eta v in + under_args2 union (f l) (f u). + + Definition apply_to_split_range_under_args {A} {n} (f : zrange -> nary_T A zrange n) (v : zrange) : nary_T A zrange n + := match split_range_at_0 v with + | (Some n, Some z, Some p) => under_args2 union (under_args2 union (f n) (f p)) (f z) + | (Some v1, Some v2, None) | (Some v1, None, Some v2) | (None, Some v1, Some v2) => under_args2 union (f v1) (f v2) + | (Some v, None, None) | (None, Some v, None) | (None, None, Some v) => f v + | (None, None, None) => f v + end. + + Definition apply_to_each_split_range_under_args {A} {n} (f : BinInt.Z -> nary_T A zrange n) (v : zrange) : nary_T A zrange n + := apply_to_split_range_under_args (apply_to_range_under_args f) v. + + Fixpoint n_corners {n : nat} : nary_T Z Z n -> nary_T zrange zrange n + := match n with + | O => constant + | S n + => fun (f : Z -> nary_T Z Z n) (v : zrange) + => apply_to_range_under_args (fun x => n_corners (f x)) v + end. + + Fixpoint n_corners_and_zero {n : nat} : nary_T Z Z n -> nary_T zrange zrange n + := match n with + | O => constant + | S n + => fun (f : Z -> nary_T Z Z n) (v : zrange) + => apply_to_each_split_range_under_args (fun x => n_corners_and_zero (f x)) v + end. + Definition two_corners (f : Z -> Z) (v : zrange) : zrange := apply_to_range (fun x => constant (f x)) v. Definition four_corners (f : Z -> Z -> Z) (x y : zrange) : zrange |