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).
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).