Adding support for lemmas in the command verit

2 files changed, 362 insertions, 0 deletions

diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index 827dc4b..f39e904 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -14,6 +14,28 @@ Proof.
   verit.
 Qed.
 
+(* In standard coq we need decidability of Int31.digits *)
+(* Lemma fun_const : *)
+(*   forall f (g : int -> int -> bool), *)
+(*     (forall x, g (f x) 2) -> g (f 3) 2. *)
+(* Proof. *)
+(*   intros f g Hf. *)
+(*   verit_base Hf; vauto. *)
+(*   exists (fun x y => match (x, y) with (Int31.D0, Int31.D0) | (Int31.D1, Int31.D1) => true | _ => false end). *)
+(*   intros x y; destruct x, y; constructor; try reflexivity; try discriminate. *)
+(*   exists Int63Native.eqb. *)
+(*   apply Int63Properties.reflect_eqb. *)
+(* Qed. *)
+
+Open Scope Z_scope.
+
+Lemma fun_const2 :
+  forall f (g : Z -> Z -> bool),
+    (forall x, g (f x) 2) -> g (f 3) 2.
+Proof.
+  intros f g Hf.
+  verit_base Hf; vauto.
+Qed.
 
 (* veriT vernacular commands *)
 
@@ -73,6 +95,10 @@ Section Checker_Sat13.
   Verit_Checker "sat13.smt2" "sat13.vtlog".
 End Checker_Sat13.
 
+Section Checker_Sat14.
+  Verit_Checker "sat14.smt2" "sat14.vtlog".
+End Checker_Sat14.
+
 Section Checker_Hole4.
   Verit_Checker "hole4.smt2" "hole4.vtlog".
 End Checker_Hole4.
@@ -830,6 +856,23 @@ Proof.
   verit.
 Qed.
 
+(* Misc *)
+
+Lemma irrelf_ltb a b c:
+  (Z.ltb a b) && (Z.ltb b c) && (Z.ltb c a) = false.
+Proof.
+  verit.
+Qed.
+
+Lemma comp f g (x1 x2 x3 : Z) :
+  ifb (Z.eqb x1 (f x2))
+      (ifb (Z.eqb x2 (g x3))
+           (Z.eqb x1 (f (g x3)))
+           true)
+      true.
+Proof. 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.
@@ -930,3 +973,312 @@ Qed.
    coq-load-path: ((rec "../src" "SMTCoq"))
    End:
 *)
