From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Init/Tactics.v | 100 ++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 96 insertions(+), 4 deletions(-)

(limited to 'theories/Init/Tactics.v')

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 5d1e87ae..8df533e7 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   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        *)
+(*    //   *    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 Notations.
@@ -236,3 +238,93 @@ Tactic Notation "clear" "dependent" hyp(h) :=
 
 Tactic Notation "revert" "dependent" hyp(h) :=
  generalize dependent h.
+
+(** Provide an error message for dependent induction that reports an import is
+required to use it. Importing Coq.Program.Equality will shadow this notation
+with the actual [dependent induction] tactic. *)
+
+Tactic Notation "dependent" "induction" ident(H) :=
+  fail "To use dependent induction, first [Require Import Coq.Program.Equality.]".
+
+(** *** [inversion_sigma] *)
+(** The built-in [inversion] will frequently leave equalities of
+    dependent pairs.  When the first type in the pair is an hProp or
+    otherwise simplifies, [inversion_sigma] is useful; it will replace
+    the equality of pairs with a pair of equalities, one involving a
+    term casted along the other.  This might also prove useful for
+    writing a version of [inversion] / [dependent destruction] which
+    does not lose information, i.e., does not turn a goal which is
+    provable into one which requires axiom K / UIP.  *)
+
+Ltac simpl_proj_exist_in H :=
+  repeat match type of H with
+         | context G[proj1_sig (exist _ ?x ?p)]
+           => let G' := context G[x] in change G' in H
+         | context G[proj2_sig (exist _ ?x ?p)]
+           => let G' := context G[p] in change G' in H
+         | context G[projT1 (existT _ ?x ?p)]
+           => let G' := context G[x] in change G' in H
+         | context G[projT2 (existT _ ?x ?p)]
+           => let G' := context G[p] in change G' in H
+         | context G[proj3_sig (exist2 _ _ ?x ?p ?q)]
+           => let G' := context G[q] in change G' in H
+         | context G[projT3 (existT2 _ _ ?x ?p ?q)]
+           => let G' := context G[q] in change G' in H
+         | context G[sig_of_sig2 (@exist2 ?A ?P ?Q ?x ?p ?q)]
+           => let G' := context G[@exist A P x p] in change G' in H
+         | context G[sigT_of_sigT2 (@existT2 ?A ?P ?Q ?x ?p ?q)]
+           => let G' := context G[@existT A P x p] in change G' in H
+         end.
+Ltac induction_sigma_in_using H rect :=
+  let H0 := fresh H in
+  let H1 := fresh H in
+  induction H as [H0 H1] using (rect _ _ _ _);
+  simpl_proj_exist_in H0;
+  simpl_proj_exist_in H1.
+Ltac induction_sigma2_in_using H rect :=
+  let H0 := fresh H in
+  let H1 := fresh H in
+  let H2 := fresh H in
+  induction H as [H0 H1 H2] using (rect _ _ _ _ _);
+  simpl_proj_exist_in H0;
+  simpl_proj_exist_in H1;
+  simpl_proj_exist_in H2.
+Ltac inversion_sigma_step :=
+  match goal with
+  | [ H : _ = exist _ _ _ |- _ ]
+    => induction_sigma_in_using H @eq_sig_rect
+  | [ H : _ = existT _ _ _ |- _ ]
+    => induction_sigma_in_using H @eq_sigT_rect
+  | [ H : exist _ _ _ = _ |- _ ]
+    => induction_sigma_in_using H @eq_sig_rect
+  | [ H : existT _ _ _ = _ |- _ ]
+    => induction_sigma_in_using H @eq_sigT_rect
+  | [ H : _ = exist2 _ _ _ _ _ |- _ ]
+    => induction_sigma2_in_using H @eq_sig2_rect
+  | [ H : _ = existT2 _ _ _ _ _ |- _ ]
+    => induction_sigma2_in_using H @eq_sigT2_rect
+  | [ H : exist2 _ _ _ _ _ = _ |- _ ]
+    => induction_sigma_in_using H @eq_sig2_rect
+  | [ H : existT2 _ _ _ _ _ = _ |- _ ]
+    => induction_sigma_in_using H @eq_sigT2_rect
+  end.
+Ltac inversion_sigma := repeat inversion_sigma_step.
+
+(** A version of [time] that works for constrs *)
+
+Ltac time_constr tac :=
+  let eval_early := match goal with _ => restart_timer end in
+  let ret := tac () in
+  let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in
+  ret.
+
+(** Useful combinators *)
+
+Ltac assert_fails tac :=
+  tryif tac then fail 0 tac "succeeds" else idtac.
+Ltac assert_succeeds tac :=
+  tryif (assert_fails tac) then fail 0 tac "fails" else idtac.
+Tactic Notation "assert_succeeds" tactic3(tac) :=
+  assert_succeeds tac.
+Tactic Notation "assert_fails" tactic3(tac) :=
+  assert_fails tac.
-- 
cgit v1.2.3