Require Export ZArith.
Require Export Integers.
Export Int.
(*
Require Export Values.
Require Export Mem.
*)
Require Export Bool.

Require Export tactics.

Open Scope Z_scope.

Load param.

Lemma eq_optint_dec : forall a b : option int, {a = b} + {a <> b}.
Proof.
decide equality.
apply eq_dec.
Defined.

Lemma samerepr_eqm : forall x y, repr x = repr y -> eqm x y.
Proof.
unfold repr.
injection 1.
unfold eqm.
unfold eqmod.
unfold Zmod.
case_eq (Zdiv_eucl x modulus).
intros q r Hx.
case_eq (Zdiv_eucl y modulus).
intros s t Hy.
intros.
subst.
generalize (Z_div_mod x modulus modulus_pos).
rewrite Hx.
destruct 1; subst.
generalize (Z_div_mod y modulus modulus_pos).
rewrite Hy.
destruct 1; subst.
exists (q - s).
rewrite (Zmult_comm (q - s)).
rewrite Zplus_assoc.
rewrite <- Zmult_plus_distr_r.
f_equal.
f_equal.
omega.
Qed .

Lemma eq_prop_eq_bool : forall a b, a = b -> eq a b = true.
Proof.
intros.
subst.
unfold eq.
destruct (Coqlib.zeq (unsigned b) (unsigned b)) ; eauto.
Qed.

Corollary neq_bool_neq_prop : forall a b, eq a b = false -> a = b -> False.
Proof.
intros a b ? Hab.
generalize (eq_prop_eq_bool Hab).
intros.
discr.
Qed.

Lemma signed_inj : forall b c, signed b = signed c -> b = c.
Proof.
destruct b.
destruct c.
unfold signed.
unfold unsigned.
simpl.
unfold Coqlib.zlt.
intros.
cut (intval = intval0).
intros.
subst.
rewrite (Coqlib.proof_irrelevance _ intrange intrange0).
trivial.
genclear H.
case (Z_lt_ge_dec intval half_modulus) ; 
case (Z_lt_ge_dec intval0 half_modulus) ; intros ; eauto with *.
Qed.

Lemma eq_bool_eq_prop : forall a b, eq a b = true -> a = b.
Proof.
unfold eq.
introvars.
destruct (Coqlib.zeq (unsigned a) (unsigned b)) as [e |].
intros _.
genclear e.
unfold unsigned.
unfold intval.
destruct a.
destruct b.
intros.
subst.
rewrite (Coqlib.proof_irrelevance _ intrange0 intrange).
trivial.
discriminate 1.
Qed.


Corollary neq_prop_neq_bool : forall a b, (a = b -> False) -> eq a b = false.
intros.
subst.
case_eq (eq a b); auto.
intro Heq; contradiction (eq_bool_eq_prop Heq).
Qed.

Lemma min_max : min_signed <= max_signed.
Proof.
destruct (signed_range zero); auto with *.
Qed.

Hint Resolve min_max.

Lemma lt_is_signed_lt a b : cmp Clt a b = true -> signed a < signed b.
Proof.
introvars.
unfold cmp.
unfold lt.
destruct (Coqlib.zlt (signed a) (signed b)) ; auto.
discriminate 1.
Qed.

Lemma signed_lt_is_lt a b : signed a < signed b -> cmp Clt a b = true.
Proof.
intros.
unfold cmp.
unfold lt.
destruct (Coqlib.zlt (signed a) (signed b)) ; auto.
Qed.

Lemma le_is_signed_le a b : cmp Cle a b = true -> signed a <= signed b.
Proof.
introvars.
unfold cmp.
unfold lt.
destruct (Coqlib.zlt (signed b) (signed a)).
discriminate 1.
intros _.
apply Zge_le.
auto.
Qed.

Lemma signed_le_is_le a b : signed a <= signed b -> cmp Cle a b = true.
Proof.
introvars.
unfold cmp.
unfold lt.
destruct (Coqlib.zlt (signed b) (signed a)).
intro Hab.
apply False_ind.
auto with zarith.
auto.
Qed.

Hint Resolve le_is_signed_le lt_is_signed_lt.

Lemma le_is_lt_or_eq : forall a b, cmp Cle a b = true -> {a = b} + {cmp Clt a b = true}.
Proof.
intros a b Hab.
generalize (le_is_signed_le Hab).
intros HSab.
destruct (Z_le_lt_eq_dec _ _ HSab).
right.
apply signed_lt_is_lt.
auto.
left.
apply signed_inj.
auto.
Defined.

Lemma lt_is_le_neq : forall a b,
cmp Cle a b = true ->
(a = b -> False) ->
cmp Clt a b = true.
Proof.
intros a b Hab Hneq.
destruct (le_is_lt_or_eq Hab).
contradiction.
auto.
Qed.


Lemma add_sub_id : forall a x, sub (add a x) x = a.
Proof.
intros.
rewrite sub_add_opp.
rewrite add_assoc.
rewrite add_neg_zero.
rewrite add_zero.
trivial.
Qed.

Hint Resolve add_sub_id.

Lemma sub_add_id : forall a x, add (sub a x) x = a.
Proof.
intros.
rewrite <- sub_add_l.
eauto.
Qed.

Hint Resolve sub_add_id.

Lemma neg_neg : forall x, neg (neg x) = x.
Proof with auto with ints.
intros.
unfold neg.
pattern x at 2.
replace x with (repr (unsigned x))...
apply eqm_samerepr.
apply eqm_trans with (- ( - unsigned x))...
replace (- - unsigned x) with (unsigned x)...
omega.
Qed.

Corollary neg_inj : forall a b, neg a = neg b -> a = b.
Proof.
intros.
rewrite <- (neg_neg a).
rewrite <- (neg_neg b).
f_equal.
assumption.
Qed.

Hint Resolve neg_neg.

Lemma sub_anticommut : forall a b, sub a b = neg (sub b a).
Proof.
intros.
rewrite sub_add_opp.
rewrite sub_add_opp.
rewrite neg_add_distr.
rewrite neg_neg.
apply add_commut.
Qed.

Lemma add_zero_recip_r a b : add b a = a -> b = zero.
Proof.
introvars.
intros Hab.
rewrite <- (sub_idem a).
rewrite <- (add_sub_id b a).
rewrite Hab.
auto.
Qed.

Corollary add_zero_recip_l a b : add a b = a -> b = zero.
Proof.
introvars.
rewrite add_commut.
apply add_zero_recip_r.
Qed.


Hint Resolve add_zero_recip_l add_zero_recip_r.

