diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/Tuple.v | 36 | ||||
-rw-r--r-- | src/Util/ZRange.v | 2 |
2 files changed, 13 insertions, 25 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 2b049d86e..7682c2d24 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -255,18 +255,6 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys. -Fixpoint pointwise2' {n A B} (R:A -> B -> Prop) : tuple' A n -> tuple' B n -> Prop - := match n with - | 0 => R - | S n' => fun (x y : tuple' _ _ * _) - => @pointwise2' n' A B R (fst x) (fst y) /\ R (snd x) (snd y) - end. -Definition pointwise2 {n A B} (R:A -> B -> Prop) : tuple A n -> tuple B n -> Prop - := match n with - | 0 => fun _ _ => True - | S n' => pointwise2' R - end. - Lemma to_list'_ext {n A} (xs ys:tuple' A n) : to_list' n xs = to_list' n ys -> xs = ys. Proof. induction n; simpl in *; [cbv; congruence|]; destruct_head' prod. @@ -472,17 +460,17 @@ Proof. | intro ]. Qed. -Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' A n) (b:tuple' B n) {struct n} : Prop. - destruct n; simpl @tuple' in *. - { exact (R a b). } - { exact (R (snd a) (snd b) /\ fieldwise' _ _ n R (fst a) (fst b)). } -Defined. - -Definition fieldwise {A B} (n:nat) (R:A->B->Prop) (a:tuple A n) (b:tuple B n) : Prop. - destruct n; simpl @tuple in *. - { exact True. } - { exact (fieldwise' _ R a b). } -Defined. +Fixpoint fieldwise' {A B} (n:nat) (R:A -> B -> Prop) : tuple' A n -> tuple' B n -> Prop + := match n with + | 0 => R + | S n' => fun (x y : tuple' _ _ * _) + => @fieldwise' A B n' R (fst x) (fst y) /\ R (snd x) (snd y) + end. +Definition fieldwise {A B} (n:nat) (R:A -> B -> Prop) : tuple A n -> tuple B n -> Prop + := match n with + | 0 => fun _ _ => True + | S n' => fieldwise' n' R + end. Local Ltac Equivalence_fieldwise'_t := let n := match goal with |- ?R (fieldwise' ?n _) => n end in @@ -566,7 +554,7 @@ End fieldwise_map. Fixpoint fieldwiseb' {A B} (n:nat) (R:A->B->bool) (a:tuple' A n) (b:tuple' B n) {struct n} : bool. destruct n; simpl @tuple' in *. { exact (R a b). } - { exact (R (snd a) (snd b) && fieldwiseb' _ _ n R (fst a) (fst b))%bool. } + { exact (fieldwiseb' _ _ n R (fst a) (fst b) && R (snd a) (snd b))%bool. } Defined. Definition fieldwiseb {A B} (n:nat) (R:A->B->bool) (a:tuple A n) (b:tuple B n) : bool. diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v index fab098037..2c286aa9e 100644 --- a/src/Util/ZRange.v +++ b/src/Util/ZRange.v @@ -34,7 +34,7 @@ Section with_bitwidth. end. Definition is_bounded_by {n} : Tuple.tuple zrange n -> Tuple.tuple Z n -> Prop - := Tuple.pointwise2 is_bounded_by'. + := Tuple.fieldwise is_bounded_by'. End with_bitwidth. Definition is_tighter_than_bool (x y : zrange) : bool |