From 13223ba6649dfd7501a34a700abc09c2e7169636 Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 7 Feb 2007 20:12:34 +0000
Subject: Add tactics for induction on subterms.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9623 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile                 |  2 +-
 contrib/subtac/Tactics.v | 22 ++++++++++++++++++++++
 contrib/subtac/Utils.v   |  4 ++++
 3 files changed, 27 insertions(+), 1 deletion(-)
 create mode 100644 contrib/subtac/Tactics.v

diff --git a/Makefile b/Makefile
index c9156cb17..4b8580d66 100644
--- a/Makefile
+++ b/Makefile
@@ -1101,7 +1101,7 @@ JPROVERVO=
 
 CCVO=
 
-SUBTACVO=contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \
+SUBTACVO=contrib/subtac/Tactics.vo contrib/subtac/Utils.vo contrib/subtac/FixSub.vo contrib/subtac/Subtac.vo \
 	contrib/subtac/FunctionalExtensionality.vo
 
 RTAUTOVO = \
diff --git a/contrib/subtac/Tactics.v b/contrib/subtac/Tactics.v
new file mode 100644
index 000000000..25d8d8319
--- /dev/null
+++ b/contrib/subtac/Tactics.v
@@ -0,0 +1,22 @@
+Ltac induction_with_subterm c H :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  (set(x := c) ; assert(y:x = c) by reflexivity ;
+  rewrite <- y in H ; 
+  induction H ; subst).
+
+Ltac induction_on_subterm c :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  (set(x := c) ; assert(y:x = c) by reflexivity ; clearbody x ; induction x ; inversion y ; try subst ; 
+  clear y).
+
+Ltac induction_with_subterms c c' H :=
+  let x := fresh "x" in
+  let y := fresh "y" in
+  let z := fresh "z" in
+  let w := fresh "w" in
+  (set(x := c) ; assert(y:x = c) by reflexivity ;
+  set(z := c') ; assert(w:z = c') by reflexivity ;
+  rewrite <- y in H ; rewrite <- w in H ; 
+  induction H ; subst).
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 569c52e89..fc002a01b 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -4,6 +4,8 @@ Notation "'fun' { x : A | P } => Q" :=
   (fun x:{x:A|P} => Q)
   (at level 200, x ident, right associativity).
 
+Notation " {{ x }} " := (tt : { y : unit | x }).
+
 Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
 
 Notation " ! " := (False_rect _ _).
@@ -82,6 +84,8 @@ Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
+Axiom pair : Type -> Type -> Type.
+Extract Constant pair "'a" "'b" => " 'a * 'b ".
 Extract Inductive prod => "pair" [ "" ].
 Extract Inductive sigT => "pair" [ "" ].
 
-- 
cgit v1.2.3