Lemma add_reg_r a b d : add a d = add b d -> a = b.
Proof.
intros.
rewrite <- (add_sub_id a d).
rewrite <- (add_sub_id b d).
congruence.
Qed.

Lemma add_reg_l a b d : add d a = add d b -> a = b.
Proof.
introvars.
rewrite (add_commut d a).
rewrite (add_commut d b).
apply add_reg_r.
Qed.

Lemma sub_permut : forall a b c, sub (sub a b) c = sub (sub a c) b.
intros.
rewrite sub_add_opp.
rewrite sub_add_opp.
rewrite sub_add_opp.
rewrite sub_add_opp.
rewrite add_assoc.
rewrite (add_commut (neg b) (neg c)).
rewrite <- add_assoc.
trivial.
Qed.

Lemma lt_is_le_s : forall a b, cmp Clt a b = true ->
cmp Cle (add a one) b = true.
Proof.
intros a b Hab.
generalize (lt_is_signed_lt Hab).
intros.
apply signed_le_is_le.
rewrite add_signed.
change (signed one) with 1.
rewrite signed_repr.
auto with *.
generalize (signed_range a).
destruct 1 as [Hamin Hamax].
split.
apply Zle_trans with (signed a).
auto.
auto with *.
generalize (signed_range b).
destruct 1 as [Hbmin Hbmax].
auto with *.
Qed.

Hint Resolve lt_is_le_s.

Lemma max_upper_bound : forall a, cmp Cle a (repr max_signed) = true.
Proof.
intros.
apply signed_le_is_le.
destruct (signed_range a); auto.
Qed.

Hint Resolve max_upper_bound.

Lemma min_upper_bound : forall a, cmp Cle (repr min_signed) a = true.
Proof.
intros.
apply signed_le_is_le.
destruct (signed_range a); auto.
Qed.

Hint Resolve min_upper_bound.

Lemma not_le_s_is_max : forall a, {cmp Cle a (add a one) = true} + {a = repr max_signed}.
Proof.
intro.
destruct (eq_dec a (repr max_signed)) as [|Hneq].
auto.
left.
apply signed_le_is_le.
rewrite add_signed.
change (signed one) with 1.
rewrite (signed_repr).
auto with *.
destruct (signed_range a).
split ; auto with *.
cut (signed a < max_signed); intros; auto with *.
cut (signed a <> max_signed); auto with *.
intro.
apply Hneq.
apply signed_inj.
rewrite signed_repr; auto.
split; auto with *.
Defined.

Corollary not_lt_s_is_max : forall a, {cmp Clt a (add a one) = true} + {a = repr max_signed}.
Proof.
intros a.
destruct (not_le_s_is_max a); auto.
left.
apply lt_is_le_neq.
auto.
intros.
apply one_not_zero.
apply add_reg_l with a.
rewrite add_zero.
auto.
Defined.




Lemma max_plus_one_is_min : add (repr max_signed) one = repr min_signed.
Proof.
rewrite add_signed.
apply eqm_samerepr.
rewrite signed_repr.
change (signed one) with 1.
unfold max_signed.
unfold min_signed.
change (half_modulus - 1 + 1) with half_modulus.
change (- half_modulus) with (0 + - half_modulus).
assert (half_modulus = modulus + -half_modulus) as e.
auto.
pattern half_modulus at 1.
rewrite e.
apply eqm_add.
unfold eqm.
unfold eqmod.
exists 1.
auto.
apply eqm_refl.
split; auto with *.
Qed.

Hint Resolve max_plus_one_is_min.

Corollary min_minus_one_is_max : sub (repr min_signed) one = repr max_signed.
rewrite <- (add_sub_id (repr max_signed) one).
f_equal.
auto.
Qed.

Hint Resolve min_minus_one_is_max.

Lemma not_le_p_is_min : forall a, {cmp Cle (sub a one) a = true} + {a = repr min_signed}.
Proof.
intro.
destruct (not_le_s_is_max (sub a one)).
left.
rewrite sub_add_id in e; auto.
right.
rewrite <- max_plus_one_is_min.
rewrite <- (sub_add_id a one).
f_equal.
assumption.
Defined.

Lemma not_lt_p_is_min : forall a, {cmp Clt (sub a one) a = true} + {a = repr min_signed}.
Proof.
intro.
destruct (not_lt_s_is_max (sub a one)).
left.
rewrite sub_add_id in e; auto.
right.
rewrite <- max_plus_one_is_min.
rewrite <- (sub_add_id a one).
f_equal.
assumption.
Defined.

Lemma lt_is_le_p : forall a b, cmp Clt a b = true ->
cmp Cle a (sub b one) = true.
Proof.
intros a b Hab.
generalize (lt_is_signed_lt Hab).
intros.
apply signed_le_is_le.
rewrite sub_add_opp.
rewrite add_signed.
change (signed (neg one)) with (-1).
rewrite signed_repr.
auto with *.
generalize (signed_range a).
destruct 1 as [Hamin Hamax].
split.
apply Zle_trans with (signed a).
auto.
auto with *.
generalize (signed_range b).
destruct 1 as [Hbmin Hbmax].
auto with *.
Qed.


Section Le_lt_bool.

Lemma le_is_not_lt_conv : forall a b,
cmp Cle a b = negb (cmp Clt b a).

Proof.
trivial.
Qed.

Lemma lt_is_not_le_conv : forall a b,
cmp Clt a b = negb (cmp Cle b a).

Proof.
simpl.
unfold negb.
intros.
case (lt a b) ; eauto.
Qed.

Lemma negb_false_true : forall x,
x = false -> negb x = true.

Proof.
intros ; subst ; trivial.
Qed.

Lemma negb_true_false : forall x,
x = true -> negb x = false.

Proof.
intros ; subst ; trivial.
Qed.

Hint Resolve le_is_not_lt_conv lt_is_not_le_conv negb_false_true negb_true_false.

Lemma le_true_lt_false : forall a b,
cmp Cle a b = true -> cmp Clt b a = false.

Proof.
 eauto.
Qed.

Lemma lt_true_le_false : forall a b,
cmp Clt a b = true -> cmp Cle b a = false.

Proof.
 eauto.
Qed.

Lemma le_false_lt_true : forall a b,
cmp Cle a b = false -> cmp Clt b a = true.

Proof.
 eauto.
Qed.

Lemma lt_false_le_true : forall a b,
cmp Clt a b = false -> cmp Cle b a = true.

Proof.
 eauto.
Qed.

End Le_lt_bool.

Lemma int_lt_irrefl_3 : forall a b, cmp Clt a b = true -> cmp Cle b a = true -> False.
Proof.
unfold cmp.
introvars.
case (lt a b); intros; discr.
Qed.

