diff options
author | 2018-04-12 10:08:05 +0200 | |
---|---|---|
committer | 2018-05-15 09:58:47 +0200 | |
commit | 15059d887c3059e6d925310be860dd2a3cf97796 (patch) | |
tree | e0c769cbad3b137e738c3e9da766f7f5f5795428 /test-suite/ssr/derive_inversion.v | |
parent | 3008ce85ed4de549816a1cac4701cb28bee4fad6 (diff) |
[ssr] import ssreflect test suite from math-comp
Diffstat (limited to 'test-suite/ssr/derive_inversion.v')
-rw-r--r-- | test-suite/ssr/derive_inversion.v | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/test-suite/ssr/derive_inversion.v b/test-suite/ssr/derive_inversion.v new file mode 100644 index 000000000..abf63a20c --- /dev/null +++ b/test-suite/ssr/derive_inversion.v @@ -0,0 +1,29 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ssreflect ssrbool. + +Set Implicit Arguments. + + Inductive wf T : bool -> option T -> Type := + | wf_f : wf false None + | wf_t : forall x, wf true (Some x). + + Derive Inversion wf_inv with (forall T b (o : option T), wf b o) Sort Prop. + + Lemma Problem T b (o : option T) : + wf b o -> + match b with + | true => exists x, o = Some x + | false => o = None + end. + Proof. + by case: b; elim/wf_inv=> //; case: o=> // a *; exists a. + Qed. |