proposition: Lemma BDDshare_put_preserves_nodes : forall (share : BDDsharing_map) (x x' : BDDvar) (l l' r r' counter counter' : ad), BDDshare_lookup share x' l' r' = Some counter' -> (x, (l, r)) <> (x', (l', r')) -> BDDshare_lookup (BDDshare_put share x l r counter) x' l' r' = Some counter'.
proof: Proof. intros share x x' l l' r r' counter counter' H H0. cut (N.eqb l l' = true \/ N.eqb l l' = false). cut (N.eqb r r' = true \/ N.eqb r r' = false). cut (N.eqb x x' = true \/ N.eqb x x' = false). intros H1 H2 H3. cut (N.eqb x x' = false \/ N.eqb l l' = false \/ N.eqb r r' = false). intro H4. unfold BDDshare_lookup in |- *. unfold BDDshare_lookup in H. unfold BDDshare_put in |- *. rewrite (MapPut_semantics (Map (Map ad)) share l (MapPut (Map ad) match MapGet (Map (Map ad)) share l with | None => newMap (Map ad) | Some y => y end r (MapPut ad match MapGet (Map ad) match MapGet (Map (Map ad)) share l with | None => newMap (Map ad) | Some y => y end r with | None => newMap ad | Some y => y end x counter)) l'). elim H3. intro H5. rewrite H5. clear H3. cut (l = l'). intro H3. rewrite <- H3 in H. elim (option_sum _ (MapGet (Map (Map ad)) share l)). intro y. elim y. clear y. intros x0 y. rewrite y. rewrite y in H. elim H2. intro H6. cut (r = r'). intro H7. rewrite (MapPut_semantics (Map ad) x0 r (MapPut ad match MapGet (Map ad) x0 r with | None => newMap ad | Some y => y end x counter) r'). rewrite H6. elim (option_sum _ (MapGet (Map ad) x0 r')). intro y0. elim y0. clear y0. intros x1 y0. rewrite y0 in H. elim (option_sum _ (MapGet ad x1 x')). intros y1. elim y1. clear y1. intros x2 y1. rewrite y1 in H. rewrite <- H7 in y0. rewrite y0. elim H1. intros H8. rewrite H3 in H0. rewrite H7 in H0. cut (x = x'). intro H9. rewrite H9 in H0. cut False. tauto. apply H0. reflexivity. apply Neqb_complete. assumption. intros H8. rewrite (MapPut_semantics ad x1 x counter x'). rewrite H8. rewrite y1. assumption. intro y1. rewrite y1 in H. discriminate H. intro y0. rewrite y0 in H. discriminate H. apply Neqb_complete. assumption. intros H6. rewrite (MapPut_semantics (Map ad) x0 r (MapPut ad match MapGet (Map ad) x0 r with | None => newMap ad | Some y => y end x counter) r'). rewrite H6. assumption. intro y. rewrite y in H. discriminate H. apply Neqb_complete. assumption. intro H5. rewrite H5. assumption. elim H1. intro H4. cut (x = x'). intro H5. elim H2. intro H6. cut (r = r'). intro H7. elim H3. intro H8. cut (l = l'). intro H9. rewrite H5 in H0. rewrite H7 in H0. rewrite H9 in H0. cut False. tauto. apply H0. trivial. apply Neqb_complete. assumption. auto. apply Neqb_complete. assumption. auto. apply Neqb_complete. assumption. auto. elim (N.eqb x x'). auto. auto. elim (N.eqb r r'). auto. auto. elim (N.eqb l l'). auto. auto. Qed.
imports: Bool Sumbool Arith ZArith NArith Nnat Ndec Ndigits IntMap(Allmaps) Wf_nat BDDvar_ad_nat