(*
Hint Resolve int_lt_irrefl_3.
*)

Lemma int_le_lt_weak : forall a b,
cmp Clt a b = true -> cmp Cle a b = true.
Proof.
 intros.
 apply signed_le_is_le.
 apply Zlt_le_weak.
 auto with *.
Qed.

Lemma not_le_le_conv : forall a b, cmp Cle a b = false -> cmp Cle b a = true.
Proof.
introvars.
intros Hnot.
generalize (le_false_lt_true Hnot).
apply int_le_lt_weak.
Qed.

Lemma int_lt_irrefl_2 : forall a b, cmp Clt a b = true -> cmp Clt b a = true -> False.
Proof.
 intros.
 eapply int_lt_irrefl_3.
 eauto.
 eapply int_le_lt_weak; eauto.
Qed.

(*
Hint Resolve int_lt_irrefl_2.
*)

Corollary int_lt_irrefl_1 : forall a, cmp Clt a a = true -> False.
Proof.
intros; eapply int_lt_irrefl_2; eauto.
Qed.

Corollary int_lt_irrefl : forall a, cmp Clt a a = false.
Proof.
intro a ; case_eq (cmp Clt a a); auto; intros; apply False_ind; eapply int_lt_irrefl_1; eauto.
Qed.

Hint Resolve int_lt_irrefl.

Corollary int_lt_irrefl_0 : forall a b, cmp Clt a b = true -> a = b -> False.
Proof.
intros.
subst.
eapply int_lt_irrefl_1.
eassumption.
Qed.


Lemma int_le_refl_1 : forall a, cmp Cle a a = true.
Proof.
intros ; apply lt_false_le_true; eauto.
Qed.

Hint Resolve int_le_refl_1.

Corollary int_le_refl : forall a b, a = b -> cmp Cle a b = true.

Proof.
intros ; subst ; eauto.
Qed.

Lemma int_le_antisym : forall a b, cmp Cle a b = true -> cmp Cle b a = true -> a = b.
Proof.
intros.
apply signed_inj.
apply Zle_antisym; auto.
Qed.

Corollary max_supremum : forall a, cmp Cle (repr max_signed) a = true -> a = repr max_signed.
Proof.
intros.
apply int_le_antisym; auto.
Qed.

Corollary min_infimum : forall a, cmp Cle a (repr min_signed) = true -> a = repr min_signed.
Proof.
intros.
apply int_le_antisym; auto.
Qed.

Hint Resolve max_supremum min_infimum.

Lemma int_le_s_dec : forall a x, cmp Cle a x = true -> cmp Cle x (add a one) = true -> {x = a} + {x = add a one}.
Proof.
intros a x Ha Ha1.
destruct (le_is_lt_or_eq Ha).
auto.
right.
apply int_le_antisym; auto.
Defined.

Lemma lt_step : forall a b, cmp Clt a b = true -> cmp Clt a (add a one) = true.
Proof.
intros a b Hab.
destruct (not_lt_s_is_max a); auto.
generalize (int_le_lt_weak Hab).
intro Hab'.
subst.
generalize (max_supremum Hab').
intro.
subst.
destruct (int_lt_irrefl_1 Hab).
Qed.

Lemma lt_step_p : forall a b, cmp Clt a b = true -> cmp Clt (sub b one) b = true.
Proof.
intros a b Hab.
destruct (not_lt_p_is_min b); auto.
generalize (int_le_lt_weak Hab).
intro Hab'.
subst.
generalize (min_infimum Hab').
intro.
subst.
destruct (int_lt_irrefl_1 Hab).
Qed.



(* Transitivity. *)

Lemma int_le_trans a b : cmp Cle a b = true -> forall c, cmp Cle b c = true -> cmp Cle a c = true.
Proof.
intros.
apply signed_le_is_le.
eapply Zle_trans; eauto.
Qed.

Lemma int_le_lt_trans a b : cmp Cle a b = true -> forall c, cmp Clt b c =true -> cmp Clt a c = true.
Proof.
intros.
apply signed_lt_is_lt.
eapply Zle_lt_trans; eauto.
Qed.

Lemma int_lt_le_trans a b : cmp Clt a b = true -> forall c, cmp Cle b c =true -> cmp Clt a c = true.
Proof.
intros.
apply signed_lt_is_lt.
eapply Zlt_le_trans; eauto.
Qed.

Ltac int_lt_trans_tac x z :=
match goal with
| H: cmp Clt x z = true |- _ => exact H
| H: cmp Clt x ?y = true |- _ => refine (@int_lt_le_trans x y H z _)
| H: cmp Clt ?y z = true |- _ => refine (@int_le_lt_trans x y _ z H)
| H: cmp Cle x ?y = true |- _ => refine (@int_le_lt_trans x y H z _)
| H: cmp Cle ?y z = true |- _ => refine (@int_lt_le_trans x y _ z H)
end.

Ltac int_le_trans_tac x z :=
match goal with
| H: cmp Cle x z = true |- _ => exact H
| H: cmp Clt x z = true |- _ => exact (@int_le_lt_weak x z H)
| H: cmp Clt x ?y = true |- _ => refine (@int_le_trans x y (@int_le_lt_weak x y H) z _)
| H: cmp Clt ?y z = true |- _ => refine (@int_le_trans x y _ z (@int_le_lt_weak y z H))
| H: cmp Cle x ?y = true |- _ => refine (@int_le_trans x y H z _)
| H: cmp Cle ?y z = true |- _ => refine (@int_le_trans x y _ z H)
end.

Ltac int_le_lt_trans_tac :=
match goal with
| |- cmp Clt ?x ?z = true => int_lt_trans_tac x z
| |- cmp Cle ?x ?z = true => int_le_trans_tac x z
end.

(* Hint Resolve int_lt_trans int_le_trans int_le_lt_trans int_lt_le_trans. *)



Definition two := repr 2.
Definition three := repr 3.
Definition four := repr 4.
Definition eight := repr 8.

Lemma H_4_3_1 : four = add three one.
reflexivity.
Qed.

Lemma Hcalc : forall b0, (add (sub b0 four) three = sub b0 one).
intros.
rewrite sub_add_opp.
rewrite sub_add_opp.
rewrite add_assoc.
f_equal.
rewrite add_commut.
rewrite <- sub_add_opp.
auto.
Qed.


Lemma four_not_zero : four = zero -> False.
inversion 1.
Qed.

Lemma one_not_zero : one = zero -> False.
inversion 1.
Qed.

Lemma two_not_zero : two = zero -> False.
inversion 1.
Qed.

Lemma three_not_zero : three = zero -> False.
inversion 1.
Qed.

Lemma four_positions : forall b x, 
cmp Cle b x = true ->
cmp Cle x (add b three) = true ->
{x = b} + {x = add b one} + {x = add b two} + {x = add b three}.
Proof.
change three with (add two one).
introvars.
rewrite <- add_assoc.
intros.
case_eq (cmp Cle x (add b one)).
intros.
destruct (@int_le_s_dec b x); auto.
intro Hle1.
generalize (le_false_lt_true Hle1).
intro Hlt1.
generalize (lt_is_le_s Hlt1).
rewrite add_assoc.
change (add one one) with two.
intros Hle2.
destruct (@int_le_s_dec (add b two) x) ; auto.
Defined.

Inductive disjoint_intervals a1 b1 a2 b2 : Prop := 
| disjoint_intervals_intro : (forall x,
cmp Cle a1 x = true ->
cmp Cle x b1 = true ->
cmp Cle a2 x = true ->
cmp Cle x b2 = true ->
False) ->
@disjoint_intervals a1 b1 a2 b2.

Hint Constructors disjoint_intervals.

Lemma disjoint_sym : forall a1 b1 a2 b2,
disjoint_intervals a1 b1 a2 b2 -> disjoint_intervals a2 b2 a1 b1.

Proof.
inversion 1; eauto.
Qed.

Lemma disjoint_incl_left : forall a1 b1 a2 b2, disjoint_intervals a1 b1 a2 b2 ->
forall c, cmp Cle a2 c = true -> cmp Cle c b2 = true ->
disjoint_intervals a1 b1 a2 c.

Proof.
 inversion 1 as [Hd] ; subst ; intros; apply disjoint_intervals_intro.
 intro x.
 intros.
 apply Hd with x; auto.
 int_le_lt_trans_tac; auto.
Qed.

Lemma disjoint_incl_right : forall a1 b1 a2 b2, disjoint_intervals a1 b1 a2 b2 ->
forall c, cmp Cle a2 c = true -> cmp Cle c b2 = true ->
disjoint_intervals a1 b1 c b2.

Proof.
 inversion 1 as [Hd] ; subst ; intros; apply disjoint_intervals_intro.
 intro x.
 intros.
 apply Hd with x; auto.
 int_le_lt_trans_tac; auto.
Qed.

Lemma disjoint_indep : forall a b c d, cmp Clt b c = true ->
disjoint_intervals a b c d.
Proof.
intros.
apply disjoint_intervals_intro.
intros.
apply int_lt_irrefl_1 with x.
apply int_le_lt_trans with b.
auto.
int_le_lt_trans_tac.
auto.
Qed.

(* Hint Resolve disjoint_incl_left disjoint_incl_right. *)
Ltac disjoint_incl_tac2 a1 b1 a2 b2 :=
match goal with
| H: disjoint_intervals a1 b1 a2 b2 |- _ => exact H
| H1: cmp Cle a2 b2 = true, H2: cmp Cle b2 ?b2' = true |- _  => refine (@disjoint_incl_left a1 b1 a2 b2' _ b2 H1 H2)
| H1: cmp Cle ?a2' a2 = true, H2: cmp Cle a2 b2 = true |- _  => refine (@disjoint_incl_right a1 b1 a2' b2 _ a2 H1 H2)
| H: disjoint_intervals a1 b1 a2 ?b2' |- _  => refine (@disjoint_incl_left a1 b1 a2 b2' H b2 _ _)
| H: disjoint_intervals a1 b1 ?a2' b2 |- _  => refine (@disjoint_incl_right a1 b1 a2' b2 H a2 _ _)
end.

