proposition: Lemma BDDmake_bool_fun : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), BDDconfig_OK cfg -> config_node_OK cfg l -> config_node_OK cfg r -> (is_internal_node cfg l -> BDDcompare (var cfg l) x = Datatypes.Lt) -> (is_internal_node cfg r -> BDDcompare (var cfg r) x = Datatypes.Lt) -> bool_fun_eq (bool_fun_of_BDD (fst (BDDmake cfg x l r)) (snd (BDDmake cfg x l r))) (bool_fun_if x (bool_fun_of_BDD cfg r) (bool_fun_of_BDD cfg l)).
proof: Proof. intros cfg l r x H H0 H1 H2 H3. cut (forall (xl : BDDvar) (ll rl : ad), MapGet _ (fst cfg) l = Some (xl, (ll, rl)) -> BDDcompare xl x = Datatypes.Lt). cut (forall (xr : BDDvar) (lr rr : ad), MapGet _ (fst cfg) r = Some (xr, (lr, rr)) -> BDDcompare xr x = Datatypes.Lt). intros H4 H5. cut (node_OK (fst cfg) l). cut (node_OK (fst cfg) r). intros H6 H7. cut (BDDconfig_OK (fst (BDDmake cfg x l r)) /\ (N.eqb l r = false -> MapGet _ (fst (fst (BDDmake cfg x l r))) (snd (BDDmake cfg x l r)) = Some (x, (l, r))) /\ (N.eqb l r = true -> snd (BDDmake cfg x l r) = l) /\ (forall (a l' r' : ad) (x' : BDDvar), (MapGet _ (fst (fst (BDDmake cfg x l r))) a = Some (x', (l', r')) -> MapGet _ (fst cfg) a = Some (x', (l', r')) \/ snd (BDDmake cfg x l r) = a) /\ (MapGet _ (fst cfg) a = Some (x', (l', r')) -> MapGet _ (fst (fst (BDDmake cfg x l r))) a = Some (x', (l', r')))) /\ node_OK (fst (fst (BDDmake cfg x l r))) (snd (BDDmake cfg x l r))). intros H8. elim H8; clear H8; intros. elim H9; clear H9; intros. elim H10; clear H10; intros. elim H11; clear H11; intros. elim (sumbool_of_bool (N.eqb l r)). intro y. rewrite (H10 y). apply bool_fun_eq_trans with (bf2 := bool_fun_of_BDD cfg l). apply bool_fun_preservation. assumption. assumption. intros x0 l0 r0 a H13. exact (proj2 (H11 a l0 r0 x0) H13). assumption. cut (l = r). intro H13. rewrite <- H13. unfold bool_fun_if in |- *. unfold bool_fun_eq in |- *. unfold bool_fun_eval in |- *. intro vb. elim (vb x). simpl in |- *. reflexivity. simpl in |- *. reflexivity. apply Neqb_complete. assumption. intro y. cut (is_internal_node (fst (BDDmake cfg x l r)) (snd (BDDmake cfg x l r))). intro H13. rewrite (proj2 (proj2 (bool_fun_of_BDD_semantics (fst (BDDmake cfg x l r)) H8)) (snd (BDDmake cfg x l r)) H13). unfold bool_fun_eq in |- *. intro vb. unfold bool_fun_eval in |- *. unfold var in |- *. rewrite (H9 y). unfold bool_fun_if in |- *. unfold ifb in |- *. unfold high, low in |- *. rewrite (H9 y). cut (bool_fun_eq (bool_fun_of_BDD (fst (BDDmake cfg x l r)) r) (bool_fun_of_BDD cfg r)). cut (bool_fun_eq (bool_fun_of_BDD (fst (BDDmake cfg x l r)) l) (bool_fun_of_BDD cfg l)). intros H14 H15. unfold bool_fun_eq in H14, H15. unfold bool_fun_eval in H14, H15. rewrite (H14 vb). rewrite (H15 vb). reflexivity. apply bool_fun_preservation. assumption. assumption. intros x0 l0 r0 a H14. exact (proj2 (H11 a l0 r0 x0) H14). assumption. apply bool_fun_preservation. assumption. intros. assumption. intros x0 l0 r0 a H14. exact (proj2 (H11 a l0 r0 x0) H14). assumption. split with x. split with l. split with r. apply H9. assumption. apply BDDmake_semantics. assumption. assumption. assumption. assumption. assumption. assumption. assumption. intros xr lr rr H4. intros. unfold is_internal_node in H3. unfold var in H3. rewrite H4 in H3. apply H3. split with xr. split with lr. split with rr. reflexivity. intros xl ll rl H4. unfold is_internal_node in H2. unfold var in H2. rewrite H4 in H2. apply H2. split with xl. split with ll. split with rl. reflexivity. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat bdd1 bdd2 bdd3 bdd4 bdd5_1 bdd5_2