proposition: Lemma log2_impl : log2_spec n0.
proof: Proof. apply Imperative with state init ok; [ exists (mkstate n0 0 true) | intros a pre; apply while_not with init invar stat_order final a; [ simple induction s; intros state_n0 state_p0 state_b0 i; elim (le_lt_eq_dec 1 state_n0); [ right | left | idtac ] | simple induction s; intros state_n0 state_p0 state_b0; elim state_b0; intros h i; elim (Unshift state_n0); intros m b'; [ elim b'; [ exists (mkstate m (S state_p0) true) | exists (mkstate m (S state_p0) false) ] | exists (mkstate m (S state_p0) false) ] | idtac | idtac | idtac | idtac ] | simple induction a; intros state_n0 state_p0 state_b0; elim state_b0; intro h; exists state_p0 ]. Hint Unfold init: arith. split; auto; split; auto. red in |- *; intros f; inversion f; auto. rewrite <- H0 in a0; simpl in a0. absurd (1 < 1); auto with arith. rewrite <- b; constructor 1. inversion i; auto. cut (one < state_n0). intro n_ge_1. 2: apply not_final with state_p0 true; auto with arith. inversion i. split. left. rewrite two_power_S. rewrite <- mult_assoc; auto with arith. unfold shift in a0. rewrite <- a0; auto. unfold shift in a0. apply quotient_positive with state_n0 two; auto. rewrite mult_comm; exact a0. unfold stat_order, ltof in |- *. apply half_lt. apply lt_trans with one; auto with arith. auto with arith. cut (one < state_n0). intro n_ge_1. 2: apply not_final with state_p0 true; auto with arith. inversion i. split. right. rewrite two_power_S. rewrite <- mult_assoc; auto with arith. rewrite (invar_inv1 state_n0 state_p0); auto. rewrite b. unfold shift in |- *. auto with arith. rewrite two_power_S. rewrite <- mult_assoc. rewrite (invar_inv1 state_n0 state_p0); auto. rewrite b. unfold shift in |- *. apply mult_lt_l. auto with arith. simpl in |- *; auto with arith. case (lt_or_Zero m); auto with arith. intro. absurd (one < state_n0); auto with arith. rewrite b. rewrite H3; simpl in |- *; auto with arith. unfold stat_order, ltof in |- *; apply half_lt. simpl in |- *. apply lt_trans with one; auto with arith. auto with arith. cut (one < state_n0). intro n_ge_1. 2: apply not_final with state_p0 false; auto with arith. inversion i. cut (two_power (S state_p0) * m < n0). intro n0_left'. cut (n0 < two_power (S state_p0) * S m). intro n0_right'. cut (m < state_n0). intro m_little. split. right; auto with arith. case (lt_or_Zero m); auto with arith. intro. absurd (one < state_n0); auto with arith. simpl in b'; elim b'; intros eg; rewrite eg. rewrite H4; simpl in |- *; auto with arith. rewrite H4; simpl in |- *; auto with arith. unfold stat_order, ltof in |- *. simpl in |- *. exact m_little. apply half_lt. apply lt_trans with one; auto with arith. simpl in b'; elim b'; auto with arith. simpl in b'; elim b'; intros eg. apply lt_trans with (two_power state_p0 * S state_n0); auto with arith. rewrite two_power_S. rewrite <- mult_assoc; auto with arith. apply mult_lt_l. auto with arith. rewrite eg. unfold shift in |- *; simpl in |- *; auto with arith. replace (two_power (S state_p0) * S m) with (two_power state_p0 * S state_n0). elim (invar_inv2 state_n0 state_p0); auto with arith. elim H0; auto with arith. rewrite two_power_S. rewrite <- mult_assoc. simpl in |- *. unfold shift in |- *; simpl in |- *. rewrite <- plus_n_Sm. rewrite eg; auto with arith. apply le_lt_trans with (two_power state_p0 * state_n0); auto with arith. simpl in b'; elim b'; intro eg. rewrite eg. rewrite two_power_S. rewrite <- mult_assoc; auto with arith. rewrite eg. rewrite two_power_S. rewrite <- mult_assoc; auto with arith. simple induction s. simple induction state_b0. intros. rewrite (final_inv state_n0 state_p0 true). left. rewrite (invar_inv1 _ _ H0). rewrite (final_inv _ _ _ H). auto with arith. auto with arith. intros. rewrite (final_inv state_n0 state_p0 false). right. elim (invar_inv2 _ _ H0). rewrite (final_inv _ _ _ H). intros. rewrite <- (mult_1_r (two_power state_p0)); auto with arith. elim (invar_inv2 _ _ H0). rewrite (final_inv _ _ _ H). intros. rewrite two_power_S. exact H2. auto with arith. simple induction s. simple induction state_b0. intro. inversion_clear H. elim H1. simpl in |- *; intros. left. rewrite H; simpl in |- *. rewrite <- H0; auto with arith. simpl in H0; rewrite H0; auto with arith. intro. inversion_clear H. elim H1. intros. simpl in H2. discriminate H2. auto with arith. auto with arith. left. inversion h; auto. right. inversion h; split; auto. Qed.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl Euclid shift Compare_dec imperative while two_power log2_spec