(* Misc arithmetic on natural numbers *)

Module misc Import sector lib_nat_plus_thms trich ;

(* Predicate that says the Rel defines a function on a range of numbers. *)

[ ExistsRelR =
     [Rel : nat -> word -> Prop] [lower,upper:nat]
     {i:nat} (Lt lower i) -> (Lt i upper) -> <w:word> Rel i w ];

[ UniqueRelR =
     [RelA : nat -> word -> Prop][RelB : nat -> word -> Prop] [lower,upper:nat]
     {i:nat} (Lt lower i) -> (Lt i upper) ->
         {w,W : word} (RelA i w) -> (RelB i W) -> Eq w W ];

[ FuncRelR =
     [Rel : nat -> word -> Prop] [lower,upper:nat]
     (ExistsRelR Rel lower upper) # (UniqueRelR Rel Rel lower upper) ];

(********** Some misc lt theorems ************)

Goal {i,j:nat} (not (Eq i zero)) -> (Lt i (suc j)) -> Lt (pred i) j;
intros i j ne lt ;
Refine Lt_resp_pred ;
Refine Eq_subst ? [x:nat] Lt x (suc j);
Immed ;
Refine suc_pred ;
Immed;
Save my_Lt_resp_pred;

Goal {i,j:nat} (Lt i j) -> Lt (pred i) j;
intros i j;
(* The induction is really just a case *)
Induction i;
(* case zero *)
intros lt;
Immed ;
(* case S n *)
intros _ _ lt ;
Refine Lt_trans|(pred (suc x1))|(suc x1)|j;
Refine n_Lt_suc_n;
Immed;
Save Lt_imp_pred_Lt ;

Goal {i,j:nat} (Lt (pred i) j) -> (Lt i j \/ Eq i j);
intros i j;
Induction i ;
(* Case i = 0 *)
intros _ ;
Refine inl ;
Immed ;
intros ii _ lt ;
Refine n_Lt_suc_m_character|(suc ii)|j;
Refine Lt_resp_suc ;
Immed ;
Save Lt_pred_character ;

Goal {i,j:nat} (Lt i j) -> (Lt (pred j) i) -> absurd ;
intros i j lt gt ;
Refine Lt_pred_character ? ? gt ;
Refine not_Lt_Gt i j lt ;
Refine not_Gt_Eq j i lt ;
Save Lt_strong_antisym ;

(* Absurdity lifting using induction absurdity. *)
Inductive [iAbsurd : Prop];

Goal {T:Type} absurd -> T;
intros T nonsense ;
Induction nonsense|iAbsurd ;
Save absurd_lift;