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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import ZArithRing.
Require Import ZArith_base.
Require Export Omega.
Require Import Wf_nat.
Local Open Scope Z_scope.
(**********************************************************************)
(** About parity *)
Notation two_or_two_plus_one := Z_modulo_2 (only parsing).
(**********************************************************************)
(** The biggest power of 2 that is stricly less than [a]
Easy to compute: replace all "1" of the binary representation by
"0", except the first "1" (or the first one :-) *)
Fixpoint floor_pos (a:positive) : positive :=
match a with
| xH => 1%positive
| xO a' => xO (floor_pos a')
| xI b' => xO (floor_pos b')
end.
Definition floor (a:positive) := Zpos (floor_pos a).
Lemma floor_gt0 : forall p:positive, floor p > 0.
Proof. reflexivity. Qed.
Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p.
Proof.
unfold floor. induction p; simpl.
- rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. omega.
- rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. omega.
- omega.
Qed.
(**********************************************************************)
(** Two more induction principles over [Z]. *)
Theorem Z_lt_abs_rec :
forall P:Z -> Set,
(forall n:Z, (forall m:Z, Z.abs m < Z.abs n -> P m) -> P n) ->
forall n:Z, P n.
Proof.
intros P HP p.
set (Q := fun z => 0 <= z -> P z * P (- z)).
enough (H:Q (Z.abs p)) by
(destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
apply (Z_lt_rec Q); auto with zarith.
subst Q; intros x H.
split; apply HP.
- rewrite Z.abs_eq; auto; intros.
destruct (H (Z.abs m)); auto with zarith.
destruct (Zabs_dec m) as [-> | ->]; trivial.
- rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
destruct (H (Z.abs m)); auto with zarith.
destruct (Zabs_dec m) as [-> | ->]; trivial.
Qed.
Theorem Z_lt_abs_induction :
forall P:Z -> Prop,
(forall n:Z, (forall m:Z, Z.abs m < Z.abs n -> P m) -> P n) ->
forall n:Z, P n.
Proof.
intros P HP p.
set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *.
enough (Q (Z.abs p)) by
(destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
apply (Z_lt_induction Q); auto with zarith.
subst Q; intros.
split; apply HP.
- rewrite Z.abs_eq; auto; intros.
elim (H (Z.abs m)); intros; auto with zarith.
elim (Zabs_dec m); intro eq; rewrite eq; trivial.
- rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
destruct (H (Z.abs m)); auto with zarith.
destruct (Zabs_dec m) as [-> | ->]; trivial.
Qed.
(** To do case analysis over the sign of [z] *)
Lemma Zcase_sign :
forall (n:Z) (P:Prop), (n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P.
Proof.
intros x P Hzero Hpos Hneg.
destruct x; [apply Hzero|apply Hpos|apply Hneg]; easy.
Qed.
Lemma sqr_pos n : n * n >= 0.
Proof.
Z.swap_greater. apply Z.square_nonneg.
Qed.
(**********************************************************************)
(** A list length in Z, tail recursive. *)
Require Import List.
Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z :=
match l with
| nil => acc
| _ :: l => Zlength_aux (Z.succ acc) A l
end.
Definition Zlength := Zlength_aux 0.
Arguments Zlength [A] l.
Section Zlength_properties.
Variable A : Type.
Implicit Type l : list A.
Lemma Zlength_correct l : Zlength l = Z.of_nat (length l).
Proof.
assert (H : forall l acc, Zlength_aux acc A l = acc + Z.of_nat (length l)).
clear l. induction l.
auto with zarith.
intros. simpl length; simpl Zlength_aux.
rewrite IHl, Nat2Z.inj_succ; auto with zarith.
unfold Zlength. now rewrite H.
Qed.
Lemma Zlength_nil : Zlength (A:=A) nil = 0.
Proof. reflexivity. Qed.
Lemma Zlength_cons (x:A) l : Zlength (x :: l) = Z.succ (Zlength l).
Proof.
intros. now rewrite !Zlength_correct, <- Nat2Z.inj_succ.
Qed.
Lemma Zlength_nil_inv l : Zlength l = 0 -> l = nil.
Proof.
rewrite Zlength_correct.
destruct l as [|x l]; auto.
now rewrite <- Nat2Z.inj_0, Nat2Z.inj_iff.
Qed.
End Zlength_properties.
Arguments Zlength_correct [A] l.
Arguments Zlength_cons [A] x l.
Arguments Zlength_nil_inv [A] l _.
|
