blob: 8629ae784b1f99ae1a6f11d2db343b5a2fdbe0c1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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.
|
