From 73b4ee3b13bfab41382441deb43fb12508369423 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Mon, 5 Oct 2020 14:26:54 -0500
Subject: [PATCH] Add a more substantial reduction test

---
 tests/gmap.ref |  8 ++++++++
 tests/gmap.v   | 15 +++++++++++++--
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/tests/gmap.ref b/tests/gmap.ref
index a4d42549..afb49b4c 100644
--- a/tests/gmap.ref
+++ b/tests/gmap.ref
@@ -70,3 +70,11 @@ Failed to progress.
   
   ============================
   bool_decide (∅ ⊆ {[1; 2; 3]}) = true
+1 goal
+  
+  ============================
+  {[3 := false; 2 := true]} = {[2 := true; 3 := false]}
+1 goal
+  
+  ============================
+  Some true = Some true
diff --git a/tests/gmap.v b/tests/gmap.v
index e8e90b61..4de79e14 100644
--- a/tests/gmap.v
+++ b/tests/gmap.v
@@ -1,4 +1,4 @@
-From stdpp Require Import gmap.
+From stdpp Require Import pmap gmap.
 
 Goal {[1; 2; 3]} =@{gset nat} ∅.
 Proof.
@@ -71,4 +71,15 @@ Qed.
 
 Theorem gmap_insert_comm :
   <[3:=false]> {[2:=true]} =@{gmap nat bool} <[2:=true]> {[3:=false]}.
-Proof. reflexivity. Qed.
+Proof.
+  simpl. Show.
+  reflexivity.
+Qed.
+
+Transparent gmap_empty.
+Arguments map_insert _ _ _ / _ _ _ _ : assert.
+Arguments Plookup _ _ _ / : assert.
+
+Theorem gmap_lookup_concrete :
+  lookup (M:=gmap nat bool) 2 (<[3:=false]> {[2:=true]}) = Some true.
+Proof. simpl. Show. reflexivity. Qed.
-- 
GitLab