From 6c6267a2b8272d2151c6470d8f4b676b0696b1b8 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Wed, 7 Oct 2020 13:30:09 -0500
Subject: [PATCH] Add a complexity test

---
 tests/gmap.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/tests/gmap.v b/tests/gmap.v
index 4de79e14..3f0415e7 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -83,3 +83,28 @@ Arguments Plookup _ _ _ / : assert.
 Theorem gmap_lookup_concrete :
   lookup (M:=gmap nat bool) 2 (<[3:=false]> {[2:=true]}) = Some true.
 Proof. simpl. Show. reflexivity. Qed.
+
+Fixpoint insert_l (m:gmap Z unit) (l: list Z) : gmap Z unit :=
+  match l with
+  | [] => m
+  | p::l => <[p:=tt]> (insert_l m l)
+  end.
+
+Fixpoint n_positives (n:nat) (p:Z) : list Z :=
+  match n with
+  | 0 => []
+  | S n => p :: n_positives n (1 + p)%Z
+  end.
+
+Fixpoint n_positives_rev (n:nat) (p:Z) : list Z :=
+  match n with
+  | 0 => []
+  | S n => p :: n_positives_rev n (p - 1)%Z
+  end.
+
+Theorem gmap_lookup_insert_fwd_rev :
+  insert_l ∅ (n_positives 500 1) = insert_l ∅ (n_positives_rev 500 500).
+Proof.
+  cbn [n_positives n_positives_rev Z.add Z.pos_sub Pos.add Pos.succ].
+  Time reflexivity.
+Qed.
-- 
GitLab