diff options
Diffstat (limited to 'examples/Example.v')
-rw-r--r-- | examples/Example.v | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/examples/Example.v b/examples/Example.v new file mode 100644 index 0000000..9dacc6a --- /dev/null +++ b/examples/Example.v @@ -0,0 +1,67 @@ +(* "Require Import SMTCoq." is needed to use the SMTCoq program *) + +Require Import 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. |