Require Import Utf8.

(*====================================================================== *)
(* Bounded nat *)
(* Isomorphic to Fin.t, with constructors consistent with O and S of nat *)

Inductive bn : nat → Set :=
| BO : ∀ n, bn (S n)
| BS : ∀ n, bn n → bn (S n).
Definition BO_ {n} := BO n.
Definition BS_ {n} := BS n.

(* *)

Inductive bnO : Set := .
Inductive bnS n : Set :=
| BO_S : bnS n
| BS_S : bn n → bnS n.
Definition bn_dispatch n :=
  match n with
  | O   => bnO
  | S n => bnS n
  end.
Definition bn_inv {n} (i : bn n) : bn_dispatch n :=
  match i with
  | BO n    => BO_S n
  | BS n i' => BS_S n i'
  end.

Inductive bnOd : bn O → Set := .
Inductive bnSd n : bn (S n) → Set :=
| BO_Sd : bnSd _ BO_
| BS_Sd (i : bn n) : bnSd _ (BS n i).
Definition bn_dispatchd n :=
  match n with
  | O   => bnOd
  | S n => bnSd n
  end.
Definition bn_invd {n} (i : bn n) : bn_dispatchd n i :=
  match i with
  | BO n    => BO_Sd n
  | BS n i' => BS_Sd n i'
  end.

(*=============================================================== *)
(* Additions *)

