From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 test-suite/ssr/set_pattern.v | 64 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)
 create mode 100644 test-suite/ssr/set_pattern.v

(limited to 'test-suite/ssr/set_pattern.v')

diff --git a/test-suite/ssr/set_pattern.v b/test-suite/ssr/set_pattern.v
new file mode 100644
index 00000000..3ce75e87
--- /dev/null
+++ b/test-suite/ssr/set_pattern.v
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*         *   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.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Ltac T1 x := match goal with |- _ => set t := (x in X in _ = X) end.
+Ltac T2 x := first [set t := (x in RHS)].
+Ltac T3 x := first [set t := (x in Y in _ = Y)|idtac].
+Ltac T4 x := set t := (x in RHS); idtac.
+Ltac T5 x := match goal with |- _ => set t := (x in RHS) | |- _ => idtac end.
+
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Open Scope nat_scope.
+
+Lemma foo x y : x.+1 = y + x.+1.
+set t := (_.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (x in _ = x). match goal with |- x.+1 = t => rewrite /t {t} end.
+set t := (x in X in _ = X).
+  match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (y + (1 + x) as X in _ = X).
+  match goal with |- x.+1 = t => rewrite /t addSn add0n {t} end.
+set t := x.+1. match goal with |- t = y + t => rewrite /t {t} end.
+set t := (x).+1. match goal with |- t = y + t => rewrite /t {t} end.
+set t := ((x).+1 in X in _ = X).
+  match goal with |- x.+1 = y + t => rewrite /t {t} end.
+set t := (x.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T1 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T2 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T3 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T4 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T5 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+rewrite [RHS]addnC.
+  match goal with |- x.+1 = x.+1 + y => rewrite -[RHS]addnC end.
+rewrite -[in RHS](@subnK 1 x.+1) //.
+  match goal with |- x.+1 = y + (x.+1 - 1 + 1) => rewrite subnK // end.
+have H : x.+1 = y by myadmit.
+set t := _.+1 in H |- *.
+  match goal with H : t = y |- t = y + t => rewrite /t {t} in H * end.
+set t := (_.+1 in X in _ + X) in H |- *.
+  match goal with H : x.+1 = y |- x.+1 = y + t => rewrite /t {t} in H * end.
+set t := 0. match goal with t := 0 |- x.+1 = y + x.+1 => clear t end.
+set t := y + _. match goal with |- x.+1 = t => rewrite /t {t} end.
+set t : nat := 0. clear t.
+set t : nat := (x in RHS).
+  match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t : nat := RHS. match goal with |- x.+1 = t => rewrite /t {t} end.
+(* set t := 0 + _. *)
+(* set t := (x).+1 in X in _ + X in H |-. *)
+(* set t := (x).+1 in X in _ = X.*)
+Admitted.
-- 
cgit v1.2.3