diff options
| author | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-11-01 09:45:35 +0000 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-11-01 09:45:35 +0000 |
| commit | 184f1644fe15cc78e72cea799f3f85cb36b32627 (patch) | |
| tree | 9b802c4e2e08db5f8c72346adedbe51a8582955a /examples | |
| parent | caa7946a4da47b64807662468e68ecc2788a0980 (diff) | |
| download | smtcoq-184f1644fe15cc78e72cea799f3f85cb36b32627.tar.gz smtcoq-184f1644fe15cc78e72cea799f3f85cb36b32627.zip | |
extended example on groups
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/examples/Example.v b/examples/Example.v index 42a124c..2141843 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -214,11 +214,19 @@ Section group. Hypothesis associative : forall a b c : Z, op a (op b c) =? op (op a b) c. - Hypothesis identity : - forall a : Z, (op e a =? a) && (op a e =? a). Hypothesis inverse : - forall a : Z, (op a (inv a) =? e) && (op (inv a) a =? e). + forall a : Z, (op (inv a) a =? e). + Hypothesis identity : + forall a : Z, (op e a =? a). Add_lemmas associative identity inverse. + Lemma inverse' : + forall a : Z, (op a (inv a) =? e). + Proof. verit. Qed. + Add_lemmas inverse'. + Lemma identity' : + forall a : Z, (op a e =? a). + Proof. verit. Qed. + Add_lemmas identity'. Lemma unique_identity e': (forall z, op e' z =? z) -> e' =? e. |