From e3535ade2bd4c7b75ec093e9e0f124f84c506b8f Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 25 Sep 2008 20:25:06 +0000
Subject: Various little improvements: - A new [dependent pattern] tactic to do
 a pattern on an object in an inductive family and generalize by both the
 indexes and the object itself. Useful to prepare a goal for elimination with
 a dependent principle. - Better dependent elimination simplification tactic
 that doesn't throw away non-dependent equalities if they can't be injected. -
 Add [fold_sub] and [unfold_sub] tactics for folding/unfolding well-founded
 definitions using measures built by Program.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11420 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/FunctionalExtensionality.v | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

(limited to 'theories/Program/FunctionalExtensionality.v')

diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 440217bfec..8bd2dfb905 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -22,7 +22,7 @@ Require Import Coq.Program.Equality.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** The converse of functional equality. *)
+(** The converse of functional extensionality. *)
 
 Lemma equal_f : forall A B : Type, forall (f g : A -> B), 
   f = g -> forall x, f x = g x.
@@ -32,7 +32,7 @@ Proof.
   auto.
 Qed.
 
-(** Statements of functional equality for simple and dependent functions. *)
+(** Statements of functional extensionality for simple and dependent functions. *)
 
 Axiom fun_extensionality_dep : forall A, forall B : (A -> Type), 
   forall (f g : forall x : A, B x), 
@@ -106,4 +106,18 @@ Proof.
   rewrite H0 ; auto.
 Qed.
 
+(** Tactics to fold/unfold definitions based on [Fix_measure_sub]. *)
 
+Ltac fold_sub f :=
+  match goal with
+    | [ |- ?T ] => 
+      match T with
+        appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => 
+        let app := context C [ f arg ] in
+         change app
+      end
+  end.
+
+Ltac unfold_sub f fargs := 
+  set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; 
+  rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
-- 
cgit v1.2.3