From faaa2848c37444f8f37ac432c25f9f813e1df39b Mon Sep 17 00:00:00 2001
From: Quentin Garchery <garchery.quentin@gmail.com>
Date: Sat, 27 Oct 2018 20:08:44 +0200
Subject: Adding support for lemmas in the command verit

---
 examples/Example.v             | 76 ++++++++++++++++++++++++++++++++++++++++++
 examples/Non_terminating.v     | 11 ++++++
 examples/one_equality_switch.v | 25 ++++++++++++++
 examples/switching_input.v     | 10 ++++++
 examples/sym_zeq.v             | 12 +++++++
 5 files changed, 134 insertions(+)
 create mode 100644 examples/Non_terminating.v
 create mode 100644 examples/one_equality_switch.v
 create mode 100644 examples/switching_input.v
 create mode 100644 examples/sym_zeq.v

(limited to 'examples')

diff --git a/examples/Example.v b/examples/Example.v
index 0c50909..60d1a2b 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -136,3 +136,79 @@ verit.
 Qed.
 
 Local Close Scope nat_scope.
+
+Open Scope Z_scope.
+
+(* 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 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.
+
+Section Without_lemmas.
+  Lemma fSS:
+    forall (f : Z -> Z) (k : Z) (x : Z),
+      implb (f (x+1) =? f x + k)
+     (implb (f (x+2) =? f (x+1) + k)
+            (f (x+2) =? f x + 2 * k)).
+  Proof. verit. Qed.
+End Without_lemmas.
+
+Section With_lemmas.
+  Variable f : Z -> Z.
+  Variable k : Z.
+  Hypothesis f_k_linear : forall x, f (x + 1) =? f x + k.
+
+  Lemma fSS2:
+    forall x, f (x + 2) =? f x + 2 * k.
+  Proof. verit_base f_k_linear; vauto. Qed.
+End With_lemmas.
+
+(* 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 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 7 =? 21.
+  Proof. verit. Qed.
+
+  Clear_lemmas.
+End mult3.
+
+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/examples/Non_terminating.v b/examples/Non_terminating.v
new file mode 100644
index 0000000..087301a
--- /dev/null
+++ b/examples/Non_terminating.v
@@ -0,0 +1,11 @@
+Require Import SMTCoq.
+
+Parameter g : Z -> Z.
+
+Axiom g_2_linear : forall x, Zeq_bool (g (x + 1)) ((g x) + 2).
+
+Lemma apply_lemma_multiple :
+  forall x y, Zeq_bool (g (x + y)) ((g x) + y * 2).
+
+Proof.
+  verit g_2_linear.
diff --git a/examples/one_equality_switch.v b/examples/one_equality_switch.v
new file mode 100644
index 0000000..3473d08
--- /dev/null
+++ b/examples/one_equality_switch.v
@@ -0,0 +1,25 @@
+Require Import SMTCoq.
+Require Import Bool.
+Local Open Scope int63_scope.
+
+Parameter f : Z -> Z.
+
+Lemma sym_zeq_bool x y :
+  Zeq_bool x y = Zeq_bool y x.
+
+Proof.
+  case_eq (Zeq_bool x y).
+  rewrite <- Zeq_is_eq_bool. intro H. symmetry. now rewrite <- Zeq_is_eq_bool.
+  symmetry. apply not_true_is_false.
+  intro H1. rewrite <- Zeq_is_eq_bool in H1.
+  symmetry in H1. rewrite Zeq_is_eq_bool in H1.
+  rewrite H in H1. discriminate H1.
+Qed.
+
+Axiom f_spec : forall x, (f (x+1) =? f x + 1) && (f 0 =? 0).
+
+Lemma f_1 : f 1 =? 1.
+
+Proof.
+  verit_base f_spec; vauto; rewrite Z.eqb_sym; auto.
+Qed.
diff --git a/examples/switching_input.v b/examples/switching_input.v
new file mode 100644
index 0000000..52261d8
--- /dev/null
+++ b/examples/switching_input.v
@@ -0,0 +1,10 @@
+Require Import SMTCoq.
+Require Import Bool.
+Local Open Scope int63_scope.
+
+Parameter m : Z -> Z.
+Axiom m_0 : m 0 =? 5.
+
+Lemma cinq_m_0 :
+  m 0 =? 5.
+Proof. verit_base m_0; vauto. Qed.
diff --git a/examples/sym_zeq.v b/examples/sym_zeq.v
new file mode 100644
index 0000000..b940490
--- /dev/null
+++ b/examples/sym_zeq.v
@@ -0,0 +1,12 @@
+Require Import SMTCoq.
+Require Import Bool.
+Local Open Scope int63_scope.
+
+Open Scope Z_scope.
+
+Parameter h : Z -> Z -> Z.
+Axiom h_Sm_n : forall x y, h (x+1) y =? h x y.
+
+Lemma h_1_0 :
+  h 1 0 =? h 0 0.
+Proof. verit_base h_Sm_n; vauto. Qed.
-- 
cgit