From 80a54a0e1974729d4756d2cc8483a2548c8dd2d0 Mon Sep 17 00:00:00 2001 From: ckeller Date: Thu, 26 Mar 2020 12:14:05 +0100 Subject: Test asynchronous and make the selected lemmas persistant (#66) * Add a test target for asynchronous proof checking (does not fully reflect the coqide behavior though) * Make the selected lemmas persistant Co-authored-by: Chantal Keller --- unit-tests/Makefile | 11 +- unit-tests/Tests_lfsc_tactics.v | 155 ++++++++++++++------------ unit-tests/Tests_verit_tactics.v | 224 ++++++++++++++++++++------------------ unit-tests/Tests_zchaff_tactics.v | 58 ++++++---- 4 files changed, 246 insertions(+), 202 deletions(-) (limited to 'unit-tests') diff --git a/unit-tests/Makefile b/unit-tests/Makefile index d8e9be0..4820887 100644 --- a/unit-tests/Makefile +++ b/unit-tests/Makefile @@ -7,6 +7,7 @@ OBJ=$(ZCHAFFLOG) $(VERITLOG) COQLIBS?= -R ../src SMTCoq OPT?= COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) +VIOFLAG?=-quick COQC?=$(COQBIN)coqc @@ -39,9 +40,17 @@ logs: $(OBJ) $(COQC) $(COQDEBUG) $(COQFLAGS) $* +%.vio: %.v logs + $(COQC) $(VIOFLAG) $(COQDEBUG) $(COQFLAGS) $* + + +parallel: Tests_zchaff_tactics.vio Tests_verit_tactics.vio Tests_lfsc_tactics.vio + coqtop -schedule-vio-checking 3 Tests_zchaff_tactics Tests_verit_tactics Tests_lfsc_tactics + + clean: cleanvo rm -rf *~ $(ZCHAFFLOG) $(VERITLOG) cleanvo: - rm -rf *~ *.vo *.glob + rm -rf *~ *.vo *.glob *.vio diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v index ee9df76..2268cb9 100644 --- a/unit-tests/Tests_lfsc_tactics.v +++ b/unit-tests/Tests_lfsc_tactics.v @@ -29,7 +29,7 @@ Local Open Scope bv_scope. Goal forall (a b c: bitvector 4), (c = (bv_and a b)) -> ((bv_and (bv_and c a) b) = c). - Proof. + Proof using. smt. Qed. @@ -38,19 +38,19 @@ Local Open Scope bv_scope. bv2 = #b|1|0|0|0| /\ bv3 = #b|1|1|0|0| -> bv_ultP bv1 bv2 /\ bv_ultP bv2 bv3. - Proof. + Proof using. smt. Qed. Goal forall (a: bitvector 32), a = a. - Proof. + Proof using. smt. Qed. Goal forall (bv1 bv2: bitvector 4), bv1 = bv2 <-> bv2 = bv1. - Proof. + Proof using. smt. Qed. @@ -64,7 +64,7 @@ Section Arrays. Goal forall (a:farray Z Z) i j, i = j -> a[i] = a[j]. - Proof. + Proof using. smt. Qed. @@ -74,7 +74,7 @@ Section Arrays. (f: Z -> Z), (a[x <- v] = b) /\ a[y <- w] = b -> (f x) = (f y) \/ (g a) = (g b). - Proof. + Proof using. smt. Qed. @@ -85,7 +85,7 @@ Section Arrays. (* d = b[0%Z <- 4][1%Z <- 4] -> *) (* a = d[1%Z <- b[1%Z]] -> *) (* a = c. *) - (* Proof. *) + (* Proof using. *) (* smt. *) (* Qed. *) @@ -93,7 +93,7 @@ Section Arrays. (* Goal forall (a b: farray Z Z) i, (select (store (store (store a i 3%Z) 1%Z (select (store b i 4) i)) 2%Z 2%Z) 1%Z) = 4. - Proof. + Proof using. smt. rewrite read_over_other_write; try easy. rewrite read_over_same_write; try easy; try apply Z_compdec. @@ -111,7 +111,7 @@ Section EUF. (x y: Z) (f: Z -> Z), y = x -> (f x) = (f y). - Proof. + Proof using. smt. Qed. @@ -119,7 +119,7 @@ Section EUF. (x y: Z) (f: Z -> Z), (f x) = (f y) -> (f y) = (f x). - Proof. + Proof using. smt. Qed. @@ -128,7 +128,7 @@ Section EUF. (x y: Z) (f: Z -> Z), x + 1 = (y + 1) -> (f y) = (f x). - Proof. + Proof using. smt. Qed. @@ -137,7 +137,7 @@ Section EUF. (x y: Z) (f: Z -> Z), x = (y + 1) -> (f y) = (f (x - 1)). - Proof. + Proof using. smt. Qed. @@ -145,7 +145,7 @@ Section EUF. (x y: Z) (f: Z -> Z), x = (y + 1) -> (f (y + 1)) = (f x). - Proof. + Proof using. smt. Qed. @@ -156,44 +156,44 @@ Section LIA. Goal forall (a b: Z), a = b <-> b = a. - Proof. + Proof using. smt. Qed. Goal forall (x y: Z), (x >= y) -> (y < x) \/ (x = y). - Proof. + Proof using. smt. Qed. Goal forall (f : Z -> Z) (a:Z), ((f a) > 1) -> ((f a) + 1) >= 2 \/((f a) = 30) . - Proof. + Proof using. smt. Qed. Goal forall x: Z, (x = 0%Z) -> (8 >= 0). - Proof. + Proof using. smt. Qed. Goal forall x: Z, ~ (x < 0%Z) -> (8 >= 0). - Proof. + Proof using. smt. Qed. Goal forall (a b: Z), a < b -> a < (b + 1). - Proof. + Proof using. smt. Qed. Goal forall (a b: Z), (a < b) -> (a + 2) < (b + 3). - Proof. + Proof using. smt. Qed. Goal forall a b, a < b -> a < (b + 10). - Proof. + Proof using. smt. Qed. @@ -208,141 +208,152 @@ Section PR. (* Simple connectors *) Goal forall (a:bool), a || negb a. +Proof using. smt. Qed. Goal forall a, negb (a || negb a) = false. +Proof using. smt. Qed. Goal forall a, (a && negb a) = false. +Proof using. smt. Qed. Goal forall a, negb (a && negb a). +Proof using. smt. Qed. Goal forall a, a --> a. +Proof using. smt. Qed. Goal forall a, negb (a --> a) = false. +Proof using. smt. Qed. Goal forall a , (xorb a a) || negb (xorb a a). +Proof using. smt. Qed. Goal forall a, (a||negb a) || negb (a||negb a). +Proof using. smt. Qed. (* Polarities *) Goal forall a b, andb (orb (negb (negb a)) b) (negb (orb a b)) = false. -Proof. +Proof using. smt. Qed. Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false. -Proof. +Proof using. smt. Qed. (* Multiple negations *) Goal forall a, orb a (negb (negb (negb a))) = true. -Proof. +Proof using. smt. Qed. 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. +Proof using. smt. Qed. Goal true. +Proof using. smt. Qed. Goal negb false. +Proof using. smt. Qed. Goal forall a, Bool.eqb a a. -Proof. +Proof using. smt. Qed. Goal forall (a:bool), a = a. +Proof using. smt. Qed. Goal (false || true) && false = false. -Proof. +Proof using. smt. Qed. Goal negb true = false. -Proof. +Proof using. smt. Qed. Goal false = false. -Proof. +Proof using. smt. Qed. Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)). -Proof. +Proof using. smt. Qed. Goal forall x y, Bool.eqb (x --> y) ((x && y) || (negb x)). -Proof. +Proof using. smt. Qed. Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)). -Proof. +Proof using. smt. Qed. Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false. -Proof. +Proof using. smt. Qed. Goal forall a, ((a || a) && (negb a)) = false. -Proof. +Proof using. smt. Qed. Goal forall a, (negb (a || (negb a))) = false. -Proof. +Proof using. smt. Qed. 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. +Proof using. smt. Qed. @@ -353,19 +364,19 @@ Goal forall i j k, 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. +Proof using. smt. Qed. Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false. -Proof. +Proof using. smt. Qed. @@ -458,35 +469,35 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42 (orb (orb (orb x13 x23) x33) x43) && (orb (orb (orb x14 x24) x34) x44) && (orb (orb (orb x15 x25) x35) x45)) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c f p, ((Z.eqb a c) && (Z.eqb b c) && ((negb (Z.eqb (f a) (f b))) || ((p a) && (negb (p b))))) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c (p : Z -> bool), ((((p a) && (p b)) || ((p b) && (p c))) && (negb (p b))) = false. -Proof. +Proof using. smt. Qed. Goal forall x y z f, ((Z.eqb x y) && (Z.eqb y z) && (negb (Z.eqb (f x) (f z)))) = false. -Proof. +Proof using. smt. Qed. Goal forall x y z f, ((negb (Z.eqb (f x) (f y))) && (Z.eqb y z) && (Z.eqb (f x) (f (f z))) && (Z.eqb x y)) = false. -Proof. +Proof using. smt. Qed. Goal forall a b c d e f, ((Z.eqb a b) && (Z.eqb b c) && (Z.eqb c d) && (Z.eqb c e) && (Z.eqb e f) && (negb (Z.eqb a f))) = false. -Proof. +Proof using. smt. Qed. @@ -494,54 +505,54 @@ Qed. Goal forall x y z, ((x <=? 3) && ((y <=? 7) || (z <=? 9))) --> ((x + y <=? 10) || (x + z <=? 12)) = true. -Proof. +Proof using. smt. Qed. Goal forall x, (Z.eqb (x - 3) 7) --> (x >=? 10) = true. -Proof. +Proof using. smt. Qed. Goal forall x y, (x >? y) --> (y + 1 <=? x) = true. -Proof. +Proof using. smt. Qed. Goal forall x y, Bool.eqb (x =? 0) || (x <=? - (3))) && (x >=? 0) = false. - Proof. + Proof using. smt. Qed. Goal forall x, (andb ((x - 3) <=? 7) (7 <=? (x - 3))) --> (x >=? 10) = true. -Proof. +Proof using. smt. Qed. Goal forall x, (Z.eqb (x - 3) 7) --> (10 <=? x) = true. -Proof. +Proof using. smt. Qed. (* More general examples *) 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. +Proof using. smt. Qed. Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), (negb (Z.eqb (f a) b)) || (negb (P (f a))) || (P b). -Proof. +Proof using. smt. Qed. @@ -551,7 +562,7 @@ Goal forall b1 b2 x1 x2, (ifb b2 (Z.eqb (2*x1+1) (2*x2+1)) (Z.eqb (2*x1+1) (2*x2))) (ifb b2 (Z.eqb (2*x1) (2*x2+1)) (Z.eqb (2*x1) (2*x2)))) --> ((b1 --> b2) && (b2 --> b1) && (Z.eqb x1 x2)). -Proof. +Proof using. smt. Qed. @@ -560,14 +571,14 @@ Qed. Goal forall b, let a := b in a && (negb a) = false. -Proof. +Proof using. smt. Qed. Goal forall b, let a := b in a || (negb a) = true. -Proof. +Proof using. smt. Qed. @@ -575,14 +586,14 @@ Qed. Goal forall i j, let a := i == j in a && (negb a) = false. -Proof. +Proof using. smt. Qed. Goal forall i j, let a := i == j in a || (negb a) = true. -Proof. +Proof using. smt. Qed. @@ -590,19 +601,19 @@ Qed. (* Congruence in which some premises are REFL *) Goal forall (f:Z -> Z -> Z) x y z, (Z.eqb x y) --> (Z.eqb (f z x) (f z y)). -Proof. +Proof using. smt. Qed. Goal forall (f:Z -> Z -> Z) x y z, (x = y) -> (f z x) = (f z y). -Proof. +Proof using. smt. Qed. Goal forall (P:Z -> Z -> bool) x y z, (Z.eqb x y) --> ((P z x) --> (P z y)). -Proof. +Proof using. smt. Qed. @@ -625,7 +636,7 @@ Section A_BV_EUF_LIA_PR. (* d = b[bv1 <- 4][bv2 <- 4] -> *) (* a = d[bv2 <- b[bv2]] -> *) (* a = c. *) - (* Proof. *) + (* Proof using. *) (* smt. *) (* Qed. *) @@ -638,7 +649,7 @@ Section A_BV_EUF_LIA_PR. (* d = b[bv1 <- 4][bv2 <- 4] /\ *) (* a = d[bv2 <- b[bv2]] -> *) (* a = c. *) - (* Proof. *) + (* Proof using. *) (* smt. *) (* Qed. *) @@ -652,7 +663,7 @@ Section A_BV_EUF_LIA_PR. r = s /\ h r = v /\ h s = y -> v < x + 1 /\ v > x - 1 -> f (h r) = f (h s) \/ g a = g b. - Proof. + Proof using. smt. (** "cvc4. verit." also solves the goal *) Qed. @@ -666,7 +677,7 @@ Section A_BV_EUF_LIA_PR. a[z <- w] = b /\ a[t <- v] = b -> r = s -> v < x + 10 /\ v > x - 5 -> ~ (g a = g b) \/ f (h r) = f (h s). - Proof. + Proof using. smt. (** "cvc4. verit." also solves the goal *) Qed. @@ -677,7 +688,7 @@ Section A_BV_EUF_LIA_PR. b[bv_add y x <- v] = a /\ b = a[bv_add x y <- v] -> a = b. - Proof. + Proof using. smt. (* CVC4 preprocessing hole on BV *) replace (bv_add x y) with (bv_add y x) @@ -686,12 +697,12 @@ Section A_BV_EUF_LIA_PR. Qed. Goal forall (a:farray Z Z), a = a. - Proof. + Proof using. smt. Qed. Goal forall (a b: farray Z Z), a = b <-> b = a. - Proof. + Proof using. smt. Qed. @@ -714,15 +725,15 @@ Section group. Lemma inverse' : forall a : Z, (op a (inv a) =? e). - Proof. smt. Qed. + Proof using associative identity inverse. smt. Qed. Lemma identity' : forall a : Z, (op a e =? a). - Proof. smt inverse'. Qed. + Proof using associative identity inverse. smt inverse'. Qed. Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. - Proof. intros pe'; smt pe'. Qed. + Proof using associative identity inverse. intros pe'; smt pe'. Qed. Clear_lemmas. End group. diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 6ed1d67..6f0cb7e 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -23,14 +23,14 @@ Open Scope Z_scope. Lemma check_univ (x1: bool): (x1 && (negb x1)) = false. -Proof. +Proof using. verit. Qed. Lemma fun_const2 : forall f (g : Z -> Z -> bool), (forall x, g (f x) 2) -> g (f 3) 2. -Proof. +Proof using. intros f g Hf. verit Hf. Qed. @@ -38,51 +38,62 @@ Qed. (* Simple connectives *) Goal forall (a:bool), a || negb a. +Proof using. verit. Qed. Goal forall a, negb (a || negb a) = false. +Proof using. verit. Qed. Goal forall a, (a && negb a) = false. +Proof using. verit. Qed. Goal forall a, negb (a && negb a). +Proof using. verit. Qed. Goal forall a, implb a a. +Proof using. verit. Qed. Goal forall a, negb (implb a a) = false. +Proof using. verit. Qed. Goal forall a , (xorb a a) || negb (xorb a a). +Proof using. verit. Qed. Goal forall a, (a||negb a) || negb (a||negb a). +Proof using. verit. Qed. Goal true. +Proof using. verit. Qed. Goal negb false. +Proof using. verit. Qed. Goal forall a, Bool.eqb a a. -Proof. +Proof using. verit. Qed. Goal forall (a:bool), a = a. +Proof using. verit. Qed. @@ -90,43 +101,43 @@ Qed. (* Other connectives *) Goal (false || true) && false = false. -Proof. +Proof using. verit. Qed. Goal negb true = false. -Proof. +Proof using. verit. Qed. Goal false = false. -Proof. +Proof using. verit. Qed. Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)). -Proof. +Proof using. verit. Qed. Goal forall x y, Bool.eqb (negb (xorb x y)) ((x && y) || ((negb x) && (negb y))). -Proof. +Proof using. verit. Qed. Goal forall x y, Bool.eqb (implb x y) ((x && y) || (negb x)). -Proof. +Proof using. verit. Qed. Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)). -Proof. +Proof using. verit. Qed. @@ -134,7 +145,7 @@ Qed. (* Multiple negations *) Goal forall a, orb a (negb (negb (negb a))) = true. -Proof. +Proof using. verit. Qed. @@ -142,13 +153,13 @@ Qed. (* Polarities *) Goal forall a b, andb (orb a b) (negb (orb a b)) = false. -Proof. +Proof using. verit. Qed. Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false. -Proof. +Proof using. verit. Qed. @@ -157,7 +168,7 @@ Qed. (* ((a ∧ b) ∨ (b ∧ c)) ∧ ¬b = ⊥ *) Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false. -Proof. +Proof using. verit. Qed. @@ -166,7 +177,7 @@ Qed. (* (a ∨ a) ∧ ¬a = ⊥ *) Goal forall a, ((a || a) && (negb a)) = false. -Proof. +Proof using. verit. Qed. @@ -175,7 +186,7 @@ Qed. (* ¬(a ∨ ¬a) = ⊥ *) Goal forall a, (negb (a || (negb a))) = false. -Proof. +Proof using. verit. Qed. @@ -185,7 +196,7 @@ Qed. 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. +Proof using. verit. Qed. @@ -197,7 +208,7 @@ Goal forall i j k, 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. +Proof using. verit. Qed. @@ -206,7 +217,7 @@ Qed. (* (a ∧ b) ∧ (c ∨ d) ∧ ¬(c ∨ (a ∧ b ∧ d)) = ⊥ *) Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false. -Proof. +Proof using. verit. Qed. @@ -215,7 +226,7 @@ Qed. (* a ∧ b ∧ c ∧ (¬a ∨ ¬b ∨ d) ∧ (¬d ∨ ¬c) = ⊥ *) Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false. -Proof. +Proof using. verit. Qed. @@ -309,7 +320,7 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42 (orb (orb (orb x13 x23) x33) x43) && (orb (orb (orb x14 x24) x34) x44) && (orb (orb (orb x15 x25) x35) x45)) = false. -Proof. +Proof using. verit. Qed. @@ -317,7 +328,7 @@ Qed. (* uf1.smt *) Goal forall a b c f p, ( (a =? c) && (b =? c) && ((negb (f a =?f b)) || ((p a) && (negb (p b))))) = false. -Proof. +Proof using. verit. Qed. @@ -325,7 +336,7 @@ Qed. (* uf2.smt *) Goal forall a b c (p : Z -> bool), ((((p a) && (p b)) || ((p b) && (p c))) && (negb (p b))) = false. -Proof. +Proof using. verit. Qed. @@ -333,7 +344,7 @@ Qed. (* uf3.smt *) Goal forall x y z f, ((x =? y) && (y =? z) && (negb (f x =? f z))) = false. -Proof. +Proof using. verit. Qed. @@ -341,7 +352,7 @@ Qed. (* uf4.smt *) Goal forall x y z f, ((negb (f x =? f y)) && (y =? z) && (f x =? f (f z)) && (x =? y)) = false. -Proof. +Proof using. verit. Qed. @@ -349,7 +360,7 @@ Qed. (* uf5.smt *) Goal forall a b c d e f, ((a =? b) && (b =? c) && (c =? d) && (c =? e) && (e =? f) && (negb (a =? f))) = false. -Proof. +Proof using. verit. Qed. @@ -358,28 +369,28 @@ Qed. Goal forall x y z, implb ((x <=? 3) && ((y <=? 7) || (z <=? 9))) ((x + y <=? 10) || (x + z <=? 12)) = true. -Proof. +Proof using. verit. Qed. (* lia2.smt *) Goal forall x, implb (x - 3 =? 7) (x >=? 10) = true. -Proof. +Proof using. verit. Qed. (* lia3.smt *) Goal forall x y, implb (x >? y) (y + 1 <=? x) = true. -Proof. +Proof using. verit. Qed. (* lia4.smt *) Goal forall x y, Bool.eqb (x =? 0) || (x <=? - (3))) && (x >=? 0) = false. -Proof. +Proof using. verit. Qed. (* lia6.smt *) Goal forall x, implb (andb ((x - 3) <=? 7) (7 <=? (x - 3))) (x >=? 10) = true. -Proof. +Proof using. verit. Qed. (* lia7.smt *) Goal forall x, implb (x - 3 =? 7) (10 <=? x) = true. -Proof. +Proof using. verit. Qed. @@ -409,7 +420,7 @@ Qed. Lemma irrelf_ltb a b c: (Z.ltb a b) && (Z.ltb b c) && (Z.ltb c a) = false. -Proof. +Proof using. verit. Qed. @@ -419,20 +430,20 @@ Lemma comp f g (x1 x2 x3 : Z) : (Z.eqb x1 (f (g x3))) true) true. -Proof. verit. Qed. +Proof using. verit. Qed. (* More general examples *) 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. +Proof using. verit. Qed. Goal forall (a b : Z) (P : Z -> bool) (f : Z -> Z), (negb (f a =? b)) || (negb (P (f a))) || (P b). -Proof. +Proof using. verit. Qed. @@ -443,7 +454,7 @@ Goal forall b1 b2 x1 x2, (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2)) (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)). -Proof. +Proof using. verit. Qed. @@ -453,21 +464,21 @@ Qed. Goal forall b, let a := b in a && (negb a) = false. -Proof. +Proof using. verit. Qed. Goal forall b, let a := b in a || (negb a) = true. -Proof. +Proof using. verit. Qed. (* Does not work since the [is_true] coercion includes [let in] Goal forall b, let a := b in a || (negb a). -Proof. +Proof using. verit. Qed. *) @@ -477,27 +488,27 @@ Qed. Goal forall i j, let a := i == j in a && (negb a) = false. -Proof. +Proof using. verit. Qed. Goal forall i j, let a := i == j in a || (negb a) = true. -Proof. +Proof using. verit. Qed. (* TODO: fails with native-coq: "compilation error" Goal forall (i j:int), (i == j) && (negb (i == j)) = false. -Proof. +Proof using. verit. exact int63_compdec. Qed. Goal forall i j, (i == j) || (negb (i == j)). -Proof. +Proof using. verit. exact int63_compdec. Qed. @@ -508,13 +519,13 @@ Qed. Goal forall (f:Z -> Z -> Z) x y z, implb (x =? y) (f z x =? f z y). -Proof. +Proof using. verit. Qed. Goal forall (P:Z -> Z -> bool) x y z, implb (x =? y) (implb (P z x) (P z y)). -Proof. +Proof using. verit. Qed. @@ -524,80 +535,80 @@ Qed. Lemma taut1 : forall f, f 2 =? 0 -> f 2 =? 0. -Proof. intros f p. verit p. Qed. +Proof using. intros f p. verit p. Qed. Lemma taut2 : forall f, 0 =? f 2 -> 0 =?f 2. -Proof. intros f p. verit p. Qed. +Proof using. intros f p. verit p. Qed. Lemma taut3 : forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0. -Proof. intros f p1 p2. verit p1 p2. Qed. +Proof using. intros f p1 p2. verit p1 p2. Qed. Lemma taut4 : forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0. -Proof. intros f p1 p2. verit p1 p2. Qed. +Proof using. intros f p1 p2. verit p1 p2. Qed. Lemma test_eq_sym a b : implb (a =? b) (b =? a). -Proof. verit. Qed. +Proof using. verit. Qed. Lemma taut5 : forall f, 0 =? f 2 -> f 2 =? 0. -Proof. intros f p. verit p. Qed. +Proof using. intros f p. verit p. Qed. Lemma fun_const_Z : forall f , (forall x, f x =? 2) -> f 3 =? 2. -Proof. intros f Hf. verit Hf. Qed. +Proof using. intros f Hf. verit Hf. Qed. Lemma lid (A : bool) : A -> A. -Proof. intro a. verit a. Qed. +Proof using. intro a. verit a. Qed. Lemma lpartial_id A : (xorb A A) -> (xorb A A). -Proof. intro xa. verit xa. Qed. +Proof using. intro xa. verit xa. Qed. Lemma llia1 X Y Z: (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) -> (X + Y <=? 10) || (X + Z <=? 12). -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma llia2 X: X - 3 =? 7 -> X >=? 10. -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma llia3 X Y: X >? Y -> Y + 1 <=? X. -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma llia6 X: andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10. -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma even_odd b1 b2 x1 x2: (ifb b1 (ifb b2 (2*x1+1 =? 2*x2+1) (2*x1+1 =? 2*x2)) (ifb b2 (2*x1 =? 2*x2+1) (2*x1 =? 2*x2))) -> ((implb b1 b2) && (implb b2 b1) && (x1 =? x2)). -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma lcongr1 (a b : Z) (P : Z -> bool) f: (f a =? b) -> (P (f a)) -> P b. -Proof. intros eqfab pfa. verit eqfab pfa. Qed. +Proof using. intros eqfab pfa. verit eqfab pfa. Qed. Lemma lcongr2 (f:Z -> Z -> Z) x y z: x =? y -> f z x =? f z y. -Proof. intro p. verit p. Qed. +Proof using. intro p. verit p. Qed. Lemma lcongr3 (P:Z -> Z -> bool) x y z: x =? y -> P z x -> P z y. -Proof. intros eqxy pzx. verit eqxy pzx. Qed. +Proof using. intros eqxy pzx. verit eqxy pzx. Qed. Lemma test20 : forall x, (forall a, a 0 <=? x = false. -Proof. intros x H. verit H. Qed. +Proof using. intros x H. verit H. Qed. Lemma test21 : forall x, (forall a, negb (x <=? a)) -> negb (0 <=? x). -Proof. intros x H. verit H. Qed. +Proof using. intros x H. verit H. Qed. Lemma un_menteur (a b c d : Z) dit: dit a =? c -> @@ -606,13 +617,13 @@ Lemma un_menteur (a b c d : Z) dit: (a =? c) || (a =? d) -> (b =? c) || (b =? d) -> a =? d. -Proof. intros H1 H2 H3 H4 H5. verit H1 H2 H3 H4 H5. Qed. +Proof using. intros H1 H2 H3 H4 H5. verit H1 H2 H3 H4 H5. Qed. Lemma const_fun_is_eq_val_0 : forall f : Z -> Z, (forall a b, f a =? f b) -> forall x, f x =? f 0. -Proof. intros f Hf. verit Hf. Qed. +Proof using. intros f Hf. verit Hf. Qed. (* You can use to permanently add the lemmas H1 .. Hn to the environment. If you did so in a section then, at the end of the section, @@ -624,7 +635,7 @@ Section S. Hypothesis th : forall x, Z.eqb (f x) 3. Add_lemmas th. Goal forall x, Z.eqb ((f x) + 1) 4. - Proof. verit. Qed. + Proof using th. verit. Qed. Clear_lemmas. End S. @@ -635,7 +646,7 @@ Section fins_sat6. Add_lemmas andab orcd. Lemma sat6 : orb c (andb a (andb b d)). - Proof. verit. Qed. + Proof using andab orcd. verit. Qed. Clear_lemmas. End fins_sat6. @@ -649,7 +660,7 @@ Section fins_lemma_multiple. Add_lemmas g_k_linear f'_equal_k. Lemma apply_lemma_multiple : forall x y, g (x + 1) =? g x + f' y. - Proof. verit. Qed. + Proof using g_k_linear f'_equal_k. verit. Qed. Clear_lemmas. End fins_lemma_multiple. @@ -661,11 +672,11 @@ Section fins_find_apply_lemma. Add_lemmas u_is_constant. Lemma apply_lemma : forall x, u x =? u 2. - Proof. verit. Qed. + Proof using u_is_constant. verit. Qed. Lemma find_inst : implb (u 2 =? 5) (u 3 =? 5). - Proof. verit. Qed. + Proof using u_is_constant. verit. Qed. Clear_lemmas. End fins_find_apply_lemma. @@ -678,7 +689,7 @@ Section mult3. Add_lemmas mult3_0 mult3_Sn. Lemma mult3_4_12 : mult3 4 =? 12. - Proof. verit. Qed. (* slow to verify with standard coq *) + Proof using mult3_0 mult3_Sn. verit. Qed. (* slow to verify with standard coq *) Clear_lemmas. End mult3. @@ -691,7 +702,7 @@ End mult3. (* Hypothesis mult_Sx : forall x y, mult (x+1) y =? mult x y + y. *) (* Lemma mult_1_x : forall x, mult 1 x =? x. *) -(* Proof. verit mult_0 mult_Sx. *) +(* Proof using. verit mult_0 mult_Sx. *) (* Qed. *) (* End mult. *) @@ -704,7 +715,7 @@ Section implicit_transform. Lemma implicit_transform : f a2. - Proof. verit. Qed. + Proof using f_const f_a1. verit. Qed. Clear_lemmas. End implicit_transform. @@ -724,23 +735,23 @@ Section list. Lemma in_cons1 : inlist 1 (1::2::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. Lemma in_cons2 : inlist 12 (2::4::12::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. Lemma in_cons3 : inlist 1 (5::1::(0-1)::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. Lemma in_cons4 : inlist 22 ((- (1))::22::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. Lemma in_cons5 : inlist 1 ((- 1)::1::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons. verit. Qed. (* Lemma in_cons_false1 : *) (* inlist 1 (2::3::nil). *) @@ -764,15 +775,15 @@ Section list. Lemma in_app1 : inlist 1 (1::2::nil ++ nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed. Lemma in_app2 : inlist 1 (nil ++ 2::1::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed. Lemma in_app3 : inlist 1 (1::3::nil ++ 2::1::nil). - Proof. verit. Qed. + Proof using dec_Zlist in_eq in_cons in_or_app. verit. Qed. (* Lemma in_app_false1 : *) (* inlist 1 (nil ++ 2::3::nil). *) @@ -802,7 +813,7 @@ Section list. Lemma coqhammer_example l1 l2 x y1 y2 y3: implb (orb (inlist x l1) (orb (inlist x l2) (orb (x =? y1) (inlist x (y2 ::y3::nil))))) (inlist x (y1::(l1 ++ (y2 :: (l2 ++ (y3 :: nil)))))). - Proof. verit_no_check. Qed. + Proof using dec_Zlist in_eq in_cons in_or_app in_nil in_inv inlist_app_comm_cons. verit_no_check. Qed. Clear_lemmas. End list. @@ -823,59 +834,59 @@ Section group. Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. - Proof. intros pe'. verit pe'. Qed. + Proof using associative identity inverse. intros pe'. verit pe'. Qed. Lemma simplification_right x1 x2 y: op x1 y =? op x2 y -> x1 =? x2. - Proof. intro H. verit H. Qed. + Proof using associative identity inverse. intro H. verit H. Qed. Lemma simplification_left x1 x2 y: op y x1 =? op y x2 -> x1 =? x2. - Proof. intro H. verit H. Qed. + Proof using associative identity inverse. intro H. verit H. Qed. Clear_lemmas. End group. Section Linear1. - Parameter f : Z -> Z. - Axiom f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0). + Variable f : Z -> Z. + Hypothesis f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0). (* Cuts are not automatically proved when one equality is switched *) Lemma f_1 : f 1 =? 1. - Proof. + Proof using f_spec. verit_bool f_spec; replace (0 =? f 0) with (f 0 =? 0) by apply Z.eqb_sym; auto. Qed. End Linear1. Section Linear2. - Parameter g : Z -> Z. + Variable g : Z -> Z. - Axiom g_2_linear : forall x, Z.eqb (g (x + 1)) ((g x) + 2). + Hypothesis g_2_linear : forall x, Z.eqb (g (x + 1)) ((g x) + 2). (* The call to veriT does not terminate *) (* Lemma apply_lemma_infinite : *) (* forall x y, Z.eqb (g (x + y)) ((g x) + y * 2). *) -(* Proof. verit g_2_linear. *) +(* Proof using. verit g_2_linear. *) End Linear2. Section Input_switched1. - Parameter m : Z -> Z. + Variable m : Z -> Z. - Axiom m_0 : m 0 =? 5. + Hypothesis m_0 : m 0 =? 5. (* veriT switches the input lemma in this case *) Lemma cinq_m_0 : m 0 =? 5. - Proof. verit m_0. Qed. + Proof using m_0. verit m_0. Qed. End Input_switched1. Section Input_switched2. - Parameter h : Z -> Z -> Z. + Variable h : Z -> Z -> Z. - Axiom h_Sm_n : forall x y, h (x+1) y =? h x y. + Hypothesis h_Sm_n : forall x y, h (x+1) y =? h x y. (* veriT switches the input lemma in this case *) Lemma h_1_0 : h 1 0 =? h 0 0. - Proof. verit h_Sm_n. Qed. + Proof using h_Sm_n. verit h_Sm_n. Qed. End Input_switched2. @@ -887,7 +898,7 @@ Goal forall (f : positive -> positive) (x y : positive), implb ((x + 3) =? y) ((f (x + 3)) <=? (f y)) = true. -Proof. +Proof using. pos_convert. verit. Qed. @@ -896,7 +907,7 @@ Goal forall (f : positive -> positive) (x y : positive), implb ((x + 3) =? y) ((3 N) (x y : N), implb ((x + 3) =? y) ((f (x + 3)) <=? (f y)) = true. -Proof. +Proof using. N_convert. verit. Qed. @@ -918,7 +929,7 @@ Goal forall (f : N -> N) (x y : N), implb ((x + 3) =? y) ((2 nat) (x y : nat), implb (Nat.eqb (x + 3) y) ((f (x + 3)) <=? (f y)) = true. -Proof. +Proof using. nat_convert. verit. Qed. @@ -941,7 +952,7 @@ Goal forall (f : nat -> nat) (x y : nat), implb (Nat.eqb (x + 3) y) ((2 nat -> N, forall (x : positive) (y : nat), (implb (Nat.eqb y 7) (implb (f 3%positive 7%nat =? 12)%N (f x y =? 12)%N)) = true. +Proof using. pos_convert. nat_convert. N_convert. diff --git a/unit-tests/Tests_zchaff_tactics.v b/unit-tests/Tests_zchaff_tactics.v index c6ed4e3..cf86bc1 100644 --- a/unit-tests/Tests_zchaff_tactics.v +++ b/unit-tests/Tests_zchaff_tactics.v @@ -23,7 +23,7 @@ Local Open Scope int63_scope. Lemma check_univ (x1: bool): (x1 && (negb x1)) = false. -Proof. +Proof using. zchaff. Qed. @@ -31,55 +31,67 @@ Qed. (* zChaff tactic *) Goal forall a, a || negb a. +Proof using. zchaff. Qed. Goal forall a, negb (a || negb a) = false. +Proof using. zchaff. Qed. Goal forall a, negb (negb (a || negb a)). +Proof using. zchaff. Qed. Goal forall a, (a && negb a) = false. +Proof using. zchaff. Qed. Goal forall a, negb (a && negb a). +Proof using. zchaff. Qed. Goal forall a, implb a a. +Proof using. zchaff. Qed. Goal forall a, negb (implb a a) = false. +Proof using. zchaff. Qed. Goal forall a , (xorb a a) || negb (xorb a a). +Proof using. zchaff. Qed. Goal forall a, (a||negb a) || negb (a||negb a). +Proof using. zchaff. Qed. Goal true. +Proof using. zchaff. Qed. Goal negb false. +Proof using. zchaff. Qed. Goal forall a, Bool.eqb a a. -Proof. +Proof using. zchaff. Qed. Goal forall (a:bool), a = a. +Proof using. zchaff. Qed. @@ -88,7 +100,7 @@ Qed. (* ((a ∧ b) ∨ (b ∧ c)) ∧ ¬b = ⊥ *) Goal forall a b c, (((a && b) || (b && c)) && (negb b)) = false. -Proof. +Proof using. zchaff. Qed. @@ -97,7 +109,7 @@ Qed. (* (a ∨ a) ∧ ¬a = ⊥ *) Goal forall a, ((a || a) && (negb a)) = false. -Proof. +Proof using. zchaff. Qed. @@ -106,7 +118,7 @@ Qed. (* ¬(a ∨ ¬a) = ⊥ *) Goal forall a, (negb (a || (negb a))) = false. -Proof. +Proof using. zchaff. Qed. @@ -116,7 +128,7 @@ Qed. 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. +Proof using. zchaff. Qed. @@ -125,7 +137,7 @@ Qed. Goal forall i j k, ((i == j) || (j == k) || (k == i)) && ((negb (i == j)) || (negb (j == k)) || (negb (k == i))) && ((negb (i == j)) || (j == k)) && ((negb (j == k)) || (k == i)) && ((negb (k == i)) || (i == j)) = false. -Proof. +Proof using. zchaff. Qed. @@ -134,7 +146,7 @@ Goal forall i j k, 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. +Proof using. zchaff. Qed. @@ -143,7 +155,7 @@ Qed. (* (a ∧ b) ∧ (c ∨ d) ∧ ¬(c ∨ (a ∧ b ∧ d)) = ⊥ *) Goal forall a b c d, ((a && b) && (c || d) && (negb (c || (a && b && d)))) = false. -Proof. +Proof using. zchaff. Qed. @@ -152,7 +164,7 @@ Qed. (* a ∧ b ∧ c ∧ (¬a ∨ ¬b ∨ d) ∧ (¬d ∨ ¬c) = ⊥ *) Goal forall a b c d, (a && b && c && ((negb a) || (negb b) || d) && ((negb d) || (negb c))) = false. -Proof. +Proof using. zchaff. Qed. @@ -160,37 +172,37 @@ Qed. (* Other connectives *) Goal (false || true) && false = false. -Proof. +Proof using. zchaff. Qed. Goal negb true = false. -Proof. +Proof using. zchaff. Qed. Goal false = false. -Proof. +Proof using. zchaff. Qed. Goal forall x y, Bool.eqb (xorb x y) ((x && (negb y)) || ((negb x) && y)). -Proof. +Proof using. zchaff. Qed. Goal forall x y, Bool.eqb (implb x y) ((x && y) || (negb x)). -Proof. +Proof using. zchaff. Qed. Goal forall x y z, Bool.eqb (ifb x y z) ((x && y) || ((negb x) && z)). -Proof. +Proof using. zchaff. Qed. @@ -198,7 +210,7 @@ Qed. (* Multiple negations *) Goal forall a, orb a (negb (negb (negb a))) = true. -Proof. +Proof using. zchaff. Qed. @@ -206,13 +218,13 @@ Qed. (* Polarities *) Goal forall a b, andb (orb a b) (negb (orb a b)) = false. -Proof. +Proof using. zchaff. Qed. Goal forall a b, andb (orb a b) (andb (negb a) (negb b)) = false. -Proof. +Proof using. zchaff. Qed. @@ -307,7 +319,7 @@ Goal forall x11 x12 x13 x14 x15 x21 x22 x23 x24 x25 x31 x32 x33 x34 x35 x41 x42 (orb (orb (orb x13 x23) x33) x43) && (orb (orb (orb x14 x24) x34) x44) && (orb (orb (orb x15 x25) x35) x45)) = false. -Proof. +Proof using. zchaff. Qed. @@ -316,12 +328,12 @@ Qed. (* Goal forall x, x && (negb x). -Proof. +Proof using. zchaff. Abort. Goal forall x y, (implb (implb x y) (implb y x)). -Proof. +Proof using. zchaff. Abort. @@ -391,7 +403,7 @@ Goal forall x11 x12 x13 x14 x21 x22 x23 x24 x31 x32 x33 x34 x41 x42 x43 x44, ( (orb (orb (orb x12 x22) x32) x42) && (orb (orb (orb x13 x23) x33) x43) && (orb (orb (orb x14 x24) x34) x44)) = false. -Proof. +Proof using. zchaff. Abort. *) -- cgit