proposition: Lemma BDDalloc_keeps_sharing_OK : forall (cfg : BDDconfig) (l r : ad) (x : BDDvar), BDDconfig_OK cfg -> node_OK (fst cfg) l -> node_OK (fst cfg) r -> (forall (x' : BDDvar) (l' r' a : ad), MapGet _ (fst cfg) a = Some (x', (l', r')) -> (x, (l, r)) <> (x', (l', r'))) -> BDDsharing_OK (fst (fst (BDDalloc cfg x l r))) (fst (snd (fst (BDDalloc cfg x l r)))).
proof: Proof. intro cfg. elim cfg. clear cfg. intro bs. intro y. elim y. clear y. intros share counter. split. simpl in |- *. intros H3. cut (BDDshare_lookup share x0 l0 r0 = Some a \/ (x, (l, r)) = (x0, (l0, r0))). intros H4. elim H4. clear H4. intros H4. cut (MapGet _ bs a = Some (x0, (l0, r0))). intro H5. change (MapGet (BDDvar * (ad * ad)) (fst (fst (BDDalloc (bs, (share, counter)) x l r))) a = Some (x0, (l0, r0))) in |- *. apply BDDalloc_preserves_nodes. assumption. exact H5. lapply (BDDsharing_lookup_semantics bs share a l0 r0 x0). intro H5. elim H5. clear H5. intros H5 H6. apply H5. assumption. exact (proj1 (proj2 H)). intro H5. clear H4. rewrite <- H5. injection H5. intros H4 H6 H7. rewrite <- H4 in H3. rewrite <- H6 in H3. rewrite <- H7 in H3. rewrite (BDDshare_put_puts share x l r counter) in H3. injection H3. intro H8. rewrite (MapPut_semantics (BDDvar * (ad * ad)) bs counter (x, (l, r)) a). cut (N.eqb counter a = true). intro H9. rewrite H9. trivial. rewrite H8. apply Neqb_correct. apply BDDshare_put_no_new_node with (x' := x0) (l' := l0) (r' := r0) (counter := counter). assumption. intro H3. cut (a = snd (snd (bs, (share, counter))) \/ MapGet _ (fst (bs, (share, counter))) a = Some (x0, (l0, r0))). intro H4. elim H4. clear H4. intro H4. cut ((x0, (l0, r0)) = (x, (l, r))). intro H5. injection H5. intros H6 H7 H8. rewrite H6. rewrite H7. rewrite H8. simpl in |- *. simpl in H4. rewrite H4. apply BDDshare_put_puts. simpl in H3. rewrite (MapPut_semantics (BDDvar * (ad * ad)) bs counter (x, (l, r)) a) in H3. simpl in H4. cut (N.eqb counter a = true). intros H5. rewrite H5 in H3. inversion H3. trivial. rewrite H4. apply Neqb_correct. intro H5. clear H4. cut (BDDshare_lookup (fst (snd (bs, (share, counter)))) x0 l0 r0 = Some a). intro H4. simpl in |- *. simpl in H4. apply BDDshare_put_preserves_nodes. assumption. apply H2 with (a := a). assumption. elim H. intros H4 H6. elim H6. intros. simpl in |- *. simpl in H5. unfold BDDsharing_OK in H7. unfold iff in H7. apply (proj2 (H7 x0 l0 r0 a)). assumption. apply BDDalloc_no_new_node with (x := x) (l := l) (r := r). assumption. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat