Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from

svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses

........
  r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Comment grammar error
........
  r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
  
  The initial Type Classes patch.
  This patch introduces type classes and instance definitions a la Haskell.
  Technically, it uses the implicit arguments mechanism which was extended a bit. 
  The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
  It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). 
........
  r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix interface
........
  r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
  
  Fix more xlate code
........
  r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
  r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
  
  Bug fixes in Instance decls.
........
  r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
  
  Streamline typeclass context implementation, prepare for class binders in proof statements.
........
  r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
  
  Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
  r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
  
  Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
  r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
  
  Stupid bug
........
  r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
  r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
  
  Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
  r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
  
  Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
  New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
  Other bugs related to naming in typeclasses fixed. 
........
  r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
  
  Progress on setoids using type classes, recognize setoid equalities in hyps better.
  Streamline implementation to return more information when resolving setoids (return the results setoid).
........
  r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
  
  Syntax change, more like Coq
........
  r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
  
  Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
  r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
  
  Work on type classes based rewrite tactic.
........
  r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
  
  Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
  r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
  
  Forgot to add a file
........
  r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
  
  Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and 
  implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
  r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
  
  Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. 
  Add useful tactics to Program.Subsets.
........


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 442 insertions, 54 deletions

diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index c61d89a00..ee3d5fe0d 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -40,7 +40,7 @@ Proof.
   induction n.
     auto with arith.
     elim IHn; auto with arith.
-Qed.
+Defined.
 
 Lemma not_even_and_odd : forall n, even n -> odd n -> False.
 Proof.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
