Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import ZArith NArith Nnat Ndec Ndigits.
Require Import Allmaps.
Definition BDDzero := N0.
Definition BDDone := Npos 1.

Definition BDDcompare (x y : BDDvar) :=
match x, y with
| N0, N0Datatypes.Eq
| N0, Npos _Datatypes.Lt
| Npos _, N0Datatypes.Gt
| Npos p1, Npos p2Pcompare p1 p2 Datatypes.Eq
end.

Definition BDDvar_eq := Neqb.

match a with
| N0Npos 1
| Npos pNpos (Psucc p)
end.

Proof.
simple induction a. reflexivity.
simpl in |- ×. unfold nat_of_P in |- ×. intro p. exact (Pmult_nat_succ_morphism p 1).
Qed.

Lemma lt_pred : x y : nat, x < yx 0 → pred x < pred y.
Proof.
simple induction x. intros y H H0. absurd (0 = 0). assumption. reflexivity. intros n H y H0 H1.
apply lt_pred. assumption.
Qed.

Lemma O_N0 : x : ad, nat_of_N x = 0 → x = N0.
Proof.
cut (0 = nat_of_N N0). intro H. rewrite H. intros x H0. replace x with (N_of_nat (nat_of_N x)).
replace N0 with (N_of_nat (nat_of_N N0)). rewrite H0. reflexivity.
rewrite (N_of_nat_of_N N0). reflexivity. rewrite (N_of_nat_of_N x).
reflexivity. reflexivity.
Qed.
Lemma INFERIEUR_neq_O :
x y : ad, BDDcompare x y = Datatypes.Lty N0.
Proof.
double induction x y. simpl in |- ×. intro; discriminate. unfold not in |- *; intros.
discriminate. simpl in |- ×. intros; discriminate. unfold not in |- *; intros. discriminate.
Qed.

Lemma BDDcompare_trans :
x y z : BDDvar,
BDDcompare x y = Datatypes.Lt
BDDcompare y z = Datatypes.LtBDDcompare x z = Datatypes.Lt.
Proof.
double induction x y. simpl in |- ×. intros z H H0. discriminate H. simpl in |- ×. intro p.
simple induction z. intros H H0. discriminate H0. trivial. simpl in |- ×. intros p z H H0.
discriminate H. intro p. intro p0. simple induction z. simpl in |- ×. trivial. intro p1.
simpl in |- ×. intros H H0. cut (nat_of_P p0 < nat_of_P p).
cut (nat_of_P p < nat_of_P p1). intros H1 H2.
apply nat_of_P_lt_Lt_compare_complement_morphism. apply lt_trans with (m := nat_of_P p).
assumption. assumption. apply nat_of_P_lt_Lt_compare_morphism. assumption.
apply nat_of_P_lt_Lt_compare_morphism. assumption.
Qed.

x y : ad, Nleb (ad_S x) y = trueNleb x y = true.
Proof.
intros x y H. cut (Nleb x (ad_S x) = true). intro H0.
apply Nleb_trans with (b := ad_S x). assumption. assumption. unfold Nleb in |- ×.
apply leb_correct. rewrite (ad_S_is_S x). apply le_S. apply le_n.
Qed.

Lemma le_then_le_S :
x y : ad, Nleb x y = trueNleb x (ad_S y) = true.
Proof.
intros x y H. cut (Nleb y (ad_S y) = true). intro H0. apply Nleb_trans with (b := y).
assumption. assumption. unfold Nleb in |- ×. apply leb_correct. rewrite (ad_S_is_S y).
apply le_S. apply le_n.
Qed.

x y : ad, Nleb (ad_S x) y = trueNeqb x y = false.
Proof.
intros x y H. cut (Neqb x y = true Neqb x y = false). intro H0. elim H0.
clear H0. intro H0. cut (x = y). intro H1. rewrite H1 in H. unfold Nleb in H.
cut (leb (S (nat_of_N y)) (nat_of_N y) = false). rewrite H. intro H2.
discriminate H2. cut (nat_of_N y < S (nat_of_N y)). intro H2.
apply leb_correct_conv. assumption. unfold lt in |- ×. trivial.
apply Neqb_complete. assumption. trivial. elim (Neqb x y). auto. auto.
Qed.

Lemma BDDcompare_succ :
a : BDDvar, BDDcompare a (ad_S a) = Datatypes.Lt.
Proof.
simple induction a. simpl in |- ×. trivial. simpl in |- ×. intro p.
cut (nat_of_P p < nat_of_P (Psucc p)). intro H.
apply nat_of_P_lt_Lt_compare_complement_morphism. assumption.
cut (nat_of_P (Psucc p) = 1 + nat_of_P p). intro H. rewrite H.
simpl in |- ×. unfold lt in |- ×. trivial. unfold nat_of_P in |- ×. apply Pmult_nat_succ_morphism.
Qed.

Lemma BDDcompare_lt :
x y : BDDvar,
BDDcompare x y = Datatypes.Ltnat_of_N x < nat_of_N y.
Proof.
double induction x y. simpl in |- ×. intro H. discriminate. simpl in |- ×. intros p H.
cut ( h : nat, nat_of_P p = S h). intro H0. inversion H0. rewrite H1.
apply lt_O_Sn. apply ZL4. simpl in |- ×. intros p H. discriminate. simpl in |- ×. intros p p0 H.
apply nat_of_P_lt_Lt_compare_morphism. assumption.
Qed.

