proposition: Lemma BDDshare_put_no_new_node : forall (share : BDDsharing_map) (x x' : BDDvar) (l l' r r' counter counter' : ad), BDDshare_lookup (BDDshare_put share x l r counter) x' l' r' = Some counter' -> BDDshare_lookup share x' l' r' = Some counter' \/ (x, (l, r)) = (x', (l', r')).
proof: Proof. intros share x x' l l' r r' counter counter'. unfold BDDshare_put in |- *. elim (option_sum _ (MapGet (Map (Map ad)) share l)). intro y. elim y. clear y. intros x0 y H. rewrite y in H. elim (option_sum _ (MapGet (Map ad) x0 r)). intro y0. elim y0. clear y0. intros x1 y0. rewrite y0 in H. unfold BDDshare_lookup in |- *. unfold BDDshare_lookup in H. rewrite (MapPut_semantics (Map (Map ad)) share l (MapPut (Map ad) x0 r (MapPut ad x1 x counter)) l') in H. cut (N.eqb l l' = true \/ N.eqb l l' = false). intro H0. elim H0. clear H0. intro H0. rewrite H0 in H. rewrite (MapPut_semantics (Map ad) x0 r (MapPut ad x1 x counter) r') in H. cut (N.eqb r r' = true \/ N.eqb r r' = false). intro H1. elim H1. clear H1. intro H1. rewrite H1 in H. rewrite (MapPut_semantics ad x1 x counter x') in H. cut (N.eqb x x' = true \/ N.eqb x x' = false). intro H2. elim H2. clear H2. intro H2. rewrite H2 in H. right. cut (x = x'). cut (l = l'). cut (r = r'). intros H3 H4 H5. rewrite H3. rewrite H4. rewrite H5. trivial. apply Neqb_complete. assumption. apply Neqb_complete. assumption. apply Neqb_complete. assumption. intro H3. rewrite H3 in H. cut (l = l'). intro H4. cut (r = r'). intro H5. rewrite <- H4. rewrite <- H5. rewrite y. rewrite y0. left. assumption. apply Neqb_complete. assumption. apply Neqb_complete. assumption. elim (N.eqb x x'). auto. auto. intro H2. rewrite H2 in H. cut (l = l'). intro H3. rewrite <- H3. rewrite y. left. assumption. apply Neqb_complete. assumption. elim (N.eqb r r'). auto. auto. intro H1. rewrite H1 in H. left. assumption. elim (N.eqb l l'). auto. auto. intro y0. unfold BDDshare_lookup in |- *. unfold BDDshare_lookup in H. rewrite y0 in H. cut (N.eqb l l' = true \/ N.eqb l l' = false). intro H0. elim H0. clear H0. intro H0. rewrite (MapPut_semantics (Map (Map ad)) share l (MapPut (Map ad) x0 r (MapPut ad (newMap ad) x counter)) l') in H. rewrite H0 in H. rewrite (MapPut_semantics (Map ad) x0 r (MapPut ad (newMap ad) x counter) r') in H. cut (N.eqb r r' = true \/ N.eqb r r' = false). intro H1. elim H1. clear H1. intros H1. rewrite H1 in H. cut (l = l'). cut (r = r'). intros H2 H3. rewrite <- H2. rewrite <- H3. rewrite y. rewrite y0. cut (N.eqb x x' = true \/ N.eqb x x' = false). intro H4. elim H4. clear H4. intro H4. cut (x = x'). intro H5. rewrite <- H5. auto. apply Neqb_complete. assumption. intro H5. left. rewrite (MapPut_semantics ad (newMap ad) x counter x') in H. rewrite H5 in H. simpl in H. assumption. elim (N.eqb x x'). auto. auto. apply Neqb_complete. assumption. apply Neqb_complete. assumption. intro H2. rewrite H2 in H. cut (l = l'). intro H3. rewrite <- H3. rewrite y. auto. apply Neqb_complete. assumption. elim (N.eqb r r'). auto. auto. intro H1. rewrite (MapPut_semantics (Map (Map ad)) share l (MapPut (Map ad) x0 r (MapPut ad (newMap ad) x counter)) l') in H. rewrite H1 in H. auto. elim (N.eqb l l'). auto. auto. intro y. unfold BDDshare_lookup in |- *. rewrite y. rewrite (MapPut_semantics (Map (Map ad)) share l (MapPut (Map ad) (newMap (Map ad)) r (MapPut ad match MapGet (Map ad) (newMap (Map ad)) r with | None => newMap ad | Some y => y end x counter)) l'). cut (N.eqb l l' = true \/ N.eqb l l' = false). cut (N.eqb x x' = true \/ N.eqb x x' = false). cut (N.eqb r r' = true \/ N.eqb r r' = false). intros H H0 H1 H2. elim H1. clear H1. intro H1. rewrite H1 in H2. rewrite (MapPut_semantics (Map ad) (newMap (Map ad)) r (MapPut ad match MapGet (Map ad) (newMap (Map ad)) r with | None => newMap ad | Some y => y end x counter) r') in H2. elim H. clear H. intro H. rewrite H in H2. simpl in H2. elim H0. intro H3. cut (l = l'). cut (r = r'). cut (x = x'). intros H4 H5 H6. rewrite <- H4. rewrite <- H5. rewrite <- H6. auto. apply Neqb_complete. assumption. apply Neqb_complete. assumption. apply Neqb_complete. assumption. intro H3. rewrite H3 in H2. discriminate H2. intro H3. rewrite H3 in H2. simpl in H2. discriminate H2. intro H3. rewrite H3 in H2. auto. elim (N.eqb r r'). auto. auto. elim (N.eqb x x'). 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