new file mode 100644
index 000000000..307005382
--- /dev/null
+++ b/theories/Classes/Init.v
@@ -0,0 +1 @@
+Instantiation Tactic := eauto 50 with typeclass_instances || eauto.
diff --git a/theories/Classes/Init.v.d b/theories/Classes/Init.v.d
new file mode 100644
index 000000000..482ac0796
--- /dev/null
+++ b/theories/Classes/Init.v.d
@@ -0,0 +1 @@
+theories/Classes/Init.vo theories/Classes/Init.glob: theories/Classes/Init.v
diff --git a/theories/Classes/Setoid.v b/theories/Classes/Setoid.v
new file mode 100644
index 000000000..915a7a944
--- /dev/null
+++ b/theories/Classes/Setoid.v
@@ -0,0 +1,192 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Certified Haskell Prelude.
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+Require Import Coq.Classes.Init.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** We first define setoids on a carrier, it amounts to an equivalence relation. 
+   Now [equiv] is overloaded for every [Setoid].
+*)
+
+Require Export Coq.Relations.Relations.
+
+Class Setoid (carrier : Type) (equiv : relation carrier) :=
+  equiv_prf : equivalence carrier equiv.
+
+(** Overloaded notation for setoid equivalence. Not to be confused with [eq] and [=]. *)
+
+Definition equiv [ Setoid A R ] : _ := R.
+
+Infix "==" := equiv (at level 70, no associativity).
+
+Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf.
+Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf.
+Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf.
+
+
+Ltac refl :=
+  match goal with
+    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
+    | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
+    | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X)
+    | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X)
+    | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X)
+  end.
+
+Ltac sym := 
+  match goal with
+    | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
+    | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X))
+    | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X))
+    | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X))
+    | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X))
+  end.
+
+Ltac trans Y := 
+  match goal with
+    | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z))
+    | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z))
+    | [ |- ?R ?A ?X ?Z ] => apply (equiv_trans (R:=R A) (x:=X) (y:=Y) (z:=Z))
+    | [ |- ?R ?A ?B ?X ?Z ] => apply (equiv_trans (R:=R A B) (x:=X) (y:=Y) (z:=Z))
+    | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z))
+  end.
+
+Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] (m : a -> b) : Prop :=
+  forall x y, eqa x y -> eqb (m x) (m y).
+
+Class [ Setoid a eqa, Setoid b eqb ] => Morphism (m : a -> b) :=
+  respect : respectful m.
+
+(** Here we build a setoid instance for functions which relates respectful ones only. *)
+
+Definition respecting [ Setoid a R, Setoid b R' ] : Type := { morph : a -> b | respectful morph }.
+
+Obligations Tactic := try red ; program_simpl ; unfold equiv in * ; try tauto.
+
+Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
+  Setoid ({ morph : a -> b | respectful morph })
+  (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) :=
+  equiv_prf := Build_equivalence _ _ _ _ _.
+
+Next Obligation.
+Proof.
+  trans (y x0) ; eauto.
+  apply H.
+  refl.
+Qed.
+
+Next Obligation.
+Proof.
+  sym ; apply H.
+  sym ; auto.
+Qed.
+
+(** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from 
+   some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *)
+
+Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] (m : a -> b -> c) : Prop :=
+  forall x y, eqa x y -> 
+    forall z w, eqb z w -> eqc (m x z) (m y w).
+
+Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => BinaryMorphism (m : a -> b -> c) :=
+  respect2 : binary_respectful m.
+
+Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] (m : a -> b -> c -> d) : Prop :=
+  forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v).
+
+Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => TernaryMorphism (m : a -> b -> c -> d) :=
+  respect3 : ternary_respectful m.
+
+(** Definition of the usual morphisms in [Prop]. *)
+
+Program Instance iff_setoid : Setoid Prop iff :=
+  equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym.
+
+Program Instance not_morphism : Morphism Prop iff Prop iff not.
+
+Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and.
+
+(* We make the setoids implicit, they're always [iff] *)
+
+Implicit Arguments Enriching BinaryMorphism [[!sa] [!sb] [!sc]].
+
+Program Instance or_morphism : ? BinaryMorphism or.
+
+Definition impl (A B : Prop) := A -> B.
+
+Program Instance impl_morphism : ? BinaryMorphism impl.
+
+Next Obligation.
+Proof.
+  unfold impl. tauto.
+Qed.
+
+(** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
+
+Program Instance [ Setoid a R ] => setoid_morphism : ? BinaryMorphism R.
+
+Next Obligation.
+Proof with auto.
+  split ; intros.
+  trans x. sym... trans z...
+  trans y... trans w... sym...
+Qed.
+  
+Definition iff_morphism : BinaryMorphism iff := setoid_morphism.
+
+Existing Instance iff_morphism.
+
+Implicit Arguments eq [[A]].
+
+Program Instance eq_setoid : Setoid A eq :=
+  equiv_prf := Build_equivalence _ _ _ _ _.
+
+Program Instance eq_morphism : BinaryMorphism A eq A eq Prop iff eq.
+
+Program Instance arrow_morphism : BinaryMorphism A eq B eq C eq m.
+
+Implicit Arguments arrow_morphism [[A] [B] [C]].
+
+Program Instance type_setoid : Setoid Type (fun x y => x = y) :=
+  equiv_prf := Build_equivalence _ _ _ _ _.
+
+Lemma setoid_subst : forall (x y : Type), x == y -> x -> y.
+Proof.
+  intros.
+  rewrite <- H.
+  apply X.
+Qed.
+
+Lemma prop_setoid_subst : forall (x y : Prop), x == y -> x -> y.
+Proof.
+  intros.
+  clrewrite <- H.
+  apply H0.
+Qed.
+
+Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc,
+  ? Morphism sb sc g, ? Morphism sa sb f ] => 
+  compose_morphism : ? Morphism sa sc (fun x => g (f x)).
+
+Next Obligation.
+Proof.
+  apply (respect (m0:=m)).
+  apply (respect (m0:=m0)).
+  assumption.
+Qed.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
new file mode 100644
index 000000000..8e037db1a
--- /dev/null
+++ b/theories/Classes/SetoidTactics.v
@@ -0,0 +1,37 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Certified Haskell Prelude.
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Classes.Setoid.
+
+Ltac rew H := clrewrite H.
+
+Lemma setoideq_eq [ sa : Setoid a eqa ] : forall x y, eqa x y -> x = y.
+Proof.
+  admit.
+Qed.
+
+Implicit Arguments setoideq_eq [[a] [eqa] [sa]].
+
+Ltac setoideq :=
+  match goal with
+    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
+  end.
+
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index d0bf5bee9..d9f5d10a1 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -9,7 +9,7 @@
   (*i $Id$ i*)
 
 Require Import Le Gt Minus Min Bool.
-Require Import Setoid.
+Require Import Coq.Setoids.Setoid.
 
 Set Implicit Arguments.
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 96c1c8f4d..85ed18891 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -85,17 +85,6 @@ Ltac abstract_eq_hyp H' p :=
       end
     end.
 
-(** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *)
-
-Ltac abstract_any_hyp H' p := 
-  match type of p with
-    ?X => 
-    match goal with 
-      | [ H : X |- _ ] => fail 1
-      | _ => set (H':=p) ; try (change p with H') ; clearbody H' ; simpl in H'
-    end
-  end.
-
 (** Apply the tactic tac to proofs of equality appearing as coercion arguments. 
    Just redefine this tactic (using [Ltac on_coerce_proof tac ::=]) to handle custom coercion operators.
    *)
@@ -180,3 +169,39 @@ Ltac clear_eqs := repeat clear_eq.
 Ltac simplify_eqs := 
   simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ;  
     try subst ; simpl ; repeat simpl_uip ; rewrite_refl_id.
+
+(** A tactic to remove trivial equality guards in hypotheses. *)
+
+Ltac simpl_IH_eq H :=
+  let tac H' := clear H ; rename H' into H in
+  let H' := fresh "H" in
+    match type of H with
+      | JMeq _ _ -> _ =>
+        assert (H' := H (JMeq_refl _)) ; tac H'
+      | _ = _ -> _ =>
+        assert (H' := H (refl_equal _)) ; tac H'
+    end.
+
+Ltac simpl_IH_eqs H := repeat simpl_IH_eq H.
+
+Ltac simpl_IHs_eqs := 
+  match goal with
+    | [ H : JMeq _ _ -> _ |- _ ] => simpl_IH_eqs H
+    | [ H : _ = _ -> _ |- _ ] => simpl_IH_eqs H
+  end.
+
+Require Import Coq.Program.Tactics.
+
+(** The following tactics allow to do induction on an already instantiated inductive predicate
+   by first generalizing it and adding the proper equalities to the context, in a maner similar to 
+   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
+
+Tactic Notation "dependent" "induction" ident(H) := 
+  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
+    induction H ; intros ; subst* ; try discriminates ; try simpl_IHs_eqs.
+
+(** This tactic also generalizes the goal by the given variables before the induction. *)
+
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
+  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
+    generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates ; try simpl_IHs_eqs.
diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v
index 22cb93d56..382252ce2 100644
--- a/theories/Program/FunctionalExtensionality.v
+++ b/theories/Program/FunctionalExtensionality.v
@@ -48,13 +48,13 @@ Ltac apply_ext :=
 
 (** For a function defined with Program using a well-founded order. *)
 
-Lemma fix_sub_eq_ext :
+Program Lemma fix_sub_eq_ext :
   forall (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R)
     (P : A -> Set)
-    (F_sub : forall x : A, (forall  {y : A | R y x}, P (`y)) -> P x),
+    (F_sub : forall x : A, (forall (y : A | R y x), P y) -> P x),
     forall x : A,
       Fix_sub A R Rwf P F_sub x =
-        F_sub x (fun {y : A | R y x}=> Fix A R Rwf P F_sub (`y)).
+        F_sub x (fun (y : A | R y x) => Fix A R Rwf P F_sub y).
 Proof.
   intros ; apply Fix_eq ; auto.
   intros.
@@ -65,12 +65,12 @@ Qed.
 
 (** For a function defined with Program using a measure. *)
 
-Lemma fix_sub_measure_eq_ext :
+Program Lemma fix_sub_measure_eq_ext :
   forall (A : Type) (f : A -> nat) (P : A -> Type)
-    (F_sub : forall x : A, (forall  {y : A | f y < f x}, P (`y)) -> P x),
+    (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x),
     forall x : A,
       Fix_measure_sub A f P F_sub x =
-        F_sub x (fun {y : A | f y < f x}=> Fix_measure_sub A f P F_sub (`y)).
+        F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y).
 Proof.
   intros ; apply Fix_measure_eq ; auto.
   intros.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index 39c5b7734..fb172db84 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -1,3 +1,4 @@
 Require Export Coq.Program.Utils.
 Require Export Coq.Program.Wf.
 Require Export Coq.Program.Equality.
+Require Export Coq.Program.Subset.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
new file mode 100644
index 000000000..54d830c89
--- /dev/null
+++ b/theories/Program/Subset.v
@@ -0,0 +1,141 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import Coq.Program.Utils.
+Require Import Coq.Program.Equality.
+
+(** Tactics related to subsets and proof irrelevance. *)
+
+(** Simplify dependent equality using sigmas to equality of the codomains if possible. *)
+
+Ltac simpl_existT :=
+  match goal with
+    [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => 
+    let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H
+  end.
+
+Ltac simpl_existTs := repeat simpl_existT.
+
+(** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to 
+   factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
+
+Ltac on_subset_proof_aux tac T :=
+  match T with
+    | context [ exist ?P _ ?p ] => try on_subset_proof_aux tac P ; tac p
+  end.
+
+Ltac on_subset_proof tac :=
+  match goal with
+    [ |- ?T ] => on_subset_proof_aux tac T
+  end.
+
+Ltac abstract_any_hyp H' p := 
+  match type of p with
+    ?X => 
+    match goal with 
+      | [ H : X |- _ ] => fail 1
+      | _ => set (H':=p) ; try (change p with H') ; clearbody H'
+    end
+  end.
+
+Ltac abstract_subset_proof := 
+  on_subset_proof ltac:(fun p => let H := fresh "eqH" in abstract_any_hyp H p ; simpl in H).
+
+Ltac abstract_subset_proofs := repeat abstract_subset_proof.
+
+Ltac pi_subset_proof_hyp p :=
+  match type of p with
+    ?X => 
+    match goal with 
+      | [ H : X |- _ ] => 
+        match p with
+          | H => fail 2
+          | _ => rewrite (proof_irrelevance X p H)
+        end
+      | _ => fail " No hypothesis with same type "
+    end
+  end.
+
+Ltac pi_subset_proof := on_subset_proof pi_subset_proof_hyp.
+
+Ltac pi_subset_proofs := repeat pi_subset_proof.
+
+(** Clear duplicated hypotheses *)
+
+Ltac clear_dup :=
+  match goal with 
+    | [ H : ?X |- _ ] => 
+      match goal with
+        | [ H' : X |- _ ] =>
+          match H' with
+            | H => fail 2 
+            | _ => clear H' || clear H
+          end
+      end
+  end.
+
+Ltac clear_dups := repeat clear_dup.
+
+(** The two preceding tactics in sequence. *)
+
+Ltac clear_subset_proofs :=
+  abstract_subset_proofs ; simpl in * |- ; pi_subset_proofs ; clear_dups.
+
+Ltac pi := repeat progress f_equal ; apply proof_irrelevance.
+
+Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> (`n) = (`m).
+Proof.
+  induction n.
+  induction m.
+  simpl.
+  split ; intros ; subst.
+
+  inversion H.
+  reflexivity.
+
+  pi.
+Qed.
+
+(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] 
+   in tactics. *)
+
+Program Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
+  fn (exist _ x (refl_equal x)).
+
+(* This is what we want to be able to do: replace the originaly matched object by a new, 
+   propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
+
+Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B) 
+  (y : A | y = x),
+  match_eq A B x fn = fn y.
+Proof.
+  intros.
+  unfold match_eq.
+  f_equal.
+  destruct y.
+  (* uses proof-irrelevance *)
+  apply <- subset_eq.
+  symmetry. assumption.
+Qed.
+
+(** Now we make a tactic to be able to rewrite a term [t] which is applied to a [match_eq] using an arbitrary
+   equality [t = u], and [u] is now the subject of the [match]. *)
+
+Ltac rewrite_match_eq H := 
+  match goal with
+    [ |- ?T ] => 
+    match T with
+      context [ match_eq ?A ?B ?t ?f ] =>
+      rewrite (match_eq_rewrite A B t f (exist _ _ (sym_eq H)))
+    end
+  end.
+
+(** Otherwise we can simply unfold [match_eq] and the term trivially reduces to the original definition. *)
+
+Ltac simpl_match_eq := unfold match_eq ; simpl.
+
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index e4c60e14a..ac0f5cf71 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -50,6 +50,7 @@ Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].
 Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H].
 
 (** Discriminate that also work on a [x <> x] hypothesis. *)
+
 Ltac discriminates :=
   match goal with
     | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity
@@ -151,21 +152,12 @@ Ltac bang :=
 Tactic Notation "contradiction" "by" constr(t) := 
   let H := fresh in assert t as H by auto with * ; contradiction.
 
-(** The following tactics allow to do induction on an already instantiated inductive predicate
-   by first generalizing it and adding the proper equalities to the context, in a manner similar to 
-   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
-
-Tactic Notation "dependent" "induction" ident(H) := 
-  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
-    induction H ; intros ; subst* ; try discriminates.
-
-(** This tactic also generalizes the goal by the given variables before the induction. *)
-
-Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
-  generalize_eqs H ; clear H ; (intros until 1 || intros until H) ; 
-    generalize l ; clear l ; induction H ; intros ; subst* ; try discriminates.
+(** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto with *]
+   is overkill and slows things down, better rebind using [Obligations Tactic := tac] in this case, 
+   possibly using [program_simplify] to use standard goal-cleaning tactics. *)
 
-(** The default simplification tactic used by Program. *)
+Ltac program_simplify :=
+  simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; 
+    try (solve [ red ; intros ; destruct_conjs ; discriminate ]).
 
-Ltac program_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; 
-  try (solve [ red ; intros ; destruct_conjs ; discriminate ]) ; auto with *.  
+Ltac program_simpl := program_simplify ; auto with *.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index a268f0afb..6af81a410 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -18,9 +18,9 @@ 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.
+(* Notation "{ ( x , y )  :  A  |  P }" :=  *)
+(*   (sig (fun anonymous : A => let (x,y) := anonymous in P)) *)
+(*   (x ident, y ident, at level 10) : type_scope. *)
 
 (** Generates an obligation to prove False. *)
 
@@ -45,13 +45,13 @@ 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 "'fun' ( x : A | P ) => Q" := *)
+(*   (fun (x :A|P} => Q) *)
+(*   (at level 200, x ident, right associativity). *)
 
-Notation "'forall' { x : A | P } , Q" :=
-  (forall x:{x:A|P}, Q)
-  (at level 200, x ident, right associativity).
+(* Notation "'forall' ( x : A | P ), Q" := *)
+(*   (forall (x : A | P), Q) *)
+(*   (at level 200, x ident, right associativity). *)
 
 Require Import Coq.Bool.Sumbool.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 55784671f..70b1b1b5a 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -34,11 +34,11 @@ Section Well_founded.
     Hypothesis
       F_ext :
       forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
-        (forall y:{ y:A | R y x}, f y = g y) -> F_sub x f = F_sub x g.
+        (forall (y : A | R y x), f y = g y) -> F_sub x f = F_sub x g.
 
     Lemma Fix_F_eq :
       forall (x:A) (r:Acc R x),
-        F_sub x (fun (y:{y:A|R y x}) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
+        F_sub x (fun (y:A|R y x) => Fix_F (`y) (Acc_inv r (proj1_sig y) (proj2_sig y))) = Fix_F x r.
     Proof. 
       destruct r using Acc_inv_dep; auto.
     Qed.
@@ -52,7 +52,7 @@ Section Well_founded.
       rewrite (proof_irrelevance (Acc R x) r s) ; auto.
     Qed.
 
-    Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:{y:A|R y x}) => Fix (proj1_sig y)).
+    Lemma Fix_eq : forall x:A, Fix x = F_sub x (fun (y:A|R y x) => Fix (proj1_sig y)).
     Proof.
       intro x; unfold Fix in |- *.
       rewrite <- (Fix_F_eq ).
@@ -64,7 +64,7 @@ Section Well_founded.
         forall x : A,
           Fix_sub P F_sub x =
           let f_sub := F_sub in
-            f_sub x (fun  {y : A | R y x}=> Fix (`y)).
+            f_sub x (fun (y : A | R y x) => Fix (`y)).
       exact Fix_eq.
     Qed.
 
@@ -98,7 +98,7 @@ Section Well_founded_measure.
   Section FixPoint.
     Variable P : A -> Type.
     
-    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
+    Variable F_sub : forall x:A, (forall (y : A | m y < m x), P (proj1_sig y)) -> P x.
     
     Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
     
@@ -106,8 +106,8 @@ Section Well_founded_measure.
     
     Hypothesis
       F_ext :
-      forall (x:A) (f g:forall y:{y:A | m y < m x}, P (`y)),
-        (forall y:{ y:A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
+      forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)),
+        (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
 
     Lemma Fix_measure_F_eq :
       forall (x:A) (r:Acc lt (m x)),
@@ -137,7 +137,7 @@ Section Well_founded_measure.
         forall x : A,
           Fix_measure_sub P F_sub x =
           let f_sub := F_sub in
-            f_sub x (fun  {y : A | m y < m x}=> Fix_measure (`y)).
+            f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
       exact Fix_measure_eq.
     Qed.
 
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 18e8b6e77..f93a12955 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -1,4 +1,3 @@
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/Setoids/Setoid_tac.v b/theories/Setoids/Setoid_tac.v
index f979ec11c..664316805 100644
--- a/theories/Setoids/Setoid_tac.v
+++ b/theories/Setoids/Setoid_tac.v
@@ -1,4 +1,3 @@
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)