diff options
| author | QGarchery <QGarchery@users.noreply.github.com> | 2019-02-12 14:52:13 +0100 |
|---|---|---|
| committer | ckeller <ckeller@users.noreply.github.com> | 2019-02-12 14:52:13 +0100 |
| commit | 66f68dfa5aac0252563816d3abef9456e8622adf (patch) | |
| tree | ded537507b8eb5b432a528fb7598773052275629 /examples/one_equality_switch.v | |
| parent | 769c2054cc14af50e70a38b0d2340ae6170863e0 (diff) | |
| download | smtcoq-66f68dfa5aac0252563816d3abef9456e8622adf.tar.gz smtcoq-66f68dfa5aac0252563816d3abef9456e8622adf.zip | |
Cleaning (#35)
Removing tests from the example folder
More commentaries in Example.v
Diffstat (limited to 'examples/one_equality_switch.v')
| -rw-r--r-- | examples/one_equality_switch.v | 37 |
1 files changed, 0 insertions, 37 deletions
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. |