From 1c19d56200c1794a11efaef2d74bb764ed6d52d2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 24 May 2016 12:08:06 -0400 Subject: Remove unfolding, rewrite -> setoid_rewrite Moving the [scalar] argument to the beginning of [iter_op] makes inference of the [Proper] lemmas a bit easier. Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows [setoid_rewrite] to work; since [setoid_rewrite] does more unfolding than [rewrite], we no longer need to unfold things to make the [rewrite] work. --- src/Util/IterAssocOp.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/Util/IterAssocOp.v') diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 5e23bb987..6116312e1 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -5,12 +5,12 @@ 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) - {scalar : Type} (testbit : scalar -> nat -> bool) (scToN : scalar -> N) (testbit_spec : forall x i, testbit x i = N.testbit_nat (scToN x) i). @@ -63,7 +63,7 @@ Section IterAssocOp. | S i' => (i', if testbit sc i' then op a acc2 else acc2) end. - Definition iter_op sc a bound : T := + Definition iter_op sc a bound : T := snd (funexp (test_and_op sc a) (bound, neutral) bound). Definition test_and_op_inv sc a (s : nat * T) := @@ -152,8 +152,8 @@ 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) -> + 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. @@ -183,7 +183,7 @@ Section IterAssocOp. rewrite Nat2N.id. auto. Qed. - + 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. -- cgit v1.2.3