1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
|
(** * Basics: Functional Programming in Coq *)
From QuickChick Require Import QuickChick.
Import QcNotation. Open Scope qc_scope.
Import GenLow GenHigh.
Require Import List ZArith.
Import ListNotations.
(*
From mathcomp Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import seq ssrnat eqtype.
*)
Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
Definition test_next_weekday :=
(next_weekday (next_weekday saturday)) = tuesday.
(* BCP: Needs an equality test.
QuickCheck test_next_weekday. *)
(* BCP: QC needs the native one. (Unless we make this Checkable somehow.)
Inductive bool : Type :=
| true : bool
| false : bool.
*)
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => b2
| false => false
end.
Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => true
| false => b2
end.
Definition nandb (b1:bool) (b2:bool) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *) := false.
Definition test_nandb1 := (nandb true false).
(*! QuickChick test_nandb1. *)
Definition minustwo (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
Definition oddb (n:nat) : bool := negb (evenb n).
Definition test_oddb1 := oddb 1.
(*! QuickChick test_oddb1. *)
Module NatPlayground2.
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Fixpoint mult (n m : nat) : nat :=
match n with
| O => O
| S n' => plus m (mult n' m)
end.
Definition test_mult1 := (mult 3 3) =? 9.
(*! QuickChick test_mult1. *)
Fixpoint minus (n m:nat) : nat :=
match n, m with
| O , _ => O
| S _ , O => n
| S n', S m' => minus n' m'
end.
End NatPlayground2.
Fixpoint exp (base power : nat) : nat :=
match power with
| O => S O
| S p => mult base (exp base p)
end.
Fixpoint factorial (n:nat) : nat
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *) := 0.
Definition test_factorial1 := (factorial 3) =? 6.
(*! QuickChick test_factorial1. *)
Notation "x + y" := (plus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x - y" := (minus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x * y" := (mult x y)
(at level 40, left associativity)
: nat_scope.
Check ((0 + 1) + 1).
Fixpoint beq_nat (n m : nat) : bool :=
match n with
| O => match m with
| O => true
| S m' => false
end
| S n' => match m with
| O => false
| S m' => beq_nat n' m'
end
end.
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb n' m'
end
end.
Notation "'FORALLX' x : T , c" :=
(forAllShrink (@arbitrary T _) shrink (fun x => c))
(at level 200, x ident, T at level 200, c at level 200, right associativity
(* , format "'[' 'exists' '/ ' x .. y , '/ ' p ']'" *) )
: type_scope.
Definition plus_O_n := FORALL n:nat, 0 + n =? n.
(*! QuickChick plus_O_n. *)
(* BCP: This should be automatable, we guessed... *)
Instance bool_eq (x y : bool) : Dec (x = y).
constructor. unfold ssrbool.decidable. repeat (decide equality). Defined.
(* BCP: Should be able to use Dec everywhere now :-) *)
Definition negb_involutive (b: bool) :=
(negb (negb b) = b)?.
Check negb_involutive.
QuickChick negb_involutive.
Definition negb_involutive2 (b: bool) :=
Bool.eqb (negb (negb b)) b.
(*! QuickChick negb_involutive2. *)
Definition andb_commutative := fun b c => Bool.eqb (andb b c) (andb c b).
(*! QuickCheck andb_commutative. *)
(* BCP: Don't know what to do with this one!
Theorem identity_fn_applied_twice :
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
*)
Definition andb_eq_orb :=
fun (b c : bool) =>
(Bool.eqb (andb b c) (orb b c))
==>
(Bool.eqb b c).
(*! QuickCheck andb_eq_orb. *)
|
