(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2011-2018 Sylvie Boldo
#<br />#
Copyright (C) 2011-2018 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

Require Import ZArith Omega.
Require Import Zquot.
Section Zmissing.
Proof.
intros.
omega.
Qed.
Proof.
intros x y Hxy.
apply Zplus_le_reg_r with (-x - y)%Z.
ring_simplify.
easy.
Qed.
Proof.
intros.
red.
intros.
subst.
intuition.
Qed.
Proof.
intros x y H Hn.
apply Z.lt_irrefl with x.
rewrite Hn at 1.
easy.
Qed.
End Zmissing.
Section Proof_Irrelevance.
Scheme eq_dep_elim := Induction for eq Sort Type.
Definition eqbool_dep P (h1 : P true) b :=
  match b return P b -> Prop with
  | true => fun (h2 : P true) => h1 = h2
  | false => fun (h2 : P false) => False
  end.
Proof.
Admitted.
Proof.
assert (forall (h : true = true), refl_equal true = h).
{
apply (eq_dep_elim bool true (eqbool_dep _ _) (refl_equal _)).
}
{
intros b.
case b.
{
intros h1 h2.
rewrite <- (H h1).
easy.
}
{
intros h.
discriminate h.
}
}
Qed.
End Proof_Irrelevance.
Section Even_Odd.
Proof.
Admitted.
Proof.
intros [|[n|n|]|[n|n|]].
{
exists Z0.
easy.
}
{
exists (Zpos n).
easy.
}
{
exists (Zpos n).
easy.
}
{
exists Z0.
easy.
}
{
exists (Zneg n - 1)%Z.
change (2 * Zneg n - 1 = 2 * (Zneg n - 1) + 1)%Z.
ring.
}
{
exists (Zneg n).
easy.
}
{
exists (-1)%Z.
easy.
}
Qed.
End Even_Odd.
Section Zpower.
Proof.
induction n.
destruct k1.
destruct k2.
intros.
eauto.
intuition.
intros.
eauto.
destruct k2.
intros.
simpl.
ring.
simpl.
intuition.
intros.
easy.
intros.
easy.
destruct k1.
destruct k2.
intros.
easy.
intuition.
intros.
easy.
destruct k2.
intros.
simpl.
ring.
simpl.
intuition.
intros.
easy.
intros.
easy.
destruct k1.
destruct k2.
intros.
easy.
intuition.
intros.
easy.
destruct k2.
intros.
simpl.
ring.
simpl.
intuition.
intros.
easy.
intros.
easy.
Qed.
Proof.
intros n k1 k2 H1 H2.
apply Zpower_exp.
{
apply Z.le_ge.
easy.
}
{
apply Z.le_ge.
easy.
}
Qed.
Proof.
Admitted.
Proof.
intros b [|e|e] He.
{
apply refl_equal.
}
{
apply Zpower_pos_nat.
}
{
elim He.
apply refl_equal.
}
Qed.
Proof.
intros.
unfold Zpower_nat.
unfold nat_rect.
f_equal.
Qed.
Proof.
intros b e.
rewrite (Zpower_nat_is_exp 1 e).
apply (f_equal (fun x => x * _)%Z).
apply Zmult_1_r.
Qed.
Proof.
Admitted.
Proof.
intros b p Hb.
rewrite Zpower_pos_nat.
induction (nat_of_P p).
{
easy.
}
{
rewrite Zpower_nat_S.
apply Zmult_lt_0_compat.
{
easy.
}
{
easy.
}
}
Qed.
Proof.
Admitted.
Proof.
intros b e He Hb.
destruct (Z_le_lt_eq_dec _ _ He) as [He'|He'].
{
rewrite <- Hb.
apply Z.even_pow.
easy.
}
{
rewrite <- He'.
easy.
}
Qed.
(** The radix must be greater than 1 *)
Record radix := { radix_val :> Z ; radix_prop : Zle_bool 2 radix_val = true }.
Proof.
Admitted.
Proof.
intros (r1, H1) (r2, H2) H.
simpl in H.
revert H1.
rewrite H.
intros H1.
apply f_equal.
apply eqbool_irrelevance.
Qed.
Definition radix2 := Build_radix 2 (refl_equal _).
Variable r : radix.
Proof.
red.
simpl.
destruct r.
simpl.
destruct radix_val0.
try discriminate.
eauto.
try discriminate.
Qed.
Proof.
apply Z.lt_le_trans with 2%Z.
{
easy.
}
{
apply Zle_bool_imp_le.
apply r.
}
Qed.
Proof.
Admitted.
Proof.
destruct r as (v, Hr).
simpl.
apply Z.lt_le_trans with 2%Z.
{
easy.
}
{
apply Zle_bool_imp_le.
easy.
}
Qed.
Proof.
Admitted.
Proof.
intros [|p|p] Hp.
{
try easy.
}
{
try easy.
simpl.
rewrite Zpower_pos_nat.
generalize (lt_O_nat_of_P p).
induction (nat_of_P p).
{
easy.
}
{
intros _.
rewrite Zpower_nat_S.
assert (0 < Zpower_nat r n)%Z.
{
clear.
induction n.
{
easy.
}
{
rewrite Zpower_nat_S.
apply Zmult_lt_0_compat with (2 := IHn).
apply radix_gt_0.
}
}
{
apply Z.le_lt_trans with (1 * Zpower_nat r n)%Z.
{
rewrite Zmult_1_l.
apply (Zlt_le_succ 0).
easy.
}
{
apply Zmult_lt_compat_r with (1 := H).
apply radix_gt_1.
}
}
}
}
{
try easy.
}
Qed.
Proof.
Admitted.
Proof.
intros p Hp.
rewrite Zpower_Zpower_nat with (1 := Hp).
induction (Z.abs_nat p).
{
easy.
}
{
rewrite Zpower_nat_S.
apply Zmult_lt_0_compat with (2 := IHn).
apply radix_gt_0.
}
Qed.
Proof.
Admitted.
Proof.
intros [|e|e].
{
try easy.
}
{
try easy.
apply Zlt_le_weak.
apply Zpower_gt_0.
easy.
}
{
try easy.
}
Qed.
Proof.
Admitted.
Proof.
intros e1 e2 He.
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].
{
replace e2 with (e2 - e1 + e1)%Z by ring.
rewrite Zpower_plus with (2 := H1).
{
rewrite <- (Zmult_1_l (r ^ e1)) at 1.
apply Zmult_le_compat_r.
{
apply (Zlt_le_succ 0).
apply Zpower_gt_0.
apply Zle_minus_le_0.
easy.
}
{
apply Zpower_ge_0.
}
}
{
apply Zle_minus_le_0.
easy.
}
}
{
clear He.
destruct e1 as [|e1|e1].
{
try easy.
}
{
try easy.
}
{
try easy.
apply Zpower_ge_0.
}
}
Qed.
Proof.
Admitted.
Proof.
intros e1 e2 He2 He.
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].
{
replace e2 with (e2 - e1 + e1)%Z by ring.
rewrite Zpower_plus with (2 := H1).
{
rewrite Zmult_comm.
rewrite <- (Zmult_1_r (r ^ e1)) at 1.
apply Zmult_lt_compat2.
{
split.
{
apply Zpower_gt_0.
easy.
}
{
apply Z.le_refl.
}
}
{
split.
{
easy.
}
{
apply Zpower_gt_1.
clear -He.
omega.
}
}
}
{
apply Zle_minus_le_0.
apply Zlt_le_weak.
easy.
}
}
{
revert H1.
clear -He2.
destruct e1.
{
try easy.
}
{
try easy.
}
{
try easy.
intros _.
apply Zpower_gt_0.
easy.
}
}
Qed.
Proof.
Admitted.
Proof.
intros e1 e2 He.
apply Znot_gt_le.
intros H.
apply Zlt_not_le with (1 := He).
apply Zpower_le.
clear -H.
omega.
Qed.
Proof.
Admitted.
Proof.
intros [|n|n].
{
try easy.
}
{
try easy.
simpl.
rewrite Zpower_pos_nat.
rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
induction (nat_of_P n).
{
easy.
}
{
rewrite inj_S.
change (Zpower_nat r (S n0)) with (r * Zpower_nat r n0)%Z.
unfold Z.succ.
apply Z.lt_le_trans with (r * (Z_of_nat n0 + 1))%Z.
{
clear.
apply Zlt_0_minus_lt.
replace (r * (Z_of_nat n0 + 1) - (Z_of_nat n0 + 1))%Z with ((r - 1) * (Z_of_nat n0 + 1))%Z by ring.
apply Zmult_lt_0_compat.
{
cut (2 <= r)%Z.
{
omega.
}
{
apply Zle_bool_imp_le.
apply r.
}
}
{
apply (Zle_lt_succ 0).
apply Zle_0_nat.
}
}
{
apply Zmult_le_compat_l.
{
apply Zlt_le_succ.
easy.
}
{
apply Z.le_trans with 2%Z.
{
easy.
}
{
apply Zle_bool_imp_le.
apply r.
}
}
}
}
}
{
try easy.
}
Qed.
End Zpower.
Section Div_Mod.
Proof.
Admitted.
Proof.
intros n a [|b|b] Ha Hb.
{
rewrite 2!Zmod_0_r.
easy.
}
{
rewrite (Zmod_eq n (a * Zpos b)).
{
rewrite Zmult_assoc.
unfold Zminus.
rewrite Zopp_mult_distr_l.
apply Z_mod_plus.
easy.
}
{
apply Zmult_gt_0_compat.
{
apply Z.lt_gt.
easy.
}
{
easy.
}
}
}
{
elim Hb.
easy.
}
Qed.
Proof.
Admitted.
Proof.
intros a b.
rewrite (Z.quot_rem' a b) at 2.
ring.
Qed.
Proof.
Admitted.
Proof.
intros n a b.
assert (Z.rem n (a * b) = n + - (Z.quot n (a * b) * a) * b)%Z.
{
rewrite <- Zopp_mult_distr_l.
rewrite <- Zmult_assoc.
apply ZOmod_eq.
}
{
rewrite H.
apply Z_rem_plus.
rewrite <- H.
apply Zrem_sgn2.
}
Qed.
Proof.
Admitted.
Proof.
intros n a b Ha Hb.
destruct (Zle_lt_or_eq _ _ Ha) as [Ha'|Ha'].
{
destruct (Zle_lt_or_eq _ _ Hb) as [Hb'|Hb'].
{
rewrite (Zmod_eq n (a * b)).
{
rewrite (Zmult_comm a b) at 2.
rewrite Zmult_assoc.
unfold Zminus.
rewrite Zopp_mult_distr_l.
rewrite Z_div_plus.
{
idtac.
rewrite <- Zdiv_Zdiv.
{
idtac.
apply sym_eq.
apply Zmod_eq.
apply Z.lt_gt.
easy.
}
{
easy .
}
{
easy .
}
}
{
apply Z.lt_gt.
easy .
}
}
{
apply Zmult_gt_0_compat.
{
apply Z.lt_gt.
easy.
}
{
apply Z.lt_gt.
easy.
}
}
}
{
rewrite <- Hb'.
rewrite Zmult_0_r.
rewrite  2!Zmod_0_r.
apply Zdiv_0_l.
}
}
{
rewrite <- Ha'.
now(rewrite 2!Zdiv_0_r ).
}
Qed.
Proof.
Admitted.
Proof.
intros n a b.
destruct (Z.eq_dec a 0) as [Za|Za].
{
rewrite Za.
now(rewrite 2!Zquot_0_r ).
}
{
assert (Z.rem n (a * b) = n + - (Z.quot (Z.quot n a) b * b) * a)%Z.
{
rewrite (ZOmod_eq n (a * b)) at 1.
rewrite Zquot_Zquot.
ring.
}
{
rewrite H.
rewrite Z_quot_plus with (2 := Za).
{
apply sym_eq.
apply ZOmod_eq.
}
{
rewrite <- H.
apply Zrem_sgn2.
}
}
}
Qed.
Proof.
Admitted.
Proof.
intros a b Ha.
destruct (Zle_or_lt 0 a) as [H|H].
{
apply Z.quot_small.
split.
{
exact H.
}
{
rewrite Z.abs_eq in Ha.
{
easy.
}
{
easy.
}
}
}
{
apply Z.opp_inj.
rewrite <- Zquot_opp_l.
rewrite  Z.opp_0.
apply Z.quot_small.
generalize (Zabs_non_eq a).
omega.
}
Qed.
Proof.
Admitted.
Proof.
intros a b Ha.
destruct (Zle_or_lt 0 a) as [H|H].
{
apply Z.rem_small.
split.
{
exact H.
}
{
rewrite Z.abs_eq in Ha.
{
easy.
}
{
easy.
}
}
}
{
apply Z.opp_inj.
rewrite <- Zrem_opp_l.
apply Z.rem_small.
generalize (Zabs_non_eq a).
omega.
}
Qed.
Proof.
Admitted.
Proof.
intros a b c Hab.
destruct (Z.eq_dec c 0) as [Zc|Zc].
now rewrite Zc, 4!Zquot_0_r.
apply Zmult_reg_r with (1 := Zc).
rewrite 2!Zmult_plus_distr_l.
assert (forall d, Z.quot d c * c = d - Z.rem d c)%Z.
intros d.
rewrite ZOmod_eq.
ring.
rewrite 4!H.
rewrite <- Zplus_rem with (1 := Hab).
ring.
Qed.
End Div_Mod.
Section Same_sign.
Proof.
Admitted.
Proof.
intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw.
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
Qed.
Proof.
Admitted.
Proof.
intros [|v|v] [|u|u] [|w|w] Zv Huv Hvw.
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
discriminate Zv.
easy.
}
{
try easy.
}
{
try easy.
discriminate Zv.
easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
{
try easy.
}
Qed.
Proof.
intros.
destruct u.
omega.
simpl.
destruct v.
omega.
intuition.
intuition.
simpl.
destruct v.
omega.
apply H0.
easy.
apply H0.
easy.
Qed.
Proof.
intros [|u|u] v Hp Hn.
{
easy.
}
{
apply Zmult_le_0_compat.
{
easy.
}
{
apply Hp.
easy.
}
}
{
replace (Zneg u * v)%Z with (Zpos u * (-v))%Z.
{
apply Zmult_le_0_compat.
{
easy.
}
{
apply Hn.
easy.
}
}
{
rewrite <- Zopp_mult_distr_r.
apply Zopp_mult_distr_l.
}
}
Qed.
Proof.
Admitted.
Proof.
intros u v Hv.
apply Zsame_sign_imp.
{
intros Hu.
apply Z_quot_pos with (2 := Hv).
apply Zlt_le_weak.
easy.
}
{
intros Hu.
rewrite <- Zquot_opp_l.
apply Z_quot_pos with (2 := Hv).
apply Zlt_le_weak.
easy.
}
Qed.
End Same_sign.
(** Boolean comparisons *)

Section Zeq_bool.
Inductive Zeq_bool_prop (x y : Z) : bool -> Prop :=
  | Zeq_bool_true_ : x = y -> Zeq_bool_prop x y true
  | Zeq_bool_false_ : x <> y -> Zeq_bool_prop x y false.
Proof.
Admitted.
Proof.
intros x y.
generalize (Zeq_is_eq_bool x y).
case (Zeq_bool x y).
{
intros (H1, H2).
constructor.
apply H2.
easy.
}
{
intros (H1, H2).
constructor.
intros H.
specialize (H1 H).
discriminate H1.
}
Qed.
Proof.
Admitted.
Proof.
intros x y.
apply -> Zeq_is_eq_bool.
Qed.
Proof.
Admitted.
Proof.
intros x y.
generalize (proj2 (Zeq_is_eq_bool x y)).
case Zeq_bool.
{
intros He Hn.
elim Hn.
apply He.
easy.
}
{
intros _ _.
easy.
}
Qed.
End Zeq_bool.
Section Zle_bool.
Inductive Zle_bool_prop (x y : Z) : bool -> Prop :=
  | Zle_bool_true_ : (x <= y)%Z -> Zle_bool_prop x y true
  | Zle_bool_false_ : (y < x)%Z -> Zle_bool_prop x y false.
Proof.
Admitted.
Proof.
intros x y.
generalize (Zle_is_le_bool x y).
case Zle_bool.
{
intros (H1, H2).
constructor.
apply H2.
easy.
}
{
intros (H1, H2).
constructor.
destruct (Zle_or_lt x y) as [H|H].
{
specialize (H1 H).
easy.
}
{
exact H.
}
}
Qed.
Proof.
Admitted.
Proof.
intros x y.
apply (proj1 (Zle_is_le_bool x y)).
Qed.
Proof.
Admitted.
Proof.
intros x y Hxy.
generalize (Zle_cases x y).
case Zle_bool.
{
intros H.
elim (Z.lt_irrefl x).
apply Z.le_lt_trans with y.
{
easy.
}
{
easy.
}
}
{
intros H.
apply refl_equal.
}
Qed.
End Zle_bool.
Section Zlt_bool.
Inductive Zlt_bool_prop (x y : Z) : bool -> Prop :=
  | Zlt_bool_true_ : (x < y)%Z -> Zlt_bool_prop x y true
  | Zlt_bool_false_ : (y <= x)%Z -> Zlt_bool_prop x y false.
Proof.
Admitted.
Proof.
intros x y.
generalize (Zlt_is_lt_bool x y).
case Zlt_bool.
{
intros (H1, H2).
constructor.
apply H2.
easy.
}
{
intros (H1, H2).
constructor.
destruct (Zle_or_lt y x) as [H|H].
{
exact H.
}
{
specialize (H1 H).
easy.
}
}
Qed.
Proof.
intros.
unfold Z.ltb.
rewrite H.
eauto.
Qed.
Proof.
intros x y.
apply (proj1 (Zlt_is_lt_bool x y)).
Qed.
Proof.
Admitted.
Proof.
intros x y Hxy.
generalize (Zlt_cases x y).
case Zlt_bool.
{
intros H.
elim (Z.lt_irrefl x).
apply Z.lt_le_trans with y.
{
easy.
}
{
easy.
}
}
{
intros H.
apply refl_equal.
}
Qed.
Proof.
Admitted.
Proof.
intros x y.
case Zle_bool_spec.
{
intros H.
rewrite Zlt_bool_false.
{
easy.
}
{
easy.
}
}
{
intros H.
rewrite Zlt_bool_true.
{
easy.
}
{
easy.
}
}
Qed.
Proof.
Admitted.
Proof.
intros x y.
case Zlt_bool_spec.
{
intros H.
rewrite Zle_bool_false.
{
easy.
}
{
easy.
}
}
{
intros H.
rewrite Zle_bool_true.
{
easy.
}
{
easy.
}
}
Qed.
End Zlt_bool.
Section Zcompare.
Inductive Zcompare_prop (x y : Z) : comparison -> Prop :=
  | Zcompare_Lt_ : (x < y)%Z -> Zcompare_prop x y Lt
  | Zcompare_Eq_ : x = y -> Zcompare_prop x y Eq
  | Zcompare_Gt_ : (y < x)%Z -> Zcompare_prop x y Gt.
Proof.
Admitted.
Proof.
intros x y.
destruct (Z_dec x y) as [[H|H]|H].
{
generalize (Zlt_compare _ _ H).
case (Z.compare x y).
{
try easy.
}
{
try easy.
constructor.
easy.
}
{
try easy.
}
}
{
generalize (Zgt_compare _ _ H).
case (Z.compare x y).
{
try easy.
}
{
try easy.
}
{
try easy.
constructor.
apply Z.gt_lt.
easy.
}
}
{
generalize (proj2 (Zcompare_Eq_iff_eq _ _) H).
case (Z.compare x y).
{
try easy.
constructor.
easy.
}
{
try easy.
}
{
try easy.
}
}
Qed.
Proof.
intros.
easy.
Qed.
Proof.
easy.
Qed.
Proof.
Admitted.
Proof.
intros x y.
apply <- Zcompare_Eq_iff_eq.
Qed.
Proof.
Admitted.
Proof.
intros x y.
apply Z.lt_gt.
Qed.
End Zcompare.
Section cond_Zopp.
Definition cond_Zopp (b : bool) m := if b then Z.opp m else m.
Proof.
intros.
unfold cond_Zopp.
unfold negb.
destruct x.
intuition.
eauto.
Qed.
Proof.
intros [|] y.
{
apply sym_eq, Z.opp_involutive.
}
{
easy.
}
Qed.
Proof.
induction b.
intros.
unfold cond_Zopp.
unfold Z.opp.
destruct m.
eauto.
eauto.
eauto.
intros.
easy.
Qed.
Proof.
intros [|] m.
{
apply Zabs_Zopp.
}
{
apply refl_equal.
}
Qed.
Proof.
induction m.
eauto.
simpl.
eauto.
simpl.
eauto.
Qed.
Proof.
intros m.
apply sym_eq.
case Zlt_bool_spec.
{
intros Hm.
apply Zabs_non_eq.
apply Zlt_le_weak.
easy.
}
{
intros Hm.
apply Z.abs_eq.
easy.
}
Qed.
End cond_Zopp.
Section fast_pow_pos.
Fixpoint Zfast_pow_pos (v : Z) (e : positive) : Z :=
  match e with
  | xH => v
  | xO e' => Z.square (Zfast_pow_pos v e')
  | xI e' => Zmult v (Z.square (Zfast_pow_pos v e'))
  end.
