diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-16 13:05:41 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-16 19:00:06 -0400 |
| commit | c82fc1e10da10b5e7f83d9bed8db1dd931e41930 (patch) | |
| tree | 2b8164bed7df617cdc57008d7c03cdd66f964c55 | |
| parent | e51fb9ecd03fb1ce14870b40312d7259da0c4776 (diff) | |
IterAssocOp: parameters before arguments
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 2 | ||||
| -rw-r--r-- | src/Util/IterAssocOp.v | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index fa95a29c1..83de8a4fd 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -120,7 +120,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 bound y z) === @iter_op _ op' (proj x) _ testbit bound y (proj z). Proof. unfold iter_op. lazymatch goal with diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 8d39c8275..1d553bd55 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -60,7 +60,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 bound sc a : T := snd (funexp (test_and_op sc a) (bound, id) bound). Definition test_and_op_inv sc a (s : nat * T) := @@ -141,7 +141,7 @@ Section IterAssocOp. fst (funexp (test_and_op n a) (x, acc) y) === x - y. Proof. induction y; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity. - destruct (funexp (test_and_op n a) (x, acc) y) as [i acc']. + match goal with |- context[funexp ?a ?b ?c] => destruct (funexp a b c) as [i acc'] end. simpl in IHy. unfold test_and_op. destruct i; rewrite Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity. @@ -151,7 +151,7 @@ Section IterAssocOp. N.size_nat (scToN sc) <= bound -> test_and_op_inv sc a (funexp (test_and_op sc a) (bound, id) bound) -> - iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a. + iter_op bound sc a === 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. @@ -182,7 +182,7 @@ Section IterAssocOp. 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. + iter_op bound sc a === nat_iter_op (N.to_nat (scToN sc)) a. Proof. intros. apply iter_op_termination; auto. |