From ecf1d8a89e84a1f80f0c0cc6e4ad9c68465965ab Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 23 Oct 2016 16:06:14 -0400 Subject: Prove an admitted NatUtil lemma --- src/Util/NatUtil.v | 42 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) (limited to 'src/Util/NatUtil.v') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index ea9a5653e..51a0bb407 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -306,5 +306,45 @@ Lemma min_idempotent_S_r x : min x (S x) = x. Proof. omega *. Qed. Hint Rewrite min_idempotent_S_r : natsimplify. +Lemma mod_pow_same b e : b <> 0 -> e <> 0 -> b^e mod b = 0. +Proof. + intros; destruct e as [|e]; [ omega | simpl ]. + rewrite mul_comm, mod_mul by omega; omega. +Qed. + Lemma setbit_high : forall x i, (x < 2^i -> setbit x i = x + 2^i)%nat. -Admitted. \ No newline at end of file +Proof. + intros x i H; apply bits_inj; intro n. + rewrite setbit_eqb. + destruct (i =? n) eqn:H'; simpl. + { apply beq_nat_true in H'; subst. + symmetry; apply testbit_true. + rewrite div_minus, div_small by omega. + reflexivity. } + { assert (H'' : (((x + 2 ^ i) / 2 ^ n) mod 2) = ((x / 2 ^ n) mod 2)). + { assert (2^(i-n) <> 0) by auto with arith. + assert (2^(i-n) <> 0) by omega. + destruct (lt_eq_lt_dec i n) as [ [?|?] | ? ]; [ | subst; rewrite <- beq_nat_refl in H'; congruence | ]. + { assert (i <= n - 1) by omega. + assert (2^i <= 2^n) by auto using pow_le_mono_r with arith. + assert (2^i <= 2^(n - 1)) by auto using pow_le_mono_r with arith. + assert (2^(n-1) <> 0) by auto with arith. + assert (2^(n-1) + 2^(n-1) = 2^n) + by (transitivity (2^(S (n - 1))); [ simpl; omega | apply f_equal; omega ]). + assert ((2^(n - 1) - 1) + (2^(n - 1)) < 2^n) by omega. + rewrite !div_small; try omega. } + { replace (2^i) with (2^(i - n) * 2^n) + by (rewrite <- pow_add_r, ?le_plus_minus_r, ?sub_add by omega; omega). + rewrite div_add by auto with arith. + rewrite <- add_mod_idemp_r, mod_pow_same, add_0_r by omega. + reflexivity. } } + { match goal with + | [ |- ?x = ?y ] + => destruct x eqn:H0; destruct y eqn:H1; try reflexivity; + try apply testbit_true in H0; + try apply testbit_true in H1; + first [ rewrite <- H0; clear H0 | rewrite <- H1; clear H1 ]; + first [ symmetry; apply testbit_true | apply testbit_true ] + end; + rewrite H'' in *; assumption. } } +Qed. -- cgit v1.2.3