Proof.
Admitted.
Proof.
intros v e.
rewrite <- (Zmult_1_r (Zfast_pow_pos v e)).
unfold Z.pow_pos.
generalize 1%Z.
revert v.
induction e.
{
intros v f.
simpl.
rewrite <- 2!IHe.
rewrite Z.square_spec.
ring.
}
{
intros v f.
simpl.
rewrite <- 2!IHe.
rewrite Z.square_spec.
apply eq_sym, Zmult_assoc.
}
{
intros v f.
simpl.
apply eq_refl.
}
Qed.
End fast_pow_pos.
Section faster_div.
Proof.
Admitted.
Proof.
intros a b.
unfold Z.div.
unfold Zmod.
case Z.div_eucl.
easy.
Qed.
Fixpoint Zpos_div_eucl_aux1 (a b : positive) {struct b} :=
  match b with
  | xO b' =>
    match a with
    | xO a' => let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 * r)%Z
    | xI a' => let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 * r + 1)%Z
    | xH => (Z0, Zpos a)
    end
  | xH => (Zpos a, Z0)
  | xI _ => Z.pos_div_eucl a (Zpos b)
  end.
Proof.
Admitted.
Proof.
intros a b.
revert a.
induction b ; intros a.
-
easy.
-
change (Z.pos_div_eucl a (Zpos b~0)) with (Z.div_eucl (Zpos a) (Zpos b~0)).
rewrite Zdiv_eucl_unique.
change (Zpos b~0) with (2 * Zpos b)%Z.
rewrite Z.rem_mul_r by easy.
rewrite <- Zdiv_Zdiv by easy.
destruct a as [a|a|].
+
change (Zpos_div_eucl_aux1 a~1 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r + 1)%Z).
rewrite IHb.
clear IHb.
change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)).
rewrite Zdiv_eucl_unique.
change (Zpos a~1) with (1 + 2 * Zpos a)%Z.
rewrite (Zmult_comm 2 (Zpos a)).
rewrite Z_div_plus_full by easy.
apply f_equal.
rewrite Z_mod_plus_full.
apply Zplus_comm.
+
change (Zpos_div_eucl_aux1 a~0 b~0) with (let (q, r) := Zpos_div_eucl_aux1 a b in (q, 2 * r)%Z).
rewrite IHb.
clear IHb.
change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)).
rewrite Zdiv_eucl_unique.
change (Zpos a~0) with (2 * Zpos a)%Z.
rewrite (Zmult_comm 2 (Zpos a)).
rewrite Z_div_mult_full by easy.
apply f_equal.
now rewrite Z_mod_mult.
+
easy.
-
change (Z.pos_div_eucl a 1) with (Z.div_eucl (Zpos a) 1).
rewrite Zdiv_eucl_unique.
now rewrite Zdiv_1_r, Zmod_1_r.
Qed.
Definition Zpos_div_eucl_aux (a b : positive) :=
  match Pos.compare a b with
  | Lt => (Z0, Zpos a)
  | Eq => (1%Z, Z0)
  | Gt => Zpos_div_eucl_aux1 a b
  end.