Lemma BDDlt_compare :
x y : BDDvar,
nat_of_N x < nat_of_N yBDDcompare x y = Datatypes.Lt.
Proof.
double induction x y. simpl in |- ×. intro H. absurd (0 < 0). apply lt_n_O. assumption.
simpl in |- ×. reflexivity. simpl in |- ×. intro p. cut ( h : nat, nat_of_P p = S h). intro H.
inversion H. rewrite H0. intro H1. absurd (S x0 < 0). apply lt_n_O.
assumption. apply ZL4. simpl in |- ×. intro p. intros p0 H. apply nat_of_P_lt_Lt_compare_complement_morphism.
assumption.
Qed.

Lemma relation_sum :
r : Datatypes.comparison,
{r = Datatypes.Eq} + {r = Datatypes.Lt} + {r = Datatypes.Gt}.
Proof.
intro r. elim r. left; left; reflexivity. left; right; reflexivity. right; reflexivity.
Qed.

Lemma BDD_EGAL_complete :
x y : BDDvar, BDDcompare x y = Datatypes.Eqx = y.
Proof.
double induction x y. reflexivity. simpl in |- ×. intros; discriminate. simpl in |- ×.
intros; discriminate. simpl in |- ×. intros p p0 H. cut (p0 = p). intro H0. rewrite H0; reflexivity.
apply Pcompare_Eq_eq. assumption.
Qed.

Lemma lt_trans_1 : x y z : nat, x < yy < S zx < z.
Proof.
intros x y z H H0. unfold lt in H0. unfold lt in H. unfold lt in |- ×.
apply le_trans with (m := y). assumption. apply le_S_n. assumption.
Qed.

Lemma BDDcompare_sup_inf :
x y : BDDvar,
BDDcompare x y = Datatypes.GtBDDcompare y x = Datatypes.Lt.
Proof.
double induction x y. simpl in |- ×. intro; discriminate. simpl in |- ×. intro p. intro; discriminate.
simpl in |- ×. reflexivity. unfold BDDcompare in |- ×. intros p p0 H. apply ZC1. assumption.
Qed.

Lemma BDDcompare_1 :
x y : BDDvar,
BDDcompare x y = Datatypes.Lt
Proof.
intros x y H. elim (relation_sum (BDDcompare (ad_S x) y)). intro y0. elim y0; intro.
right. apply BDD_EGAL_complete. assumption. left; assumption. intro y0.
absurd (nat_of_N x < nat_of_N x). apply lt_irrefl. apply lt_trans_1 with (y := nat_of_N y).
apply BDDcompare_lt. assumption. rewrite <- (ad_S_is_S x). apply BDDcompare_lt.
apply BDDcompare_sup_inf. assumption.
Qed.

Definition max (m n : nat) := if leb m n then n else m.

Lemma lt_max_1_2 :
x1 y1 x2 y2 : nat, x1 < x2y1 < y2max x1 y1 < max x2 y2.
Proof.
intros x1 y1 x2 y2 H H0. unfold max in |- ×. elim (sumbool_of_bool (leb x2 y2)). intro y. rewrite y.
elim (leb x1 y1). assumption. apply lt_le_trans with (m := x2). assumption.
apply leb_complete. assumption. intro y. rewrite y. elim (leb x1 y1).
apply lt_trans with (m := y2). assumption. apply leb_complete_conv. assumption.
assumption.
Qed.

Lemma lt_max_2 :
x1 y1 x2 y2 : nat, x1 < y2y1 < y2max x1 y1 < max x2 y2.
Proof.
intros x1 y1 x2 y2 H H0. unfold max in |- ×. elim (leb x1 y1). elim (sumbool_of_bool (leb x2 y2)).
intro y. rewrite y. assumption. intro y. rewrite y. apply lt_trans with (m := y2).
assumption. apply leb_complete_conv. assumption. elim (sumbool_of_bool (leb x2 y2)).
intro y. rewrite y. assumption. intro y. rewrite y. apply lt_trans with (m := y2).
assumption. apply leb_complete_conv. assumption.
Qed.

Lemma lt_max_12 :
x1 y1 x2 y2 : nat, x1 < x2y1 < x2max x1 y1 < max x2 y2.
Proof.
intros x1 y1 x2 y2 H H0. unfold max in |- ×. elim (leb x1 y1). elim (sumbool_of_bool (leb x2 y2)); intro y; rewrite y.
apply lt_le_trans with (m := x2). assumption. apply leb_complete; assumption.
assumption. elim (sumbool_of_bool (leb x2 y2)). intro y. rewrite y. apply lt_le_trans with (m := x2).
assumption. apply leb_complete; assumption. intro y; rewrite y. assumption.
Qed.

Lemma BDDcompare_eq :
x y : BDDvar, BDDcompare x y = Datatypes.Eqx = y.
Proof.
double induction x y. reflexivity. simpl in |- ×. intros; discriminate. simpl in |- ×.
intros; discriminate. simpl in |- ×. intros p p0 H. cut (p0 = p). intro H0. rewrite H0; reflexivity.
apply Pcompare_Eq_eq. assumption.
Qed.