Skip to content
Snippets Groups Projects
Commit 8d18a771 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Tweak tests.

parent ad2f0a93
No related branches found
No related tags found
1 merge request!309Use `SProp` to obtain better definitional equality for `pmap`, `gmap`, `gset`, `Qp`, and `coPset`
This commit is part of merge request !309. Comments created here will be created in the context of that merge request.
...@@ -70,10 +70,14 @@ Failed to progress. ...@@ -70,10 +70,14 @@ Failed to progress.
============================ ============================
bool_decide (∅ ⊆ {[1; 2; 3]}) = true bool_decide (∅ ⊆ {[1; 2; 3]}) = true
"gmap_insert_comm"
: string
1 goal 1 goal
============================ ============================
{[3 := false; 2 := true]} = {[2 := true; 3 := false]} {[3 := false; 2 := true]} = {[2 := true; 3 := false]}
"gmap_lookup_concrete"
: string
1 goal 1 goal
============================ ============================
......
From stdpp Require Import pmap gmap. From stdpp Require Import strings pmap gmap.
Goal {[1; 2; 3]} =@{gset nat} ∅. Goal {[1; 2; 3]} =@{gset nat} ∅.
Proof. Proof.
...@@ -120,10 +120,12 @@ Time Eval vm_compute in gmap_insert_positives_test 512000. ...@@ -120,10 +120,12 @@ Time Eval vm_compute in gmap_insert_positives_test 512000.
Time Eval vm_compute in gmap_insert_positives_test 1000000. Time Eval vm_compute in gmap_insert_positives_test 1000000.
*) *)
Check "gmap_insert_comm".
Theorem gmap_insert_comm : Theorem gmap_insert_comm :
{[ 3:=false; 2:=true]} =@{gmap nat bool} {[ 2:=true; 3:=false ]}. {[ 3:=false; 2:=true]} =@{gmap nat bool} {[ 2:=true; 3:=false ]}.
Proof. simpl. Show. reflexivity. Qed. Proof. simpl. Show. reflexivity. Qed.
Check "gmap_lookup_concrete".
Theorem gmap_lookup_concrete : Theorem gmap_lookup_concrete :
lookup (M:=gmap nat bool) 2 {[ 3:=false; 2:=true ]} = Some true. lookup (M:=gmap nat bool) 2 {[ 3:=false; 2:=true ]} = Some true.
Proof. simpl. Show. reflexivity. Qed. Proof. simpl. Show. reflexivity. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment