# QCCore QuickChick

## The G Monad

Check returnGen.

```
===> returnGen : ?A -> G ?A
```

(* Sample (returnGen 42). *)

===> [42, 42, 42, 42, 42, 42, 42, 42, 42, 42, 42]

*function*f taking an A and yielding a random generator for B, we can plumb the two together into a generator for B that works by internally generating a random A and applying f to it.

Check bindGen.

===> bindGen : G ?A -> (?A -> G ?B) -> G ?B

Section GMonadDef.

Instance GMonad : `{Monad G} | 3 :=

{

ret := @returnGen;

bind := @bindGen

}.

End GMonadDef.

Instance GMonad : `{Monad G} | 3 :=

{

ret := @returnGen;

bind := @bindGen

}.

End GMonadDef.

## Primitive generators

Check @choose.

===> @choose : forall G : Type -> Type, Producer G -> forall A : Type, ChoosableFromInterval A -> A * A -> G A

Print ChoosableFromInterval.

===> Record ChoosableFromInterval (A : Type) : Type := Build_ChoosableFromInterval { super : Ord A; randomR : A * A -> RandomSeed -> A * RandomSeed; ... }.

(* Sample (choose (0,10)). *)

===> [ 1, 2, 1, 9, 8, 10, 3, 6, 0, 1, 8 ]

#### Exercise: 1 star, standard, optional (cfi)

Print out the full definition of ChoosableFromInterval. Can you understand what it means? ☐## Lists

Check listOf.

```
===> listOf : G ?A -> G (list ?A)
```

(* Sample (listOf (choose (0,4))). *)

===> [ [ 0, 3, 2, 0 ], [ 1, 3, 4, 1, 0, 3, 0, 2, 2, 3, 2, 2, 2, 0, 4, 2, 3, 0, 1 ], [ 3, 4, 3, 1, 2, 4, 4, 1, 0, 3, 4, 3, 2, 2, 4, 4, 1 ], [ 0 ], [ 4, 2, 3 ], [ 3, 3, 4, 0, 1, 4, 3, 2, 4, 1 ], [ 0, 4 ], [ ], [ 1, 0, 1, 3, 1 ], [ 0, 0 ], [ 1, 4 ], [ 4, 3, 2, 0, 2, 2, 4, 0 ], [ 1, 1, 0, 0, 1, 4 ], [ 2, 0, 2, 1, 3, 3 ], [ 4, 3, 3, 0, 1 ], [ 3, 3, 3 ], [ 3, 2, 4 ], [ 1, 2 ], [ ], [ ] ]

Check vectorOf.

===> vectorOf : nat -> G ?A -> G (list ?A)

(* Sample (vectorOf 3 (choose (0,4))). *)

===> [ [0, 1, 4], [1, 1, 0], [3, 3, 3], [0, 2, 1], [1, 3, 2], [3, 3, 0], [3, 0, 4], [2, 3, 3], [3, 2, 4], [1, 2, 3], [2, 0, 4] ]

Module DefineG.

Inductive G (A:Type) : Type :=

| MkG : (nat → RandomSeed → A) → G A.

Arguments MkG {A}.

End DefineG.

Inductive G (A:Type) : Type :=

| MkG : (nat → RandomSeed → A) → G A.

Arguments MkG {A}.

End DefineG.

When it is searching for counterexamples, QuickChick progressively
tries larger and larger values for the size bound n, to
gradually explore deeper into the search space.
Each generator can choose to interpret the size bound however it
wants, and there is no

*enforced*guarantee that generators pay any attention to it at all; however, it is good practice to respect this bound when programming generators.## Custom Generators

In order for commands like Sample to display colors, we should
make color an instance of the Show typeclass:

#[export] Instance show_color : Show color :=

{| show c :=

match c with

| Red ⇒ "Red"

| Green ⇒ "Green"

| Blue ⇒ "Blue"

| Yellow ⇒ "Yellow"

end

|}.

{| show c :=

match c with

| Red ⇒ "Red"

| Green ⇒ "Green"

| Blue ⇒ "Blue"

| Yellow ⇒ "Yellow"

end

|}.

To generate a random color, we just need to pick one of the
constructors Red, Green, Blue, or Yellow. This is done
using elems_.

Check elems_.

===> elems_ : ?A -> list ?A -> G ?A

Definition genColor' : G color :=

elems_ Red [ Red ; Green ; Blue ; Yellow ].