+
+(* Some examples of using verit with lemmas. Use <verit_base H1 .. Hn; vauto>
+   to temporarily add the lemmas H1 .. Hn to the verit environment. *)
+
+Lemma taut1 :
+  forall f, f 2 =? 0 -> f 2 =? 0.
+Proof. intros f p. verit_base p; vauto. Qed.
+
+Lemma taut2 :
+  forall f, 0 =? f 2 -> 0 =?f 2.
+Proof. intros f p. verit_base p; vauto. Qed.
+
+Lemma taut3 :
+  forall f, f 2 =? 0 -> f 3 =? 5 -> f 2 =? 0.
+Proof. intros f p1 p2. verit_base p1 p2; vauto. Qed.
+
+Lemma taut4 :
+  forall f, f 3 =? 5 -> f 2 =? 0 -> f 2 =? 0.
+Proof. intros f p1 p2. verit_base p1 p2; vauto. Qed.
+
+Lemma taut5 :
+  forall f, 0 =? f 2 -> f 2 =? 0.
+Proof. intros f p. verit_base p; vauto. Qed.
+
+Lemma fun_const_Z :
+  forall f , (forall x, f x =? 2) ->
+             f 3 =? 2.
+Proof. intros f Hf. verit_base Hf; vauto. Qed.
+
+Lemma lid (A : bool) :  A -> A.
+Proof. intro a. verit_base a; vauto. Qed.
+
+Lemma lpartial_id A :
+  (xorb A A) -> (xorb A A).
+Proof. intro xa. verit_base xa; vauto. Qed.
+
+Lemma llia1 X Y Z:
+  (X <=? 3) && ((Y <=? 7) || (Z <=? 9)) ->
+  (X + Y <=? 10) || (X + Z <=? 12).
+Proof. intro p. verit_base p; vauto. Qed.
+
+Lemma llia2 X:
+  X - 3 =? 7 -> X >=? 10.
+Proof. intro p. verit_base p; vauto. Qed.
+
+Lemma llia3 X Y:
+  X >? Y -> Y + 1 <=? X.
+Proof. intro p. verit_base p; vauto. Qed.
+
+Lemma llia6 X:
+  andb ((X - 3) <=? 7) (7 <=? (X - 3)) -> X >=? 10.
+Proof. intro p. verit_base p; vauto. 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_base p; vauto. Qed.
+
+Lemma lcongr1 (a b : Z) (P : Z -> bool) f:
+  (f a =? b) -> (P (f a)) -> P b.
+Proof. intros eqfab pfa. verit_base eqfab pfa; vauto. Qed.
+
+Lemma lcongr2 (f:Z -> Z -> Z) x y z:
+  x =? y -> f z x =? f z y.
+Proof. intro p. verit_base p; vauto. Qed.
+
+Lemma lcongr3 (P:Z -> Z -> bool) x y z:
+  x =? y -> P z x -> P z y.
+Proof. intros eqxy pzx. verit_base eqxy pzx; vauto. Qed.
+
+Lemma un_menteur (a b c d : Z) dit:
+  dit a =? c ->
+  dit b =? d ->
+  (d =? a) || (b =? c) ->
+  (a =? c) || (a =? d) ->
+  (b =? c) || (b =? d) ->
+  a =? d.
+Proof. intros H1 H2 H3 H4 H5. verit_base H1 H2 H3 H4 H5; vauto. 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_base Hf; vauto. Qed.
+
+(* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to
+   the environment. If you did so in a section then, at the end of the section,
+   you should use <Clear_lemmas> to empty the globally added lemmas because
+   those lemmas won't be available outside of the section. *)
+
+Section S.
+  Variable f : Z -> Z.
+  Hypothesis th : forall x, Z.eqb (f x) 3.
+  Add_lemmas th.
+  Goal forall x, Z.eqb ((f x) + 1) 4.
+  Proof. verit. Qed.
+  Clear_lemmas.
+End S.
+
+Section fins_sat6.
+  Variables a b c d : bool.
+  Hypothesis andab : andb a b.
+  Hypothesis orcd  : orb c d.
+  Add_lemmas andab orcd.
+
+  Lemma sat6 :  orb c (andb a (andb b d)).
+  Proof. verit. Qed.
+  Clear_lemmas.
+End fins_sat6.
+
+
+Section fins_lemma_multiple.
+  Variable f' : Z -> Z.
+  Variable g : Z -> Z.
+  Variable k : Z.
+  Hypothesis g_k_linear : forall x, g (x + 1) =? (g x) + k.
+  Hypothesis f'_equal_k : forall x, f' x =? k.
+  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.
+
+  Clear_lemmas.
+End fins_lemma_multiple.
+
+
+Section fins_find_apply_lemma.
+  Variable u : Z -> Z.
+  Hypothesis u_is_constant : forall x y, u x =? u y.
+  Add_lemmas u_is_constant.
+
+  Lemma apply_lemma : forall x, u x =? u 2.
+  Proof. verit. Qed.
+
+  Lemma find_inst :
+    implb (u 2 =? 5) (u 3 =? 5).
+  Proof. verit. Qed.
+
+  Clear_lemmas.
+End fins_find_apply_lemma.
+
+
+Section mult3.
+  Variable mult3 : Z -> Z.
+  Hypothesis mult3_0 : mult3 0 =? 0.
+  Hypothesis mult3_Sn : forall n, mult3 (n+1) =? mult3 n + 3.
+  Add_lemmas mult3_0 mult3_Sn.
+
+  Lemma mult3_21 : mult3 14 =? 42.
+  Proof. verit. Qed. (* very slow to verify with standard coq *)
+
+  Clear_lemmas.
+End mult3.
+
+
+(* the program veriT doesn't return in reasonable time on the following lemma*)
+(* Section mult. *)
+(*   Variable mult : Z -> Z -> Z. *)
+(*   Hypothesis mult_0 : forall x, mult 0 x =? 0. *)
+(*   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_base mult_0 mult_Sx. *)
+(*   Qed. *)
+(* End mult. *)
+
+Section implicit_transform.
+  Variable f : Z -> bool.
+  Variable a1 a2 : Z.
+  Hypothesis f_const : forall b, implb (f b) (f a2).
+  Hypothesis f_a1 : f a1.
+  Add_lemmas f_const f_a1.
+
+  Lemma implicit_transform :
+    f a2.
+  Proof. verit. Qed.
+
+  Clear_lemmas.
+End implicit_transform.
+
+Section list.
+  Variable Zlist : Type.
+  Hypothesis dec_Zlist :
+    {eq : Zlist -> Zlist -> bool & forall x y : Zlist, reflect (x = y) (eq x y)}.
+  Variable nil : Zlist.
+  Variable cons : Z -> Zlist -> Zlist.
+  Variable inlist : Z -> Zlist -> bool.
+
+  Infix "::" := cons.
+
+  Hypothesis in_eq : forall a l, inlist a (a :: l).
+  Hypothesis in_cons : forall a b l, implb (inlist a l) (inlist a (b::l)).
+  Add_lemmas in_eq in_cons.
+
+  Lemma in_cons1 :
+    inlist 1 (1::2::nil).
+  Proof. verit. Qed.
+
+  Lemma in_cons2 :
+    inlist 12 (2::4::12::nil).
+  Proof. verit. Qed.
+
+  Lemma in_cons3 :
+    inlist 1 (5::1::(0-1)::nil).
+  Proof. verit. Qed.
+
+  Lemma in_cons4 :
+    inlist 22 ((- (1))::22::nil).
+  Proof. verit. Qed.
+
+  Lemma in_cons5 :
+    inlist 1 ((- 1)::1::nil).
+  Proof. verit. Qed.
+
+  (* Lemma in_cons_false1 : *)
+  (*   inlist 1 (2::3::nil). *)
+  (* verit. (*returns unknown*) *)
+
+  (* Lemma in_cons_false2 : *)
+  (*   inlist 1 ((-1)::3::nil). *)
+  (* verit. (*returns unknown*) *)
+
+  (* Lemma in_cons_false3 : *)
+  (*   inlist 12 (11::13::(-12)::1::nil). *)
+  (*   verit. (*returns unknown*) *)
+
+  Variable append : Zlist -> Zlist -> Zlist.
+  Infix "++" := append.
+
+  Hypothesis in_or_app : forall a l1 l2,
+      implb (orb (inlist a l1) (inlist a l2))
+            (inlist a (l1 ++ l2)).
+  Add_lemmas in_or_app.
+
+  Lemma in_app1 :
+    inlist 1 (1::2::nil ++ nil).
+  Proof. verit. Qed.
+
+  Lemma in_app2 :
+    inlist 1 (nil ++ 2::1::nil).
+  Proof. verit. Qed.
+
+  Lemma in_app3 :
+    inlist 1 (1::3::nil ++ 2::1::nil).
+  Proof. verit. Qed.
+
+  (* Lemma in_app_false1 : *)
+  (*   inlist 1 (nil ++ 2::3::nil). *)
+  (*   verit. (* returns unknown *) *)
+
+  (* Lemma in_app_false2 : *)
+  (*   inlist 1 (2::3::nil ++ nil). *)
+  (*   verit. (* returns unknown *) *)
+
+
+  (* Lemma in_app_false3 : *)
+  (*   inlist 1 (2::3::nil ++ 5::6::nil). *)
+  (*   verit. (* returns unknown*) *)
+
+  Hypothesis in_nil :
+    forall a, negb (inlist a nil).
+  Hypothesis in_inv :
+    forall a b l,
+      implb (inlist b (a::l))
+            (orb (a =? b) (inlist b l)).
+  Hypothesis inlist_app_comm_cons:
+    forall l1 l2 a b,
+      Bool.eqb (inlist b (a :: (l1 ++ l2)))
+               (inlist b ((a :: l1) ++ l2)).
+  Add_lemmas in_nil in_inv inlist_app_comm_cons.
+
+  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. Qed.
+
+  Clear_lemmas.
+End list.
+
+
+Section group.
+  Variable op : Z -> Z -> Z.
+  Variable inv : Z -> Z.
+  Variable e : Z.
+
+  Hypothesis associative :
+    forall a b c : Z, op a (op b c) =? op (op a b) c.
+  Hypothesis identity :
+    forall a : Z, (op e a =? a) && (op a e =? a).
+  Hypothesis inverse :
+    forall a : Z, (op a (inv a) =? e) && (op (inv a) a =? e).
+  Add_lemmas associative identity inverse.
+
+  Lemma unique_identity e':
+    (forall z, op e' z =? z) -> e' =? e.
+  Proof. intros pe'. verit_base pe'; vauto. Qed.
+
+  Lemma simplification_right x1 x2 y:
+      op x1 y =? op x2 y -> x1 =? x2.
+  Proof. intro H. verit_base H; vauto. Qed.
+
+  Lemma simplification_left x1 x2 y:
+      op y x1 =? op y x2 -> x1 =? x2.
+  Proof. intro H. verit_base H; vauto. Qed.
+
+  Clear_lemmas.
+End group.
diff --git a/unit-tests/sat14.smt2 b/unit-tests/sat14.smt2
new file mode 100644
index 0000000..b8ffa9c
--- /dev/null
+++ b/unit-tests/sat14.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_UF)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert (not (or c (and a b d))))
+(assert (and a b))
+(assert (or c d))
+(check-sat)
+(exit)