diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 14:53:25 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 14:53:25 +0100 |
commit | 4f5ea8b8373dc994714aa563182bad9c9ed21526 (patch) | |
tree | edc169575618e05b7a7999efdd0209bdbff9fb39 /lib/Maps.v | |
parent | ed0ad804bd09b2b76ec2535367ab9dd57b2600b0 (diff) | |
download | compcert-kvx-4f5ea8b8373dc994714aa563182bad9c9ed21526.tar.gz compcert-kvx-4f5ea8b8373dc994714aa563182bad9c9ed21526.zip |
gremove_t
Diffstat (limited to 'lib/Maps.v')
-rw-r--r-- | lib/Maps.v | 36 |
1 files changed, 36 insertions, 0 deletions
@@ -676,6 +676,42 @@ Module PTree <: TREE. End COMBINE_NULL. + Section REMOVE_TREE. + + Variables A B: Type. + + Fixpoint remove_t (m1: t A) (m2: t B) {struct m1} : t A := + match m1, m2 with + | Leaf, _ | _, Leaf => m1 + | (Node l1 o1 r1), (Node l2 o2 r2) => + Node' (remove_t l1 l2) + (match o2 with + | Some _ => None + | None => o1 + end) + (remove_t r1 r2) + end. + + Theorem gremove_t: + forall m1 : t A, + forall m2 : t B, + forall i : positive, + get i (remove_t m1 m2) = match get i m2 with + | None => get i m1 + | Some _ => None + end. + Proof. + induction m1; intros; simpl. + - rewrite gleaf. + destruct get; reflexivity. + - destruct m2; simpl. + + rewrite gleaf. + reflexivity. + + rewrite gnode'. + destruct i; simpl; try rewrite IHm1_1; try rewrite IHm1; trivial. + Qed. + End REMOVE_TREE. + Fixpoint xelements (A : Type) (m : t A) (i : positive) (k: list (positive * A)) {struct m} : list (positive * A) := |