(* Sample genColor'. *)

elems_ Red [ Red ; Green ; Blue ; Yellow ].

(* Sample genColor'. *)

===> [Red, Green, Blue, Blue, Red, Yellow, Blue, Red, Blue, Blue, Red]

" 'elems' [ x ] " := elems_ x (cons x nil) " 'elems' [ x ; y ] " := elems_ x (cons x (cons y nil)) " 'elems' [ x ; y ; .. ; z ] " := elems_ x (cons x (cons y (.. (cons z nil)))) " 'elems' ( x ;; l ) " := elems_ x (cons x l)

===> [Red, Green, Blue, Blue, Red, Yellow, Blue, Red, Blue, Blue, Red]

Inductive Tree A :=

| Leaf : Tree A

| Node : A → Tree A → Tree A → Tree A.

Arguments Leaf {A}.

Arguments Node {A} _ _ _.

| Leaf : Tree A

| Node : A → Tree A → Tree A → Tree A.

Arguments Leaf {A}.

Arguments Node {A} _ _ _.

Before getting to generators for trees, we again give a
straightforward Show instance. (The need for a local let fix
declaration stems from the fact that Coq's typeclasses, unlike
Haskell's, are not automatically recursive. We could
alternatively define aux with a separate top-level
Fixpoint.)

#[export] Instance showTree {A} `{_ : Show A} : Show (Tree A) :=

{| show := let fix aux t :=

match t with

| Leaf ⇒ "Leaf"

| Node x l r ⇒

"Node (" ++ show x ++ ") ("

++ aux l ++ ") ("

++ aux r ++ ")"

end

in aux

|}.

{| show := let fix aux t :=

match t with

| Leaf ⇒ "Leaf"

| Node x l r ⇒

"Node (" ++ show x ++ ") ("

++ aux l ++ ") ("

++ aux r ++ ")"

end

in aux

|}.

This brings us to our first generator

*combinator*, called oneOf_.
Check oneOf_.

===> oneOf_ : G ?A -> list (G ?A) -> G ?A

Fixpoint genTree {A} (g : G A) : G (Tree A) := oneOf [ ret Leaf ;; liftM3 Node g (genTree g) (genTree g) ].

*expected*size of the generated trees is actually infinite!

Fixpoint genTreeSized {A} (sz : nat) (g : G A) : G (Tree A) :=

match sz with

| O ⇒ ret Leaf

| S sz' ⇒

oneOf [

ret Leaf ;

liftM3 Node g (genTreeSized sz' g) (genTreeSized sz' g)

]

end.

(* Sample (genTreeSized 3 (choose(0,3))). *)

match sz with

| O ⇒ ret Leaf

| S sz' ⇒

oneOf [

ret Leaf ;

liftM3 Node g (genTreeSized sz' g) (genTreeSized sz' g)

]

end.

(* Sample (genTreeSized 3 (choose(0,3))). *)

===> [ Leaf, Leaf, Node (3) (Node (0) (Leaf) (Leaf)) (Node (2) (Leaf) (Node (3) (Leaf) (Leaf))), Leaf, Leaf, Leaf, Node (1) (Leaf) (Node (1) (Leaf) (Node (0) (Leaf) (Leaf))), Leaf, Node (3) (Leaf) (Leaf), Node (1) (Leaf) (Leaf), Leaf, Leaf, Node (0) (Leaf) (Node (0) (Leaf) (Node (2) (Leaf) (Leaf))), Node (0) (Node (2) (Node (3) (Leaf) (Leaf)) (Leaf)) (Leaf), Node (0) (Leaf) (Leaf), Leaf, Leaf, Leaf, Leaf, Leaf ]

Check freq_.

===> freq_ : G ?A -> list (nat * G ?A) -> G ?A

Fixpoint genTreeSized' {A} (sz : nat) (g : G A) : G (Tree A) :=

match sz with

| O ⇒ ret Leaf

| S sz' ⇒

freq [ (1, ret Leaf) ;

(sz, liftM3 Node g (genTreeSized' sz' g)

(genTreeSized' sz' g))

]

end.

(* Sample (genTreeSized' 3 (choose(0,3))). *)

match sz with

| O ⇒ ret Leaf

| S sz' ⇒

freq [ (1, ret Leaf) ;

(sz, liftM3 Node g (genTreeSized' sz' g)

(genTreeSized' sz' g))

]

end.

(* Sample (genTreeSized' 3 (choose(0,3))). *)

===> [ Node (3) (Node (1) (Node (3) (Leaf) (Leaf)) (Leaf)) (Node (0) (Leaf) (Node (3) (Leaf) (Leaf))), Leaf, Node (2) (Node (1) (Leaf) (Leaf)) (Leaf), Node (0) (Leaf) (Node (0) (Node (2) (Leaf) (Leaf)) (Node (0) (Leaf) (Leaf))), Node (1) (Node (2) (Leaf) (Node (0) (Leaf) (Leaf))) (Leaf), Node (0) (Node (0) (Leaf) (Node (3) (Leaf) (Leaf))) (Node (2) (Leaf) (Leaf)), Node (1) (Node (3) (Node (2) (Leaf) (Leaf)) (Node (3) (Leaf) (Leaf))) (Node (1) (Leaf) (Node (2) (Leaf) (Leaf))), Node (0) (Node (0) (Node (0) (Leaf) (Leaf)) (Node (1) (Leaf) (Leaf))) (Node (2) (Node (3) (Leaf) (Leaf)) (Node (0) (Leaf) (Leaf))), Node (2) (Node (2) (Leaf) (Leaf)) (Node (1) (Node (2) (Leaf) (Leaf)) (Node (2) (Leaf) (Leaf))), Node (2) (Node (3) (Node (2) (Leaf) (Leaf)) (Leaf)) (Node (0) (Node (2) (Leaf) (Leaf)) (Leaf)), Leaf, Node (2) (Node (3) (Node (3) (Leaf) (Leaf)) (Leaf)) (Leaf), Leaf, Node (1) (Leaf) (Leaf), Leaf, Node (1) (Node (2) (Leaf) (Node (3) (Leaf) (Leaf))) (Node (0) (Leaf) (Node (1) (Leaf) (Leaf))), Leaf, Node (3) (Node (0) (Node (0) (Leaf) (Leaf)) (Leaf)) (Node (0) (Leaf) (Node (2) (Leaf) (Leaf))), Node (2) (Node (2) (Node (0) (Leaf) (Leaf)) (Leaf)) (Node (1) (Leaf) (Node (2) (Leaf) (Leaf))), Leaf ]

#### Exercise: 2 stars, standard (genListSized)

Write a sized generator for lists, following genTreeSized'.
(* FILL IN HERE *)

☐

☐

#### Exercise: 3 stars, standard (genColorOption)

Write a custom generator for values of type option color. Make it generate None about 1/10th of the time, and make it generate Some Red three times as often as the other colors.
(* FILL IN HERE *)

☐

☐

## Checkers

Fixpoint mirror {A : Type} (t : Tree A) : Tree A :=

match t with

| Leaf ⇒ Leaf

| Node x l r ⇒ Node x (mirror r) (mirror l)

end.

match t with

| Leaf ⇒ Leaf

| Node x l r ⇒ Node x (mirror r) (mirror l)

end.

To formulate a property about mirror, we need a structural
equality test on trees. We can obtain that with minimal effort
using the Dec typeclass and the dec_eq tactic.

#[export] Instance eq_dec_tree (t

Proof. constructor; dec_eq. Defined.

_{1}t_{2}: Tree nat) : Dec (t_{1}= t_{2}).Proof. constructor; dec_eq. Defined.

We expect that mirroring a tree twice should yield the original
tree.

Now we want to use our generator to create a lot of random trees
and, for each one, check whether mirrorP returns true or
false.
Another way to say this is that we want to use mirrorP to build
a
Let's see how this works.
(Let's open a playground module so we can show simplified
versions of the actual QuickChick definitions.)

*generator for test results*.
First, we need a type of test results -- let's call it Result.
For the moment, think of Result as just an enumerated type with
constructors Success and Failure.

Inductive Result := Success | Failure.

#[export] Instance showResult : Show Result :=

{

show r := match r with Success ⇒ "Success" | Failure ⇒ "Failure" end

}.

#[export] Instance showResult : Show Result :=

{

show r := match r with Success ⇒ "Success" | Failure ⇒ "Failure" end

}.

Then we can define the type Checker to be G Result.

That is, a Checker embodies some way of performing a randomized
test of the truth of some proposition, which, when applied to a
random seed, will yield either Success (meaning that the
proposition survived this test) or Failure (meaning that this
test demonstrates that the proposition was false).
Sampling a Checker many times with different seeds will cause
many different tests to be performed.
To check mirrorP, we'll need a way to build a Checker out of a
function from trees to booleans.
Actually, we will be wanting to build Checkers based on many
different types. So let's begin by defining a typeclass
Checkable, where an instance for Checkable A will provide a
way of converting an A into a Checker.

It is easy to give a bool instance for Checkable.

#[export] Instance checkableBool : Checkable bool :=

{

checker b := if b then ret Success else ret Failure

}.

{

checker b := if b then ret Success else ret Failure

}.

That is, the boolean value true passes every test we might
subject it to (i.e., the result of checker is a G that returns
true for every seed), while false fails all tests.
Let's see what happens if we sample checkers for our favorite
booleans, true and false.
(We need to exit the playground so that we can do Sample:
because Sample is implemented internally via extraction to
OCaml, which usually does not work from inside a Module.)

===> [Success, Success, Success, Success, Success, Success, Success, Success, Success, Success, Success]

(* Sample (CheckerPlayground1.checker false). *)

===> [Failure, Failure, Failure, Failure, Failure, Failure, Failure, Failure, Failure, Failure, Failure]

Module CheckerPlayground2.

Export CheckerPlayground1.

#[export] Instance checkableDec `{P : Prop} `{Dec P} : Checkable P :=

{

checker p := if P? then ret Success else ret Failure

}.

Export CheckerPlayground1.

#[export] Instance checkableDec `{P : Prop} `{Dec P} : Checkable P :=

{

checker p := if P? then ret Success else ret Failure

}.

(The definition looks a bit strange since it doesn't use its
argument p. The intuition is that all the information in p is
already encoded in P!)
Now suppose we pose a couple of (decidable) conjectures:

The somewhat astononishing thing about the Checkable instance
for decidable Props is that, even though these are

*conjectures*(we haven't proved them, so the "evidence" that Coq has for them internally is just an uninstantiated "evar"), we can still build checkers from them and sample from these checkers! (Why? Technically, it is because the Checkable instance for decidable properties does not look at its argument.)
(* Sample (CheckerPlayground1.checker CheckerPlayground2.c1). *)

===> [Failure, Failure, Failure, Failure, Failure, Failure, Failure, Failure, Failure, Failure, Failure]

(* Sample (CheckerPlayground1.checker CheckerPlayground2.c2). *)

===> [Success, Success, Success, Success, Success, Success, Success, Success, Success, Success, Success]

Now let's go back to mirrorP.
We have seen that the result of mirrorP is Checkable. What we
need is a way to take a function returning a checkable thing and
make the function itself checkable.
We can easily do this, as long as the argument type of the
function is something we know how to generate!

Definition forAll {A B : Type} `{Checkable B}

(g : G A) (f : A → B)

: Checker :=

a <- g ;;

checker (f a).

End CheckerPlayground3.

(g : G A) (f : A → B)

: Checker :=

a <- g ;;

checker (f a).

End CheckerPlayground3.

Let's try this out!
First, let's revisit our color example to execute a simple check.
We can define a boolean test that returns true for Red and
false for other colors.

Since we can generate elements of color and we have a
Checkable instance for bool, we can apply forAll to isRed
and sample from the resulting Checker to run some tests.

(* Sample (CheckerPlayground3.forAll genColor isRed). *)

===> [Success, Failure, Failure, Failure, Success, Failure, Failure, Success, Failure, Failure, Success]

(*

Sample (CheckerPlayground3.forAll

(genTreeSized' 3 (choose(0,3)))

mirrorP).

*)

Sample (CheckerPlayground3.forAll

(genTreeSized' 3 (choose(0,3)))

mirrorP).

*)

Definition faultyMirrorP (t : Tree nat) := (mirror t) = t ?.

(*

Sample (CheckerPlayground3.forAll

(genTreeSized' 3 (choose(0,3)))

faultyMirrorP).

*)

(*

Sample (CheckerPlayground3.forAll

(genTreeSized' 3 (choose(0,3)))

faultyMirrorP).

*)

===> [Failure, Success, Failure, Success, Success, Success, Failure, Success, Failure, Failure, Success]

*are*the tests that are failing? We can tell by looking at the samples that the property is bad, but we can't see the counterexamples!

Module CheckerPlayground4.

Inductive Result :=

| Success : Result

| Failure : ∀ {A} `{Show A}, A → Result.

#[export] Instance showResult : Show Result :=

{

show r := match r with

Success ⇒ "Success"

| Failure a ⇒ "Failure: " ++ show a

end

}.

Definition Checker := G Result.

Class Checkable A :=

{

checker : A → Checker

}.

#[export] Instance showUnit : Show unit :=

{

show u := "tt"

}.

Inductive Result :=

| Success : Result

| Failure : ∀ {A} `{Show A}, A → Result.

#[export] Instance showResult : Show Result :=

{

show r := match r with

Success ⇒ "Success"

| Failure a ⇒ "Failure: " ++ show a

end

}.

Definition Checker := G Result.

Class Checkable A :=

{

checker : A → Checker

}.

#[export] Instance showUnit : Show unit :=

{

show u := "tt"

}.

The failure cases in the bool and Dec checkers don't need to
record anything except the Failure, so we put tt (the sole
value of type unit) as the "failure reason."

#[export] Instance checkableBool : Checkable bool :=

{

checker b := if b then ret Success else ret (Failure tt)

}.

#[export] Instance checkableDec `{P : Prop} `{Dec P} : Checkable P :=

{

checker p := if P? then ret Success else ret (Failure tt)

}.

{

checker b := if b then ret Success else ret (Failure tt)

}.

#[export] Instance checkableDec `{P : Prop} `{Dec P} : Checkable P :=

{

checker p := if P? then ret Success else ret (Failure tt)

}.

The interesting case is the forAll combinator. Here, we

*do*have some useful information to record in the failure case -- namely, the argument that caused the failure.
Definition forAll {A B : Type} `{Show A} `{Checkable B}

(g : G A) (f : A → B)

: Checker :=

a <- g ;;

r <- checker (f a) ;;

match r with

Success ⇒ ret Success

| Failure b ⇒ ret (Failure (a,b))

end.

(g : G A) (f : A → B)

: Checker :=

a <- g ;;

r <- checker (f a) ;;

match r with

Success ⇒ ret Success

| Failure b ⇒ ret (Failure (a,b))

end.

Note that, rather than just returning Failure a, we package up
a together with b, which explains the reason for the failure
of f a. This allows us to write several forAlls in sequence
and capture all of their results in a nested tuple.

End CheckerPlayground4.

(*

Sample (CheckerPlayground4.forAll

(genTreeSized' 3 (choose(0,3)))

faultyMirrorP).

*)

(*

Sample (CheckerPlayground4.forAll

(genTreeSized' 3 (choose(0,3)))

faultyMirrorP).

*)

===> [Failure: (Node (2) (Node (3) (Node (2) (Leaf) (Leaf)) (Leaf)) (Node (0) (Node (2) (Leaf) (Leaf)) (Leaf)), tt), Success, Failure: (Node (2) (Node (3) (Node (3) (Leaf) (Leaf)) (Leaf)) (Leaf), tt), Success, Success, Success, Failure: (Node (1) (Node (2) (Leaf) (Node (3) (Leaf) (Leaf))) (Node (0) (Leaf) (Node (1) (Leaf) (Leaf))), tt), Success, Failure: (Node (3) (Node (0) (Node (0) (Leaf) (Leaf)) (Leaf)) (Node (0) (Leaf) (Node (2) (Leaf) (Leaf))), tt), Failure: (Node (2) (Node (2) (Node (0) (Leaf) (Leaf)) (Leaf)) (Node (1) (Leaf) (Node (2) (Leaf) (Leaf))), tt), Success]

(*

QuickChick

(forAll

(genTreeSized' 3 (choose(0,3)))

faultyMirrorP).

*)

QuickChick

(forAll

(genTreeSized' 3 (choose(0,3)))

faultyMirrorP).

*)

===> QuickChecking (forAll (genTreeSized' 3 (choose (0, 3))) faultyMirrorP) Node (0) (Node (0) (Node (2) (Leaf) (Leaf)) (Node (1) (Leaf) (Leaf))) (Node (1) (Node (0) (Leaf) (Leaf)) (Leaf)) *** Failed after 1 tests and 0 shrinks. (0 discards)

*much*larger than is really needed to illustrate the bad behavior of faultyMirrorP.

*shrinking*comes in.

# Shrinking

#[export] Instance shrinkColor : Shrink color :=

{

shrink c :=

match c with

| Red ⇒ [ ]

| Green ⇒ [ Red ]

| Blue ⇒ [ Red; Green ]

| Yellow ⇒ [ Red; Green; Blue ]

end

}.

{

shrink c :=

match c with

| Red ⇒ [ ]

| Green ⇒ [ Red ]

| Blue ⇒ [ Red; Green ]

| Yellow ⇒ [ Red; Green; Blue ]

end

}.

Most of the time, shrinking functions should try to return
elements that are "just one step" smaller than the one they are
given. For example, consider the default shrinking function for
lists provided by QuickChick.

Print shrinkList.

```
===>
shrinkList =
fun (A : Type) (H : Shrink A) =>
{| shrink := shrinkListAux shrink |}
: forall A : Type, Shrink A -> Shrink (list A)
```

Print shrinkListAux.

===> shrinkListAux = fix shrinkListAux (A : Type) (shr : A -> list A) (l : list A) : list (list A) := match l with | [] => [] | x :: xs => ((xs :: map (fun xs' : list A => x :: xs') (shrinkListAux A shr xs)) ++ map (fun x' : A => x' :: xs) (shr x)) end : forall A : Type, (A -> list A) -> list A -> list (list A)

Open Scope list.

Fixpoint shrinkTreeAux {A}

(s : A → list A) (t : Tree A)

: list (Tree A) :=

match t with

| Leaf ⇒ []

| Node x l r ⇒ [l] ++ [r] ++

map (fun x' ⇒ Node x' l r) (s x) ++

map (fun l' ⇒ Node x l' r) (shrinkTreeAux s l) ++

map (fun r' ⇒ Node x l r') (shrinkTreeAux s r)

end.

#[export] Instance shrinkTree {A} `{Shrink A} : Shrink (Tree A) :=

{| shrink x := shrinkTreeAux shrink x |}.

Fixpoint shrinkTreeAux {A}

(s : A → list A) (t : Tree A)

: list (Tree A) :=

match t with

| Leaf ⇒ []

| Node x l r ⇒ [l] ++ [r] ++

map (fun x' ⇒ Node x' l r) (s x) ++

map (fun l' ⇒ Node x l' r) (shrinkTreeAux s l) ++

map (fun r' ⇒ Node x l r') (shrinkTreeAux s r)

end.

#[export] Instance shrinkTree {A} `{Shrink A} : Shrink (Tree A) :=

{| shrink x := shrinkTreeAux shrink x |}.

With shrinkTree in hand, we can use the forAllShrink property
combinator, a variant of forAll that takes a shrinker as an
additional argument, to test properties like faultyMirrorP.

(*

QuickChick

(forAllShrink

(genTreeSized' 5 (choose (0,5)))

shrink

faultyMirrorP).

*)

QuickChick

(forAllShrink

(genTreeSized' 5 (choose (0,5)))

shrink

faultyMirrorP).

*)

===> Node (0) (Leaf) (Node (0) (Leaf) (Leaf)) *** Failed! After 1 tests and 8 shrinks

## Exercise: Ternary Trees

Inductive TernaryTree A :=

| TLeaf : TernaryTree A

| TNode :

A → TernaryTree A → TernaryTree A → TernaryTree A → TernaryTree A.

Arguments TLeaf {A}.

Arguments TNode {A} _ _ _ _.

| TLeaf : TernaryTree A

| TNode :

A → TernaryTree A → TernaryTree A → TernaryTree A → TernaryTree A.

Arguments TLeaf {A}.

Arguments TNode {A} _ _ _ _.

Also consider the following (faulty?) mirror function. We'll want to do some
testing to see what we can find about this function.

Fixpoint tern_mirror {A : Type} (t : TernaryTree A) : TernaryTree A :=

match t with

| TLeaf ⇒ TLeaf

| TNode x l m r ⇒ TNode x (tern_mirror r) m (tern_mirror l)

end.

match t with

| TLeaf ⇒ TLeaf

| TNode x l m r ⇒ TNode x (tern_mirror r) m (tern_mirror l)

end.

(* FILL IN HERE *)

☐

☐

(* FILL IN HERE *)

The following line should generate a bunch of nat ternary trees.

(* Sample (@genTernTreeSized nat 3 (choose (0,10))). *)

☐

☐

(* FILL IN HERE *)

☐

☐

A direction tells us which child node we wish to visit. The
traverse_node function uses a direction to visit the
corresponding child.

Definition traverse_node {A} (t:direction) (l m r: TernaryTree A) :=

match t with

| Left ⇒ l

| Middle ⇒ m

| Right ⇒ r

end.

match t with

| Left ⇒ l

| Middle ⇒ m

| Right ⇒ r

end.

A path in a ternary tree is a list of directions.

We can traverse a path by iterating over the directions in the
path and traversing the corresponding nodes.

Fixpoint traverse_path {A} (p:path) (t: TernaryTree A) :=

match t with

| TLeaf ⇒

TLeaf

| TNode x l m r ⇒

match p with

| h :: tl ⇒ traverse_path tl (traverse_node h l m r)

| [] ⇒ t

end

end.

match t with

| TLeaf ⇒

TLeaf

| TNode x l m r ⇒

match p with

| h :: tl ⇒ traverse_path tl (traverse_node h l m r)

| [] ⇒ t

end

end.

And we can mirror a path by simply swapping left and
right throughout.

Before we can state some properties about paths in ternary trees, it's
useful to have a decidable equality for ternary trees of nats.

#[export] Instance eq_dec_tern_tree (t

Proof. constructor; dec_eq. Defined.

_{1}t_{2}: TernaryTree nat) : Dec (t_{1}= t_{2}).Proof. constructor; dec_eq. Defined.

Traversing a path in a tree should be the same as traversing the
mirror of the path in the mirror of the tree, just with a mirrored
tree result.

Definition tern_mirror_path_flip (t:TernaryTree nat) (p:path) :=

( traverse_path p t

= tern_mirror (traverse_path (path_mirror p) (tern_mirror t))) ?.

( traverse_path p t

= tern_mirror (traverse_path (path_mirror p) (tern_mirror t))) ?.

Before using this property to test tern_mirror, we'll need to be
able to generate, show, and shrink paths. To start, we'll derive
those For directions. The Show and G definitions for
direction are simple to write; the shrink will by default go
left.

#[export] Instance showDirection : Show direction :=

{| show x :=

match x with

| Left ⇒ "Left"

| Middle ⇒ "Middle"

| Right ⇒ "Right"

end |}.

Definition genDirection : G direction :=

elems [Left; Middle; Right].

#[export] Instance shrinkDirection : Shrink direction :=

{| shrink d :=

match d with

| Left ⇒ []

| Right | Middle ⇒ [Left]

end |}.

{| show x :=

match x with

| Left ⇒ "Left"

| Middle ⇒ "Middle"

| Right ⇒ "Right"

end |}.

Definition genDirection : G direction :=

elems [Left; Middle; Right].

#[export] Instance shrinkDirection : Shrink direction :=

{| shrink d :=

match d with

| Left ⇒ []

| Right | Middle ⇒ [Left]

end |}.

For generating a list of paths, we'll use the built-in function
listOf, which takes a generator for a type and generates lists
of elements of that type. We do the same for show and shrink
with showList and shrinkList respectively.

#[export] Instance showPath : Show path := showList.

#[export] Instance genPath : Gen path :=

{arbitrary := listOf genDirection }.

#[export] Instance shrinkPath : Shrink path := shrinkList.

#[export] Instance genPath : Gen path :=

{arbitrary := listOf genDirection }.

#[export] Instance shrinkPath : Shrink path := shrinkList.

#### Exercise: 4 stars, standard (bug_finding_tern_tree)

Using genTernTreeSized and shrinkTernTree find (and fix!) any bugs in tern_mirror.
(* FILL IN HERE *)

☐

☐

# Putting it all Together

Intuitively, Gen is a way of uniformly packaging up the
generators for various types so that we do not need to remember
their individual names -- we can just call them all
arbitrary.

Next, for convenience we package Gen and Shrink together into
an Arbitrary typeclass that is a subclass of both.

(The empty "body" of Arbitrary is elided.)

We can use the top-level QuickChick command on quantified
propositions with generatable and decidable conclusions, stating
just the property and letting the typeclass machinery figure out
the rest.
For example, suppose we want to test this:

Since we have already defined Gen and Shrink instances for
color, we automatically get an Arbitrary instance. The Gen
part is used by the checker instance for "forall" propositions to
generate random color arguments.
To show that the conclusion is decidable, we need to define a
Dec instance for equality on colors.

Putting it all together:

(* QuickChick every_color_is_red. *)

===> QuickChecking every_color_is_red Green *** Failed after 1 tests and 1 shrinks. (0 discards)

# Sized Generators

Module DefineSized.

Import DefineG.

Definition sized {A : Type} (f : nat → G A) : G A :=

MkG

(fun n r ⇒

match f n with

MkG g ⇒ g n r

end).

End DefineSized.

Import DefineG.

Definition sized {A : Type} (f : nat → G A) : G A :=

MkG

(fun n r ⇒

match f n with

MkG g ⇒ g n r

end).

End DefineSized.

To streamline assembling generators, it is convenient to introduce
one more typeclass, GenSized, whose instances are sized
generators.

We can then define a generic Gen instance for types that have a
GenSized instance, using sized:

#[export] Instance GenOfGenSized {A} `{GenSized A} : Gen A :=

{

arbitrary := sized arbitrarySized

}.

End DefineGenSized.

{

arbitrary := sized arbitrarySized

}.

End DefineGenSized.

Now we can make a Gen instance for trees by providing just an
implementation of arbitrarySized.

#[export] Instance genTree {A} `{Gen A} : GenSized (Tree A) :=

{| arbitrarySized n := genTreeSized' n arbitrary |}.

{| arbitrarySized n := genTreeSized' n arbitrary |}.

Finally, with the Arbitrary instance for trees, we can supply
just faultyMirrorP to the QuickChick command.

(* QuickChick faultyMirrorP. *)

#### Exercise: 2 stars, standard (tern_tree_typeclasses)

Add typeclass instances for GenSized and Shrink so that you can QuickChick tern_mirror_path_flip directly.
(* FILL IN HERE *)

(*QuickChick tern_mirror_path_flip. *)

☐

(*QuickChick tern_mirror_path_flip. *)

☐

# Automation

Derive Arbitrary for Tree.

===> GenSizedree is defined ===> ShrinkTree is defined

===> ShowTree is defined

# Collecting Statistics

Check @collect.

===> @collect : forall A prop : Type, Show A -> Checkable prop -> A -> prop -> Checker

Fixpoint size {A} (t : Tree A) : nat :=

match t with

| Leaf ⇒ O

| Node _ l r ⇒ 1 + size l + size r

end.

match t with

| Leaf ⇒ O

| Node _ l r ⇒ 1 + size l + size r

end.

We can write a dummy property treeProp to collect the sizes of
the trees we are generating.

Definition treeProp (g : nat → G nat → G (Tree nat)) n :=

forAll (g n (choose (0,n))) (fun t ⇒ collect (size t) true).

(* QuickChick (treeProp genTreeSized 5). *)

forAll (g n (choose (0,n))) (fun t ⇒ collect (size t) true).

(* QuickChick (treeProp genTreeSized 5). *)

===> 4947 : 0 1258 : 1 673 : 2 464 : 6 427 : 5 393 : 3 361 : 7 302 : 4 296 : 8 220 : 9 181 : 10 127 : 11 104 : 12 83 : 13 64 : 14 32 : 15 25 : 16 16 : 17 13 : 18 6 : 19 5 : 20 2 : 21 1 : 23 +++ OK, passed 10000 tests

(* QuickChick (treeProp genTreeSized' 5). *)

===> 1624 : 0 571 : 10 564 : 12 562 : 11 559 : 9 545 : 8 539 : 14 534 : 13 487 : 7 487 : 15 437 : 16 413 : 6 390 : 17 337 : 5 334 : 1 332 : 18 286 : 19 185 : 4 179 : 20 179 : 2 138 : 21 132 : 3 87 : 22 62 : 23 19 : 24 10 : 25 6 : 26 2 : 27 +++ OK, passed 10000 tests

#### Exercise: 2 stars, standard (genTreeSized'')

Write a generator genTreeSized'' that generates fewer empty trees. Check your results using collect.
(* FILL IN HERE *)

☐

☐

# Dealing with Preconditions

*properties with preconditions*. The default QuickChick approach of generating inputs based on type information can be inefficient for such properties, especially for those with sparse preconditions (i.e. ones that are satisfied rarely with respect to their input domain).

Consider a function that inserts a natural number into a sorted list.

Fixpoint sorted (l : list nat) :=

match l with

| [] ⇒ true

| x::xs ⇒ match xs with

| [] ⇒ true

| y :: ys ⇒ (x <=? y) && (sorted xs)

end

end.

Fixpoint insert (x : nat) (l : list nat) :=

match l with

| [] ⇒ [x]

| y::ys ⇒ if x <=? y then x :: l

else y :: insert x ys

end.

match l with

| [] ⇒ true

| x::xs ⇒ match xs with

| [] ⇒ true

| y :: ys ⇒ (x <=? y) && (sorted xs)

end

end.

Fixpoint insert (x : nat) (l : list nat) :=

match l with

| [] ⇒ [x]

| y::ys ⇒ if x <=? y then x :: l

else y :: insert x ys

end.

We could test insert using a

*conditional*property, which uses _==>_ to encode implication:
Check implication.

(*

<<

===> implication : bool -> Checker -> Checker

>>

*)

(*

<<

===> implication : bool -> Checker -> Checker

>>

*)

The

*implication*function takes a boolean (the precondition) and a Checker (the conclusion of the property); if the boolean is true, it tests the Checker, otherwise, it rejects the current test. The _==>_ notation is in*Checker_scope*.
Open Scope Checker_scope.

Definition insert_spec (x : nat) (l : list nat) :=

sorted l ==> sorted (insert x l).

Definition test_insert_spec :=

forAll (choose (0,10)) (fun x ⇒

forAll (listOf (choose (0,10))) (fun l ⇒

insert_spec x l)).

(* QuickChick test_insert_spec. *)

Definition insert_spec (x : nat) (l : list nat) :=

sorted l ==> sorted (insert x l).

Definition test_insert_spec :=

forAll (choose (0,10)) (fun x ⇒

forAll (listOf (choose (0,10))) (fun l ⇒

insert_spec x l)).

(* QuickChick test_insert_spec. *)

===> QuickChecking test_insert_spec +++ Passed 10000 tests (17325 discards)

*check*whether the generated l is sorted, and, if it is, proceed to check the conclusion. If it is not, it will discard the generated inputs and try again.

Definition insert_spec' (x : nat) (l : list nat) :=

collect (List.length l) (insert_spec x l).

Definition test_insert_spec' :=

forAll (choose (0,10)) (fun x ⇒

forAll (listOf (choose (0,10))) (fun l ⇒

insert_spec' x l)).

(* QuickChick test_insert_spec'. *)

collect (List.length l) (insert_spec x l).

Definition test_insert_spec' :=

forAll (choose (0,10)) (fun x ⇒

forAll (listOf (choose (0,10))) (fun l ⇒

insert_spec' x l)).

(* QuickChick test_insert_spec'. *)

===> QuickChecking insert_spec' 3652 : (Discarded) 7 3582 : 0 3568 : (Discarded) 6 3542 : 1 3469 : (Discarded) 5 3200 : (Discarded) 4 2830 : (Discarded) 3 1842 : 2 1606 : (Discarded) 2 716 : 3 248 : 4 61 : 5 8 : 6 1 : 7 +++ Passed 10000 tests (18325 discards)The vast majority of inputs have length 2 or less, while the larger lists are almost always discarded!

Fixpoint genSortedList (low high : nat) (size : nat)

: G (list nat) :=

match size with

| O ⇒ ret []

| S size' ⇒

if high <? low then

ret []

else

freq [ (1, ret []) ;

(size, x <- choose (low, high);;

xs <- genSortedList x high size';;

ret (x :: xs)) ] end.

: G (list nat) :=

match size with

| O ⇒ ret []

| S size' ⇒

if high <? low then

ret []

else

freq [ (1, ret []) ;

(size, x <- choose (low, high);;

xs <- genSortedList x high size';;

ret (x :: xs)) ] end.

We use a size parameter as usual to control the length of generated
lists.
If size is zero, we can only return the empty list which
is always sorted. If size is nonzero, we need to perform an
additional check whether high is less than low (in which case
we also return the empty list). If it is not, we can proceed to
choose to generate a cons cell, with its head generated between
low and high and its tail generated recursively.

(* Sample (genSortedList 0 10 10). *)

Finally, we can use forAllShrink to define a property using the
new generator:

Definition insert_spec_sorted (x : nat) :=

forAllShrink

(genSortedList 0 10 10)

shrink

(fun l ⇒ insert_spec' x l).

forAllShrink

(genSortedList 0 10 10)

shrink

(fun l ⇒ insert_spec' x l).

Now the distribution of lengths looks much better, and we don't
discard any tests!

===> QuickChecking insert_spec_sorted 947 : 0 946 : 4 946 : 10 938 : 6 922 : 9 916 : 2 900 : 7 899 : 3 885 : 8 854 : 5 847 : 1 +++ Passed 10000 tests (0 discards)Does this mean we are happy?

#### Exercise: 5 stars, standard, optional (uniform_sorted)

Using "collect", find out whether generating a sorted list of numbers between 0 and 5 is uniform in the frequencies with which different*numbers*are found in the generated lists.

(* FILL IN HERE *)

☐

☐

## Another Precondition: Binary Search Trees

*binary search trees*.

Fixpoint isBST (low high: nat) (t : Tree nat) :=

match t with

| Leaf ⇒ true

| Node x l r ⇒ (low <? x) && (x <? high)

&& (isBST low x l) && (isBST x high r)

end.

match t with

| Leaf ⇒ true

| Node x l r ⇒ (low <? x) && (x <? high)

&& (isBST low x l) && (isBST x high r)

end.

Here is a (faulty?) insertion function for binary search trees.

Fixpoint insertBST (x : nat) (t : Tree nat) :=

match t with

| Leaf ⇒ Node x Leaf Leaf

| Node x' l r ⇒ if x <? x' then Node x' (insertBST x l) r

else Node x' l (insertBST x r)

end.

match t with

| Leaf ⇒ Node x Leaf Leaf

| Node x' l r ⇒ if x <? x' then Node x' (insertBST x l) r

else Node x' l (insertBST x r)

end.

We would expect that if we insert an element that is within
the bounds low and high into a binary search tree, then
the result is also a binary search tree.

Definition insertBST_spec (low high : nat) (x : nat) (t : Tree nat) :=

(low <? x) ==>

(x <? high) ==>

(isBST low high t) ==>

isBST low high (insertBST x t).

(* QuickChick insertBST_spec. *)

(low <? x) ==>

(x <? high) ==>

(isBST low high t) ==>

isBST low high (insertBST x t).

(* QuickChick insertBST_spec. *)

===> QuickChecking insertBST_spec 0 5 4 Node (4) (Leaf) (Leaf) *** Failed after 85 tests and 1 shrinks. (1274 discards)

Fixpoint insertBST' (x : nat) (t : Tree nat) :=

match t with

| Leaf ⇒ Node x Leaf Leaf

| Node x' l r ⇒ if x <? x' then Node x' (insertBST' x l) r

else if x' <? x then Node x' l (insertBST' x r)

else t

end.

Definition insertBST_spec' (low high : nat) (x : nat) (t : Tree nat) :=

(low <? x) ==> (x <? high) ==> (isBST low high t) ==>

isBST low high (insertBST' x t).

match t with

| Leaf ⇒ Node x Leaf Leaf

| Node x' l r ⇒ if x <? x' then Node x' (insertBST' x l) r

else if x' <? x then Node x' l (insertBST' x r)

else t

end.

Definition insertBST_spec' (low high : nat) (x : nat) (t : Tree nat) :=

(low <? x) ==> (x <? high) ==> (isBST low high t) ==>

isBST low high (insertBST' x t).

... and try again...

(* QuickChick insertBST_spec'. *)

===> QuickChecking insertBST_spec' *** Gave up! Passed only 1281 tests Discarded: 20000... we see that 90% of tests are being discarded.

#### Exercise: 4 stars, standard (gen_bst)

Write a generator that produces binary search trees directly, so that you run 10000 tests with 0 discards.
(* FILL IN HERE *)

☐

☐

(* 2023-08-27 16:20 *)