Proof.
Admitted.
Proof.
intros a b.
unfold Zpos_div_eucl_aux.
change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)).
rewrite Zdiv_eucl_unique.
case Pos.compare_spec ; intros H.
now rewrite H, Z_div_same, Z_mod_same.
now rewrite Zdiv_small, Zmod_small by (split ; easy).
rewrite Zpos_div_eucl_aux1_correct.
change (Z.pos_div_eucl a (Zpos b)) with (Z.div_eucl (Zpos a) (Zpos b)).
apply Zdiv_eucl_unique.
Qed.
Definition Zfast_div_eucl (a b : Z) :=
  match a with
  | Z0 => (0, 0)%Z
  | Zpos a' =>
    match b with
    | Z0 => (0, 0)%Z
    | Zpos b' => Zpos_div_eucl_aux a' b'
    | Zneg b' =>
      let (q, r) := Zpos_div_eucl_aux a' b' in
      match r with
      | Z0 => (-q, 0)%Z
      | Zpos _ => (-(q + 1), (b + r))%Z
      | Zneg _ => (-(q + 1), (b + r))%Z
      end
    end
  | Zneg a' =>
    match b with
    | Z0 => (0, 0)%Z
    | Zpos b' =>
      let (q, r) := Zpos_div_eucl_aux a' b' in
      match r with
      | Z0 => (-q, 0)%Z
      | Zpos _ => (-(q + 1), (b - r))%Z
      | Zneg _ => (-(q + 1), (b - r))%Z
      end
    | Zneg b' => let (q, r) := Zpos_div_eucl_aux a' b' in (q, (-r)%Z)
    end
  end.
