(* 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) -> 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;