From 4f5ea8b8373dc994714aa563182bad9c9ed21526 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Feb 2020 14:53:25 +0100
Subject: gremove_t

---
 lib/Maps.v | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

(limited to 'lib/Maps.v')

diff --git a/lib/Maps.v b/lib/Maps.v
index 0beb11b4..5a0e6d5a 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -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) :=
-- 
cgit