fun_pow_id_to_iso.v

Require Import Coq.Arith.Arith.
Open Scope function_scope.

Fixpoint fun_pow {A} (f : A -> A) (n : nat) (x : A) : A
  := match n with
     | O => x
     | S n => f (fun_pow f n x)
     end.

Infix "^" := fun_pow : function_scope.
Infix "∈" := List.In (at level 70) : list_scope.

Lemma fun_pow_assoc {A} (f : A -> A) n
  : forall x, f ((f^n) x) = (f^n) (f x).
Proof.
  induction n as [|n IHn]; cbn; [ reflexivity | ].
  intros; now rewrite IHn.
Qed.

Lemma fun_pow_O {A f} x : (f^0) x = x :> A.
Proof. reflexivity. Qed.

Lemma fun_pow_S {A f} n x
  : (f^S n) x = f ((f^n) x) :> A.
Proof. cbn; now rewrite fun_pow_assoc. Qed.

Lemma fun_pow_S' {A f} n x
  : (f^S n) x = (f^n) (f x) :> A.
Proof. cbn; now rewrite fun_pow_assoc. Qed.

Lemma fun_pow_add {A f} n m x
  : (f^(n+m)) x = (f^n) ((f^m) x) :> A.
Proof. revert m x; induction n; cbn; intros; congruence. Qed.

Lemma fun_pow_add' {A f} n m x
  : (f^(n+m)) x = (f^m) ((f^n) x) :> A.
Proof. now rewrite Nat.add_comm, fun_pow_add. Qed.

Lemma fun_pow_mul {A f} n m x
  : (f^(n*m)) x = ((f^m)^n) x :> A.
Proof. revert m x; induction n; cbn; intros; rewrite ?fun_pow_add; congruence. Qed.

Lemma fun_pow_mul' {A f} n m x
  : (f^(n*m)) x = ((f^n)^m) x :> A.
Proof. now rewrite Nat.mul_comm, fun_pow_mul. Qed.

Lemma fun_pow_id {A f} n x
  : f x = x -> (f^n) x = x :> A.
Proof.
  intro H; induction n; rewrite ?fun_pow_S', ?fun_pow_O, ?H; congruence.
Qed.

Section __.
  Context (A : Type)
          (f : A -> A)
          (n : A -> nat)
          (Hf : forall x, (f^S (n x)) x = x).

  Lemma f_inj : forall x y, f x = f y -> x = y.
  Proof using Hf.
    intros x y Hxy.
    transitivity ((f^(S (n x) * S (n y))) x); [ symmetry | transitivity ((f^(S (n x) * S (n y))) y) ].
    1: rewrite fun_pow_mul'.
    3: rewrite fun_pow_mul.
    1, 3: rewrite fun_pow_id; rewrite ?Hf; reflexivity.
    cbn [Nat.mul Nat.add]; rewrite !fun_pow_S'.
    congruence.
  Qed.

  Definition f_inv (x : A) := (f^n x) x.

  Lemma f_split_surj : forall y, f (f_inv y) = y.
  Proof.
    intro y; transitivity ((f^S (n y)) y); [ | apply Hf ].
    now cbv [f_inv]; rewrite fun_pow_S.
  Qed.

  Lemma f_inv_left : forall x, f_inv (f x) = x.
  Proof.
    intro x; pose proof (f_split_surj (f x)) as H.
    apply f_inj in H; assumption.
  Qed.
End __.