New tactic [setoid_]rewrite ... in ... [generate side conditions ...].

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

5 files changed, 65 insertions, 31 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 05f92985ba..eb90fa213e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -97,7 +97,9 @@ let general_rewrite_in lft2rgt id (c,l) gl =
   let _,t = splay_prod env sigma ctype in
   match match_with_equation t with
     | None -> (* Do not deal with setoids yet *) 
-        error "The term provided does not end with an equation" 
+	if l = NoBindings
+	then general_s_rewrite_in id lft2rgt c [] gl
+	else error "The term provided does not end with an equation" 
     | Some (hdcncl,_) -> 
         let hdcncls = string_of_inductive hdcncl in 
 	let suffix =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1457f09daa..6fac3703e5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -180,6 +180,10 @@ TACTIC EXTEND SetoidRewrite
    -> [ general_s_rewrite b c ~new_goals:[] ]
  | [ "Setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ]
    -> [ general_s_rewrite b c ~new_goals:l ]
+ | [ "Setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] ->
+      [ general_s_rewrite_in h b c ~new_goals:[] ]
+ | [ "Setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] ->
+      [ general_s_rewrite_in h b c ~new_goals:l ]
 END
 
 VERNAC COMMAND EXTEND AddSetoid1
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 42cee320a4..4c5dc08b0d 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1339,8 +1339,7 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
    Use_rewrite ->
     !general_rewrite (input_direction = Left2Right) (snd hyp) gl
 
-let general_s_rewrite lft2rgt c ~new_goals gl =
- let direction = if lft2rgt then Left2Right else Right2Left in
+let analyse_hypothesis gl c =
  let ctype = pf_type_of gl c in
  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
@@ -1348,11 +1347,34 @@ let general_s_rewrite lft2rgt c ~new_goals gl =
    | [c1;c2] -> (c1, c2)
    | x::y::z -> get_last_two (y::z)
    | _ -> error "The term provided is not an equivalence" in
- let (c1,c2) = get_last_two args in
+ let c1,c2 = get_last_two args in
+  eqclause,c1,c2
+
+let general_s_rewrite lft2rgt c ~new_goals gl =
+ let direction = if lft2rgt then Left2Right else Right2Left in
+ let eqclause,c1,c2 = analyse_hypothesis gl c in
   match direction with
      Left2Right -> relation_rewrite c1 c2 (direction,eqclause) ~new_goals gl
    | Right2Left -> relation_rewrite c2 c1 (direction,eqclause) ~new_goals gl
 
+let general_s_rewrite_in id lft2rgt c ~new_goals gl =
+ let eqclause,c1,c2 = analyse_hypothesis gl c in
+ let hyp = pf_type_of gl (mkVar id) in
+ let new_hyp =
+  if lft2rgt then
+   Termops.replace_term c1 c2 hyp
+  else
+   Termops.replace_term c2 c1 hyp
+ in
+  tclTHENS
+   (cut new_hyp)
+   [ (* Try to insert the new hyp at the same place *)
+     tclORELSE (intro_replacing id)
+       (tclTHEN (clear [id]) (introduction id));
+     tclTHENLAST
+      (general_s_rewrite (not lft2rgt) c ~new_goals)
+      (exact_check (mkVar id))] gl
+
 exception Use_replace
 
 (*CSC: still setoid in the name *)
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index d815954ec4..3b71708b4a 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -11,7 +11,7 @@
 open Term
 open Proof_type
 open Topconstr
-
+open Names
 
 type morphism_signature = (bool option * constr_expr) list * constr_expr
 
@@ -28,6 +28,8 @@ val setoid_replace :
  constr option -> constr -> constr -> new_goals:constr list -> tactic
 
 val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic
+val general_s_rewrite_in :
+ identifier -> bool -> constr -> new_goals:constr list -> tactic
 
 val add_relation :
  constr_expr -> constr_expr -> constr_expr option -> constr_expr option -> unit
diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8
index a57f7f2d1e..86f54406e3 100644
--- a/test-suite/success/setoid_test2.v8
+++ b/test-suite/success/setoid_test2.v8
@@ -3,22 +3,18 @@ Require Export Setoid.
 (* Testare:
    +1. due setoidi con ugualianza diversa sullo stesso tipo
    +2. due setoidi sulla stessa uguaglianza
-    3. due morfismi sulla stessa funzione ma setoidi diversi
+   +3. due morfismi sulla stessa funzione ma setoidi diversi
    +4. due morfismi sulla stessa funzione e stessi setoidi
    +5. setoid_replace
-    6. solo cammini mal tipati (attualmente non verifico mai che il
-       cammino trovato prendendo a caso sia mal-tipato)
-       ==> non riesco ancora a fare l'esempio perche' mi manca la sintassi.
-       Dovrei giocare con i moduli...
+   +6. solo cammini mal tipati
    +7. esempio (f (g (h E1)))
        dove h:(T1,=1) -> T2, g:T2->(T3,=3), f:(T3,=3)->Prop
    +8. test con occorrenze non lineari del pattern
    +9. test in cui setoid_replace fa direttamente fallback su replace
    10. sezioni
    11. setoid_rewrite invocata su una Leibniz equality ritorna un errore
-       invece di provare rewrite. Provare rewrite divergerebbe ==> trovare
-       una soluzione.
-   12. goal con Imp
+       invece di provare rewrite.
+  +12. goal con impl
   +13. testare *veramente* setoid_replace (ora testato solamente il caso
        di fallback su replace)
 
@@ -28,24 +24,35 @@ Require Export Setoid.
     3. iff invece di if in "Add Morphism" nel caso di predicati
     4. setoid_replace poteva riscrivere sia c1 in c2 che c2 in c1
 
-### setoid_replace ... with ... dovrebbe tentare le due vie;
-    che fare se entrambe funzionano?
-### coq_impl (in mark_occur) ha implicitamente tipo 'a -> 'a
-    dove 'a = (Prop,iff) oppure 'a = (Prof,impl). Altri tipi (e.g.
-    (Prop,iff) -> (Prop,impl)) non sono ammessi.
-### Pre-dichiarare il morfismo impl.
+### Come evitare di dover fare "Require Setoid" prima di usare la
+    tattica?
+
+### scelta: quando ci sono piu' scelte dare un warning oppure fallire?
+    difficile quando la tattica e' rewrite ed e' usata in tattiche
+    automatiche
+
+### in test4.v il setoid_rewrite non si puo' sostituire con rewrite
+    perche' questo ultimo fallisce per via dell'unificazione
+
+### ??? <-> non e' sottorelazione di ->. Quindi ora puo' capitare
+    di non riuscire a provare goal del tipo A /\ B dove (A, <->) e
+    (B, ->) (per esempio)
+
 ### Dichiarazione dentro a un module type e a una sezione: ???
 ### Relazioni universalmente quantificate: ???
 ### Implementare zucchero sintattico per partial setoids.
+    Stessa cosa per ogni relazione transitiva? In effetti basta lo
+    zucchero sintattico per le transitive.
 ### Nota: il parsing e pretty printing delle relazioni non e' in synch!
     eq contro (ty,eq). Uniformare
 
+### il messaggio di errore non e' assolutamente significativo quando
+    nessuna marcatura viene trovata
+
   Implementare:
    -1. user-defined subrelations && user-proved subrelations
     0. trucco di Bruno
-    1. rewrite ... in ...
     2. setoid_replace ... with ... in ...
-    3. perche' rewrite ma non replace?
     4. [setoid_]symmetry, [setoid_]reflexivity, [setoid_]transitivity (?!?)
 
   Sorgenti di inefficacia:
@@ -69,9 +76,9 @@ Require Export Setoid.
     6. permette di gestire riscritture ove ad almeno una funzione venga
        associato piu' di un morfismo. Vengono automaticamente calcolate
        le scelte globali che rispettano il tipaggio.
-   #7. se esistono piu' scelte globali che rispettano le regole di tipaggio
+    7. se esistono piu' scelte globali che rispettano le regole di tipaggio
        l'utente puo' esplicitamente disambiguare la scelta globale fornendo
-       esplicitamente la scelta per alcune occorrenze di una funzione.
+       esplicitamente la scelta delle side conditions generate.
     8. nel caso in cui la setoid_replace sia stata invocata al posto
        della replace la setoid_replace invoca direttamente la replace
     9. permette di gestire termini in cui il prefisso iniziale dell'albero
@@ -80,14 +87,11 @@ Require Export Setoid.
        Ovvero ammette anche morfismi il cui dominio e/o codominio sia
        l'uguaglianza di Leibniz. (Se entrambi sono uguaglianze di Leibniz
        allora il setoide e' una semplice funzione).
-  ?10. maggiore uniformita' sintattica: rewrite == setoid_rewrite;
-       replace == setoid_replace; symmetry == setoid_symmetry;
-       reflexivity == setoid_reflexivity. Nota: in tal caso, pero',
-       si e' sempre in presenza di ambiguita' per tutte le tattiche tranne
-       che la rewrite (in quanto c'e' sempre almeno la scelta setoide vs
-       Leibniz). Dare un comando che permette
-       di indicare il setoide di default associato a una funzione in un
-       determinato momento?
+  ?10. [setoid_]rewrite ... in ...
+       setoid_replace ... in
+       [setoid_]reflexivity???
+       [setoid_]transitivity???
+       [setoid_]symmetry???
 *)
 
 Axiom S1: Set.