diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2018-10-31 18:44:16 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2018-10-31 18:44:16 +0100 |
| commit | caa7946a4da47b64807662468e68ecc2788a0980 (patch) | |
| tree | afdc7fcd4e4a5465c03bb330b8b8f6fdac8918b6 /examples | |
| parent | 8a2f393bb52c3be681a301064539df65015bee22 (diff) | |
| download | smtcoq-caa7946a4da47b64807662468e68ecc2788a0980.tar.gz smtcoq-caa7946a4da47b64807662468e68ecc2788a0980.zip | |
One more example + typos in README
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/Example.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/examples/Example.v b/examples/Example.v index 98175a2..42a124c 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -197,6 +197,16 @@ Section mult3. Clear_lemmas. End mult3. +Section NonLinear. + Lemma distr_right_inst a b (mult : Z -> Z -> Z) : + (forall x y z, mult (x + y) z =? mult x z + mult y z) -> + (mult (3 + a) b =? mult 3 b + mult a b). + Proof. + intro H. + verit_base H; vauto. + Qed. +End NonLinear. + Section group. Variable op : Z -> Z -> Z. Variable inv : Z -> Z. @@ -223,4 +233,4 @@ Section group. Proof. intro H. verit_base H; vauto. Qed. Clear_lemmas. -End group.
\ No newline at end of file +End group. |