Ltac disjoint_incl_tac0 a1 b1 a2 b2 :=
disjoint_incl_tac2 a1 b1 a2 b2 || (apply disjoint_sym; disjoint_incl_tac2 a2 b2 a1 b1).

Ltac disjoint_incl_tac :=
match goal with |- disjoint_intervals ?a1 ?b1 ?a2 ?b2 => disjoint_incl_tac0 a1 b1 a2 b2 end.

(*
Hint Extern 1 (disjoint_intervals ?a1 ?b1 ?a2 ?b2) => disjoint_incl_tac a1 b1 a2 b2.
*)

Lemma int_sequence_dec a1 x b1 : {cmp Cle a1 x = true /\ cmp Cle x b1 = true} +
{cmp Cle a1 x = true -> cmp Cle x b1 = true -> False}.

Proof.
intros.
case_eq (cmp Cle a1 x); case_eq (cmp Cle x b1); intros; auto; right; intros; discr.
Defined. 

Lemma add_interval_reduce_left : forall delta, (delta = zero -> False) -> forall n, cmp Cle n (add n delta) = true ->
cmp Clt n (add n one) = true.
Proof.
intros delta Hdelta_nz n Hn.
destruct (not_lt_s_is_max n); auto.
subst.
destruct Hdelta_nz.
eapply add_zero_recip_l.
apply max_supremum.
assumption.
Qed.

Lemma add_interval_reduce_right : forall delta, (delta = zero -> False) -> forall n, cmp Cle n (add n delta) = true ->
cmp Clt (sub (add n delta) one) (add n delta) = true.
Proof.
intros delta Hdelta_nz n Hn.
destruct (not_lt_p_is_min (add n delta)); auto.
subst.
destruct Hdelta_nz.
eapply add_zero_recip_l.
eapply trans_equal.
eassumption.
symmetry.
apply min_infimum.
congruence.
Qed.


Lemma four_three_right : forall n, cmp Cle n (add n four) = true ->
cmp Cle (add n three) (add n four) = true.
Proof.
intro n.
rewrite <- (add_commut three).
change three with (sub four one).
rewrite <- sub_add_l.
intros.
apply int_le_lt_weak.
rewrite (add_commut four).
apply add_interval_reduce_right.
apply four_not_zero.
assumption.
Qed.

Lemma add_interval_reduce_big_right : forall delta, (delta = zero -> False) -> forall n, cmp Cle n (add n delta) = true ->
cmp Cle n (sub (add n delta) one) = true.
Proof.
intros delta Hdelta_nz n Hn.
apply lt_is_le_p.
apply lt_is_le_neq.
assumption.
intro.
destruct Hdelta_nz.
apply add_zero_recip_l with n.
congruence.
Qed.

Lemma add_interval_reduce_big_left : forall delta, (delta = zero -> False) -> forall n, cmp Cle n (add n delta) = true ->
cmp Cle (add n one) (add n delta) = true.
Proof.
intros delta Hdelta_nz n Hn.
apply lt_is_le_s.
apply lt_is_le_neq.
auto.
intro.
destruct Hdelta_nz.
apply add_zero_recip_l with n.
congruence.
Qed.

