Add the full example of the webpage in the unit tests

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"))