From 90d3ce10b41159c0bfe266ce403e4b5f31d970cf Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 16 Jan 2020 12:16:12 +0100 Subject: Add the full example of the webpage in the unit tests --- unit-tests/Tests_lfsc_tactics.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v index c868864..ee9df76 100644 --- a/unit-tests/Tests_lfsc_tactics.v +++ b/unit-tests/Tests_lfsc_tactics.v @@ -698,6 +698,36 @@ Section A_BV_EUF_LIA_PR. End A_BV_EUF_LIA_PR. +(* Example of the webpage *) + +Section group. + Variable e : Z. + Variable inv : Z -> Z. + Variable op : Z -> Z -> Z. + + Hypothesis associative : + forall a b c, op a (op b c) =? op (op a b) c. + Hypothesis identity : forall a, (op e a =? a). + Hypothesis inverse : forall a, (op (inv a) a =? e). + + Add_lemmas associative identity inverse. + + Lemma inverse' : + forall a : Z, (op a (inv a) =? e). + Proof. smt. Qed. + + Lemma identity' : + forall a : Z, (op a e =? a). + Proof. smt inverse'. Qed. + + Lemma unique_identity e': + (forall z, op e' z =? z) -> e' =? e. + Proof. intros pe'; smt pe'. Qed. + + Clear_lemmas. +End group. + + (* Local Variables: coq-load-path: ((rec "../src" "SMTCoq")) -- cgit