New commands

 setoid_reflexivity
 setoid_symmetry
 setoid_transitivity

The command
 setoid_symmetry in ...
is not implemented yet (it behaves just as symmetry in ... for now).


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

5 files changed, 132 insertions, 31 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bbcdce92d2..fd90a0a497 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -228,6 +228,19 @@ VERNAC COMMAND EXTEND AddRelation3
    [ add_relation n a aeq None None (Some t) ]
 END
 
+TACTIC EXTEND SetoidSymmetry
+   [ "Setoid_symmetry" ] -> [ setoid_symmetry ]
+ | [ "Setoid_symmetry" "in" ident(n) ] -> [ setoid_symmetry_in n ]
+END
+
+TACTIC EXTEND SetoidReflexivity
+   [ "Setoid_reflexivity" ] -> [ setoid_reflexivity ]
+END
+
+TACTIC EXTEND SetoidTransitivity
+   [ "Setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ]
+END
+
 (* Inversion lemmas (Leminv) *)
 
 open Inv
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index e25c261f60..f0dc21dee9 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1143,8 +1143,7 @@ let beta_expand c args_rev =
 
 exception Use_rewrite
 
-let relation_of_hypothesis_and_term_to_rewrite new_goals gl (_,h) t =
- let hypt = pf_type_of gl h in
+let relation_class_that_matches_a_constr caller_name raise_opt new_goals hypt =
  let (heq, hargs) = decompose_app hypt in
  let rec get_all_but_last_two =
   function
@@ -1160,19 +1159,19 @@ let relation_of_hypothesis_and_term_to_rewrite new_goals gl (_,h) t =
    match rel,new_goals with
       Leibniz _,[] ->
        assert (subst = []);
-       raise Use_rewrite (* let's optimize the proof term size *)
+       raise_opt () (* let's optimize the proof term size *)
     | Leibniz (Some _), _ ->
        assert (subst = []);
        rel
     | Leibniz None, _ ->
-       (match subst with
-           [t] -> Leibniz (Some t)
-         | _ -> assert false)
+       (* for well-typedness reasons it should have been catched by the
+          previous guard in the previous iteration. *)
+       assert false
     | Relation rel,_ -> Relation (apply_to_relation (Array.of_list subst) rel)
   with Not_found ->
    if l = [] then
     (*CSC: still "setoid" in the error message *)
-    errorlabstrm "Setoid_rewrite"
+    errorlabstrm caller_name
      (prterm (mkApp (aeq, Array.of_list all_aeq_args)) ++
       str " is not a setoid equality.")
    else
@@ -1628,7 +1627,8 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
  in
   try
    let input_relation =
-    relation_of_hypothesis_and_term_to_rewrite new_goals gl hyp c1 in
+    relation_class_that_matches_a_constr "Setoid_rewrite"
+     (fun () -> raise Use_rewrite) new_goals (pf_type_of gl (snd hyp)) in
    let output_relation,output_direction,marked_but =
     mark_occur gl ~new_goals c1 but input_relation input_direction in
    let cic_output_direction = cic_direction_of_direction output_direction in
@@ -1748,3 +1748,73 @@ let setoid_replace_in id relation c1 c2 ~new_goals gl =
      tclTHENLASTn
       (setoid_replace relation c2 c1 ~new_goals)
       [| exact_check (mkVar id); tclIDTAC |] ] gl
+
+(* [setoid_]{reflexivity,symmetry,transitivity} tactics *)
+
+exception Use_reflexivity
+
+let setoid_reflexivity gl =
+ try
+  let relation_class =
+   relation_class_that_matches_a_constr "Setoid_reflexivity"
+    (fun () -> raise Use_reflexivity) [] (pf_concl gl) in
+  match relation_class with
+     Leibniz _ -> assert false (* since [] is empty *)
+   | Relation rel ->
+      match rel.rel_refl with
+         None ->
+          errorlabstrm "Setoid_reflexivity"
+           (str "The relation " ++ prrelation rel ++ str " is not reflexive.")
+       | Some refl -> apply refl gl
+ with
+  Use_reflexivity -> reflexivity gl
+
+exception Use_symmetry
+
+let setoid_symmetry gl =
+ try
+  let relation_class =
+   relation_class_that_matches_a_constr "Setoid_symmetry"
+    (fun () -> raise Use_symmetry) [] (pf_concl gl) in
+  match relation_class with
+     Leibniz _ -> assert false (* since [] is empty *)
+   | Relation rel ->
+      match rel.rel_sym with
+         None ->
+          errorlabstrm "Setoid_symmetry"
+           (str "The relation " ++ prrelation rel ++ str " is not symmetric.")
+       | Some sym -> apply sym gl
+ with
+  Use_symmetry -> symmetry gl
+
+let setoid_symmetry_in = symmetry_in
+
+exception Use_transitivity
+
+let setoid_transitivity c gl =
+ try
+  let relation_class =
+   relation_class_that_matches_a_constr "Setoid_transitivity"
+    (fun () -> raise Use_transitivity) [] (pf_concl gl) in
+  match relation_class with
+     Leibniz _ -> assert false (* since [] is empty *)
+   | Relation rel ->
+      let ctyp = pf_type_of gl c in
+      let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in
+       match rel'.rel_trans with
+          None ->
+           errorlabstrm "Setoid_transitivity"
+            (str "The relation " ++ prrelation rel ++ str " is not transitive.")
+        | Some trans ->
+           let transty = nf_betaiota (pf_type_of gl trans) in
+           let argsrev, _ =
+            Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in
+           let binder =
+            match List.rev argsrev with
+               _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2
+             | _ -> assert false
+           in
+            apply_with_bindings
+             (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
+ with
+  Use_transitivity -> transitivity c gl
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 0fd0548c29..917b3e02fb 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -58,6 +58,11 @@ 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 setoid_reflexivity : tactic
+val setoid_symmetry : tactic
+val setoid_symmetry_in : identifier -> tactic
+val setoid_transitivity : constr -> tactic
+
 val add_relation :
  Names.identifier -> constr_expr -> constr_expr -> constr_expr option ->
   constr_expr option -> constr_expr option -> unit
diff --git a/test-suite/success/setoid_test.v8 b/test-suite/success/setoid_test.v8
index 968ccd1d4c..5c62d12a14 100644
--- a/test-suite/success/setoid_test.v8
+++ b/test-suite/success/setoid_test.v8
@@ -54,8 +54,7 @@ split; apply add_aux.
 assumption.
 
 rewrite H.
-apply Seq_refl.
-exact setoid_set.
+setoid_reflexivity.
 Qed.
 
 Fixpoint remove (a : A) (s : set) {struct s} : set :=
diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v8
index c0a94d56d7..72b9d03ce0 100644
--- a/test-suite/success/setoid_test2.v8
+++ b/test-suite/success/setoid_test2.v8
@@ -12,10 +12,8 @@ Require Export Setoid.
    +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.
-  +12. goal con impl
-  +13. testare *veramente* setoid_replace (ora testato solamente il caso
+  +11. goal con impl
+  +12. testare *veramente* setoid_replace (ora testato solamente il caso
        di fallback su replace)
 
   Incompatibilita':
@@ -29,34 +27,47 @@ Require Export Setoid.
 ### Come evitare di dover fare "Require Setoid" prima di usare la
     tattica?
 
-### scelta: quando ci sono piu' scelte dare un warning oppure fallire?
+??? 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
+??? 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
+??? ??? <-> 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
 
 ### diminuire la taglia dei proof term
 
-### il messaggio di errore non e' assolutamente significativo quando
+??? il messaggio di errore non e' assolutamente significativo quando
     nessuna marcatura viene trovata
 
+### fare in modo che uscendo da una sezione vengano quantificate le
+    relazioni e i morfismi. Hugo: paciugare nel discharge.ml
+
+### implementare relazioni/morfismi quantificati con dei LetIn (che palle...)
+    decompose_prod da far diventare simile a un Reduction.dest_arity?
+    (ma senza riduzione??? e perche' li' c'e' riduzione?)
+    Soluzione da struzzo: fare zeta-conversione.
+
+### fare in modo che impl sia espanso nel lemma di compatibilita' del
+    morfismo (richiesta di Marco per poter fare Add Hing)
+
+??? snellire la sintassi omettendo "proved by" come proposto da Marco?  ;-(
+
+### non capisce piu' le riscritture con uguaglianze quantificate (almeno
+    nell'esempio di Marco)
+
+### unificare le varie check_...
+### sostituire a Use_* una sola eccezione Optimize
+
   Implementare:
    -2. user-defined subrelations && user-proved subrelations
    -1. trucco di Bruno
-    0. [setoid_]symmetry, [setoid_]reflexivity, [setoid_]transitivity (?!?)
 
   Sorgenti di inefficacia:
     1. scelta del setoide di default per un sostegno: per farlo velocemente
@@ -83,20 +94,23 @@ Require Export Setoid.
        l'utente puo' esplicitamente disambiguare la scelta globale fornendo
        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
+       della replace la setoid_replace invoca direttamente la replace.
+       Stessa cosa per la setoid_rewrite.
     9. permette di gestire termini in cui il prefisso iniziale dell'albero
        (fino a trovare il termine da riscrivere) non sia formato esclusivamente
        da morfismi il cui dominio e codominio sia un setoide.
        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. [setoid_]rewrite ... in ...
+   10. [setoid_]rewrite ... in ...
        setoid_replace ... in ...
-       [setoid_]reflexivity???
-       [setoid_]transitivity???
-       [setoid_]symmetry???
+       [setoid_]reflexivity
+       [setoid_]transitivity ...
+       [setoid_]symmetry
+       [setoid_]symmetry in ...
    11. permette di dichiarare dei setoidi/relazioni/morfismi in un module
        type
+   12. relazioni, morfismi e setoidi quantificati
 *)
 
 Axiom S1: Set.
@@ -122,13 +136,13 @@ Add Morphism f : f_compat2. Admitted.
 Theorem test1: forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
  intros.
  rewrite H.
- apply (Seq_refl _ _ SetoidS2).
+ setoid_reflexivity.
 Qed.
 
 Theorem test1': forall x y, (eqS1 x y) -> (eqS2 (f x 0) (f y 0)).
  intros.
  setoid_replace x with y.
- apply (Seq_refl _ _ SetoidS2).
+ setoid_reflexivity.
  assumption.
 Qed.