Corollary four_three_left : forall n, cmp Cle n (add n four) = true ->
cmp Cle n (add n three) = true.
Proof.
intros.
change three with (sub four one).
rewrite (add_commut n).
rewrite <- sub_add_l.
rewrite <- (add_commut n).
apply add_interval_reduce_big_right.
apply four_not_zero.
assumption.
Qed.

Hint Resolve four_three_left four_three_right.

Hint Resolve four_positions.

Corollary three_one_left : forall b, cmp Cle b (add b three) = true ->
cmp Cle b (add b one) = true.
Proof.
 intros.
 apply int_le_lt_weak.
 eapply add_interval_reduce_left.
 apply three_not_zero.
 assumption.
Qed.

Corollary four_one_left : forall b, cmp Cle b (add b four) = true ->
cmp Cle b (add b one) = true.
Proof.
intros.
eapply three_one_left.
eapply four_three_left.
assumption.
Qed.

Corollary three_one_right : forall b, cmp Cle b (add b three) = true ->
cmp Cle (add b one) (add b three) = true.
Proof.
 intros.
 eapply add_interval_reduce_big_left.
 apply three_not_zero.
 assumption.
Qed.

Corollary four_one_right : forall b, cmp Cle b (add b four) = true ->
cmp Cle (add b one) (add b four) = true.
Proof.
intros.
eapply int_le_trans.
eapply three_one_right.
eapply four_three_left.
assumption.
eapply four_three_right.
assumption.
Qed.

Corollary three_two_left : forall b, cmp Cle b (add b three) = true ->
cmp Cle b (add b two) = true.
Proof.
intros.
change two with (sub three one).
rewrite (add_commut b).
rewrite <- sub_add_l.
rewrite <- (add_commut b).
apply add_interval_reduce_big_right.
apply three_not_zero.
assumption.
Qed.

Corollary three_two_right : forall b, cmp Cle b (add b three) = true ->
cmp Cle (add b two) (add b three) = true.
Proof.
intros.
change two with (sub three one).
rewrite (add_commut b).
rewrite <- sub_add_l.
rewrite <- (add_commut b).
intros.
apply int_le_lt_weak.
apply add_interval_reduce_right.
apply three_not_zero.
assumption.
Qed.

Hint Resolve three_one_left three_one_right three_two_left three_two_right.

Theorem plus_positive :
forall a b, cmp Cle a (add a b) = true ->
cmp Cle zero b = true ->
signed (add a b) = signed a + signed b.
Proof.
introvars.
rewrite add_signed.
intros Hab Hb.
generalize (le_is_signed_le Hab).
clear Hab.
intro Hab.
generalize (le_is_signed_le Hb).
clear Hb.
intro Hb.
rewrite signed_repr.
trivial.
generalize (signed_range a).
change (signed zero) with 0 in Hb.
intros [H1 H2].
generalize (signed_range b).
intros [H3 H4].
change (min_signed) with (0 - half_modulus) in H1.
change (min_signed) with (0 - half_modulus) in H3.
change max_signed with (half_modulus - 1) in H2.
change max_signed with (half_modulus - 1) in H4.
assert (half_modulus > 0).
 compute; reflexivity.
change max_signed with (half_modulus - 1).
change min_signed with (0 - half_modulus).
split.
omega.
destruct (Z_le_gt_dec (signed a + signed b) (half_modulus - 1)).
assumption.
apply False_rect.
rewrite (eqm_samerepr (signed a + signed b) (signed a + signed b - modulus)) in Hab.
change modulus with (half_modulus + half_modulus) in Hab.
rewrite signed_repr in Hab.
omega.
clear Hab.
change max_signed with (half_modulus - 1).
change min_signed with (0 - half_modulus).
omega.
unfold eqm.
unfold eqmod.
exists 1.
rewrite Zmult_1_l.
omega.
Qed.

Theorem bounded_add_left : forall a b c, cmp Cle zero b = true -> cmp Cle b c = true ->
cmp Cle a (add a c) = true ->
cmp Cle a (add a b) = true.
Proof.
intros.
apply signed_le_is_le.
generalize (le_is_signed_le H).
change (signed zero) with 0.
intro.
rewrite add_signed.
rewrite signed_repr.
omega.
generalize (signed_range a).
intros [? ?].
split.
omega.
apply Zle_trans with (signed a + signed c).
generalize (le_is_signed_le H0).
omega.
rewrite <- plus_positive.
generalize (signed_range (add a c)); intros [? ?]; auto.
assumption.
repeat int_le_lt_trans_tac.
Qed.

Theorem bounded_add_right : forall a b c, cmp Cle zero b = true -> cmp Cle b c = true ->
cmp Cle a (add a c) = true ->
cmp Cle (add a b) (add a c) = true.
Proof.
intros.
apply signed_le_is_le.
assert (cmp Cle zero c = true).
 repeat int_le_lt_trans_tac.
generalize (le_is_signed_le H).
generalize (le_is_signed_le H2).
generalize (le_is_signed_le H0).
change (signed zero) with 0.
intros.
rewrite add_signed.
rewrite (plus_positive H1 H2).
rewrite signed_repr.
omega.
generalize (signed_range a).
intros [? ?].
split.
omega.
apply Zle_trans with (signed a + signed c).
omega.
rewrite <- plus_positive.
generalize (signed_range (add a c)); intros [? ?]; auto.
assumption.
repeat int_le_lt_trans_tac.
Qed.

Corollary minus_positive : forall a b, cmp Cle zero a = true -> cmp Cle a b = true ->
cmp Cle zero (sub b a) = true.
Proof.
intros.
apply signed_le_is_le.
change (signed zero) with 0.
cut (signed a <= signed (sub b a) + signed a).
omega.
rewrite <- plus_positive.
rewrite sub_add_id.
apply le_is_signed_le.
assumption.
2 : assumption.
rewrite sub_add_id.
case_eq (cmp Cle (sub b a) b); auto.
intro Habs.
generalize (le_false_lt_true Habs).
intro Hlt.
clear Habs.
assert (cmp Clt zero (sub b a) = true).
 repeat int_le_lt_trans_tac.
assert (signed b = signed (sub b a) + signed a).
 pattern b at 1.
 rewrite <- (sub_add_id b a).
 rewrite add_commut.
 rewrite Zplus_comm.
 apply plus_positive.
 rewrite add_commut.
 rewrite sub_add_id.
 assumption.
 apply int_le_lt_weak.
 assumption.
