Library Beroal.NatBound

Require Coq.Arith.Le.
Require Coq.Arith.Plus.
Definition nat_bound := fix rec (n : nat)
        := match n with
        | O => Empty_set : Type
        | S p => option (rec p)
        end.

Definition bound2nat := fix rec (b:nat) : nat_bound b -> nat
:= match b as b0 return nat_bound b0 -> nat with
        | O => fun e => match e with end
        | S pb => fun n => match n with
                | None => 0
                | Some pn => S (rec pb pn)
                end
        end.

Definition nat_bound_eq b0 (n0 : nat_bound b0) b1 (n1 : nat_bound b1)
        := bound2nat _ n0 = bound2nat _ n1.

Definition max_dec : forall b (n : nat_bound (S b)),
        { n0 : nat_bound b | nat_bound_eq _ n _ n0 } + {b = bound2nat _ n}.

Definition bound2nat_lt := fix rec (b:nat)
        : nat_bound b -> sig (fun n:nat => n<b)
:= match b as b0 return nat_bound b0 -> sig (fun n:nat => n<b0) with
        | O => fun e => match e with end
        | S p => fun nb => match nb with
                | None => exist _ 0
                        (Coq.Arith.Le.le_n_S _ _ (Coq.Arith.Le.le_O_n _))
                | Some pb => match rec p pb with exist n lt0
                        => exist _ (S n) (Coq.Arith.Le.le_n_S _ _ lt0) end
                end
        end.
Implicit Arguments bound2nat_lt [b].

Definition nat2bound := fix rec (b:nat) n {struct b}
        : n<b -> nat_bound b
:= match b as b0 return n<b0 -> nat_bound b0 with
        | O => fun lt0 => match Coq.Arith.Le.le_Sn_O _ lt0 with end
        | S pb => match n as n0 return n0 < S pb -> nat_bound (S pb) with
                | O => fun _ => None
                | S pn => fun lt0
                        => Some (rec pb pn (Coq.Arith.Le.le_S_n _ _ lt0))
                end
        end.

Implicit Arguments nat2bound [].

Definition proof_irrelevance (b n : nat) (lt0 lt1 : n<b)
        : nat2bound b n lt0 = nat2bound b n lt1.

Definition nat2bound_sig := fun b (s:sig (fun n:nat => n<b))
        => nat2bound b (proj1_sig s) (proj2_sig s).
Implicit Arguments nat2bound_sig [].

Definition nat_bound_iso0 : forall b (nb:nat_bound b),
        nb = nat2bound_sig b (bound2nat_lt nb).

Section list.
Require Import Coq.Lists.List.
Variable e : Type.
Definition list_ix := fix rec (xs : list e) : Type
        := match xs with
        | nil => Empty_set
        | x :: xss => option (rec xss)
        end.

Definition fnozsm (xs : list e) : list_ix xs = nat_bound (length xs).

End list.

Eval compute in nat_bound 2.
Eval compute in None : nat_bound 2.
Eval compute in (Some None) : nat_bound 2.

Eval compute in proj1_sig (bound2nat_lt (None : nat_bound 2)).
Eval compute in proj1_sig (bound2nat_lt ((Some None) : nat_bound 2)).

Eval compute in (nat2bound _ _ (Coq.Arith.Plus.le_plus_l _ _:0<2)).
Eval compute in (nat2bound _ _ (Coq.Arith.Plus.le_plus_l _ _:1<2)).

Inductive nat_in_type (n:nat):Prop := nat_in_type_intro.
Definition minus0 := fun (n m:nat) (p:nat_in_type (n+m)) => m.
Implicit Arguments minus0 [m].
Eval compute in minus0 3 (nat_in_type_intro 7).
Notation "n -: k" := (minus0 k (nat_in_type_intro n))
        (at level 50, left associativity).
Eval compute in (7 -: 3).