diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-02-23 18:30:24 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-02-23 18:30:24 +0100 |
commit | 3fc84368a0e957dac5574f699fb61fbe6bf049d7 (patch) | |
tree | 107ecf55d103d7dabf080da467c653e9752114d6 /unit-tests | |
parent | c05f39c2556725610840ec48b62243a10e2e098f (diff) | |
download | smtcoq-3fc84368a0e957dac5574f699fb61fbe6bf049d7.tar.gz smtcoq-3fc84368a0e957dac5574f699fb61fbe6bf049d7.zip |
Example of groups in unit tests
Diffstat (limited to 'unit-tests')
-rw-r--r-- | unit-tests/Tests_lfsc_tactics.v | 55 |
1 files changed, 37 insertions, 18 deletions
diff --git a/unit-tests/Tests_lfsc_tactics.v b/unit-tests/Tests_lfsc_tactics.v index feb1d7e..a948e06 100644 --- a/unit-tests/Tests_lfsc_tactics.v +++ b/unit-tests/Tests_lfsc_tactics.v @@ -727,32 +727,51 @@ End A_BV_EUF_LIA_PR. (* Example of the webpage *) -Section group. - Variable e : Z. - Variable inv : Z -> Z. - Variable op : Z -> Z -> Z. - +Section Group. + Variable G : Type. + (* We suppose that G has a decidable equality *) + Variable HG : CompDec G. + Variable op : G -> G -> G. + Variable inv : G -> G. + Variable e : G. + + Local Notation "a ==? b" := (@eqb_of_compdec G HG a b) (at level 60). + + (* 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, 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. - + forall a b c : G, op a (op b c) ==? op (op a b) c. + Hypothesis inverse : + forall a : G, op (inv a) a ==? e. + Hypothesis identity : + forall a : G, op e a ==? a. + Add_lemmas associative inverse identity. + + (* The "right" version of inverse *) Lemma inverse' : - forall a : Z, (op a (inv a) =? e). - Proof using associative identity inverse. smt. Qed. + forall a : G, op a (inv a) ==? e. + Proof. smt. Qed. + (* The "right" version of identity *) Lemma identity' : - forall a : Z, (op a e =? a). - Proof using associative identity inverse. smt inverse'. Qed. + forall a : G, op a e ==? a. + Proof. smt inverse'. Qed. + (* Some other interesting facts about groups *) Lemma unique_identity e': - (forall z, op e' z =? z) -> e' =? e. - Proof using associative identity inverse. intros pe'; smt pe'. Qed. + (forall z, op e' z ==? z) -> e' ==? e. + Proof. intros pe'; smt pe'. Qed. + + Lemma simplification_right x1 x2 y: + op x1 y ==? op x2 y -> x1 ==? x2. + 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. smt_no_check H inverse'. Qed. Clear_lemmas. -End group. +End Group. Section EqualityOnUninterpretedType1. |