generalize (le_is_signed_le H).
generalize (lt_is_signed_lt Hlt).
generalize (le_is_signed_le H0).
change (signed zero) with 0.
intros; apply False_ind; omega.
Qed.

Corollary plus_positive_recip : forall a b, cmp Cle zero a = true -> cmp Cle a (add a b) = true ->
  cmp Cle zero b = true.
intros.
rewrite <- (add_sub_id b a).
apply minus_positive.
trivial.
rewrite add_commut.
trivial.
Qed.

Theorem minus_bounded : forall a b, cmp Cle zero a = true -> cmp Cle a b = true ->
  cmp Cle (sub b a) b = true.
Proof.
intros.
apply signed_le_is_le.
change (signed zero) with 0.
pattern b at -1.
rewrite <- (sub_add_id b a).
rewrite plus_positive.
generalize (le_is_signed_le H).
change (signed zero) with 0.
omega.
2 : assumption.
rewrite sub_add_id.
case_eq (cmp Cle (sub b a) b); auto.
intro Habs.
generalize (le_false_lt_true Habs).
intro Hlt.
clear Habs.
assert (cmp Clt zero (sub b a) = true).
 repeat int_le_lt_trans_tac.
assert (signed b = signed (sub b a) + signed a).
 pattern b at 1.
 rewrite <- (sub_add_id b a).
 rewrite add_commut.
 rewrite Zplus_comm.
 apply plus_positive.
 rewrite add_commut.
 rewrite sub_add_id.
 assumption.
 apply int_le_lt_weak.
 assumption.
generalize (le_is_signed_le H).
generalize (lt_is_signed_lt Hlt).
generalize (le_is_signed_le H0).
change (signed zero) with 0.
intros; apply False_ind; omega.
Qed.



(* 4 divides any size (but not necessarily addresses) *)

(*
Inductive modulo_four : int -> int -> Prop :=
| mod4_4_O : modulo_four zero four
| mod4_id : forall m, modulo_four m m
| mod4_add : forall m n, modulo_four m n -> forall p q, modulo_four p q -> modulo_four (add m p) (add n q)
| mod4_neg : forall m n, modulo_four m n -> modulo_four (neg m) (neg n).

Hint Constructors modulo_four.

Lemma modulo_four_ex : forall m n, modulo_four m n -> exists k, sub n m = mul four k.
Proof.
 induction 1.
 exists (one).
 auto.
 exists zero.
 rewrite sub_idem.
 auto.
 inversion IHmodulo_four1 as [k1 Hk1].
 inversion IHmodulo_four2 as [k2 Hk2].
 exists (add k1 k2).
 rewrite mul_add_distr_r.
 rewrite <- Hk1.
 rewrite <- Hk2.
 rewrite <- sub_add_l.
 rewrite sub_add_l.
 rewrite sub_add_r.
 rewrite sub_add_opp.
 rewrite sub_add_opp.
 rewrite sub_add_opp.
 rewrite add_assoc.
 rewrite add_assoc.
 rewrite add_assoc.
 f_equal.
 rewrite add_commut.
 rewrite add_assoc.
 rewrite add_commut.
 auto.
 inversion IHmodulo_four as [k Hk].
 exists (neg k).
 rewrite <- neg_mul_distr_r.
 rewrite <- Hk.
 rewrite sub_add_opp.
 rewrite sub_add_opp.
 symmetry.
 apply neg_add_distr.
Qed. *)




Inductive modulo_four : int -> int -> Prop :=
| mod4_intro : forall m n k, sub m n = mul four k -> modulo_four m n.

Lemma mod4_4_O : modulo_four zero four.
apply mod4_intro with (neg one).
rewrite <- neg_mul_distr_r.
trivial.
Qed.

Lemma mod4_id : forall m, modulo_four m m.
intro.
apply mod4_intro with zero.
rewrite sub_idem.
auto.
Qed.

Lemma mod4_add : forall m n, modulo_four m n -> forall p q, modulo_four p q -> modulo_four (add m p) (add n q).
intros m n Hmn p q Hpq.
destruct Hmn.
destruct Hpq.
apply mod4_intro with (add k k0).
 rewrite mul_add_distr_r.
 rewrite <- H.
 rewrite <- H0.
 rewrite <- sub_add_l.
 rewrite sub_add_l.
 rewrite sub_add_r.
 rewrite sub_add_opp.
 rewrite sub_add_opp.
 rewrite sub_add_opp.
 rewrite add_assoc.
 rewrite add_assoc.
 rewrite add_assoc.
 f_equal.
 rewrite add_commut.
 rewrite add_assoc.
 rewrite add_commut.
 auto.
Qed.

Lemma mod4_neg : forall m n, modulo_four m n -> modulo_four (neg m) (neg n).
intros m n Hmn.
destruct Hmn.
apply mod4_intro with (neg k).
 rewrite <- neg_mul_distr_r.
 rewrite <- H.
 rewrite sub_add_opp.
 rewrite sub_add_opp.
 symmetry.
 apply neg_add_distr.
Qed.

Hint Resolve mod4_4_O mod4_id mod4_add mod4_neg.


Lemma mod4_sym : forall m n, modulo_four m n -> modulo_four n m.
Proof.
induction 1 ; eauto.
apply mod4_intro with (neg k).
rewrite <- neg_mul_distr_r.
rewrite sub_anticommut.
f_equal.
auto.
Qed.

Corollary mod4_O_4 : modulo_four four zero.
Proof.
eapply mod4_sym; eauto.
Qed.

Hint Resolve mod4_O_4.

Lemma mod4_sub : forall m n, modulo_four m n -> forall p q, modulo_four p q -> modulo_four (sub m p) (sub n q).
Proof.
intros.
rewrite sub_add_opp.
rewrite sub_add_opp.
eauto.
Qed.

Hint Resolve mod4_sub.


Lemma mod4_trans : forall p q, modulo_four p q -> forall r, modulo_four q r -> modulo_four p r.
Proof.
destruct 1; destruct 1; eauto.
apply mod4_intro with (add k0 k).
rewrite <- (sub_add_id (sub m n) m0).
rewrite sub_permut.
rewrite H.
rewrite <- sub_add_l.
rewrite add_commut.
rewrite sub_add_l.
rewrite H0.
rewrite mul_add_distr_r.
auto.
Qed.

Hint Resolve mod4_trans.

Definition four_divides s := modulo_four s zero.

Lemma four_divides_four : four_divides four.
Proof.
 unfold four_divides; auto.
Qed.

Lemma four_divides_add_four : forall x, four_divides x ->
four_divides (add x four).
Proof.
unfold four_divides.
intros.
apply mod4_trans with four.
cut (four = add zero four).
intro Hf.
pattern four at 2.
rewrite Hf.
auto.
auto.
auto.
Qed.

