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/Non_terminating.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 examples/Non_terminating.v (limited to 'examples/Non_terminating.v') 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. -- cgit