(* Discrete logarithm (base 10) *) Require Import Zwf. Require Import Recdef. Require Import Zdiv. Require Import Zpower. Require Import Tools. Open Scope Z_scope. Function log10 (n : Z) (*{wf (Zwf 1) n}*){measure Zabs_nat n} : Z := if Zlt_bool n 10 then 0 else 1 + log10 (n / 10). intros n teq;Zbool2Prop. generalize (Z_div_lt n 10);intros. apply Zabs_nat_lt. split. SearchAbout Zdiv. SearchPattern (_ / _ <= _/_). replace 0 with (0/10). apply Z_div_le;auto with zarith;try omega. compute;auto. apply H;auto;omega. Defined. (* Induction on the functions'graph *) Check log10_ind. (* log10_ind : forall P : Z -> Z -> Prop, (forall n : Z, Zlt_bool n 10 = true -> P n 0) -> (forall n : Z, Zlt_bool n 10 = false -> forall q r : Z, Zdiv_eucl n 10 = (q, r) -> P q (log10 q) -> P n (1 + log10 q)) -> forall n : Z, P n (log10 n) *) (* Equation associated to log10 *) Check log10_equation. Goal log10 2 = 0. rewrite log10_equation. simpl. trivial. Qed. Goal log10 103=2. repeat (rewrite log10_equation;simpl). trivial. Qed. SearchAbout Zpower. Require Import Zpow_facts. Check Zpower_pos_pos. Lemma zpower_ge_1 : forall z, 0 <= z -> 1 <= 10 ^z . Proof. intros n Hn. generalize (Zpower_le_monotone 10 0 n);intro H;replace 1 with (10^0);auto. apply H;auto with zarith. Qed. Lemma zpower_ge_10 : forall n, 0 < n -> 10 <= 10 ^ n . Proof. intros n Hn; generalize (Zpower_le_monotone 10 1 n);intro H;replace 10 with (10^1);auto. apply H;auto with zarith. Qed. Lemma div_mult_le : forall a b, 0 <= a -> 0 < b -> a/b * b <= a. Proof. intros a b Ha Hb;generalize (Z_div_mod_eq_full a b). intro H;pattern a at 2; rewrite H;clear H. rewrite Zmult_comm at 1;destruct (Z_mod_lt a b);omega. omega. Qed. Lemma exp10_lt_10 : forall p, 0 <= p -> 10 ^p < 10 -> p = 0. Proof. intros p Hp; destruct (Z_dec 0 p);auto. destruct s. generalize ( zpower_ge_10 p); omega. omega. Qed. Lemma log10_OK : forall n p, 0 <= p -> 10 ^ p <= n < 10^(p+1)-> log10 n = p. intro n . functional induction (log10 n). intros. Zbool2Prop. destruct H0. symmetry;apply exp10_lt_10;auto;try omega. intros. Zbool2Prop. destruct (Z_le_lt_eq_dec _ _ H). assert (H' : 0 <= n / 10). SearchAbout [Zdiv Zle]. replace 0 with (0/10). apply Z_div_le;auto with zarith. compute;auto. generalize (IHz (p-1)). intro H2. assert (0 <= p - 1 ) by auto with zarith. apply H2 in H1; try omega. replace p with (p-1+1) in H0;try omega. do 2 rewrite Zpower_exp in H0;auto;try omega. replace (10 ^1) with 10 in H0;auto;try omega. destruct H0;split. assert (10 > 0) by auto with zarith. generalize (Z_div_le _ _ _ H4 H0);auto with zarith;intro. rewrite Z_div_mult_full in H5;auto with zarith. assert (10 > 0) by auto with zarith. assert (n/10 <= 10 ^(p-1+1)). assert (n <= 10 ^ (p - 1 + 1) * 10). auto with zarith. generalize (Z_div_le _ _ _ H4 H5). intros. rewrite Z_div_mult_full in H6;auto. omega. destruct (Z_le_lt_eq_dec _ _ H5);auto. assert (n/10 * 10 <= n). apply div_mult_le;try omega. rewrite e0 in H6;try omega. subst p. simpl in H0. unfold Zpower_pos in H0;simpl in H0. omega. Qed. Eval simpl in log10 67. Extraction "log10.ml" log10.