1 files changed, 45 insertions, 55 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index 4a2208ce..76f49dd3 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -1,75 +1,65 @@
+Require Export Coq.subtac.SubtacTactics.
+
 Set Implicit Arguments.
 
-Notation "'fun' { x : A | P } => Q" :=
-  (fun x:{x:A|P} => Q)
-  (at level 200, x ident, right associativity).
+(** Wrap a proposition inside a subset. *)
 
-Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+Notation " {{ x }} " := (tt : { y : unit | x }).
+
+(** A simpler notation for subsets defined on a cartesian product. *)
+
+Notation "{ ( x , y )  :  A  |  P }" := 
+  (sig (fun anonymous : A => let (x,y) := anonymous in P))
+  (x ident, y ident) : type_scope.
+
+(** Generates an obligation to prove False. *)
 
 Notation " ! " := (False_rect _ _).
 
-Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A.
-intros.
-induction t.
-exact x.
-Defined.
+(** Abbreviation for first projection and hiding of proofs of subset objects. *)
+
+Notation " ` t " := (proj1_sig t) (at level 10) : core_scope.
+Notation "( x & ? )" := (@exist _ _ x _) : core_scope.
+
+(** Coerces objects to their support before comparing them. *)
 
-Lemma ex_pi2  : forall (A : Prop) (P : A -> Prop) (t : ex P),
- P (ex_pi1 t).
-intros A P.
-dependent inversion t.
-simpl.
-exact p.
-Defined.
+Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70).
 
+(** Quantifying over subsets. *)
+
+Notation "'fun' { x : A | P } => Q" :=
+  (fun x:{x:A|P} => Q)
+  (at level 200, x ident, right associativity).
 
-Notation "` t" := (proj1_sig t) (at level 100) : core_scope.
 Notation "'forall' { x : A | P } , Q" :=
   (forall x:{x:A|P}, Q)
   (at level 200, x ident, right associativity).
 
-Lemma subset_simpl : forall (A : Set) (P : A -> Prop) 
-	(t : sig P), P (` t).
-Proof.
-intros.
-induction t.
- simpl ; auto.
-Qed.
-
-Ltac destruct_one_pair :=
- match goal with
- | [H : (ex _) |- _] => destruct H
- | [H : (ex2 _) |- _] => destruct H
- | [H : (sig _) |- _] => destruct H
- | [H : (_ /\ _) |- _] => destruct H
-end.
-
-Ltac destruct_exists := repeat (destruct_one_pair) .
-
-Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; auto with arith.  
-
-(* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *)
-Ltac destruct_call f :=
-  match goal with
-    | H : ?T |- _  =>
-      match T with
-         context [f ?x ?y ?z] => destruct (f x y z)
-       | context [f ?x ?y] => destruct (f x y)
-       | context [f ?x] => destruct (f x)        
-      end
-    | |- ?T  =>
-      match T with
-        context [f ?x ?y ?z] => let n := fresh "H" in set (n:=f x y z); destruct n
-        | context [f ?x ?y] => let n := fresh "H" in set (n:=f x y); destruct n
-        | context [f ?x] => let n := fresh "H" in set (n:=f x); destruct n
-      end
-    end.
+Require Import Coq.Bool.Sumbool.
+
+(** Construct a dependent disjunction from a boolean. *)
+
+Notation "'dec'" := (sumbool_of_bool) (at level 0). 
 
+(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
+
+Notation in_right := (@right _ _ _).
+Notation in_left := (@left _ _ _).
+
+(** Default simplification tactic. *)
+
+Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
+  try (solve [ red ; intros ; discriminate ]) ; auto with *.  
+
+(** Extraction directives *)
 Extraction Inline proj1_sig.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
-Extract Inductive prod => "pair" [ "" ].
-Extract Inductive sigT => "pair" [ "" ].
+(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
+(* Extract Inductive sigT => "prod" [ "" ]. *)
 
 Require Export ProofIrrelevance.
+Require Export Coq.subtac.Heq.
+
+Delimit Scope program_scope with program.