(* Auxiliary definitions lift_right (resp. lift_left) transforming
   (bn n) (resp. (bn m) into bn (n + m) *)

(* The easiest *)
Fixpoint lift_right {n} (i : bn n) m : bn (n + m) :=
  match i in bn n return bn (n + m) with
  | BO n   => BO (n + m)
  | BS n i => BS (n + m) (lift_right i m)
  end.

(* To define lift_left we need pseudo-constructors for bn (n + S m) *)
(* Warning: defind par recusion on n, important for proofs below. *)
Definition BOm n m : bn (n + S m) :=
  match n with
  | O   => BO m
  | S n => BO (n + S m)
  end.

Definition BSm n m : bn (n + m) → bn (n + S m) :=
  (fix loop n : bn (n + m) → bn (n + S m) :=
     match n return bn (n + m) → bn (n + S m) with
     | O   => λ i, BS m i
     | S n => λ i,
         let i' :=
           match bn_inv i with
           | BO_S _   => BOm n m
           | BS_S _ i => loop n i
           end in
         BS (n + S m) i'
     end
  ) n.

Definition BSm_ {n m} := BSm n m.

Lemma BS_BSm {n m} (i : bn (n + m)) : BS_ (BSm_ i) = BSm (S n) _ (BS_ i).
Proof.
  induction n as [ | n Hn].
  - cbn in *. reflexivity.
  - destruct (bn_invd i) as [ | i]; fold Nat.add in *.
    + cbn. reflexivity.
    + simpl. rewrite Hn. reflexivity.
Qed.

Fixpoint lift_left n {m} (j : bn m) : bn (n + m) :=
  match j in bn m return bn (n + m) with
  | BO m   => BOm n m
  | BS m j => BSm n m (lift_left n j)
  end.

(* We then have 2 symetrical definitions of the addition of
   (i : bn n) and (j : bn m), respectively by recursion on i (on j).
   However the base case BO requires the adaquate lift function, that
   procceds by recursion on the other argument j (respectively i).
   Those definitions are extensionnally equal, and each one can be prefered
   to the other depending on the situation.
   NB : (badd i j) and (badd j i) have non convertible types,
   commutativity of addition on nat is not usable.
 *)

Fixpoint badd1 {n m : nat} (i : bn n) (j : bn m) : bn (n + m) :=
  match i with
  | BO n   => lift_left (S n) j
  | BS n i => BS (n + m) (badd1 i j)
  end.

Fixpoint badd2 {n m : nat} (i : bn n) (j : bn m) : bn (n + m) :=
  match j with
  | BO m => lift_right i (S m)
  | BS m j => BSm n m (badd2 i j)
  end.

Lemma badd_eq n m (i : bn n) (j : bn m) : badd1 i j = badd2 i j.
Proof.
  induction i as [ n | n i Hi].
  - cbn.
    induction j as [m | m j Hj].
    + cbn. reflexivity.
    + cbn [lift_left badd2]. case Hj. reflexivity.
  - cbn. rewrite Hi. clear Hi.
    induction j as [m | m j Hj].
    + cbn. reflexivity.
    + cbn [badd2]. case Hj. apply BS_BSm.
Qed.

(*=============================================================== *)
(* even bounded numbers *)

Inductive even : ∀ {n}, bn n → Prop :=
| E0 n :           even (BO n)
| E2 n (i: bn n) : even i → even (BS_ (BS_ i)).
Definition E0_ {n} := E0 n.
Definition E2_ {n} := E2 n.

(* Let us prove that if (i + j) is even, 
   then (even i) is equivalent to (even j). *)


(* *)
Inductive even_0 n : even (BO n) → Prop :=
| E0_0 : even_0 n (E0 n).

Inductive even_SS {n} (i: bn n) : even (BS_ (BS_ i)) → Prop :=
| E2_SS : ∀ e : even i, even_SS i (E2_ i e).

Definition even_dispatch {n} (i : bn n) : even i → Prop :=
    match i with
    | BO n => even_0 n
    | BS n i => 
      match i with
      | BO n   => λ _, False
      | BS n i => even_SS i
      end
    end.

Definition even_inv {n} {i: bn n} (e : even i) : even_dispatch i e :=
  match e with
  | E0 n     => E0_0 n
  | E2 n i e => E2_SS i e
  end.

(* *)

(* Lemmas on even and pseudo-constructors *) 
Lemma even_BSm_BOm {n m} : even (BSm_ (BOm n m)) → False.
Proof.
  destruct n as [ | [ | n]]; simpl; intro e; destruct (even_inv e).
Qed.

Fixpoint even_BSm n m (i : bn (n + m)) : even (BSm_ (BSm_ i)) → even i.
Proof.
  destruct n as [ | [ | n]].
  - cbn in *. intro e. destruct (even_inv e) as [e]. exact e.
  - destruct (bn_invd i) as [ | i]; fold Nat.add in *; simpl; intro e.
    + constructor 1.
    + destruct (even_inv e) as [e]. exact e.
  - destruct (bn_invd i) as [ | i]. 
    + intro e. constructor 1.
    + fold Nat.add in *. change (BS ?n ?i) with (BS_ i).
      destruct (bn_invd i) as [ | i]; simpl; repeat change (BS ?n ?i) with (BS_ i).
      * intro e.
        destruct (even_inv e) as [e].
        case (even_BSm_BOm e).
      * intro e. destruct (even_inv e) as [e].
        constructor 2. apply even_BSm, e.
Qed.

(* Lemmas en even and lifting functions *) 
Fixpoint even_lift_left n {m} {j: bn m} : even (lift_left n j) → even j.
Proof.
  destruct j as [ m | m j]; simpl.
  - intro e. constructor 1.
  - destruct j as [ m | m j]; simpl.
    + destruct n as [ | [ | n]]; simpl; intro e; destruct (even_inv e).
    + intro e. constructor 2. apply (even_lift_left n).
      apply even_BSm, e.
Qed.

Fixpoint even_lift_right {n} (i: bn n) : ∀ m, even (lift_right i m) → even i.
Proof.
  intros m e.
  destruct i as [ | n i]; simpl in e.
  - constructor 1.
  - destruct i as [ | n i]; simpl in e.
    + destruct (even_inv e).
    + destruct (even_inv e) as [e]. constructor 2. apply (even_lift_right n i m e).
Qed.

(* Expected lemmas on even and addition *)
Lemma even_plus1_left n m (i: bn n) (j: bn m) : even (badd1 i j) → even i → even j.
Proof.
  intros eij ei.
  induction ei as [ | n i ei IHei]; simpl in eij.
  - apply (even_lift_left (S n) eij).
  - destruct (even_inv eij) as [eij]. exact (IHei eij).
Qed.


Lemma even_plus2_right n m (i: bn n) (j: bn m) : even (badd2 i j) → even j → even i.
Proof.
  intros eij ej.
  induction ej as [ m | m j ej IHej]; simpl in eij.
  - exact (even_lift_right _ _ eij).
  - exact (IHej (even_BSm _ _ _ eij)).
Qed.


(* ====================================================================== *)
(* Supplémentary matéril : other definitions for lift_left *)
(* 
The first version proceeds by rewriting, 
that coud be considered as bad taste.
See above remark on commutativity of +.

The second makes explicit the hidden recursion inside plus_n_Sm.

The final version above is a kind of simplification of lift_left_rew_like. *)


Definition bn_n_Sm_rew n m (i : bn (S (n + m))) : bn (n + S m).
Proof. case plus_n_Sm; exact i. Defined.

Fixpoint lift_left_rew n {m} (j : bn m) : bn (n + m) :=
  match j in bn m return bn (n + m) with
  | BO m   => bn_n_Sm_rew n m (BO (n+m))
  | BS m j => bn_n_Sm_rew n m (BS (n+m) (lift_left_rew n j))
  end.

(* With an explicit recursion *)

Definition bn_n_Sm {n m} : bn (S n + m) → bn (n + S m) :=
  (fix loop n :=
    match n return bn (S n + m) → bn (n + S m) with
    | O   => λ i, i
    | S n => λ i,
        match bn_inv i with
        | BO_S _   => BO (n + S m)
        | BS_S _ i => BS (n + S m) (loop n i)
        end
    end) n.

Fixpoint lift_left_rew_like n {m} (j : bn m) : bn (n + m) :=
  match j in bn m return bn (n + m) with
  | BO m   => bn_n_Sm (BO (n + m))
  | BS m j => bn_n_Sm (BS (n + m) (lift_left_rew_like n j))
  end.

(* Remak: we can go back and prove isomorphisms *)
Definition bn_n_Sm_back {n m} : bn (n + S m) → bn (S n + m) :=
  (fix loop n :=
    match n return bn (n + S m) → bn (S n + m) with
    | O   => λ i, i
    | S n => λ i,
        match bn_inv i with
        | BO_S _   => BO (S n + m)
        | BS_S _ i => BS (S n + m) (loop n i)
        end
    end) n.

Lemma bn_n_Sm_iso {n m} (i : bn (S n + m)) : i = bn_n_Sm_back (bn_n_Sm i).
Proof.
  induction n as [ | n Hn].
  - reflexivity.
  - destruct (bn_invd i) as [ | i].
    + reflexivity.
    + fold Nat.add in *.
      change (bn_n_Sm (BS _ ?i)) with (BS _ (bn_n_Sm i)).
      change (@bn_n_Sm_back (S n) m (BS _ ?i')) with (BS _ (bn_n_Sm_back i')).
      case (Hn i). reflexivity.
Qed.

Lemma bn_n_Sm_back_iso {n m} (i : bn (n + S m)) : i = bn_n_Sm (bn_n_Sm_back i).
Proof.
  induction n as [ | n Hn].
  - reflexivity.
  - destruct (bn_invd i) as [ | i].
    + reflexivity.
    + fold Nat.add in *.
      change (@bn_n_Sm_back (S n) m (BS _ ?i)) with (BS _ (bn_n_Sm_back i)).
      change (bn_n_Sm (BS _ ?i)) with (BS _ (bn_n_Sm i)).
      case (Hn i). reflexivity.
Qed.


(* Training on right neutrality of zero *)
Definition bn_n_0 : ∀ {n}, bn n -> bn (n + 0) :=
  fix loop n :=
    match n with
    | O   => λ i, i
    | S n => λ i,
        match bn_inv i with
        | BO_S _   => BO (n + 0)
        | BS_S _ i => BS (n + 0) (loop n i)
        end
    end.

Definition bn_n_0_back : ∀ {n}, bn (n + 0) → bn n :=
  fix loop n :=
    match n with
    | O   => λ i, i
    | S n => λ i,
        match bn_inv i with
        | BO_S _   => BO n
        | BS_S _ i => BS n (loop n i)
        end
    end.

Lemma bn_n_0_iso {n} (i : bn n) : i = bn_n_0_back (bn_n_0 i).
Proof.
  induction n as [ | n Hn]; cbn.
  - reflexivity.
  - destruct (bn_invd i); cbn.
    + reflexivity.
    + case (Hn i). reflexivity.
Qed.

Lemma bn_n_0_back_iso {n} (i : bn (n + 0)) : i = bn_n_0 (bn_n_0_back i).
Proof.
  induction n as [ | n Hn]; cbn.
  - reflexivity.
  - destruct (bn_invd i); cbn.
    + reflexivity.
    + case (Hn i). reflexivity.
Qed.