Proof.
Admitted.
Proof.
unfold Zfast_div_eucl.
intros [|a|a] [|b|b].
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
{
try rewrite Zpos_div_eucl_aux_correct.
easy.
}
Qed.
End faster_div.
Section Iter.
Context {A : Type}.
Variable (f : A -> A).
Fixpoint iter_nat (n : nat) (x : A) {struct n} : A :=
  match n with
  | S n' => iter_nat n' (f x)
  | O => x
  end.
Proof.
Admitted.
Proof.
induction q.
{
rewrite plus_0_r.
easy.
}
{
intros x.
rewrite <- plus_n_Sm.
apply IHq.
}
Qed.
Proof.
induction p.
simpl.
intros.
eauto.
intros x.
eauto.
Qed.
Proof.
induction p.
{
easy.
}
{
simpl.
intros x.
apply IHp.
}
Qed.
Fixpoint iter_pos (n : positive) (x : A) {struct n} : A :=
  match n with
  | xI n' => iter_pos n' (iter_pos n' (f x))
  | xO n' => iter_pos n' (iter_pos n' x)
  | xH => f x
  end.
Proof.
Admitted.
Proof.
induction p.
{
intros x.
rewrite Pos2Nat.inj_xI.
simpl.
rewrite plus_0_r.
rewrite iter_nat_plus.
rewrite (IHp (f x)).
apply IHp.
}
{
intros x.
rewrite Pos2Nat.inj_xO.
simpl.
rewrite plus_0_r.
rewrite iter_nat_plus.
rewrite (IHp x).
apply IHp.
}
{
intros x.
easy.
}
Qed.
End Iter.