(* Pierre Castéran *) Require Import Even. Require Import Arith. Require Import Wf_nat. Require Import Omega. Require Import Epsilon. Require Import Relations. Require Import Recdef. Lemma inh_nat : inhabited nat. Proof inhabits 0. (** * An ideal (partial) half function *) (** * ihalf n is THE p such that p + p = n *) Definition ihalf n := iota inh_nat (fun p => p + p = n). (* numbers of the form 2^p *) Function exp2 (n:nat) {struct n} : nat := match n with 0 => 1 | S p => 2 * (exp2 p) end. Lemma exp2_inj : forall n p, exp2 n = exp2 p -> n = p. Proof. induction n; destruct p;auto. simpl; omega. simpl; omega. simpl; generalize (IHn p);omega. Qed. Lemma exp2_of_plus : forall n p, exp2 (n+p) = exp2 n * exp2 p. Proof. induction n;simpl;auto with arith. intros;rewrite IHn. repeat rewrite mult_plus_distr_r. omega. Qed. (** * log2 n is THE p such that 2^p = n *) Definition log2 (n:nat) := iota inh_nat (fun p => exp2 p = n). (** * A function defined as a (partial) fixpoint *) Definition FLog2 (f : nat -> nat) := fun n => match n with 0 => unspec inh_nat |1 => 0 |p => S (f (ihalf p)) end. (** * log2' is some function which satisfies a fixpoint equation on some set *) Definition log2' := epsilon (inhabits (fun n:nat => n)) (fun f => forall n, n = 1 \/ 0 < n /\ even n -> f n = FLog2 f n). (* more on even-ness *) (** * a boolean test *) Function even_odd (n:nat) {struct n} : bool := match n with 0 => true | 1 => false | S (S p) => even_odd p end. Fixpoint nat_double_rect (P:nat->Type) (P0:P 0) (P1 :P 1) (P2: forall n, P n -> P (S (S n))) (n:nat) {struct n} : P n := match n return P n with 0 => P0 | 1 => P1 | S (S p) => P2 p (nat_double_rect P P0 P1 P2 p) end. Lemma even_ind2 : forall P:nat->Prop, P 0 -> (forall p, even p -> P p -> P (S (S p))) -> forall n, even n -> P n. Proof. intros P H0 HSS. assert (forall n, even n /\ P n \/ odd n /\ P (S n)). induction n. left;split;auto;constructor. case IHn. right; split. constructor. case H;auto. apply HSS. case H;auto. case H;auto. left; split. constructor;firstorder. firstorder. intros n Hn. case (H n). firstorder. destruct 1. case (not_even_and_odd n);firstorder. Qed. Lemma even_odd_ok : forall n, if even_odd n then even n else odd n. Proof. induction n using nat_double_rect. simpl;constructor. simpl; constructor;auto. constructor. simpl. revert IHn; case (even_odd n). repeat constructor;auto. repeat constructor;auto. Qed. Lemma even_ok : forall n, even_odd n = true -> even n. Proof. intro n; generalize (even_odd_ok n). case (even_odd n);intros;try discriminate;auto. Qed. Ltac even_tac := apply even_ok;compute;auto. Goal even 50. even_tac. Qed. (* powers of two *) Inductive is_a_power_of_2 : nat -> Prop := is_a_power_of_2_one : is_a_power_of_2 1 | p2_double : forall n p, n = p + p -> is_a_power_of_2 p -> is_a_power_of_2 n. Lemma zero_not_exp2 : forall n, is_a_power_of_2 n -> n <> 0. Proof. induction 1. discriminate. subst n. omega. Qed. Lemma exp2_positive : forall n, is_a_power_of_2 n -> 0 < n. Proof. intros n H; generalize (zero_not_exp2 _ H). omega. Qed. Lemma is_a_power_of_2_one_or_even : forall n, is_a_power_of_2 n -> n=1 \/ even n. Proof. induction 1;auto. case IHis_a_power_of_2;intro H1. subst p;subst n;right;even_tac. subst n;right. apply even_even_plus;trivial. Qed. Lemma is_a_power_of_2_even : forall n, is_a_power_of_2 n -> n<>1 -> even n. Proof. intro n;generalize (is_a_power_of_2_one_or_even n);firstorder. Qed. Lemma is_a_power_of_2_exists_log2 : forall n, is_a_power_of_2 n -> exists! p, exp2 p = n. Proof. induction 1. exists 0;split. reflexivity. intros;eapply exp2_inj. simpl;auto. case IHis_a_power_of_2;intros p0 Hp0. exists (S p0). split. simpl. destruct Hp0. omega. intros;eapply exp2_inj. subst n. simpl. case Hp0. intros. rewrite H. omega. Qed. Lemma is_a_power_of_2_intro : forall n, is_a_power_of_2 (exp2 n). Proof. intro n; pattern n, (exp2 n). apply exp2_rect. constructor. simpl. intros;rewrite plus_0_r. econstructor 2. reflexivity. auto. Qed. (* A total half function *) Function half (n:nat) {struct n} : nat := match n with 0 => 0 | 1 => 0 | S (S p) => S (half p) end. Eval compute in (half 16). (* the following computation is irrelevant ! *) Eval compute in (half 15). (* A proof by functional induction *) Lemma half_of_even : forall n, even n -> half n + half n = n. Proof. intro n; pattern n, (half n) at 1 2. apply half_rect. simpl;auto. inversion 2. inversion H1. intros. simpl. rewrite <- plus_n_Sm. rewrite H. auto. inversion_clear H0. inversion H1;auto. Qed. Lemma half_power : forall n, even n -> is_a_power_of_2 n -> is_a_power_of_2 (half n). Proof. intros. inversion H0. subst n. inversion H. inversion H2. replace (half n) with p. auto. generalize (half_of_even _ H). intro. omega. Qed. (** the idealized function ihalf is defined on all even numbers *) Lemma ihalf_defined : forall n, even n -> ihalf n + ihalf n = n. Proof. induction 1 using even_ind2. epsilon_e (ihalf 0). intros b (H1,H2);auto. exists 0. split. auto. intros;omega. epsilon_e (ihalf (S (S p))). intros b (H1,H2);auto. exists (S (ihalf p)). split. simpl. rewrite <- plus_n_Sm. auto. generalize IHeven ; generalize (ihalf p). intros;omega. Qed. (* both functions coincide on even numbers ! *) Lemma ihalf_ok : forall n, even n -> ihalf n = half n. Proof. intros n Hn. generalize (ihalf_defined n Hn). generalize (half_of_even n Hn). intros;omega. Qed. Lemma half_28 : ihalf 28 = 14. Proof. rewrite ihalf_ok. reflexivity. even_tac. Qed. Lemma abort : ihalf 15=7. Proof. rewrite ihalf_ok. reflexivity. Abort. (* a technical lemma *) Lemma half_lt : forall n, 0 < n -> half n < n. Proof. intro n. pattern n,(half n). apply half_rect. auto. auto. destruct p. simpl;auto. simpl. case p. auto. intros. omega. Qed. (* a total log2 function *) Function total_log2 (n:nat) {wf lt n} : nat := match n with 0 => 0 | 1 => 0 | p => S(total_log2 (half p)) end. apply lt_wf. induction n. discriminate 1. intros. apply half_lt. auto with arith. Defined. Function opt_log2 (n:nat) {wf lt n} : option nat := match n with | 0 => None | 1 => Some 0 | S (S n1) => if even_odd (S (S n1)) then match (opt_log2 (half (S (S n1)))) with | Some r => Some (S r) | _ => None end else None end. Proof. apply lt_wf. intros n n0 teq n1 teq0 teq1;apply half_lt. auto with *. Defined. Eval compute in opt_log2 64. Eval compute in (opt_log2 80). Eval compute in (total_log2 2). Eval compute in (total_log2 8). Eval compute in (total_log2 24). (* in order to prove log'2 is partially defined, I use total_log2 as a witness *) Lemma log2'_defined : forall n, is_a_power_of_2 n -> log2' n = FLog2 log2' n. Proof. epsilon_e log2'. exists total_log2. unfold FLog2;destruct 1. subst n;reflexivity. decompose [and] H. case_eq n. intro;subst n;inversion H0. intros n0 e;subst n. rewrite total_log2_equation. case_eq n0. auto. intros;subst n0. rewrite ihalf_ok;auto. intros f Hf n;case n. intros. case (zero_not_exp2 _ H);auto. intros. rewrite Hf. auto. generalize H;case n0. auto. intros n1 H1. right. split. auto with arith. apply is_a_power_of_2_even;auto with arith. Qed. Function p2_test (n:nat) {measure (fun n => n)} : bool := match n with 0 => false | 1 => true | p => if even_odd p then p2_test (half p) else false end. intros. apply half_lt. subst n;auto with arith. Defined. Lemma p2_test_ok : forall n, p2_test n = true -> is_a_power_of_2 n. Proof. intro n; pattern n, (p2_test n). apply p2_test_rect. discriminate 2. constructor. intros. assert (half p + half p = p). apply half_of_even. apply even_ok;assumption. rewrite <- H1. econstructor 2. reflexivity. auto. discriminate 4. Qed. Ltac exp2_tac := apply p2_test_ok;reflexivity. Goal is_a_power_of_2 8. Proof. exp2_tac. Qed. Lemma L : log2' 8 = 3. Proof. rewrite log2'_defined;auto;try exp2_tac. simpl; rewrite ihalf_ok ;try even_tac. simpl; rewrite log2'_defined; try exp2_tac. simpl; rewrite ihalf_ok ; try even_tac. simpl; rewrite log2'_defined;try exp2_tac. simpl; rewrite ihalf_ok ; try even_tac. simpl; rewrite log2'_defined;try exp2_tac. reflexivity. Qed. Print L. Lemma total_log2_ok : forall n, is_a_power_of_2 n -> total_log2 n = log2' n. Proof. intro n; pattern n, (total_log2 n);apply total_log2_rect. intros. case (zero_not_exp2 _ H). auto. intros. rewrite log2'_defined. simpl. auto. auto. intros n0 p H; subst n0. case p. contradiction. intro n0;case n0. contradiction. intros. rewrite (log2'_defined _ H0). rewrite H. unfold FLog2. rewrite ihalf_ok. auto. apply is_a_power_of_2_even. auto. red;discriminate. apply half_power. apply is_a_power_of_2_even;auto. auto. Qed. (* An idealized log2 function *) Lemma log2_defined : forall n, is_a_power_of_2 n -> exp2 (log2 n) = n. Proof. intros n H; epsilon_e (log2 n). firstorder. apply is_a_power_of_2_exists_log2;auto. Qed. Lemma exp2_of_log2 : forall n, is_a_power_of_2 n -> exp2 (total_log2 n) = n. Proof. intro n. pattern n, (total_log2 n);apply total_log2_rect. intros. case (zero_not_exp2 _ H). auto. simpl;auto. intros n0 p e; subst n0. case p. contradiction. destruct n0. contradiction. intros. simpl. assert (is_a_power_of_2 (half (S (S n0)))). apply half_power. apply is_a_power_of_2_even. auto. discriminate. auto. generalize (H H1). intro. simpl in H2. repeat rewrite H2. simpl. rewrite plus_0_r. rewrite <- plus_n_Sm. rewrite half_of_even;auto. generalize (is_a_power_of_2_even _ H0). intros. assert (even (S (S n0))). apply H3;discriminate. inversion H4. inversion H6;auto. Qed. Lemma is_a_power_of_two_mult : forall n p, is_a_power_of_2 n -> is_a_power_of_2 p -> is_a_power_of_2 (n*p). Proof. induction 1. simpl;auto. rewrite plus_0_r;auto. subst n. rewrite mult_plus_distr_r. intro;econstructor 2. reflexivity. auto. Qed. Lemma log2_of_mult : forall n p, is_a_power_of_2 n -> is_a_power_of_2 p -> log2 (n*p) = log2 n + log2 p. Proof. intros. epsilon_e (log2 (n*p)). 2:apply is_a_power_of_2_exists_log2;auto. 2:apply is_a_power_of_two_mult;auto. intros b (H1,H2). apply H2. rewrite exp2_of_plus. repeat rewrite log2_defined;auto. Qed. Lemma log2_ok : forall n, is_a_power_of_2 n -> log2 n = total_log2 n. Proof. intros n Hn. epsilon_e (log2 n). destruct 1. 2:apply is_a_power_of_2_exists_log2;auto. generalize ( exp2_of_log2 _ Hn). intros. apply exp2_inj. symmetry;eauto. rewrite H;auto. Qed. Lemma log2_of_double : forall n, is_a_power_of_2 n -> 0 < n -> log2 (2*n) = S (log2 n). Proof. intros. rewrite log2_of_mult;auto. rewrite (log2_ok 2). simpl;auto with arith. exp2_tac. exp2_tac. Qed. Lemma even_ok_R : forall n, even n -> even_odd n = true. Proof. intro n; generalize (even_odd_ok n). case (even_odd n);intros;try discriminate;auto. case (not_even_and_odd _ H0 H). Qed. Lemma opt_log2_is_some : forall n, is_a_power_of_2 n -> exists r, opt_log2 n = Some r. Proof. intro n; functional induction (opt_log2 n). intro. case (zero_not_exp2 _ H);auto. exists 0;auto. exists (S r);auto. intro. case IHo. apply half_power;auto. apply is_a_power_of_2_even; auto. intros. rewrite H0 in y. case y. intro. generalize (is_a_power_of_2_even _ H). intro. assert (even (S (S n1))). apply H0. discriminate. rewrite (even_ok_R _ H1 )in e0. discriminate e0. Qed. Lemma opt_log2_ok : forall n, is_a_power_of_2 n -> log2 n = match opt_log2 n with Some r => r | None => unspec inh_nat end. Proof. intro n; functional induction (opt_log2 n). intro H; case (zero_not_exp2 _ H);auto. intro;rewrite log2_ok. simpl;auto. exp2_tac. generalize IHo e1; case (opt_log2 (half (S (S n1)))). injection 2. intro ; subst n. intro; replace (S (S n1)) with (2* half (S (S n1))). rewrite log2_of_double. rewrite IHo0. auto. apply half_power. apply is_a_power_of_2_even. auto. discriminate. auto. apply half_power;auto. apply is_a_power_of_2_even; auto. simpl;auto with arith. replace (2 * half (S (S n1))) with (half (S (S n1)) + half (S (S n1))). rewrite half_of_even. auto. apply is_a_power_of_2_even;auto. simpl;auto. discriminate 2. intro. case_eq (opt_log2_is_some (half (S (S n1)))). apply half_power;auto. apply is_a_power_of_2_even; auto. intros x Hx. rewrite Hx in y. case y. intro. assert (even (S (S n1))). apply is_a_power_of_2_even;auto. rewrite (even_ok_R _ H0) in e0. discriminate e0. Qed. Goal log2 64 = 6. rewrite opt_log2_ok. compute;trivial. exp2_tac. Qed. (* A relational approach *) Lemma L64: log2 64 = 6. Proof. rewrite log2_ok; [reflexivity | exp2_tac]. Qed. Print L64. Definition L64' : {n:nat |log2 64 = n}. rewrite (log2_ok 64). let r := eval compute in (total_log2 64) in replace (total_log2 64) with r. esplit. eauto. auto. exp2_tac. Defined. Inductive rlog2 : nat -> nat -> Prop := | rlog2_1 : rlog2 1 0 | rlog2_even : forall n q, 0 < n -> even n -> rlog2 (ihalf n) q -> rlog2 n (S q). Lemma rlog2_inv : forall n p, rlog2 n p -> n=1 /\ p= 0 \/ 0 < n /\ even n /\ exists q, rlog2 (ihalf n) q /\ p = S q. Proof. intros n p H; case H. auto. intros n0 q pos ev Hhalf ;right. repeat split;auto. exists q;auto. Qed. Definition rflog2 (n:nat) := iota inh_nat (fun p => rlog2 n p). Lemma rlog2_functional : functional rlog2. Proof. red. induction 1. inversion_clear 1;auto. inversion_clear H1. inversion_clear H. inversion 1. subst n;inversion H0. inversion H5. rewrite (IHrlog2 q0);trivial. Qed. Lemma ihalf_double_rw : forall n, ihalf (n+n) = n. Proof. intro n; epsilon_e (ihalf (n+n)). intros b (Hb,Hb'). apply Hb'. auto. exists n;auto. red. split;auto;intros;omega. Qed. Lemma rlog2_defined : forall n, is_a_power_of_2 n -> exists p, rlog2 n p. induction 1. exists 0. constructor. case IHis_a_power_of_2;intros p0 Hp0. exists (S p0). eright. generalize (zero_not_exp2 _ H0). omega. subst n; case (even_or_odd p). intro;apply even_even_plus;auto. intro;apply odd_even_plus;auto. subst n;rewrite ihalf_double_rw. auto. Qed. Lemma rlog2_fun : forall n, is_a_power_of_2 n -> exists! p, rlog2 n p. Proof. intros n H. ex_unique_intro. apply rlog2_defined;trivial. intros; eapply rlog2_functional;eauto. Qed. Lemma rflog2_1 : rflog2 1 = 0. Proof. epsilon_e (rflog2 1). destruct 1. apply H0. constructor. apply rlog2_fun. exp2_tac. Qed. Lemma not_even_1 : ~ even 1. Proof. red;inversion 1. inversion H1. Qed. Lemma rflog2_even : forall n, 0 < n -> even n -> (exists q, rlog2 (ihalf n) q) -> rflog2 n = S (rflog2 (ihalf n)). Proof. intros n Hn Hn' (q,Hq). epsilon_e (rflog2 n). intros b (H1,H2). epsilon_e (rflog2 (ihalf n)). intros b0 (H3,H4). apply H2. right;auto. exists q. split;auto. intros;eapply rlog2_functional. 2:eexact H. auto. exists (S q). split. right;auto. intros;eapply rlog2_functional. 2:eexact H. right;auto. Qed. Lemma rlog2_of_exp2 : forall n, rlog2 (exp2 n) n. Proof. induction n. simpl. constructor. right. elim n;simpl;auto with arith. case (even_or_odd (exp2 n)). simpl. intro;apply even_even_plus;auto. rewrite plus_0_r;auto. simpl;rewrite plus_0_r. intro;apply odd_even_plus;auto. simpl. rewrite plus_0_r; rewrite ihalf_double_rw. auto. Qed. Lemma rflog2_defined : forall n, rflog2 (exp2 n) = n. Proof. intros. epsilon_e (rflog2 (exp2 n)). intros b (H1,H2). apply H2. apply rlog2_of_exp2. apply rlog2_fun. apply is_a_power_of_2_intro. Qed. Lemma rflog2_ok : forall n, is_a_power_of_2 n -> rflog2 n = log2 n. Proof. intros n Hn; case (is_a_power_of_2_exists_log2 _ Hn). destruct 1. subst . rewrite rflog2_defined. epsilon_e ( log2 (exp2 x)). destruct 1. eauto. exists x;trivial. split;auto. Qed. Lemma total_log2_ok' : forall n, is_a_power_of_2 n -> total_log2 n = rflog2 n. Proof. intro n; pattern n, (total_log2 n);apply total_log2_rect. intros. case (zero_not_exp2 _ H). auto. intros. epsilon_e ( rflog2 1). intros b (H1,H2). symmetry;apply H2. constructor. exists 0. split. constructor. intros;eapply rlog2_functional;eauto. constructor. intros n0 p H; subst n0. case p. contradiction. intro n0;case n0. contradiction. intros. rewrite rflog2_even. rewrite ihalf_ok. rewrite H. auto. apply half_power. apply is_a_power_of_2_even. auto. discriminate. auto. apply is_a_power_of_2_even. auto. discriminate. auto with arith. apply is_a_power_of_2_even. auto. discriminate. apply rlog2_defined. rewrite ihalf_ok. apply half_power. apply is_a_power_of_2_even. auto. discriminate. auto. apply is_a_power_of_2_even. auto. discriminate. Qed. SearchRewrite (rflog2 _). SearchRewrite (log2 _).