Module BinRec
Require Import Coqlib.
Binary induction:
Lemma even_or_odd :
forall x,
exists a,
x = 2 *
a \/
x = 2 *
a + 1.
Proof.
Lemma binrecN :
forall P : (
Z ->
Prop),
P 0 ->
(
forall z,
P z ->
P (2*
z)) ->
(
forall z,
P z ->
P (2*
z+1)) ->
(
forall z, 0 <=
z ->
P z).
Proof.
intros P H0 Hr1 Hr2 z Hpos.
apply Zlt_0_ind;
auto.
intros x Hind Hposx.
destruct (
zeq x 0).
-
subst.
auto.
-
pose proof even_or_odd x.
destruct H as [
a [
H |
H]].
+
rewrite H.
apply Hr1.
apply Hind.
omega.
+
rewrite H.
apply Hr2.
apply Hind.
omega.
Qed.
Lemma binrecZ :
forall P : (
Z ->
Prop),
P 0 ->
P (-1) ->
(
forall z,
P z ->
P (2*
z)) ->
(
forall z,
P z ->
P (2*
z+1)) ->
(
forall z,
P z).
Proof.
intros P H0 Hm1 Hr1 Hr2 z.
destruct (
zlt z 0).
-
remember (
fun n =>
P (-
n-1))
as Q.
assert(
P z =
Q (-
z-1)).
{
rewrite HeqQ.
f_equal.
omega. }
rewrite H.
apply binrecN;
try rewrite HeqQ;
auto.
+
intros z0.
replace (- (2 *
z0) - 1)
with (2 * (-
z0 - 1) + 1)
by omega.
auto.
+
intros z0.
replace (- (2 *
z0 + 1) - 1)
with (2 * (-
z0 - 1))
by omega.
auto.
+
omega.
-
apply binrecN;
auto.
omega.
Qed.
Lemma binrecZZ :
forall P : (
Z ->
Z ->
Prop),
P 0 0 ->
P 0 (-1) ->
P (-1) 0 ->
P (-1) (-1) ->
(
forall x y,
P x y ->
P (2*
x) (2*
y)) ->
(
forall x y,
P x y ->
P (2*
x) (2*
y+1)) ->
(
forall x y,
P x y ->
P (2*
x+1) (2*
y)) ->
(
forall x y,
P x y ->
P (2*
x+1) (2*
y+1)) ->
(
forall x y,
P x y).
Proof.
intros P H00 H0m1 Hm10 Hm1m1.
intros Hr00 Hr01 Hr10 Hr11.
remember (
fun n =>
forall x y, -1-
n <=
x <=
n -> -1-
n <=
y <=
n ->
P x y)
as Q.
assert (
H:
forall n, 0 <=
n ->
Q n).
{
apply binrecN;
rewrite HeqQ.
-
intros x y Hx Hy.
assert (
H: (
x = 0 \/
x = -1) /\ (
y = 0 \/
y = -1))
by omega.
clear Hx Hy.
destruct H as [[
Hx |
Hx] [
Hy |
Hy]];
subst;
auto.
-
intros n Hind.
intros x y.
rewrite (
Zdiv2_odd_eqn x).
rewrite (
Zdiv2_odd_eqn y).
intros Hx Hy.
destruct (
Z.odd x);
destruct (
Z.odd y);
simpl;
try rewrite !
Z.add_0_r.
+
apply Hr11.
apply Hind;
omega.
+
apply Hr10.
apply Hind;
omega.
+
apply Hr01.
apply Hind;
omega.
+
apply Hr00.
apply Hind;
omega.
-
intros n Hind.
intros x y.
rewrite (
Zdiv2_odd_eqn x).
rewrite (
Zdiv2_odd_eqn y).
intros Hx Hy.
destruct (
Z.odd x);
destruct (
Z.odd y);
simpl;
try rewrite !
Z.add_0_r.
+
apply Hr11.
apply Hind;
omega.
+
apply Hr10.
apply Hind;
omega.
+
apply Hr01.
apply Hind;
omega.
+
apply Hr00.
apply Hind;
omega.
}
rewrite HeqQ in H.
intros x y.
pose proof Z.abs_nonneg x as Habsx.
pose proof Z.abs_nonneg y as Habsy.
pose proof Z.abs_le x (
Z.abs x).
pose proof Z.abs_le y (
Z.abs y).
apply H with (
Z.abs x +
Z.abs y);
omega.
Qed.
Lemma binrecZZ_short :
forall P : (
Z ->
Z ->
Prop),
(
forall (
xb yb:
bool),
P (-
Z.b2z xb) (-
Z.b2z yb)) ->
(
forall (
xb yb:
bool) (
x y:
Z),
P x y ->
P (2*
x +
Z.b2z xb) (2*
y +
Z.b2z yb)) ->
(
forall x y,
P x y).
Proof.