diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2020-01-16 12:49:42 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2020-01-16 12:49:42 +0100 |
commit | 7a16f9d5a06abeb029abd54c29d8396f11fa58c9 (patch) | |
tree | dc96ccbb7a7983b55055c7ee48672d7083816713 /examples | |
parent | 2e7f2df3955cb0714af19d971dadc353547bc11a (diff) | |
download | smtcoq-7a16f9d5a06abeb029abd54c29d8396f11fa58c9.tar.gz smtcoq-7a16f9d5a06abeb029abd54c29d8396f11fa58c9.zip |
Use smt in the group example
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Example.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/examples/Example.v b/examples/Example.v index 04f82a7..2d48776 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -337,8 +337,8 @@ Section group. Variable inv : Z -> Z. Variable e : Z. - (* We can prove automatically that we have a group if we only have the "left" versions - of the axioms of a group *) + (* We can prove automatically that we have a group if we only have the + "left" versions of the axioms of a group *) Hypothesis associative : forall a b c : Z, op a (op b c) =? op (op a b) c. Hypothesis inverse : @@ -350,25 +350,25 @@ Section group. (* The "right" version of inverse *) Lemma inverse' : forall a : Z, (op a (inv a) =? e). - Proof. verit_no_check. Qed. - Add_lemmas inverse'. + Proof. smt. Qed. + (* The "right" version of identity *) Lemma identity' : forall a : Z, (op a e =? a). - Proof. verit_no_check. Qed. - Add_lemmas identity'. + Proof. smt inverse'. Qed. (* Some other interesting facts about groups *) Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. - Proof. intros pe'. verit pe'. Qed. + Proof. intros pe'; smt pe'. Qed. + Lemma simplification_right x1 x2 y: op x1 y =? op x2 y -> x1 =? x2. - Proof. intro H. verit_no_check H. Qed. + Proof. intro H. smt_no_check H inverse'. Qed. Lemma simplification_left x1 x2 y: op y x1 =? op y x2 -> x1 =? x2. - Proof. intro H. verit_no_check H. Qed. + Proof. intro H. smt_no_check H inverse'. Qed. Clear_lemmas. End group. |