The Coq part of the reflexive part can now deal with irreflexive relations too.

In particular it can deal with partial setoids (also called typoids).
The latter feature was request by Marco Maggesi.

This commit is just a porting of the ML part of the tactic to the new
Coq part. It does not allow to exploit the new potentialities, yet.


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

1 files changed, 46 insertions, 21 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 195ba3c61b..f331a15a4d 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -99,6 +99,10 @@ let coq_AsymmetricReflexive = lazy(constant ["Setoid"] "AsymmetricReflexive")
 let coq_SymmetricReflexive = lazy(constant ["Setoid"] "SymmetricReflexive")
 let coq_Leibniz = lazy(constant ["Setoid"] "Leibniz")
 
+let coq_RAsymmetricReflexive = lazy(constant ["Setoid"] "RAsymmetricReflexive")
+let coq_RSymmetricReflexive = lazy(constant ["Setoid"] "RSymmetricReflexive")
+let coq_RLeibniz = lazy(constant ["Setoid"] "RLeibniz")
+
 let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl")
 let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym")
 let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans")
@@ -122,8 +126,8 @@ let coq_make_compatibility_goal_aux_ref =
  lazy(reference ["Setoid"] "make_compatibility_goal_aux")
 
 let coq_App = lazy(constant ["Setoid"] "App")
-let coq_Toreplace = lazy(constant ["Setoid"] "Toreplace")
-let coq_Tokeep = lazy(constant ["Setoid"] "Tokeep")
+let coq_ToReplace = lazy(constant ["Setoid"] "ToReplace")
+let coq_ToKeep = lazy(constant ["Setoid"] "ToKeep")
 let coq_fcl_singl = lazy(constant ["Setoid"] "fcl_singl")
 let coq_fcl_cons = lazy(constant ["Setoid"] "fcl_cons")
 
@@ -448,6 +452,20 @@ let cic_relation_class_of_X_relation_class typ value =
       [| Lazy.force typ ; refl_a ; refl_aeq; sym ; refl_refl |])
   | ACLeibniz t -> mkApp ((Lazy.force coq_Leibniz), [| Lazy.force typ ; t |])
 
+let cic_reflexive_relation_class_of_relation_class =
+ function
+    ACReflexive
+     {refl_a=refl_a; refl_aeq=refl_aeq; refl_refl=refl_refl; refl_sym=None}
+    ->
+     mkApp ((Lazy.force coq_RAsymmetricReflexive),
+      [| refl_a ; refl_aeq; refl_refl |])
+  | ACReflexive
+     {refl_a=refl_a; refl_aeq=refl_aeq; refl_refl=refl_refl; refl_sym=Some sym}
+    ->
+     mkApp ((Lazy.force coq_RSymmetricReflexive),
+      [| refl_a ; refl_aeq; sym ; refl_refl |])
+  | ACLeibniz t -> mkApp ((Lazy.force coq_RLeibniz), [| t |])
+
 let cic_relation_class_of_relation_class =
  cic_relation_class_of_X_relation_class coq_unit coq_tt
 
@@ -594,12 +612,12 @@ let add_setoid a aeq th =
 
 type constr_with_marks =
   | MApp of constr * morphism_class * constr_with_marks array 
-  | Toreplace
-  | Tokeep of constr
+  | ToReplace
+  | ToKeep of constr
 
 let is_to_replace = function
- | Tokeep _ -> false
- | Toreplace -> true
+ | ToKeep _ -> false
+ | ToReplace -> true
  | MApp _ -> true
 
 let get_mark a = 
@@ -644,12 +662,12 @@ let relation_of_hypothesis_and_term_to_rewrite gl (_,h) t =
 let mark_occur t in_c =
  let rec aux in_c =
   if eq_constr t in_c then
-    Toreplace
+    ToReplace
   else
     match kind_of_term in_c with
       | App (c,al) -> 
           let a = Array.map aux al in
-           if not (get_mark a) then Tokeep in_c
+           if not (get_mark a) then ToKeep in_c
            else
             let mor =
               try
