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
|
(* [Require Import SMTCoq.SMTCoq.] loads the SMTCoq library.
If you are using native-coq instead of Coq 8.6, replace it with:
Require Import SMTCoq.
*)
Require Import SMTCoq.SMTCoq.
Require Import Bool.
Local Open Scope int63_scope.
(* Examples that check ZChaff certificates *)
Zchaff_Checker "sat.cnf" "sat.log".
Zchaff_Theorem sat "sat.cnf" "sat.log".
Check sat.
Zchaff_Checker "hole4.cnf" "hole4.log".
(* Example that checks a VeriT certificate, for logic QF_UF *)
Section Verit.
Verit_Checker "euf.smt2" "euf.log".
End Verit.
(* Examples of the zchaff tactic (requires zchaff in your PATH
environment variable):
- with booleans
- with concrete terms *)
Goal forall a b c,
(a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
Proof.
zchaff.
Qed.
Goal forall i j k,
let a := i == j in
let b := j == k in
let c := k == i in
(a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a) = false.
Proof.
zchaff.
Qed.
(* Examples of the verit tactic (requires verit in your PATH environment
variable):
- with booleans
- in logics QF_UF and QF_LIA *)
Goal forall a b c, ((a || b || c) && ((negb a) || (negb b) || (negb c)) && ((negb a) || b) && ((negb b) || c) && ((negb c) || a)) = false.
Proof.
verit.
Qed.
Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z),
(negb (Zeq_bool (f a) b)) || (negb (P (f a))) || (P b).
Proof.
verit.
Qed.
Goal forall b1 b2 x1 x2,
implb
(ifb b1
(ifb b2 (Zeq_bool (2*x1+1) (2*x2+1)) (Zeq_bool (2*x1+1) (2*x2)))
(ifb b2 (Zeq_bool (2*x1) (2*x2+1)) (Zeq_bool (2*x1) (2*x2))))
((implb b1 b2) && (implb b2 b1) && (Zeq_bool x1 x2)).
Proof.
verit.
Qed.
(* Examples of using the conversion tactics *)
Local Open Scope positive_scope.
Goal forall (f : positive -> positive) (x y : positive),
implb ((x + 3) =? y)
((f (x + 3)) <=? (f y))
= true.
Proof.
pos_convert.
verit.
Qed.
Goal forall (f : positive -> positive) (x y : positive),
implb ((x + 3) =? y)
((3 <? y) && ((f (x + 3)) <=? (f y)))
= true.
Proof.
pos_convert.
verit.
Qed.
Local Close Scope positive_scope.
Local Open Scope N_scope.
Goal forall (f : N -> N) (x y : N),
implb ((x + 3) =? y)
((f (x + 3)) <=? (f y))
= true.
Proof.
N_convert.
verit.
Qed.
Goal forall (f : N -> N) (x y : N),
implb ((x + 3) =? y)
((2 <? y) && ((f (x + 3)) <=? (f y)))
= true.
Proof.
N_convert.
verit.
Qed.
Local Close Scope N_scope.
Require Import NPeano.
Local Open Scope nat_scope.
Goal forall (f : nat -> nat) (x y : nat),
implb (Nat.eqb (x + 3) y)
((f (x + 3)) <=? (f y))
= true.
Proof.
nat_convert.
verit.
Qed.
Goal forall (f : nat -> nat) (x y : nat),
implb (Nat.eqb (x + 3) y)
((2 <? y) && ((f (x + 3)) <=? (f y)))
= true.
Proof.
nat_convert.
verit.
Qed.
Local Close Scope nat_scope.
|
