Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoids
  Basics.Equivalences Basics.Decidable Basics.Classes.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Empty Types.Sigma Types.Sum Types.Prod Types.Equiv.
Require Import Spaces.Nat.Core.
Require Import Finite.Fin.

Local Open Scope nat_scope.

Set Universe Minimization ToSet.

Definition FinNat@{} (n : nat) : Type0 := {x : nat | x < n}.

Definition zero_finnat@{} (n : nat) : FinNat n.+1
  := (0; _ : 0 < n.+1).

Definition succ_finnat@{} {n : nat} (u : FinNat n) : FinNat n.+1
  := (u.1.+1; leq_succ u.2).

Definition path_succ_finnat {n : nat} (x : nat) (h : x.+1 < n.+1)
  : succ_finnat (x; leq_pred' h) = (x.+1; h).
n, x: nat
h: x.+1 < n.+1
succ_finnat (x; leq_pred' h) = (x.+1; h)
Proof.
n, x: nat
h: x.+1 < n.+1
succ_finnat (x; leq_pred' h) = (x.+1; h)
  by apply path_sigma_hprop.
Defined.

Definition last_finnat@{} (n : nat) : FinNat n.+1
  := exist (fun x => x < n.+1) n (leq_refl n.+1).

Definition incl_finnat@{} {n : nat} (u : FinNat n) : FinNat n.+1
  := (u.1; leq_trans u.2 (leq_succ_r (leq_refl n))).

Definition finnat_ind@{u} (P : forall n : nat, FinNat n -> Type@{u})
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
  {n : nat} (u : FinNat n)
  : P n u.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
P n u
Proof.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
P n u
  simple_induction n n IHn; intro u.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
u: FinNat 0
P 0 u
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
u: FinNat n.+1
P n.+1 u
  -
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
u: FinNat 0
P 0 u elim (not_lt_zero_r u.1 u.2).
  -
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
u: FinNat n.+1
P n.+1 u destruct u as [x h].
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x < n.+1
P n.+1 (x; h)
    destruct x as [| x].
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
h: 0 < n.+1
P n.+1 (0; h)
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x.+1 < n.+1
P n.+1 (x.+1; h)
    +
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
h: 0 < n.+1
P n.+1 (0; h) nrefine (transport (P n.+1) _ (z _)).
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
h: 0 < n.+1
zero_finnat n = (0; h)
      by apply path_sigma_hprop.
    +
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x.+1 < n.+1
P n.+1 (x.+1; h) refine (transport (P n.+1) (path_succ_finnat _ _) _).
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x.+1 < n.+1
P n.+1 (succ_finnat (x; leq_pred' h))
      apply s.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
IHn: forall u : FinNat n, P n u
x: nat
h: x.+1 < n.+1
P n (x; leq_pred' h) apply IHn.
Defined.

Definition finnat_ind_beta_zero@{u} (P : forall n : nat, FinNat n -> Type@{u})
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n), P n u -> P n.+1 (succ_finnat u))
  (n : nat)
  : finnat_ind P z s (zero_finnat n) = z n.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
finnat_ind P z s (zero_finnat n) = z n
Proof.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
finnat_ind P z s (zero_finnat n) = z n
  snapply (transport2 _ (q:=idpath@{Set})).
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
path_sigma_hprop (zero_finnat n)
  (0; (zero_finnat n).2) 1 = 1
  rapply path_ishprop.
Defined.

Definition finnat_ind_beta_succ@{u} (P : forall n : nat, FinNat n -> Type@{u})
  (z : forall n : nat, P n.+1 (zero_finnat n))
  (s : forall (n : nat) (u : FinNat n),
       P n u -> P n.+1 (succ_finnat u))
  {n : nat} (u : FinNat n)
  : finnat_ind P z s (succ_finnat u) = s n u (finnat_ind P z s u).
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
finnat_ind P z s (succ_finnat u) =
s n u (finnat_ind P z s u)
Proof.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n: nat
u: FinNat n
finnat_ind P z s (succ_finnat u) =
s n u (finnat_ind P z s u)
  destruct u as [u1 u2]; simpl; unfold path_succ_finnat.
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
transport (P n.+1)
  (path_sigma_hprop
     (succ_finnat (u1; leq_pred' (leq_succ u2)))
     (u1.+1; leq_succ u2) 1)
  (s n (u1; leq_pred' (leq_succ u2))
     (finnat_ind P z s (u1; leq_pred' (leq_succ u2)))) =
s n (u1; u2) (finnat_ind P z s (u1; u2))
  destruct (path_ishprop u2 (leq_pred' (leq_succ u2))).
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
transport (P n.+1)
  (path_sigma_hprop (succ_finnat (u1; u2))
     (u1.+1; leq_succ u2) 1)
  (s n (u1; u2) (finnat_ind P z s (u1; u2))) =
s n (u1; u2) (finnat_ind P z s (u1; u2))
  refine (transport2 _ (q:=idpath@{Set}) _ _).
P: forall n : nat, FinNat n -> Type
z: forall n : nat, P n.+1 (zero_finnat n)
s: forall (n : nat) (u : FinNat n),
P n u -> P n.+1 (succ_finnat u)
n, u1: nat
u2: u1 < n
path_sigma_hprop (succ_finnat (u1; u2))
  (u1.+1; leq_succ u2) 1 = 1
  rapply path_ishprop.
Defined.

Definition is_bounded_fin_to_nat@{} {n} (k : Fin n)
  : fin_to_nat k < n.
n: nat
k: Fin n
fin_to_nat k < n
Proof.
n: nat
k: Fin n
fin_to_nat k < n
  induction n as [| n IHn].
k: Fin 0
fin_to_nat k < 0
n: nat
k: Fin n.+1
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat k < n.+1
  -
k: Fin 0
fin_to_nat k < 0 elim k.
  -
n: nat
k: Fin n.+1
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat k < n.+1 destruct k as [k | []].
n: nat
k: Fin n
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inl k) < n.+1
n: nat
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inr tt) < n.+1
    +
n: nat
k: Fin n
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inl k) < n.+1 rapply lt_succ_r. (* Typeclass search finds a different solution, but we want this one. *)
    +
n: nat
IHn: forall k : Fin n, fin_to_nat k < n
fin_to_nat (inr tt) < n.+1 exact _.
Defined.

Definition fin_to_finnat {n} (k : Fin n) : FinNat n
  := (fin_to_nat k; is_bounded_fin_to_nat k).

(** Because the proof of [is_bounded_fin_to_nat] was chosen carefully, we have the following definitional equality. *)
Definition path_fin_to_finnat_fin_incl_incl_finnat_fin_to_finnat {n} (k : Fin n)
  : fin_to_finnat (fin_incl k) = incl_finnat (fin_to_finnat k)
  := idpath.

Fixpoint finnat_to_fin@{} {n : nat} : FinNat n -> Fin n
  := match n with
     | 0 => fun u => Empty_rec (not_lt_zero_r _ u.2)
     | n.+1 => fun u =>
        match u with
        | (0; _) => fin_zero
        | (x.+1; h) => fsucc (finnat_to_fin (x; leq_pred' h))
        end
     end.

Definition path_fin_to_finnat_fsucc@{} {n : nat} (k : Fin n)
  : fin_to_finnat (fsucc k) = succ_finnat (fin_to_finnat k).
n: nat
k: Fin n
fin_to_finnat (fsucc k) =
succ_finnat (fin_to_finnat k)
Proof.
n: nat
k: Fin n
fin_to_finnat (fsucc k) =
succ_finnat (fin_to_finnat k)
  apply path_sigma_hprop.
n: nat
k: Fin n
(fin_to_finnat (fsucc k)).1 =
(succ_finnat (fin_to_finnat k)).1
  apply path_nat_fsucc.
Defined.

Definition path_fin_to_finnat_fin_zero@{} (n : nat)
  : fin_to_finnat (@fin_zero n) = zero_finnat n.
n: nat
fin_to_finnat fin_zero = zero_finnat n
Proof.
n: nat
fin_to_finnat fin_zero = zero_finnat n
  apply path_sigma_hprop.
n: nat
(fin_to_finnat fin_zero).1 = (zero_finnat n).1
  exact path_nat_fin_zero.
Defined.

Definition path_finnat_to_fin_succ@{} {n : nat} (u : FinNat n)
  : finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u).
n: nat
u: FinNat n
finnat_to_fin (succ_finnat u) =
fsucc (finnat_to_fin u)
Proof.
n: nat
u: FinNat n
finnat_to_fin (succ_finnat u) =
fsucc (finnat_to_fin u)
  cbn.
n: nat
u: FinNat n
fsucc
  (finnat_to_fin
     (u.1;
     leq_rec u.1.+2
       (fun (m : nat) (_ : u.1.+2 <= m) =>
        u.1.+1 <= nat_pred m) (leq_refl u.1.+1)
       (fun (m : nat) (_ : u.1.+2 <= m)
          (IHleq : u.1.+1 <= nat_pred m) =>
        leq_trans IHleq pred_leq) n.+1 (leq_succ u.2))) =
fsucc (finnat_to_fin u) do 2 f_ap.
n: nat
u: FinNat n
(u.1;
leq_rec u.1.+2
  (fun (m : nat) (_ : u.1.+2 <= m) =>
   u.1.+1 <= nat_pred m) (leq_refl u.1.+1)
  (fun (m : nat) (_ : u.1.+2 <= m)
     (IHleq : u.1.+1 <= nat_pred m) =>
   leq_trans IHleq pred_leq) n.+1 (leq_succ u.2)) = u by apply path_sigma_hprop.
Defined.

Definition path_finnat_to_fin_incl@{} {n : nat} (u : FinNat n)
  : finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u).
n: nat
u: FinNat n
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
Proof.
n: nat
u: FinNat n
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
  revert n u.
forall (n : nat) (u : FinNat n),
finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
  snapply finnat_ind.
forall n : nat,
(fun (n0 : nat) (u : FinNat n0) =>
 finnat_to_fin (incl_finnat u) =
 fin_incl (finnat_to_fin u)) n.+1 (zero_finnat n)
forall (n : nat) (u : FinNat n),
(fun (n0 : nat) (u0 : FinNat n0) =>
 finnat_to_fin (incl_finnat u0) =
 fin_incl (finnat_to_fin u0)) n u ->
(fun (n0 : nat) (u0 : FinNat n0) =>
 finnat_to_fin (incl_finnat u0) =
 fin_incl (finnat_to_fin u0)) n.+1 (succ_finnat u)
  1: reflexivity.
forall (n : nat) (u : FinNat n),
(fun (n0 : nat) (u0 : FinNat n0) =>
 finnat_to_fin (incl_finnat u0) =
 fin_incl (finnat_to_fin u0)) n u ->
(fun (n0 : nat) (u0 : FinNat n0) =>
 finnat_to_fin (incl_finnat u0) =
 fin_incl (finnat_to_fin u0)) n.+1 (succ_finnat u)
  intros n u; cbn beta; intros p.
n: nat
u: FinNat n
p: finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
finnat_to_fin (incl_finnat (succ_finnat u)) =
fin_incl (finnat_to_fin (succ_finnat u))
  lhs exact (path_finnat_to_fin_succ (incl_finnat u)).
n: nat
u: FinNat n
p: finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
fsucc (finnat_to_fin (incl_finnat u)) =
fin_incl (finnat_to_fin (succ_finnat u))
  lhs exact (ap fsucc p).
n: nat
u: FinNat n
p: finnat_to_fin (incl_finnat u) =
fin_incl (finnat_to_fin u)
fsucc (fin_incl (finnat_to_fin u)) =
fin_incl (finnat_to_fin (succ_finnat u))
  exact (ap fin_incl (path_finnat_to_fin_succ _))^.
Defined.

Definition path_finnat_to_fin_last@{} (n : nat)
  : finnat_to_fin (last_finnat n) = fin_last.
n: nat
finnat_to_fin (last_finnat n) = fin_last
Proof.
n: nat
finnat_to_fin (last_finnat n) = fin_last
  induction n as [| n IHn].
finnat_to_fin (last_finnat 0) = fin_last
n: nat
IHn: finnat_to_fin (last_finnat n) = fin_last
finnat_to_fin (last_finnat n.+1) = fin_last
  -
finnat_to_fin (last_finnat 0) = fin_last reflexivity.
  -
n: nat
IHn: finnat_to_fin (last_finnat n) = fin_last
finnat_to_fin (last_finnat n.+1) = fin_last exact (ap fsucc IHn).
Defined.

Definition path_finnat_to_fin_to_finnat@{} {n : nat} (u : FinNat n)
  : fin_to_finnat (finnat_to_fin u) = u.
n: nat
u: FinNat n
fin_to_finnat (finnat_to_fin u) = u
Proof.
n: nat
u: FinNat n
fin_to_finnat (finnat_to_fin u) = u
  induction n as [| n IHn].
u: FinNat 0
fin_to_finnat (finnat_to_fin u) = u
n: nat
u: FinNat n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
fin_to_finnat (finnat_to_fin u) = u
  -
u: FinNat 0
fin_to_finnat (finnat_to_fin u) = u elim (not_lt_zero_r _ u.2).
  -
n: nat
u: FinNat n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
fin_to_finnat (finnat_to_fin u) = u destruct u as [x h].
n, x: nat
h: x < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
fin_to_finnat (finnat_to_fin (x; h)) = (x; h)
    apply path_sigma_hprop.
n, x: nat
h: x < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x; h))).1 = (x; h).1
    destruct x as [| x].
n: nat
h: 0 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (0; h))).1 = (0; h).1
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x.+1; h))).1 =
(x.+1; h).1
    +
n: nat
h: 0 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (0; h))).1 = (0; h).1 exact (ap pr1 (path_fin_to_finnat_fin_zero n)).
    +
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(fin_to_finnat (finnat_to_fin (x.+1; h))).1 =
(x.+1; h).1 refine ((path_fin_to_finnat_fsucc _)..1 @ _).
n, x: nat
h: x.+1 < n.+1
IHn: forall u : FinNat n, fin_to_finnat (finnat_to_fin u) = u
(succ_finnat
   (fin_to_finnat
      ((fix finnat_to_fin (n : nat) :
            FinNat n -> Fin n :=
          match
            n as n0 return (FinNat n0 -> Fin n0)
          with
          | 0 =>
              fun u : FinNat 0 =>
              Empty_rec (not_lt_zero_r u.1 u.2)
          | n0.+1 =>
              fun u : FinNat n0.+1 =>
              let u0 := u in
              let proj1 := u0.1 in
              let h := u0.2 in
              match
                proj1 as proj2
                return (proj2 < n0.+1 -> Fin n0.+1)
              with
              | 0 => fun _ : 0 < n0.+1 => fin_zero
              | x.+1 =>
                  fun h0 : x.+1 < n0.+1 =>
                  fsucc
                    (finnat_to_fin n0
                       (x; leq_pred' h0))
              end h
          end) n (x; leq_pred' h)))).1 = (x.+1; h).1
      exact (ap S (IHn (x; leq_pred' h))..1).
Defined.

Definition path_fin_to_finnat_to_fin@{} {n : nat} (k : Fin n)
  : finnat_to_fin (fin_to_finnat k) = k.
n: nat
k: Fin n
finnat_to_fin (fin_to_finnat k) = k
Proof.
n: nat
k: Fin n
finnat_to_fin (fin_to_finnat k) = k
  induction n as [| n IHn].
k: Fin 0
finnat_to_fin (fin_to_finnat k) = k
n: nat
k: Fin n.+1
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat k) = k
  -
k: Fin 0
finnat_to_fin (fin_to_finnat k) = k elim k.
  -
n: nat
k: Fin n.+1
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat k) = k destruct k as [k | []].
n: nat
k: Fin n
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inl k)) = inl k
n: nat
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inr tt)) = inr tt
    +
n: nat
k: Fin n
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inl k)) = inl k specialize (IHn k).
n: nat
k: Fin n
IHn: finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inl k)) = inl k
      refine (path_finnat_to_fin_incl (fin_to_finnat k) @ _).
n: nat
k: Fin n
IHn: finnat_to_fin (fin_to_finnat k) = k
fin_incl (finnat_to_fin (fin_to_finnat k)) = inl k
      exact (ap fin_incl IHn).
    +
n: nat
IHn: forall k : Fin n, finnat_to_fin (fin_to_finnat k) = k
finnat_to_fin (fin_to_finnat (inr tt)) = inr tt apply path_finnat_to_fin_last.
Defined.

Definition equiv_fin_finnat@{} (n : nat) : Fin n <~> FinNat n
  := equiv_adjointify fin_to_finnat finnat_to_fin
      path_finnat_to_fin_to_finnat
      path_fin_to_finnat_to_fin.