From c3c409f8fb014273fb8049aeb8b171390f18022f Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 26 Feb 2016 15:46:47 -0500 Subject: generic binary exponentiation correctness proof in 3 one-liners --- src/Util/IterAssocOp.v | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 src/Util/IterAssocOp.v (limited to 'src/Util/IterAssocOp.v') diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v new file mode 100644 index 000000000..8629ae784 --- /dev/null +++ b/src/Util/IterAssocOp.v @@ -0,0 +1,39 @@ +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. +Require Import NArith BinPosDef. +Local Open Scope equiv_scope. + +Generalizable All Variables. +Section IterAssocOp. + Context `{Equivalence T} + (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_neutral : forall a, op a neutral === a). + Existing Instance op_proper. + + Fixpoint nat_iter_op n a := + match n with + | 0%nat => neutral + | S n' => op a (nat_iter_op n' a) + end. + + Definition N_iter_op n a := + match n with + | 0%N => neutral + | 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. + 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_neutral; 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. + Proof. + induction n using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity. + Qed. +End IterAssocOp. \ No newline at end of file -- cgit v1.2.3