blob: 930c4a85088a54f72f33cc874f226197d608feca (
plain)
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
|
(* [Require Import SMTCoq.] loads the SMTCoq library.
If you are using native-coq instead of Coq 8.5, 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.
|