Lemma four_divides_sub_four : forall x, four_divides x ->
four_divides (sub x four).
Proof.
unfold four_divides.
intros.
apply mod4_trans with (neg four).
rewrite <- sub_zero_r.
auto.
rewrite <- (neg_zero).
auto.
Qed.

Hint Resolve four_divides_add_four four_divides_sub_four.

Lemma four_divides_add_four_back : forall x, four_divides (add x four) ->
four_divides x.
Proof.
intros.
rewrite <- (add_sub_id x four).
auto.
Qed.

Lemma four_divides_sub_four_back : forall x, four_divides (sub x four) ->
four_divides x.
Proof.
intros.
rewrite <- (sub_add_id x four).
auto.
Qed.

Lemma modulo_four_four_divides_add : forall a k, four_divides k ->
modulo_four a (add a k).
Proof.
unfold four_divides.
intros.
pattern a at 1.
rewrite <- (add_zero a).
apply mod4_sym.
auto.
Qed.

Corollary modulo_four_four_divides_sub : forall a k, four_divides k ->
modulo_four (sub a k) a.
Proof.
intros.
pattern a at 2.
rewrite <- (sub_add_id a k).
eapply modulo_four_four_divides_add; eauto.
Qed.

Theorem four_divides_4_divides : forall x, four_divides (repr x) -> exists q, x = 4 * q.
Proof.
inversion 1.
subst.
genclear H0.
rewrite sub_zero_l.
unfold mul.
intro Habs.
generalize (samerepr_eqm Habs).
unfold eqm.
unfold eqmod.
change (unsigned four) with 4.
intros [k0 Hk0].
subst.
case_eq (Zdiv_eucl modulus 4).
intros q r Hqr.
assert (r = 0).
 genclear Hqr.
 simpl.
 injection 1; auto.
assert (4 > 0).
 omega.
subst.
generalize (Z_div_mod modulus 4 H1).
rewrite Hqr.
intros [Hmod ?].
rewrite Hmod.
rewrite Zplus_0_r.
rewrite Zmult_assoc.
rewrite (Zmult_comm k0).
rewrite <- Zmult_assoc.
rewrite <- (Zmult_plus_distr_r).
exists (k0 * q + unsigned k); trivial.
Qed.

Corollary modulo_four_modulo_4 : forall x y, modulo_four (repr x) (repr y) -> exists q, x - y = 4 * q.
Proof.
inversion 1.
subst.
genclear H0.
unfold sub.
assert (eqm (unsigned (repr x) - unsigned (repr y)) (x - y)) as Heq.
 apply eqm_sym.
 apply eqm_sub.
 apply eqm_unsigned_repr.
 apply eqm_unsigned_repr.
rewrite (eqm_samerepr _ _ Heq).
intros.
apply four_divides_4_divides.
unfold four_divides.
eapply mod4_intro.
rewrite sub_zero_l.
eassumption.
Qed.

Lemma mult_4_lt_reg : (forall x y, 4 * x < 4 * y -> x < y).
 intros x y. 
 repeat rewrite (Zmult_comm 4).
 intros Hxy.
 refine (Zmult_lt_reg_r _ _ _ _ Hxy).
 omega.
Qed .

Theorem four_does_not_divide_one : four_divides one -> False.
Proof.
intro Habs.
destruct (four_divides_4_divides Habs) as [k Hk].
cut (0 < k < 1).
 intros.
 omega .
split; (
 apply mult_4_lt_reg;
 rewrite <- Hk;
 omega 
).
Qed .

Corollary four_does_not_divide_neg_one : four_divides (neg one) -> False.
Proof.
intros.
apply four_does_not_divide_one .
unfold four_divides.
rewrite <- (neg_neg zero).
rewrite <- (neg_neg one).
apply mod4_neg.
change (neg zero) with zero.
auto.
Qed .

Corollary four_does_not_divide_three : four_divides three -> False.
Proof.
change three with (sub four one). 
unfold four_divides.
rewrite sub_add_opp.
rewrite add_commut.
intro Habs.
apply four_does_not_divide_neg_one.
unfold four_divides.
eapply mod4_trans.
apply modulo_four_four_divides_add.
apply four_divides_four.
assumption.
Qed .

Theorem four_does_not_divide_two : four_divides two -> False.
Proof.
intro Habs.
destruct (four_divides_4_divides Habs) as [k Hk].
cut (0 < k < 1).
 intros.
 omega .
split; (
 apply mult_4_lt_reg;
 rewrite <- Hk;
 omega 
).
Qed .

