diff options
author | Jade Philipoom <jadep@mit.edu> | 2016-03-08 13:16:10 -0500 |
---|---|---|
committer | Jade Philipoom <jadep@mit.edu> | 2016-03-08 13:16:10 -0500 |
commit | b690b5180af6c8dadcf28dbe6661b43deff47331 (patch) | |
tree | aeec416fbd794b6abe66ba6a0a55a5361b9591a3 /src/Util/IterAssocOp.v | |
parent | bcc6f9c4de22dd4702da372e15e2725c6e8b4217 (diff) |
IterAssocOp: now uses arbitrary representation of scalar that implements testbit
Diffstat (limited to 'src/Util/IterAssocOp.v')
-rw-r--r-- | src/Util/IterAssocOp.v | 52 |
1 files changed, 29 insertions, 23 deletions
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 238fdfe73..fc21b997b 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -9,7 +9,11 @@ Section IterAssocOp. (assoc: forall a b c, op a (op b c) === op (op a b) c) (neutral:T) (neutral_l : forall a, op neutral a === a) - (neutral_r : forall a, op a neutral === a). + (neutral_r : forall a, op a neutral === a) + {scalar : Type} + (testbit : scalar -> nat -> bool) + (scToN : scalar -> N) + (testbit_spec : forall x i, testbit x i = N.testbit_nat (scToN x) i). Existing Instance op_proper. Fixpoint nat_iter_op n a := @@ -51,19 +55,19 @@ Section IterAssocOp. | S exp' => f (funexp f a exp') end. - Definition test_and_op n a (state : nat * T) := + Definition test_and_op sc a (state : nat * T) := let '(i, acc) := state in let acc2 := op acc acc in match i with | O => (0, acc) - | S i' => (i', if N.testbit_nat n i' then op a acc2 else acc2) + | S i' => (i', if testbit sc i' then op a acc2 else acc2) end. - Definition iter_op n a bound : T := - snd (funexp (test_and_op n a) (bound, neutral) bound). + Definition iter_op sc a bound : T := + snd (funexp (test_and_op sc a) (bound, neutral) bound). - Definition test_and_op_inv n a (s : nat * T) := - snd s === nat_iter_op (N.to_nat (N.shiftr_nat n (fst s))) a. + Definition test_and_op_inv sc a (s : nat * T) := + snd s === nat_iter_op (N.to_nat (N.shiftr_nat (scToN sc) (fst s))) a. Hint Rewrite N.succ_double_spec @@ -91,7 +95,7 @@ Section IterAssocOp. reflexivity. Qed. - Lemma shiftr_succ : forall n i, + Lemma Nshiftr_succ : forall n i, N.to_nat (N.shiftr_nat n i) = if N.testbit_nat n i then S (2 * N.to_nat (N.shiftr_nat n (S i))) @@ -115,21 +119,23 @@ Section IterAssocOp. apply N2Nat.id. Qed. - Lemma test_and_op_inv_step : forall n a s, - test_and_op_inv n a s -> - test_and_op_inv n a (test_and_op n a s). + Lemma test_and_op_inv_step : forall sc a s, + test_and_op_inv sc a s -> + test_and_op_inv sc a (test_and_op sc a s). Proof. destruct s as [i acc]. unfold test_and_op_inv, test_and_op; simpl; intro Hpre. destruct i; [ apply Hpre | ]. simpl. - rewrite shiftr_succ. - case_eq (N.testbit_nat n i); intro; simpl; rewrite Hpre, <- plus_n_O, nat_iter_op_plus; reflexivity. + rewrite Nshiftr_succ. + case_eq (testbit sc i); intro testbit_eq; simpl; + rewrite testbit_spec in testbit_eq; rewrite testbit_eq; + rewrite Hpre, <- plus_n_O, nat_iter_op_plus; reflexivity. Qed. - Lemma test_and_op_inv_holds : forall n a i s, - test_and_op_inv n a s -> - test_and_op_inv n a (funexp (test_and_op n a) s i). + Lemma test_and_op_inv_holds : forall sc a i s, + test_and_op_inv sc a s -> + test_and_op_inv sc a (funexp (test_and_op sc a) s i). Proof. induction i; intros; auto; simpl; apply test_and_op_inv_step; auto. Qed. @@ -144,14 +150,14 @@ Section IterAssocOp. destruct i; rewrite NPeano.Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity. Qed. - Lemma iter_op_termination : forall n a bound, N.size_nat n <= bound -> - test_and_op_inv n a - (funexp (test_and_op n a) (bound, neutral) bound) -> - iter_op n a bound === nat_iter_op (N.to_nat n) a. + Lemma iter_op_termination : forall sc a bound, + N.size_nat (scToN sc) <= bound -> + test_and_op_inv sc a + (funexp (test_and_op sc a) (bound, neutral) bound) -> + iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a. Proof. unfold test_and_op_inv, iter_op; simpl; intros ? ? ? ? Hinv. rewrite Hinv, funexp_test_and_op_index, Minus.minus_diag. - replace (N.shiftr_nat n 0) with n by auto. reflexivity. Qed. @@ -178,8 +184,8 @@ Section IterAssocOp. auto. Qed. - Lemma iter_op_spec : forall n a bound, N.size_nat n <= bound -> - iter_op n a bound === nat_iter_op (N.to_nat n) a. + Lemma iter_op_spec : forall sc a bound, N.size_nat (scToN sc) <= bound -> + iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a. Proof. intros. apply iter_op_termination; auto. |