Support for occurences and 'in' in class_setoid, work on corresponding tactics in SetoidClass

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

3 files changed, 116 insertions, 36 deletions

diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index b05b7ec8c2..66324158dd 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -83,7 +83,7 @@ let resolve_morphism_evd env evd app =
   let evm' = Evd.evars_of evd' in
     match Evd.evar_body (Evd.find evm' (fst (destEvar ev))) with
 	Evd.Evar_empty -> raise Not_found
-      | Evd.Evar_defined c -> evd := Evarutil.nf_evar_defs evd'; c
+      | Evd.Evar_defined c -> evd := Evarutil.nf_evar_defs evd'; Evarutil.nf_isevar !evd c
 
 let is_equiv env sigma t = 
   isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t
@@ -136,7 +136,6 @@ let resolve_morphism env sigma direction oldt m args args' =
   evars := Evarutil.nf_evar_defs !evars;
   let evm = Evd.evars_of !evars in
   let ctxargs = List.map (Reductionops.nf_evar evm) subst in
-(*   let ctx, sup = Util.list_chop len ctxargs in *)
   let m' = Reductionops.nf_evar evm m' in
   let appproj = applistc (mkConst proj) (ctxargs @ [m' ; morph_instance]) in
   let projargs, respars, typeargs = 
@@ -159,26 +158,41 @@ let resolve_morphism env sigma direction oldt m args args' =
 	[ a ; r ; s ] -> (proof, (a, r, s, oldt, newt))
       | _ -> assert(false)
       
-let build_new gl env setoid direction origt newt hyp hypinfo concl =
-  let rec aux t = 
+let build_new gl env setoid direction occs origt newt hyp hypinfo concl =
+  let is_occ occ = occs = [] || List.mem occ occs in
+  let rec aux t occ = 
     match kind_of_term t with
       | _ when eq_constr t origt -> 
-	  Some (hyp, hypinfo)
+	  if is_occ occ then
+	    Some (hyp, hypinfo), succ occ
+	  else None, succ occ
+
       | App (m, args) ->
-	  let args' = Array.map aux args in
-	    if array_for_all (fun x -> x = None) args' then None
+	  let args', occ = 
+	    Array.fold_left 
+	      (fun (acc, occ) arg -> let res, occ = aux arg occ in (res :: acc, occ))
+	      ([], occ) args
+	  in
+	  let res = 
+	    if List.for_all (fun x -> x = None) args' then None
 	    else 
-	      (try Some (resolve_morphism env (project gl) direction t m args args')
-		with Not_found -> None)
+	      let args' = Array.of_list (List.rev args') in
+		(try Some (resolve_morphism env (project gl) direction t m args args')
+		  with Not_found -> None)
+	  in res, occ
+
       | Prod (_, x, b) -> 
-	  let x', b' = aux x, aux b in
+	  let x', occ = aux x occ in
+	  let b', occ = aux b occ in
+	  let res = 
 	    if x' = None && b' = None then None
 	    else 
 	      (try Some (resolve_morphism env (project gl) direction t (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |])
 		with Not_found -> None)
-		
-      | _ -> None
-  in aux concl
+	  in res, occ
+
+      | _ -> None, occ
+  in aux concl 1
 
 let decompose_setoid_eqhyp env sigma c dir t = 
   match kind_of_term t with
@@ -194,29 +208,53 @@ let decompose_setoid_eqhyp env sigma c dir t =
 	  with Not_found -> error "Not a (declared) setoid equality")
     | _ -> error "Not a setoid equality"
 
-let cl_rewrite c left2right gl =
+let cl_rewrite_clause c left2right occs clause gl =
   let env = pf_env gl in
   let sigma = project gl in
   let hyp = pf_type_of gl c in
   let hypt, (typ, rel, setoid, origt, newt as hypinfo) = decompose_setoid_eqhyp env sigma c left2right hyp in
-  let concl = pf_concl gl in
-  let _concltyp = pf_type_of gl concl in
-  let eq = build_new gl env setoid left2right origt newt hypt hypinfo concl in
+  let concl, is_hyp = 
+    match clause with
+	Some ((_, id), _) -> pf_get_hyp_typ gl id, Some id
+      | None -> pf_concl gl, None
+  in
+  let eq, _ = build_new gl env setoid left2right occs origt newt hypt hypinfo concl in
     match eq with  
 	Some (p, (_, _, _, _, t)) -> 
 	  let proj = 
 	    if left2right then 
-	      applistc (Lazy.force coq_proj2)
-		[ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] 
+	      let proj = if is_hyp <> None then coq_proj1 else coq_proj2 in
+		applistc (Lazy.force proj)
+		  [ mkProd (Anonymous, concl, t) ; mkProd (Anonymous, t, concl) ; p ] 
 	    else 
-	      applistc (Lazy.force coq_proj1)
-		[ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] 
+	      let proj = if is_hyp <> None then coq_proj2 else coq_proj1 in
+		applistc (Lazy.force proj)
+		  [ mkProd (Anonymous, t, concl) ; mkProd (Anonymous, concl, t) ; p ] 
 	  in
-	    (Tactics.apply proj) gl
+	    (match is_hyp with
+	      | Some id -> Tactics.apply_in true id [proj,NoBindings]
+	      | None -> Tactics.apply proj) gl
       | None -> tclIDTAC gl
 	  
 open Extraargs
 
+
+
 TACTIC EXTEND class_rewrite
-| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite c o ]
+| [ "clrewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o occ (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o [] (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) constr(c) "at" occurences(occ) ] -> [ cl_rewrite_clause c o occ None ]
+| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o [] None ]
+END
+
+let clsubstitute o c =
+  let is_tac id = match kind_of_term c with Var id' when id' = id -> true | _ -> false in
+    Tacticals.onAllClauses 
+      (fun cl -> 
+	match cl with
+	  | Some ((_,id),_) when is_tac id -> tclIDTAC
+	  | _ -> cl_rewrite_clause c o [] cl)
+
+TACTIC EXTEND map_tac
+| [ "clsubstitute" orient(o) constr(c) ] -> [ clsubstitute o c ]
 END
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 3043a92397..c5befaa115 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -7,10 +7,12 @@
 (*         *       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 *)
+(* Typeclass-based setoids, tactics and standard instances.
+   TODO: explain clrewrite, clsubstitute and so on.
+ 
+   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 $ *)
 
@@ -33,9 +35,10 @@ Class Setoid (carrier : Type) (equiv : relation carrier) :=
 
 Definition equiv [ Setoid A R ] : _ := R.
 
-(** Subset objects will be first coerced to their underlying type. *)
+(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
 
-Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope.
+(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *)
+Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
 
 Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
 
@@ -86,6 +89,23 @@ Ltac do_setoid_trans Y :=
 
 Ltac trans y := do_setoid_trans y.
 
+(** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
+
+Ltac clsubst H := 
+  match type of H with
+    ?x == ?y => clsubstitute H ; clear H x
+  end.
+
+Ltac clsubst_nofail :=
+  match goal with
+    | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail
+    | _ => idtac
+  end.
+  
+(** [subst*] will try its best at substituting every equality in the goal. *)
+
+Tactic Notation "clsubst" "*" := clsubst_nofail.
+
 (** Tactics to immediately solve the goal without user help. *)
 
 Ltac setoid_refl :=
@@ -146,30 +166,44 @@ Ltac setoid_sat :=
     | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
   end.
 
+Ltac setoid_simplify_one :=
+  match goal with
+    | [ H : ?x == ?x |- _ ] => clear H
+    | [ H : ?x == ?y |- _ ] => clsubst H
+    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+  end.
+
+Ltac setoid_simplify := repeat setoid_simplify_one.
+
 Ltac setoid_saturate := repeat setoid_sat.
 
 Ltac setoidify_tac :=
   match goal with
     | [ s : Setoid ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
-    | [ s : Setoid ?A ?R |- ?R ?x ?y ] => change (R x y) with (@equiv A R s x y)
+    | [ s : Setoid ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
   end.
 
 Ltac setoidify := repeat setoidify_tac.
 
-Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] (m : a -> b) : Prop :=
+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 [ sa : Setoid a eqa, sb : Setoid b eqb ] => Morphism (m : a -> b) :=
+Class [ sa : Setoid a eqa, sb : 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 }.
+Definition respecting [ Setoid a R, Setoid b R' ] : Type := 
+  { morph : a -> b | respectful morph }.
 
-Ltac program_simpl ::= try red ; default_program_simpl ; try tauto.
+Ltac obligations_tactic ::= try red ; program_simpl ; try tauto.
 
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
+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 _ _ _ _ _.
 
@@ -325,4 +359,4 @@ Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid :
 
 (** Reset the default Program tactic. *)
 
-Ltac program_simpl ::= default_program_simpl.
+Ltac obligations_tactic ::= program_simpl.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 3b4d90a5c5..f68a7d3a4b 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -22,6 +22,14 @@ Unset Strict Implicit.
 
 Require Export Coq.Classes.SetoidClass.
 
+(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
+   classically. *)
+
+Require Import Coq.Logic.Decidable.
+
+Class [ Setoid A R ] => DecidableSetoid :=
+  setoid_decidable : forall x y : A, decidable (x == y).
+
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
 Class [ Setoid A R ] => EqDec :=