Nat.iter: theory for associative and commutative functions
I am cleaning up unused code in a paper repository and found some Nat.iter
theory for associative and commutative functions. I don't have the time right now to clean this up and turn it into an MR, but before these proofs get lost, here they are:
Lemma Nat_iter_assoc (A : Type) (E : Equiv A) n (f : A -> A -> A) x y :
Equivalence equiv ->
Assoc equiv f ->
Proper ((≡) ==> (≡) ==> (≡)) f ->
Nat.iter n (f x) (f x y) ≡ f (Nat.iter n (f x) x) y.
Proof.
intros.
rewrite -Nat_iter_S_r.
induction n; first done.
simpl in IHn.
by rewrite /= IHn assoc.
Qed.
Global Instance Nat_iter_proper {A : Type} n a : Proper (pointwise_relation A eq ==> eq) (λ f, Nat.iter n f a).
Proof.
clear -A.
intros ??.
intros.
induction n; first done.
by rewrite /= -IHn -H.
Qed.
Lemma Nat_iter_inj n {A : Type} (f : A -> A -> A) x1 a1 x2 a2 :
Assoc eq f ->
Comm eq f ->
f (Nat.iter n (f x1) a1) (Nat.iter n (f x2) a2) =
Nat.iter n (f (f x1 x2)) (f a1 a2).
Proof.
clear.
intros.
induction n; first done.
by rewrite /= -IHn -!assoc (assoc _ x2 _ _) (comm _ x2 (Nat.iter _ _ a1)) -assoc.
Qed.
Lemma Nat_iter_comm (A : Type) (E : Equiv A) n (f : A -> A -> A) x y z :
Equivalence equiv ->
Assoc equiv f ->
Comm equiv f ->
Proper ((≡) ==> (≡) ==> (≡)) f ->
f (Nat.iter n (f x) y) z ≡ f (Nat.iter n (f x) z) y.
Proof.
intros.
induction n; first done.
rewrite /=.
by rewrite /= -assoc IHn.
Qed.
Lemma Nat_iter_assoc_2 (A : Type) (E : Equiv A) n (f : A -> A -> A) x y z :
Equivalence equiv ->
Assoc equiv f ->
Proper ((≡) ==> (≡) ==> (≡)) f ->
Nat.iter n (f (f x y)) (f x z) ≡ f (Nat.iter n (f (f x y)) x) z.
Proof.
intros.
induction n; first done.
by rewrite /= IHn -!assoc.
Qed.
Lemma Nat_iter_swap n {A : Type} {E : Equiv A} (f : A -> A -> A) (x : A) :
Equivalence equiv ->
Assoc equiv f ->
Proper ((≡) ==> (≡) ==> (≡)) f ->
∀ a, Nat.iter (S n) (f x) a ≡ f (Nat.iter n (f x) x) a.
Proof.
clear.
intros.
rewrite -Nat_iter_assoc.
by rewrite -Nat_iter_S_r.
Qed.
These lemmas are by Joshua Yanovski.