diff options
| -rw-r--r-- | unit-tests/Tests_lfsc_tactics.v | 30 |
1 files changed, 30 insertions, 0 deletions
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")) |