Set Implicit Arguments.
Require Import FinFun.
From Undecidability.HOU Require Import std.decidable.

Inductive diag: nat -> nat -> Type :=
  | diagB: diag 0 0
  | diagC: forall m, diag 0 m -> diag (S m) 0
  | diagS: forall n m, diag (S n) m -> diag n (S m).

Fixpoint diagStepR m n (d: diag m n) : diag m (S n) :=
  match d with
  | diagB => diagS (diagC diagB)
  | diagC H => diagS (diagC (diagStepR H))
  | diagS H => diagS (diagStepR H)
  end.

Fixpoint diagStepL m n (d: diag m n) : diag (S m) n :=
  match d with
  | diagB => diagC diagB
  | diagC H => diagC (diagS (diagStepL H))
  | diagS H => diagS (diagStepL H)
  end.

Fixpoint diagZero (a: nat) : diag 0 a :=
  match a with
  | 0 => diagB
  | S a => diagStepR (diagZero a)
  end.

Fixpoint diagId m n: diag m n :=
  match m with
  | O => diagZero n
  | S m => diagStepL (diagId m n)
  end.

Definition I__P (p: nat * nat) :=
  let (m, n) := p in
  diag_rect (fun _ _ _ => nat) 0 (fun _ _ => S) (fun _ _ _ => S) (diagId m n): nat.

Fixpoint R__P (n: nat) : nat * nat :=
  match n with
    | 0 => (0,0)
    | S n => match R__P n with
            | (0, b) => (S b, 0)
            | (S a, b) => (a, S b)
      end
   end.

Lemma R__P_I__P p: R__P (I__P p) = p.
Proof.
  unfold I__P; destruct p as [m n]; induction (diagId m n); cbn.
  - reflexivity.
  - now rewrite IHd.
  - now rewrite IHd.
Qed.

Lemma R__P_injective n m: R__P n = R__P m -> n = m.
Proof.
  induction n in m |-*; destruct m; cbn; eauto.
  1: destruct (R__P m) as [[] b]; discriminate.
  1: destruct (R__P n) as [[] b]; discriminate.
  destruct (R__P n) as [[|k] p] eqn: H1, (R__P m) as [[|k'] p'] eqn: H2.
  all: injection 1; intros; subst.
  all: erewrite IHn; eauto.
  all: discriminate.
Qed.

Lemma I__P_R__P n: I__P (R__P n) = n.
Proof.
  eapply R__P_injective; now rewrite R__P_I__P.
Qed.

Require Import Arith Lia Nat Arith.Div2.

Definition I__S (s: nat + nat) :=
  match s with
  | inl n => double n
  | inr n => S (double n)
  end.

Definition R__S (n: nat) :=
  if even n then inl (div2 n) else inr (div2 n).

Lemma I__S_R__S n: I__S (R__S n) = n.
Proof.
  unfold I__S, R__S.
  destruct Nat.even eqn: H1.
  - symmetry. eapply even_double.
    now eapply Even.even_equiv, Nat.even_spec.
  - symmetry. eapply odd_double; eauto.
    eapply Even.odd_equiv, Nat.odd_spec.
    unfold odd; rewrite H1; eauto.
Qed.

Lemma R__S_I__S s: (R__S (I__S s)) = s.
Proof.
  unfold I__S, R__S.
  destruct s.
  - specialize (Nat.even_spec (Nat.double n)) as [_ H].
    rewrite H, Nat.double_twice, Nat.div2_double; eauto.
    eapply Nat.even_spec.
    unfold Nat.double.
    rewrite Nat.even_add.
    destruct (Nat.even n); reflexivity.
  - specialize (Nat.even_spec (Nat.double n)) as [_ H].
    rewrite Nat.even_succ, <-Nat.negb_even.
    rewrite H; cbn [negb].
    rewrite Nat.double_twice, Nat.div2_succ_double; eauto.
    eapply Nat.even_spec; unfold Nat.double;
      rewrite ?Nat.even_add; destruct (Nat.even n); reflexivity.
Qed.

Lemma injective_I__S : Injective I__S.
Proof.
  intros s s' H % (f_equal R__S). now rewrite !R__S_I__S in H.
Qed.

Lemma injective_I__P : Injective I__P.
Proof.
  intros s s' H % (f_equal R__P). now rewrite !R__P_I__P in H.
Qed.

Arguments I__P p : simpl never.
Arguments R__P n : simpl never.
Arguments I__S s : simpl never.
Arguments R__S n : simpl never.