blob: 1f69b04d28f18be935264830848afcfb44d00e15 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
Local Open Scope nat_scope.
Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1.
Proof.
intros.
assert (b = 1 * b) by omega.
rewrite H0 at 1.
rewrite <- Nat.div_add by auto.
reflexivity.
Qed.
Lemma divide2_1mod4_nat : forall c x, c = x / 4 -> x mod 4 = 1 -> exists y, 2 * y = (x / 2).
Proof.
assert (4 <> 0) as ne40 by omega.
induction c; intros; pose proof (div_mod x 4 ne40); rewrite <- H in H1. {
rewrite H0 in H1.
simpl in H1.
rewrite H1.
exists 0; auto.
} {
rewrite mult_succ_r in H1.
assert (4 <= x) as le4x by (apply Nat.div_str_pos_iff; omega).
rewrite <- Nat.add_1_r in H.
replace x with ((x - 4) + 4) in H by omega.
rewrite div_minus in H by auto.
apply Nat.add_cancel_r in H.
replace x with ((x - 4) + (1 * 4)) in H0 by omega.
rewrite Nat.mod_add in H0 by auto.
pose proof (IHc _ H H0).
destruct H2.
exists (x0 + 1).
rewrite <- (Nat.sub_add 4 x) in H1 at 1 by auto.
replace (4 * c + 4 + x mod 4) with (4 * c + x mod 4 + 4) in H1 by omega.
apply Nat.add_cancel_r in H1.
replace (2 * (x0 + 1)) with (2 * x0 + 2)
by (rewrite Nat.mul_add_distr_l; auto).
rewrite H2.
rewrite <- Nat.div_add by omega.
f_equal.
simpl.
apply Nat.sub_add; auto.
}
Qed.
Lemma Nat2N_inj_lt : forall n m, (N.of_nat n < N.of_nat m)%N <-> n < m.
Proof.
split; intros. {
rewrite nat_compare_lt.
rewrite Nnat.Nat2N.inj_compare.
rewrite N.compare_lt_iff; auto.
} {
rewrite <- N.compare_lt_iff.
rewrite <- Nnat.Nat2N.inj_compare.
rewrite <- nat_compare_lt; auto.
}
Qed.
Lemma beq_nat_eq_nat_dec {R} (x y : nat) (a b : R)
: (if EqNat.beq_nat x y then a else b) = (if eq_nat_dec x y then a else b).
Proof.
destruct (eq_nat_dec x y) as [H|H];
[ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity
| rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ].
Qed.
|