Theorem modulo_four_disjoint_blocks : forall b b', modulo_four b b' -> b <> b' -> (
signed b' + 4 <= (signed b)
  \/ (signed b) + 4 <= (signed b')
).
Proof.
intros b b' Hbb' Hneq.
rewrite <- (repr_signed b') in Hbb'.
rewrite <- (repr_signed b) in Hbb'.
generalize (modulo_four_modulo_4 Hbb').
intros [q Hq].
clear Hbb'.
assert (signed b <> signed b').
intro.
destruct Hneq.
rewrite <- (repr_signed b').
rewrite <- (repr_signed b).
congruence.
clear Hneq.
replace (signed b) with (4 * q + signed b'); omega.
Qed.

Section modulo_four_le.

Variables a b : int.
Hypothesis Hmod4 : modulo_four a b.
Hypothesis Hle : cmp Cle a (sub b one) = true.

Let L1 : cmp Clt a (sub b one) = true.
apply lt_is_le_neq.
assumption.
intro Habs.
subst.
apply four_does_not_divide_neg_one.
unfold four_divides.
rewrite <- (sub_idem b).
rewrite <- (add_sub_id (neg one) b).
apply mod4_sub.
rewrite add_commut.
rewrite <- sub_add_opp.
assumption.
auto.
Qed .

Let L2 : cmp Clt a (sub b two) = true.
Proof.
apply lt_is_le_neq.
 rewrite sub_add_opp.
 change two with (add one one).
 rewrite neg_add_distr.
 rewrite <- add_assoc.
 rewrite <- sub_add_opp.
 rewrite <- sub_add_opp.
 apply lt_is_le_p.
 assumption.
intro Habs.
subst.
apply four_does_not_divide_two.
unfold four_divides.
rewrite <- (neg_neg zero).
rewrite <- (neg_neg two).
apply mod4_neg.
change (neg zero) with zero.
rewrite <- (sub_idem b).
rewrite <- (add_sub_id (neg two) b).
apply mod4_sub.
rewrite add_commut.
rewrite <- sub_add_opp.
assumption.
auto.
Qed.

Let L3 : cmp Clt a (sub b three) = true.
Proof.
apply lt_is_le_neq.
 rewrite sub_add_opp.
 change three with (add two one).
 rewrite neg_add_distr.
 rewrite <- add_assoc.
 rewrite <- sub_add_opp.
 rewrite <- sub_add_opp.
 apply lt_is_le_p.
 assumption.
intro Habs.
subst.
apply four_does_not_divide_three.
unfold four_divides.
rewrite <- (neg_neg zero).
rewrite <- (neg_neg three).
apply mod4_neg.
change (neg zero) with zero.
rewrite <- (sub_idem b).
rewrite <- (add_sub_id (neg three) b).
apply mod4_sub.
rewrite add_commut.
rewrite <- sub_add_opp.
assumption.
auto.
Qed.

Lemma modulo_four_le_m1_left :
cmp Cle a (sub b four) = true.
Proof.
rewrite sub_add_opp.
change four with (add three one).
rewrite neg_add_distr.
rewrite <- add_assoc.
rewrite <- sub_add_opp.
rewrite <- sub_add_opp.
apply lt_is_le_p.
assumption.
Qed.

Let M4 : cmp Clt (sub b four) (sub b three) = true.
change four with (add one three).
rewrite sub_add_r.
rewrite <- sub_add_opp.
eapply lt_step_p.
 eassumption.
Qed.

Let M3 : cmp Clt (sub b three) (sub b two) = true.
change three with (add one two).
rewrite sub_add_r.
rewrite <- sub_add_opp.
eapply lt_step_p.
 eassumption.
Qed.

Let M2 : cmp Clt (sub b two) (sub b one) = true.
change two with (add one one).
rewrite sub_add_r.
rewrite <- sub_add_opp.
eapply lt_step_p.
eassumption.
Qed.

Lemma modulo_four_le_m1_right :
cmp Cle (sub b four) (sub b one) = true.
Proof.
apply int_le_lt_weak.
repeat int_le_lt_trans_tac.
Qed .

Let N1 : cmp Clt a (add a one) = true.
eapply lt_step.
eassumption.
Qed. 

Let N2 : cmp Clt (add a one) (add a two) = true.
change two with (add one one).
rewrite <- add_assoc.
eapply lt_step.
eapply int_le_lt_trans.
eapply lt_is_le_s.
eexact L3.
eassumption.
Qed .


Let N3 : cmp Clt (add a two) (add a three) = true.
change three with (add two one).
rewrite <- add_assoc.
eapply lt_step.
change two with (add one one).
rewrite <- add_assoc.
eapply int_le_lt_trans.
eapply lt_is_le_s.
eapply int_le_lt_trans.
eapply lt_is_le_s.
eexact L3.
eassumption.
eassumption.
Qed .

Lemma modulo_four_three_left : 
cmp Cle a (add a three) = true.
Proof.
repeat int_le_lt_trans_tac; eauto.
Qed.

Let P1 : cmp Clt (add a one) (sub b two) = true.
eapply int_le_lt_trans.
eapply lt_is_le_s.
eexact L3.
assumption.
Qed .

Let P2 : cmp Clt (add a two) (sub b one) = true.
eapply int_le_lt_trans.
change two with (add one one).
rewrite <- add_assoc.
eapply lt_is_le_s.
eexact P1.
assumption.
Qed.

Lemma modulo_four_three_right : 
cmp Cle (add a three) (sub b one) = true.
Proof.
change three with (add two one).
rewrite <- add_assoc.
apply lt_is_le_s.
assumption.
Qed.

Lemma modulo_four_le_eq_or_next_3 :
{add a four = b} + {cmp Cle a (add a four) = true /\ 
cmp Cle (add a four) (sub b one) = true
}.
Proof.
destruct (eq_dec (add a four) b).
 auto.
right.
assert (cmp Clt (add a three) (sub b one) = true).
 apply lt_is_le_neq.
 apply modulo_four_three_right.
 change three with (sub four one).
 rewrite add_commut.
 rewrite <- sub_add_l.
 repeat rewrite sub_add_opp.
 intro.
 generalize (add_reg_r H).
 rewrite add_commut; congruence.
split.
 apply (int_le_trans (int_le_lt_weak N1)).
 apply (int_le_trans (int_le_lt_weak N2)).
 apply (int_le_trans (int_le_lt_weak N3)).
 change four with (add three one).
 rewrite <- add_assoc.
 apply int_le_lt_weak.
 eapply lt_step.
 eassumption.
change four with (add three one).
rewrite <- add_assoc.
apply lt_is_le_s.
assumption.
Defined. 


Corollary modulo_four_le_eq_or_next_2 :
{add a four = b} + {cmp Cle a (add a four) = true /\ cmp Cle a (sub b four) = true /\
cmp Cle (sub b four) (sub b one) = true /\
cmp Cle (add a four) (sub b one) = true
}.
Proof.
destruct (modulo_four_le_eq_or_next_3).
left; auto.
right.
invall.
split.
assumption.
split.
apply modulo_four_le_m1_left.
auto.
auto.
split.
eapply modulo_four_le_m1_right.
eassumption.
Defined.

End modulo_four_le.

Corollary modulo_four_le_eq_or_next : forall a b, modulo_four a b ->
cmp Cle a b = true ->
{a = b} + {cmp Cle a (add a four) = true /\ 
cmp Cle a (sub b four) = true /\ cmp Cle (sub b four) b = true /\
cmp Cle (add a four) b = true}.
Proof.
intros a b Hmod Hle.
destruct (le_is_lt_or_eq Hle).
left; assumption.
right.
generalize (lt_is_le_p e).
intro Hle'.
generalize (lt_step_p e).
intro Hlt_b.
destruct (modulo_four_le_eq_or_next_2 Hmod Hle').
subst.
split.
assumption.
split.
rewrite add_sub_id.
auto.
split.
rewrite add_sub_id.
assumption.
auto.
inversion a0.
inversion H0.
inversion H2.
split; auto.
split; auto.
split; int_le_lt_trans_tac; auto.
Defined.

Lemma modulo_four_in_three_eq : forall a b, modulo_four a b ->
cmp Cle a b = true -> cmp Cle b (add a three)= true-> a = b.
Proof.
intros a b Hmod Hle Hhi.
destruct (modulo_four_le_eq_or_next Hmod Hle).
assumption.
inversion a0.
inversion H0.
inversion H2.
generalize (add_reg_l (int_le_antisym (four_three_right H) (int_le_trans H4 Hhi))).
inversion 1.
Qed.