Verified Commit 1590e131 authored by Tej Chajed's avatar Tej Chajed
Browse files

Add a complexity test

parent b7b92821
......@@ -15,3 +15,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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment