diff options
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 4 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 2 | ||||
| -rw-r--r-- | src/Util/IterAssocOp.v | 29 |
3 files changed, 15 insertions, 20 deletions
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index 0f02000d0..4f51f299d 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -106,7 +106,7 @@ Global Instance Proper_test_and_op {T scalar} `{Requiv:@Equivalence T RT} {op:T->T->T} {Proper_op:Proper (RT==>RT==>RT) op} {testbit:scalar->nat->bool} {s:scalar} {zero:T} : let R := fun x y => fst x = fst y /\ snd x === snd y in - Proper (R==>R) (test_and_op op testbit s zero). + Proper (R==>R) (@test_and_op _ op _ testbit s zero). Proof. unfold test_and_op; simpl; repeat intro; intuition; repeat match goal with @@ -119,7 +119,7 @@ Lemma iter_op_proj {T T' S} `{T'Equiv:@Equivalence T' RT'} (proj : T -> T') (op : T -> T -> T) (op' : T' -> T' -> T') {Proper_op':Proper (RT' ==> RT' ==> RT') op'} x y z (testbit : S -> nat -> bool) (bound : nat) (op_proj : forall a b, proj (op a b) === op' (proj a) (proj b)) - : proj (iter_op op x testbit y z bound) === iter_op op' (proj x) testbit y (proj z) bound. + : proj (@iter_op _ op x _ testbit y z bound) === @iter_op _ op' (proj x) _ testbit y (proj z) bound. Proof. unfold iter_op. lazymatch goal with diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 8e526745c..951f848bf 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -220,7 +220,7 @@ Section FandZ. reflexivity. Qed. - Lemma pow_nat_iter_op_correct: forall (x:F m) n, (nat_iter_op mul 1) (N.to_nat n) x = x^n. + Lemma pow_nat_iter_op_correct: forall (x:F m) n, (@nat_iter_op _ mul 1) (N.to_nat n) x = x^n. Proof. induction n using N.peano_ind; destruct (F_pow_spec x) as [pow_0 pow_succ]; diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 82d22046d..8d39c8275 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -1,49 +1,44 @@ Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Crypto.Algebra. +Import Monoid. Local Open Scope equiv_scope. Generalizable All Variables. Section IterAssocOp. - Context `{Equivalence T} - {scalar : Type} - (op:T->T->T) {op_proper:Proper (equiv==>equiv==>equiv) op} - (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) + Context {T eq op id} {moinoid : @monoid T eq op id} + {scalar : Type} (scToN : scalar -> N) (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 := + Fixpoint nat_iter_op n a : T := match n with - | 0%nat => neutral + | 0%nat => id | S n' => op a (nat_iter_op n' a) end. Lemma nat_iter_op_plus : forall m n a, op (nat_iter_op m a) (nat_iter_op n a) === nat_iter_op (m + n) a. Proof. - induction m; intros; simpl; rewrite ?neutral_l, <-?IHm, ?assoc; reflexivity. + induction m; intros; simpl; rewrite ?left_identity, <-?IHm, ?associative; reflexivity. Qed. Definition N_iter_op n a := match n with - | 0%N => neutral + | 0%N => id | Npos p => Pos.iter_op op p a end. Lemma Pos_iter_op_succ : forall p a, Pos.iter_op op (Pos.succ p) a === op a (Pos.iter_op op p a). Proof. - induction p; intros; simpl; rewrite ?assoc, ?IHp; reflexivity. + induction p; intros; simpl; rewrite ?associative, ?IHp; reflexivity. Qed. Lemma N_iter_op_succ : forall n a, N_iter_op (N.succ n) a === op a (N_iter_op n a). Proof. - destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?neutral_r; reflexivity. + destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?right_identity; reflexivity. Qed. Lemma N_iter_op_is_nat_iter_op : forall n a, N_iter_op n a === nat_iter_op (N.to_nat n) a. @@ -66,7 +61,7 @@ Section IterAssocOp. end. Definition iter_op sc a bound : T := - snd (funexp (test_and_op sc a) (bound, neutral) bound). + snd (funexp (test_and_op sc a) (bound, id) bound). 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. @@ -155,7 +150,7 @@ Section IterAssocOp. 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) -> + (funexp (test_and_op sc a) (bound, id) 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. |