proposition: Lemma BDDalloc_semantics : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), BDDconfig_OK cfg -> node_OK (fst cfg) l -> node_OK (fst cfg) r -> N.eqb l r <> true -> (forall (xl : BDDvar) (ll rl : ad), MapGet _ (fst cfg) l = Some (xl, (ll, rl)) -> BDDcompare xl x = Datatypes.Lt) -> (forall (xr : BDDvar) (lr rr : ad), MapGet _ (fst cfg) r = Some (xr, (lr, rr)) -> BDDcompare xr x = Datatypes.Lt) -> (forall (x' : BDDvar) (l' r' a : ad), MapGet _ (fst cfg) a = Some (x', (l', r')) -> (x, (l, r)) <> (x', (l', r'))) -> BDDconfig_OK (fst (BDDalloc cfg x l r)) /\ MapGet _ (fst (fst (BDDalloc cfg x l r))) (snd (BDDalloc cfg x l r)) = Some (x, (l, r)) /\ (forall (a l' r' : ad) (x' : BDDvar), (MapGet _ (fst (fst (BDDalloc cfg x l r))) a = Some (x', (l', r')) -> MapGet _ (fst cfg) a = Some (x', (l', r')) \/ snd (BDDalloc cfg x l r) = a) /\ (MapGet _ (fst cfg) a = Some (x', (l', r')) -> MapGet _ (fst (fst (BDDalloc cfg x l r))) a = Some (x', (l', r')))) /\ node_OK (fst (fst (BDDalloc cfg x l r))) (snd (BDDalloc cfg x l r)).
proof: Proof. intro cfg. elim cfg. clear cfg. intros bs y. elim y. clear y. intros share counter l r x. intros. split. unfold BDDconfig_OK in |- *. simpl in |- *. split. change (BDDstate_OK (fst (fst (BDDalloc (bs, (share, counter)) x l r)))) in |- *. apply BDDalloc_keeps_state_OK. assumption. assumption. assumption. assumption. assumption. assumption. split. change (BDDsharing_OK (fst (fst (BDDalloc (bs, (share, counter)) x l r))) (fst (snd (fst (BDDalloc (bs, (share, counter)) x l r))))) in |- *. apply BDDalloc_keeps_sharing_OK. assumption. assumption. assumption. assumption. change ((forall a : ad, Nleb (snd (snd (fst (BDDalloc (bs, (share, counter)) x l r)))) a = true -> MapGet _ (fst (fst (BDDalloc (bs, (share, counter)) x l r))) a = None) /\ Nleb (ad_S (ad_S N0)) (snd (snd (fst (BDDalloc (bs, (share, counter)) x l r)))) = true) in |- *. apply BDDalloc_adjusts_counter. assumption. assumption. split. apply BDDalloc_allocates. split. split. cut (MapGet (BDDvar * (ad * ad)) (fst (fst (BDDalloc (bs, (share, counter)) x l r))) a = Some (x', (l', r')) -> a = snd (BDDalloc (bs, (share, counter)) x l r) \/ MapGet (BDDvar * (ad * ad)) (fst (bs, (share, counter))) a = Some (x', (l', r'))). intros H6 H7. cut (a = snd (BDDalloc (bs, (share, counter)) x l r) \/ MapGet (BDDvar * (ad * ad)) (fst (bs, (share, counter))) a = Some (x', (l', r'))). intro H8. elim H8. right. rewrite H9. trivial. auto. apply H6. assumption. intro H6. cut (a = snd (snd (bs, (share, counter))) \/ MapGet _ (fst (bs, (share, counter))) a = Some (x', (l', r'))). tauto. apply BDDalloc_no_new_node with (x := x) (l := l) (r := r). assumption. exact (BDDalloc_preserves_nodes (bs, (share, counter)) l r x H a l' r' x'). unfold node_OK in |- *. right. right. unfold in_dom in |- *. simpl in |- *. rewrite (MapPut_semantics (BDDvar * (ad * ad)) bs counter (x, (l, r)) counter) . cut (N.eqb counter counter = true). intro H6. rewrite H6. trivial. apply Neqb_correct. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat