From faaa2848c37444f8f37ac432c25f9f813e1df39b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Sat, 27 Oct 2018 20:08:44 +0200 Subject: Adding support for lemmas in the command verit --- examples/one_equality_switch.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 examples/one_equality_switch.v (limited to 'examples/one_equality_switch.v') 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. -- cgit