@@ -698,7 +716,7 @@ let mark_occur t in_c =
                           let env' = push_rel (name,None,s) env in
                           begin
                            match noccurn 1 t, he with
-                              _, Tokeep arg ->
+                              _, ToKeep arg ->
                                (* generic product, to keep *)
                                find_non_dependent_function
                                 env' c ((Toapply arg)::c_args_rev)
@@ -723,7 +741,7 @@ let mark_occur t in_c =
                    (Array.to_list a))
       | Prod (_, c1, c2) -> 
           if (dependent (mkRel 1) c2)
-          then Tokeep in_c
+          then ToKeep in_c
           else 
             let c1m = aux c1 in
             let c2m = aux c2 in
@@ -732,8 +750,8 @@ let mark_occur t in_c =
                (* this can be optimized since c1 and c2 will be *)
                (* processed again                               *)
                aux (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))
-              else Tokeep in_c
-      | _ -> Tokeep in_c
+              else ToKeep in_c
+      | _ -> ToKeep in_c
  in aux in_c
 
 let cic_morphism_context_list_of_list hole_relation =
@@ -775,7 +793,7 @@ let rec cic_type_nelist_of_list =
       [| mkType (Termops.new_univ ()); value; cic_type_nelist_of_list tl |])
 
 let syntactic_but_representation_of_marked_but hole_relation =
- let rec aux out =
+ let rec aux out reflexive_out =
   function
      MApp (f, m, args) ->
       let morphism_theory, relations =
@@ -794,25 +812,29 @@ let syntactic_but_representation_of_marked_but hole_relation =
            in
             mt,List.map (fun x -> ACLeibniz x) f_args in
       let cic_relations =
-       List.map cic_relation_class_of_relation_class relations in
+       List.map
+        (fun r ->
+          cic_relation_class_of_relation_class r,
+          cic_reflexive_relation_class_of_relation_class r
+        ) relations in
       let cic_arguments =
        List.map cic_argument_class_of_argument_class relations in
       let cic_args_relations,argst =
        cic_morphism_context_list_of_list hole_relation
         (List.combine cic_arguments
-          (List.map2 (fun t v -> aux t v) cic_relations
+          (List.map2 (fun (t,refl_t) v -> aux t refl_t v) cic_relations
            (Array.to_list args)))
       in
        mkApp ((Lazy.force coq_App),
         [|hole_relation ; Lazy.force coq_Left2Right ;
           cic_args_relations ; out ; Lazy.force coq_Left2Right ;
           morphism_theory ; argst|])
-   | Toreplace ->
-      mkApp ((Lazy.force coq_Toreplace),
+   | ToReplace ->
+      mkApp ((Lazy.force coq_ToReplace),
        [| hole_relation ; Lazy.force coq_Left2Right |])
-   | Tokeep c ->
-       mkApp ((Lazy.force coq_Tokeep),
-        [| hole_relation ; Lazy.force coq_Left2Right ; out ;
+   | ToKeep c ->
+       mkApp ((Lazy.force coq_ToKeep),
+        [| hole_relation ; Lazy.force coq_Left2Right ; reflexive_out ;
            Lazy.force coq_Left2Right ; c |])
  in aux
 
@@ -822,6 +844,9 @@ let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m =
   cic_relation_class_of_relation_class (ACReflexive hole_relation) in
  let prop_relation =
   cic_relation_class_of_relation_class (Lazy.force coq_prop_relation) in
+ let reflexive_prop_relation =
+  cic_reflexive_relation_class_of_relation_class
+   (Lazy.force coq_prop_relation) in
  let hyp =
   if lft2rgt then h else
    match hole_symmetry with
@@ -839,7 +864,7 @@ let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m =
    [| hole_relation ; Lazy.force coq_Left2Right ; prop_relation ;
       Lazy.force coq_Left2Right ; c1 ; c2 ;
       syntactic_but_representation_of_marked_but hole_relation
-       prop_relation m ; hyp |])
+       prop_relation reflexive_prop_relation m ; hyp |])
 
 let relation_rewrite c1 c2 (lft2rgt,cl) gl =
  let but = pf_concl gl in