diff options
Diffstat (limited to 'test-suite/ssr/binders.v')
-rw-r--r-- | test-suite/ssr/binders.v | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/test-suite/ssr/binders.v b/test-suite/ssr/binders.v new file mode 100644 index 000000000..97b7d830f --- /dev/null +++ b/test-suite/ssr/binders.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) + +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. + +Lemma test (x : bool) : True. +have H1 x := x. +have (x) := x => H2. +have H3 T (x : T) := x. +have ? : bool := H1 _ x. +have ? : bool := H2 _ x. +have ? : bool := H3 _ x. +have ? (z : bool) : forall y : bool, z = z := fun y => refl_equal _. +have ? w : w = w := @refl_equal nat w. +have ? y : true by []. +have ? (z : bool) : z = z. + exact: (@refl_equal _ z). +have ? (z w : bool) : z = z by exact: (@refl_equal _ z). +have H w (a := 3) (_ := 4) : w && true = w. + by rewrite andbT. +exact I. +Qed. + +Lemma test1 : True. +suff (x : bool): x = x /\ True. + by move/(_ true); case=> _. +split; first by exact: (@refl_equal _ x). +suff H y : y && true = y /\ True. + by case: (H true). +suff H1 /= : true && true /\ True. + by rewrite andbT; split; [exact: (@refl_equal _ y) | exact: I]. +match goal with |- is_true true /\ True => idtac end. +by split. +Qed. + +Lemma foo n : n >= 0. +have f i (j := i + n) : j < n. + match goal with j := i + n |- _ => idtac end. +Undo 2. +suff f i (j := i + n) : j < n. + done. +match goal with j := i + n |- _ => idtac end. +Undo 3. +done. +Qed. |