Cleaning (#35)

Removing tests from the example folder

More commentaries in Example.v

5 files changed, 37 insertions, 131 deletions

diff --git a/examples/Example.v b/examples/Example.v
index d9523ca..e4a50da 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -188,7 +188,7 @@ Proof.
 Qed.
 
 
-(* Examples of using the conversion tactics *)
+(** Examples of using the conversion tactics **)
 
 Local Open Scope positive_scope.
 
@@ -271,8 +271,10 @@ Qed.
 
 Open Scope Z_scope.
 
-(* Some examples of using verit with lemmas. Use <verit H1 .. Hn>
-   to temporarily add the lemmas H1 .. Hn to the verit environment. *)
+
+(** Some examples of using verit with lemmas. Use <verit H1 .. Hn>
+   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) ->
@@ -282,15 +284,6 @@ Proof.
   verit Hf.
 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.
@@ -301,37 +294,52 @@ Section With_lemmas.
   Proof. verit_no_check f_k_linear. Qed.
 End With_lemmas.
 
-(* You can use <Add_lemmas H1 .. Hn> to permanently add the lemmas H1 .. Hn to
+(* Can't express the k-linearity of a function without lemmas *)
+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.
+
+(* Instantiating a lemma with multiple quantifiers *)
+Section NonLinear.
+  Lemma distr_right_inst a b (mult : Z -> Z -> Z) :
+    (forall x y z, mult (x + y)  z =? mult x z + mult y z) ->
+    (mult (3 + a) b =? mult 3 b + mult a b).
+  Proof.
+    intro H.
+    verit H.
+  Qed.
+End NonLinear.
+
+
+(** 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. *)
+   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 4 =? 12.
+  Lemma mult_3_4_12 : mult3 4 =? 12.
   Proof. verit_no_check. Qed.
 
   Clear_lemmas.
 End mult3.
 
-Section NonLinear.
-  Lemma distr_right_inst a b (mult : Z -> Z -> Z) :
-    (forall x y z, mult (x + y)  z =? mult x z + mult y z) ->
-    (mult (3 + a) b =? mult 3 b + mult a b).
-  Proof.
-    intro H.
-    verit H.
-  Qed.
-End NonLinear.
-
 Section group.
   Variable op : Z -> Z -> Z.
   Variable inv : Z -> Z.
   Variable e : Z.
 
+  (* We can prove automatically that we have a group if we only have the "left" versions
+     of the axioms of a group *)
   Hypothesis associative :
     forall a b c : Z, op a (op b c) =? op (op a b) c.
   Hypothesis inverse :
@@ -339,15 +347,19 @@ Section group.
   Hypothesis identity :
     forall a : Z, (op e a =? a).
   Add_lemmas associative identity inverse.
+
+  (* The "right" version of inverse *)
   Lemma inverse' :
     forall a : Z, (op a (inv a) =? e).
   Proof. verit_no_check. Qed.
   Add_lemmas inverse'.
+  (* The "right" version of identity *)
   Lemma identity' :
     forall a : Z, (op a e =? a).
   Proof. verit_no_check. Qed.
   Add_lemmas identity'.
 
+  (* Some other interesting facts about groups *)
   Lemma unique_identity e':
     (forall z, op e' z =? z) -> e' =? e.
   Proof. intros pe'. verit pe'. Qed.
diff --git a/examples/Non_terminating.v b/examples/Non_terminating.v
deleted file mode 100644
index 7dad08f..0000000
--- a/examples/Non_terminating.v
+++ /dev/null
@@ -1,23 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2019                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-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
deleted file mode 100644
index 61fd9c7..0000000
--- a/examples/one_equality_switch.v
+++ /dev/null
@@ -1,37 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2019                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-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
deleted file mode 100644
index 629a3ad..0000000
--- a/examples/switching_input.v
+++ /dev/null
@@ -1,22 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2019                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-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
deleted file mode 100644
index 1c4be83..0000000
--- a/examples/sym_zeq.v
+++ /dev/null
@@ -1,24 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2019                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-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.