helm/software/components/tactics/setoids.ml

   1 (************************************************************************)
   2 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
   3 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
   4 (*   \VV/  **************************************************************)
   5 (*    //   *      This file is distributed under the terms of the       *)
   6 (*         *       GNU Lesser General Public License Version 2.1        *)
   7 (************************************************************************)
   8
   9 (* $Id: setoid_replace.ml 8900 2006-06-06 14:40:27Z letouzey $ *)
  10
  11 let default_eq () =
  12  match LibraryObjects.eq_URI () with
  13     Some uri -> uri
  14   | None ->
  15     raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
  16
  17 let replace = ref (fun _ _ -> assert false)
  18 let register_replace f = replace := f
  19
  20 let general_rewrite = ref (fun _ _ -> assert false)
  21 let register_general_rewrite f = general_rewrite := f
  22
  23 let prlist_with_sepi sep elem =
  24  let rec aux n =
  25   function
  26    | []   -> ""
  27    | [h]  -> elem n h
  28    | h::t ->
  29       let e = elem n h and r = aux (n+1) t in
  30       e ^ sep ^ r
  31  in
  32   aux 1
  33
  34 type relation =
  35    { rel_a: Cic.term ;
  36      rel_aeq: Cic.term;
  37      rel_refl: Cic.term option;
  38      rel_sym: Cic.term option;
  39      rel_trans : Cic.term option;
  40      rel_quantifiers_no: int  (* it helps unification *);
  41      rel_X_relation_class: Cic.term;
  42      rel_Xreflexive_relation_class: Cic.term
  43    }
  44
  45 type 'a relation_class =
  46    Relation of 'a            (* the rel_aeq of the relation or the relation   *)
  47  | Leibniz of Cic.term option (* the carrier (if eq is partially instantiated)*)
  48
  49 type 'a morphism =
  50     { args : (bool option * 'a relation_class) list;
  51       output : 'a relation_class;
  52       lem : Cic.term;
  53       morphism_theory : Cic.term
  54     }
  55
  56 type funct =
  57     { f_args : Cic.term list;
  58       f_output : Cic.term
  59     }
  60
  61 type morphism_class =
  62    ACMorphism of relation morphism
  63  | ACFunction of funct
  64
  65 let constr_relation_class_of_relation_relation_class =
  66  function
  67     Relation relation -> Relation relation.rel_aeq
  68   | Leibniz t -> Leibniz t
  69
  70
  71 (*COQ
  72 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
  73 *)
  74
  75 (*COQ
  76 let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s
  77 *) let constant dir s = Cic.Implicit None
  78 (*COQ
  79 let gen_constant dir s = Coqlib.gen_constant "Setoid_replace" dir s
  80 *) let gen_constant dir s = Cic.Implicit None
  81 (*COQ
  82 let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s
  83 let eval_reference dir s = EvalConstRef (destConst (constant dir s))
  84 *) let eval_reference dir s = Cic.Implicit None
  85 (*COQ
  86 let eval_init_reference dir s = EvalConstRef (destConst (gen_constant ("Init"::dir) s))
  87 *)
  88
  89 (*COQ
  90 let current_constant id =
  91   try
  92     global_reference id
  93   with Not_found ->
  94     anomaly ("Setoid: cannot find " ^ id)
  95 *) let current_constant id = assert false
  96
  97 (* From Setoid.v *)
  98
  99 let coq_reflexive =
 100  (gen_constant ["Relations"; "Relation_Definitions"] "reflexive")
 101 let coq_symmetric =
 102  (gen_constant ["Relations"; "Relation_Definitions"] "symmetric")
 103 let coq_transitive =
 104  (gen_constant ["Relations"; "Relation_Definitions"] "transitive")
 105 let coq_relation =
 106  (gen_constant ["Relations"; "Relation_Definitions"] "relation")
 107
 108 let coq_Relation_Class = (constant ["Setoid"] "Relation_Class")
 109 let coq_Argument_Class = (constant ["Setoid"] "Argument_Class")
 110 let coq_Setoid_Theory = (constant ["Setoid"] "Setoid_Theory")
 111 let coq_Morphism_Theory = (constant ["Setoid"] "Morphism_Theory")
 112 let coq_Build_Morphism_Theory= (constant ["Setoid"] "Build_Morphism_Theory")
 113 let coq_Compat = (constant ["Setoid"] "Compat")
 114
 115 let coq_AsymmetricReflexive = (constant ["Setoid"] "AsymmetricReflexive")
 116 let coq_SymmetricReflexive = (constant ["Setoid"] "SymmetricReflexive")
 117 let coq_SymmetricAreflexive = (constant ["Setoid"] "SymmetricAreflexive")
 118 let coq_AsymmetricAreflexive = (constant ["Setoid"] "AsymmetricAreflexive")
 119 let coq_Leibniz = (constant ["Setoid"] "Leibniz")
 120
 121 let coq_RAsymmetric = (constant ["Setoid"] "RAsymmetric")
 122 let coq_RSymmetric = (constant ["Setoid"] "RSymmetric")
 123 let coq_RLeibniz = (constant ["Setoid"] "RLeibniz")
 124
 125 let coq_ASymmetric = (constant ["Setoid"] "ASymmetric")
 126 let coq_AAsymmetric = (constant ["Setoid"] "AAsymmetric")
 127
 128 let coq_seq_refl = (constant ["Setoid"] "Seq_refl")
 129 let coq_seq_sym = (constant ["Setoid"] "Seq_sym")
 130 let coq_seq_trans = (constant ["Setoid"] "Seq_trans")
 131
 132 let coq_variance = (constant ["Setoid"] "variance")
 133 let coq_Covariant = (constant ["Setoid"] "Covariant")
 134 let coq_Contravariant = (constant ["Setoid"] "Contravariant")
 135 let coq_Left2Right = (constant ["Setoid"] "Left2Right")
 136 let coq_Right2Left = (constant ["Setoid"] "Right2Left")
 137 let coq_MSNone = (constant ["Setoid"] "MSNone")
 138 let coq_MSCovariant = (constant ["Setoid"] "MSCovariant")
 139 let coq_MSContravariant = (constant ["Setoid"] "MSContravariant")
 140
 141 let coq_singl = (constant ["Setoid"] "singl")
 142 let coq_cons = (constant ["Setoid"] "cons")
 143
 144 let coq_equality_morphism_of_asymmetric_areflexive_transitive_relation =
 145  (constant ["Setoid"]
 146   "equality_morphism_of_asymmetric_areflexive_transitive_relation")
 147 let coq_equality_morphism_of_symmetric_areflexive_transitive_relation =
 148  (constant ["Setoid"]
 149   "equality_morphism_of_symmetric_areflexive_transitive_relation")
 150 let coq_equality_morphism_of_asymmetric_reflexive_transitive_relation =
 151  (constant ["Setoid"]
 152   "equality_morphism_of_asymmetric_reflexive_transitive_relation")
 153 let coq_equality_morphism_of_symmetric_reflexive_transitive_relation =
 154  (constant ["Setoid"]
 155   "equality_morphism_of_symmetric_reflexive_transitive_relation")
 156 let coq_make_compatibility_goal =
 157  (constant ["Setoid"] "make_compatibility_goal")
 158 let coq_make_compatibility_goal_eval_ref =
 159  (eval_reference ["Setoid"] "make_compatibility_goal")
 160 let coq_make_compatibility_goal_aux_eval_ref =
 161  (eval_reference ["Setoid"] "make_compatibility_goal_aux")
 162
 163 let coq_App = (constant ["Setoid"] "App")
 164 let coq_ToReplace = (constant ["Setoid"] "ToReplace")
 165 let coq_ToKeep = (constant ["Setoid"] "ToKeep")
 166 let coq_ProperElementToKeep = (constant ["Setoid"] "ProperElementToKeep")
 167 let coq_fcl_singl = (constant ["Setoid"] "fcl_singl")
 168 let coq_fcl_cons = (constant ["Setoid"] "fcl_cons")
 169
 170 let coq_setoid_rewrite = (constant ["Setoid"] "setoid_rewrite")
 171 let coq_proj1 = (gen_constant ["Init"; "Logic"] "proj1")
 172 let coq_proj2 = (gen_constant ["Init"; "Logic"] "proj2")
 173 let coq_unit = (gen_constant ["Init"; "Datatypes"] "unit")
 174 let coq_tt = (gen_constant ["Init"; "Datatypes"] "tt")
 175 let coq_eq = (gen_constant ["Init"; "Logic"] "eq")
 176
 177 let coq_morphism_theory_of_function =
 178  (constant ["Setoid"] "morphism_theory_of_function")
 179 let coq_morphism_theory_of_predicate =
 180  (constant ["Setoid"] "morphism_theory_of_predicate")
 181 let coq_relation_of_relation_class =
 182  (eval_reference ["Setoid"] "relation_of_relation_class")
 183 let coq_directed_relation_of_relation_class =
 184  (eval_reference ["Setoid"] "directed_relation_of_relation_class")
 185 let coq_interp = (eval_reference ["Setoid"] "interp")
 186 let coq_Morphism_Context_rect2 =
 187  (eval_reference ["Setoid"] "Morphism_Context_rect2")
 188 let coq_iff = (gen_constant ["Init";"Logic"] "iff")
 189 let coq_impl = (constant ["Setoid"] "impl")
 190
 191
 192 (************************* Table of declared relations **********************)
 193
 194
 195 (* Relations are stored in a table which is synchronised with the Reset mechanism. *)
 196
 197 module Gmap =
 198  Map.Make(struct type t = Cic.term let compare = Pervasives.compare end);;
 199
 200 let relation_table = ref Gmap.empty
 201
 202 let relation_table_add (s,th) = relation_table := Gmap.add s th !relation_table
 203 let relation_table_find s = Gmap.find s !relation_table
 204 let relation_table_mem s = Gmap.mem s !relation_table
 205
 206 let prrelation s =
 207   "(" ^ CicPp.ppterm s.rel_a ^ "," ^ CicPp.ppterm s.rel_aeq ^ ")"
 208
 209 let prrelation_class =
 210  function
 211     Relation eq  ->
 212      (try prrelation (relation_table_find eq)
 213       with Not_found ->
 214        "[[ Error: " ^ CicPp.ppterm eq ^
 215         " is not registered as a relation ]]")
 216   | Leibniz (Some ty) -> CicPp.ppterm ty
 217   | Leibniz None -> "_"
 218
 219 let prmorphism_argument_gen prrelation (variance,rel) =
 220  prrelation rel ^
 221   match variance with
 222      None -> " ==> "
 223    | Some true -> " ++> "
 224    | Some false -> " --> "
 225
 226 let prargument_class = prmorphism_argument_gen prrelation_class
 227
 228 let pr_morphism_signature (l,c) =
 229  String.concat "" (List.map (prmorphism_argument_gen CicPp.ppterm) l) ^
 230   CicPp.ppterm c
 231
 232 let prmorphism k m =
 233   CicPp.ppterm k ^ ": " ^
 234   String.concat "" (List.map prargument_class m.args) ^
 235   prrelation_class m.output
 236
 237 (* A function that gives back the only relation_class on a given carrier *)
 238 (*CSC: this implementation is really inefficient. I should define a new
 239   map to make it efficient. However, is this really worth of? *)
 240 let default_relation_for_carrier ?(filter=fun _ -> true) a =
 241  let rng =  Gmap.fold (fun _ y acc -> y::acc) !relation_table [] in
 242  match List.filter (fun ({rel_a=rel_a} as r) -> rel_a = a && filter r) rng with
 243     [] -> Leibniz (Some a)
 244   | relation::tl ->
 245 (*COQ
 246      if tl <> [] then
 247       prerr_endline
 248        ("Warning: There are several relations on the carrier \"" ^
 249          CicPp.ppterm a ^ "\". The relation " ^ prrelation relation ^
 250          " is chosen.") ;
 251 *)
 252      Relation relation
 253
 254 let find_relation_class rel =
 255  try Relation (relation_table_find rel)
 256  with
 257   Not_found ->
 258    let default_eq = default_eq () in
 259     match CicReduction.whd [] rel with
 260        Cic.Appl [Cic.MutInd(uri,0,[]);ty]
 261         when UriManager.eq uri default_eq -> Leibniz (Some ty)
 262      | Cic.MutInd(uri,0,[]) when UriManager.eq uri default_eq -> Leibniz None
 263      | _ -> raise Not_found
 264
 265 (*COQ
 266 let coq_iff_relation = lazy (find_relation_class (Lazy.force coq_iff))
 267 let coq_impl_relation = lazy (find_relation_class (Lazy.force coq_impl))
 268 *) let coq_iff_relation = Obj.magic 0 let coq_impl_relation = Obj.magic 0
 269
 270 let relation_morphism_of_constr_morphism =
 271  let relation_relation_class_of_constr_relation_class =
 272   function
 273      Leibniz t -> Leibniz t
 274    | Relation aeq ->
 275       Relation (try relation_table_find aeq with Not_found -> assert false)
 276  in
 277   function mor ->
 278    let args' =
 279     List.map
 280      (fun (variance,rel) ->
 281        variance, relation_relation_class_of_constr_relation_class rel
 282      ) mor.args in
 283    let output' = relation_relation_class_of_constr_relation_class mor.output in
 284     {mor with args=args' ; output=output'}
 285
 286 let equiv_list () =
 287  Gmap.fold (fun _ y acc -> y.rel_aeq::acc) !relation_table []
 288
 289 (* Declare a new type of object in the environment : "relation-theory". *)
 290
 291 let relation_to_obj (s, th) =
 292    let th' =
 293     if relation_table_mem s then
 294      begin
 295       let old_relation = relation_table_find s in
 296        let th' =
 297         {th with rel_sym =
 298           match th.rel_sym with
 299              None -> old_relation.rel_sym
 300            | Some t -> Some t}
 301        in
 302         prerr_endline
 303          ("Warning: The relation " ^ prrelation th' ^
 304           " is redeclared. The new declaration" ^
 305            (match th'.rel_refl with
 306               None -> ""
 307             | Some t -> " (reflevity proved by " ^ CicPp.ppterm t) ^
 308            (match th'.rel_sym with
 309                None -> ""
 310              | Some t ->
 311                 (if th'.rel_refl = None then " (" else " and ") ^
 312                 "symmetry proved by " ^ CicPp.ppterm t) ^
 313            (if th'.rel_refl <> None && th'.rel_sym <> None then
 314              ")" else "") ^
 315            " replaces the old declaration" ^
 316            (match old_relation.rel_refl with
 317               None -> ""
 318             | Some t -> " (reflevity proved by " ^ CicPp.ppterm t) ^
 319            (match old_relation.rel_sym with
 320                None -> ""
 321              | Some t ->
 322                 (if old_relation.rel_refl = None then
 323                   " (" else " and ") ^
 324                 "symmetry proved by " ^ CicPp.ppterm t) ^
 325            (if old_relation.rel_refl <> None && old_relation.rel_sym <> None
 326             then ")" else "") ^
 327            ".");
 328         th'
 329      end
 330     else
 331      th
 332    in
 333     relation_table_add (s,th')
 334
 335 (******************************* Table of declared morphisms ********************)
 336
 337 (* Setoids are stored in a table which is synchronised with the Reset mechanism. *)
 338
 339 let morphism_table = ref Gmap.empty
 340
 341 let morphism_table_find m = Gmap.find m !morphism_table
 342 let morphism_table_add (m,c) =
 343  let old =
 344   try
 345    morphism_table_find m
 346   with
 347    Not_found -> []
 348  in
 349   try
 350 (*COQ
 351    let old_morph =
 352     List.find
 353      (function mor -> mor.args = c.args && mor.output = c.output) old
 354    in
 355     prerr_endline
 356      ("Warning: The morphism " ^ prmorphism m old_morph ^
 357       " is redeclared. " ^
 358       "The new declaration whose compatibility is proved by " ^
 359        CicPp.ppterm c.lem ^ " replaces the old declaration whose" ^
 360        " compatibility was proved by " ^
 361        CicPp.ppterm old_morph.lem ^ ".")
 362 *) ()
 363   with
 364    Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table
 365
 366 let default_morphism ?(filter=fun _ -> true) m =
 367   match List.filter filter (morphism_table_find m) with
 368       [] -> raise Not_found
 369     | m1::ml ->
 370 (*COQ
 371         if ml <> [] then
 372           prerr_endline
 373             ("Warning: There are several morphisms associated to \"" ^
 374             CicPp.ppterm m ^ "\". Morphism " ^ prmorphism m m1 ^
 375             " is randomly chosen.");
 376 *)
 377         relation_morphism_of_constr_morphism m1
 378
 379 (************************** Printing relations and morphisms **********************)
 380
 381 let print_setoids () =
 382   Gmap.iter
 383    (fun k relation ->
 384      assert (k=relation.rel_aeq) ;
 385      prerr_endline ("Relation " ^ prrelation relation ^ ";" ^
 386       (match relation.rel_refl with
 387           None -> ""
 388         | Some t -> " reflexivity proved by " ^ CicPp.ppterm t) ^
 389       (match relation.rel_sym with
 390           None -> ""
 391         | Some t -> " symmetry proved by " ^ CicPp.ppterm t) ^
 392       (match relation.rel_trans with
 393           None -> ""
 394         | Some t -> " transitivity proved by " ^ CicPp.ppterm t)))
 395    !relation_table ;
 396   Gmap.iter
 397    (fun k l ->
 398      List.iter
 399       (fun ({lem=lem} as mor) ->
 400         prerr_endline ("Morphism " ^ prmorphism k mor ^
 401         ". Compatibility proved by " ^
 402         CicPp.ppterm lem ^ "."))
 403       l) !morphism_table
 404 ;;
 405
 406 (***************** Adding a morphism to the database ****************************)
 407
 408 (* We maintain a table of the currently edited proofs of morphism lemma
 409    in order to add them in the morphism_table when the user does Save *)
 410
 411 let edited = ref Gmap.empty
 412
 413 let new_edited id m =
 414   edited := Gmap.add id m !edited
 415
 416 let is_edited id =
 417   Gmap.mem id !edited
 418
 419 let no_more_edited id =
 420   edited := Gmap.remove id !edited
 421
 422 let what_edited id =
 423   Gmap.find id !edited
 424
 425 let list_chop n l =
 426   let rec chop_aux acc = function
 427     | (0, l2) -> (List.rev acc, l2)
 428     | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
 429     | (_, []) -> assert false
 430   in
 431   chop_aux [] (n,l)
 432
 433 let compose_thing f l b =
 434  let rec aux =
 435   function
 436      (0, env, b) -> b
 437    | (n, ((v,t)::l), b) -> aux (n-1,  l, f v t b)
 438    | _ -> assert false
 439  in
 440   aux (List.length l,l,b)
 441
 442 let compose_prod = compose_thing (fun v t b -> Cic.Prod (v,t,b))
 443 let compose_lambda = compose_thing (fun v t b -> Cic.Lambda (v,t,b))
 444
 445 (* also returns the triple (args_ty_quantifiers_rev,real_args_ty,real_output)
 446    where the args_ty and the output are delifted *)
 447 let check_is_dependent n args_ty output =
 448  let m = List.length args_ty - n in
 449  let args_ty_quantifiers, args_ty = list_chop n args_ty in
 450   let rec aux m t =
 451    match t with
 452       Cic.Prod (n,s,t) when m > 0 ->
 453        let t' = CicSubstitution.subst (Cic.Implicit None) (* dummy *) t in
 454        if t' <> t then
 455         let args,out = aux (m - 1) t' in s::args,out
 456        else
 457         raise (ProofEngineTypes.Fail (lazy
 458          "The morphism is not a quantified non dependent product."))
 459     | _ -> [],t
 460   in
 461    let ty = compose_prod (List.rev args_ty) output in
 462    let args_ty, output = aux m ty in
 463    List.rev args_ty_quantifiers, args_ty, output
 464
 465 let cic_relation_class_of_X_relation typ value =
 466  function
 467     {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} ->
 468      Cic.Appl [coq_AsymmetricReflexive ; typ ; value ; rel_a ; rel_aeq; refl]
 469   | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} ->
 470      Cic.Appl [coq_SymmetricReflexive ; typ ; rel_a ; rel_aeq; sym ; refl]
 471   | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} ->
 472      Cic.Appl [coq_AsymmetricAreflexive ; typ ; value ; rel_a ; rel_aeq]
 473   | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} ->
 474      Cic.Appl [coq_SymmetricAreflexive ; typ ; rel_a ; rel_aeq; sym]
 475
 476 let cic_relation_class_of_X_relation_class typ value =
 477  function
 478     Relation {rel_X_relation_class=x_relation_class} ->
 479      Cic.Appl [x_relation_class ; typ ; value]
 480   | Leibniz (Some t) ->
 481      Cic.Appl [coq_Leibniz ; typ ; t]
 482   | Leibniz None -> assert false
 483
 484
 485 let cic_precise_relation_class_of_relation =
 486  function
 487     {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=None} ->
 488       Cic.Appl [coq_RAsymmetric ; rel_a ; rel_aeq; refl]
 489   | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=Some refl; rel_sym=Some sym} ->
 490       Cic.Appl [coq_RSymmetric ; rel_a ; rel_aeq; sym ; refl]
 491   | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=None} ->
 492       Cic.Appl [coq_AAsymmetric ; rel_a ; rel_aeq]
 493   | {rel_a=rel_a; rel_aeq=rel_aeq; rel_refl=None; rel_sym=Some sym} ->
 494       Cic.Appl [coq_ASymmetric ; rel_a ; rel_aeq; sym]
 495
 496 let cic_precise_relation_class_of_relation_class =
 497  function
 498     Relation
 499      {rel_aeq=rel_aeq; rel_Xreflexive_relation_class=lem; rel_refl=rel_refl }
 500      ->
 501       rel_aeq,lem,not(rel_refl=None)
 502   | Leibniz (Some t) ->
 503      Cic.Appl [coq_eq ; t], Cic.Appl [coq_RLeibniz ; t], true
 504   | Leibniz None -> assert false
 505
 506 let cic_relation_class_of_relation_class rel =
 507  cic_relation_class_of_X_relation_class
 508   coq_unit coq_tt rel
 509
 510 let cic_argument_class_of_argument_class (variance,arg) =
 511  let coq_variant_value =
 512   match variance with
 513      None -> coq_Covariant (* dummy value, it won't be used *)
 514    | Some true -> coq_Covariant
 515    | Some false -> coq_Contravariant
 516  in
 517   cic_relation_class_of_X_relation_class coq_variance
 518    coq_variant_value arg
 519
 520 let cic_arguments_of_argument_class_list args =
 521  let rec aux =
 522   function
 523      [] -> assert false
 524    | [last] ->
 525       Cic.Appl [coq_singl ; coq_Argument_Class ; last]
 526    | he::tl ->
 527       Cic.Appl [coq_cons ; coq_Argument_Class ; he ; aux tl]
 528  in
 529   aux (List.map cic_argument_class_of_argument_class args)
 530
 531 let gen_compat_lemma_statement quantifiers_rev output args m =
 532  let output = cic_relation_class_of_relation_class output in
 533  let args = cic_arguments_of_argument_class_list args in
 534   args, output,
 535    compose_prod quantifiers_rev
 536     (Cic.Appl [coq_make_compatibility_goal ; args ; output ; m])
 537
 538 let morphism_theory_id_of_morphism_proof_id id =
 539  id ^ "_morphism_theory"
 540
 541 let list_map_i f =
 542   let rec map_i_rec i = function
 543     | [] -> []
 544     | x::l -> let v = f i x in v :: map_i_rec (i+1) l
 545   in
 546   map_i_rec
 547
 548 (* apply_to_rels c [l1 ; ... ; ln] returns (c Rel1 ... reln) *)
 549 let apply_to_rels c l =
 550  if l = [] then c
 551  else
 552   let len = List.length l in
 553    Cic.Appl (c::(list_map_i (fun i _ -> Cic.Rel (len - i)) 0 l))
 554
 555 let apply_to_relation subst rel =
 556  if subst = [] then rel
 557  else
 558   let new_quantifiers_no = rel.rel_quantifiers_no - List.length subst in
 559    assert (new_quantifiers_no >= 0) ;
 560    { rel_a = Cic.Appl (rel.rel_a :: subst) ;
 561      rel_aeq = Cic.Appl (rel.rel_aeq :: subst) ;
 562      rel_refl = HExtlib.map_option (fun c -> Cic.Appl (c::subst)) rel.rel_refl ;
 563      rel_sym = HExtlib.map_option (fun c -> Cic.Appl (c::subst)) rel.rel_sym;
 564      rel_trans = HExtlib.map_option (fun c -> Cic.Appl (c::subst)) rel.rel_trans;
 565      rel_quantifiers_no = new_quantifiers_no;
 566      rel_X_relation_class = Cic.Appl (rel.rel_X_relation_class::subst);
 567      rel_Xreflexive_relation_class =
 568       Cic.Appl (rel.rel_Xreflexive_relation_class::subst) }
 569
 570 let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
 571  let lem =
 572   match lemma_infos with
 573      None ->
 574       (* the Morphism_Theory object has already been created *)
 575       let applied_args =
 576        let len = List.length quantifiers_rev in
 577        let subst =
 578         list_map_i (fun i _ -> Cic.Rel (len - i)) 0 quantifiers_rev
 579        in
 580         List.map
 581          (fun (v,rel) ->
 582            match rel with
 583               Leibniz (Some t) ->
 584                assert (subst=[]);
 585                v, Leibniz (Some t)
 586             | Leibniz None ->
 587                (match subst with
 588                    [e] -> v, Leibniz (Some e)
 589                  | _ -> assert false)
 590             | Relation rel -> v, Relation (apply_to_relation subst rel)) args
 591       in
 592        compose_lambda quantifiers_rev
 593         (Cic.Appl
 594           [coq_Compat ;
 595            cic_arguments_of_argument_class_list applied_args;
 596            cic_relation_class_of_relation_class output;
 597            apply_to_rels (current_constant mor_name) quantifiers_rev])
 598    | Some (lem_name,argsconstr,outputconstr) ->
 599       (* only the compatibility has been proved; we need to declare the
 600          Morphism_Theory object *)
 601      let mext = current_constant lem_name in
 602 (*COQ
 603      ignore (
 604       Declare.declare_internal_constant mor_name
 605        (DefinitionEntry
 606          {const_entry_body =
 607            compose_lambda quantifiers_rev
 608             (Cic.Appl
 609               [coq_Build_Morphism_Theory;
 610                argsconstr; outputconstr; apply_to_rels m quantifiers_rev ;
 611                apply_to_rels mext quantifiers_rev]);
 612           const_entry_boxed = Options.boxed_definitions()},
 613         IsDefinition Definition)) ;
 614 *)ignore (assert false);
 615      mext
 616  in
 617   let mmor = current_constant mor_name in
 618   let args_constr =
 619    List.map
 620     (fun (variance,arg) ->
 621       variance, constr_relation_class_of_relation_relation_class arg) args in
 622   let output_constr = constr_relation_class_of_relation_relation_class output in
 623 (*COQ
 624    Lib.add_anonymous_leaf
 625     (morphism_to_obj (m,
 626       { args = args_constr;
 627         output = output_constr;
 628         lem = lem;
 629         morphism_theory = mmor }));
 630 *)let _ = mmor,args_constr,output_constr,lem in ignore (assert false);
 631    (*COQ Options.if_verbose prerr_endline (CicPp.ppterm m ^ " is registered as a morphism")   *) ()
 632
 633 let list_sub _ _ _ = assert false
 634
 635 (* first order matching with a bit of conversion *)
 636 let unify_relation_carrier_with_type env rel t =
 637  let raise_error quantifiers_no =
 638   raise (ProofEngineTypes.Fail (lazy
 639    ("One morphism argument or its output has type " ^ CicPp.ppterm t ^
 640     " but the signature requires an argument of type \"" ^
 641     CicPp.ppterm rel.rel_a ^ " " ^ String.concat " " (List.map (fun _ ->  "?")
 642      (Array.to_list (Array.make quantifiers_no 0))) ^ "\""))) in
 643  let args =
 644   match t with
 645      Cic.Appl (he'::args') ->
 646       let argsno = List.length args' - rel.rel_quantifiers_no in
 647       let args1 = list_sub args' 0 argsno in
 648       let args2 = list_sub args' argsno rel.rel_quantifiers_no in
 649        if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1))
 650        CicUniv.oblivion_ugraph) then
 651         args2
 652        else
 653         raise_error rel.rel_quantifiers_no
 654    | _  ->
 655      if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible []
 656      rel.rel_a t CicUniv.oblivion_ugraph) then
 657       []
 658      else
 659       begin
 660 (*COQ
 661         let evars,args,instantiated_rel_a =
 662          let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a
 663          CicUniv.oblivion_ugraph in
 664          let evd = Evd.create_evar_defs Evd.empty in
 665          let evars,args,concl =
 666           Clenv.clenv_environments_evars env evd
 667            (Some rel.rel_quantifiers_no) ty
 668          in
 669           evars, args,
 670           nf_betaiota
 671            (match args with [] -> rel.rel_a | _ -> applist (rel.rel_a,args))
 672         in
 673          let evars' =
 674           w_unify true (*??? or false? *) env Reduction.CONV (*??? or cumul? *)
 675            ~mod_delta:true (*??? or true? *) t instantiated_rel_a evars in
 676          let args' =
 677           List.map (Reductionops.nf_evar (Evd.evars_of evars')) args
 678          in
 679           args'
 680 *) assert false
 681       end
 682  in
 683   apply_to_relation args rel
 684
 685 let unify_relation_class_carrier_with_type env rel t =
 686  match rel with
 687     Leibniz (Some t') ->
 688      if fst (CicReduction.are_convertible [] t t' CicUniv.oblivion_ugraph) then
 689       rel
 690      else
 691       raise (ProofEngineTypes.Fail (lazy
 692        ("One morphism argument or its output has type " ^ CicPp.ppterm t ^
 693         " but the signature requires an argument of type " ^
 694         CicPp.ppterm t')))
 695   | Leibniz None -> Leibniz (Some t)
 696   | Relation rel -> Relation (unify_relation_carrier_with_type env rel t)
 697
 698 exception Impossible
 699
 700 (*COQ
 701 (* first order matching with a bit of conversion *)
 702 (* Note: the type checking operations performed by the function could  *)
 703 (* be done once and for all abstracting the morphism structure using   *)
 704 (* the quantifiers. Would the new structure be more suited than the    *)
 705 (* existent one for other tasks to? (e.g. pretty printing would expose *)
 706 (* much more information: is it ok or is it too much information?)     *)
 707 let unify_morphism_with_arguments gl (c,al)
 708      {args=args; output=output; lem=lem; morphism_theory=morphism_theory} t
 709 =
 710  let allen = List.length al in
 711  let argsno = List.length args in
 712  if allen < argsno then raise Impossible; (* partial application *)
 713  let quantifiers,al' = Util.list_chop (allen - argsno) al in
 714  let c' = Cic.Appl (c::quantifiers) in
 715  if dependent t c' then raise Impossible;
 716  (* these are pf_type_of we could avoid *)
 717  let al'_type = List.map (Tacmach.pf_type_of gl) al' in
 718  let args' =
 719    List.map2
 720      (fun (var,rel) ty ->
 721         var,unify_relation_class_carrier_with_type (pf_env gl) rel ty)
 722      args al'_type in
 723  (* this is another pf_type_of we could avoid *)
 724  let ty = Tacmach.pf_type_of gl (Cic.Appl (c::al)) in
 725  let output' = unify_relation_class_carrier_with_type (pf_env gl) output ty in
 726  let lem' = Cic.Appl (lem::quantifiers) in
 727  let morphism_theory' = Cic.Appl (morphism_theory::quantifiers) in
 728  ({args=args'; output=output'; lem=lem'; morphism_theory=morphism_theory'},
 729   c',al')
 730 *) let unify_morphism_with_arguments _ _ _ _ = assert false
 731
 732 let new_morphism m signature id hook =
 733 (*COQ
 734  if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
 735   raise (ProofEngineTypes.Fail (lazy (pr_id id ^ " already exists")))
 736  else
 737   let env = Global.env() in
 738   let typeofm = Typing.type_of env Evd.empty m in
 739   let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm in
 740   let argsrev, output =
 741    match signature with
 742       None -> decompose_prod typ
 743     | Some (_,output') ->
 744        (* the carrier of the relation output' can be a Prod ==>
 745           we must uncurry on the fly output.
 746           E.g: A -> B -> C vs        A -> (B -> C)
 747                 args   output     args     output
 748        *)
 749        let rel = find_relation_class output' in
 750        let rel_a,rel_quantifiers_no =
 751         match rel with
 752            Relation rel -> rel.rel_a, rel.rel_quantifiers_no
 753          | Leibniz (Some t) -> t, 0
 754          | Leibniz None -> assert false in
 755        let rel_a_n =
 756         clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in
 757        try
 758         let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in
 759         let argsrev,_ = decompose_prod output_rel_a_n in
 760         let n = List.length argsrev in
 761         let argsrev',_ = decompose_prod typ in
 762         let m = List.length argsrev' in
 763          decompose_prod_n (m - n) typ
 764        with UserError(_,_) ->
 765         (* decompose_lam_n failed. This may happen when rel_a is an axiom,
 766            a constructor, an inductive type, etc. *)
 767         decompose_prod typ
 768   in
 769   let args_ty = List.rev argsrev in
 770   let args_ty_len = List.length (args_ty) in
 771   let args_ty_quantifiers_rev,args,args_instance,output,output_instance =
 772    match signature with
 773       None ->
 774        if args_ty = [] then
 775         raise (ProofEngineTypes.Fail (lazy
 776          ("The term " ^ CicPp.ppterm m ^ " has type " ^
 777           CicPp.ppterm typeofm ^ " that is not a product."))) ;
 778        ignore (check_is_dependent 0 args_ty output) ;
 779        let args =
 780         List.map
 781          (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in
 782        let output = default_relation_for_carrier output in
 783         [],args,args,output,output
 784     | Some (args,output') ->
 785        assert (args <> []);
 786        let number_of_arguments = List.length args in
 787        let number_of_quantifiers = args_ty_len - number_of_arguments in
 788        if number_of_quantifiers < 0 then
 789         raise (ProofEngineTypes.Fail (lazy
 790          ("The morphism " ^ CicPp.ppterm m ^ " has type " ^
 791           CicPp.ppterm typeofm ^ " that attends at most " ^ int args_ty_len ^
 792           " arguments. The signature that you specified requires " ^
 793           int number_of_arguments ^ " arguments.")))
 794        else
 795         begin
 796          (* the real_args_ty returned are already delifted *)
 797          let args_ty_quantifiers_rev, real_args_ty, real_output =
 798           check_is_dependent number_of_quantifiers args_ty output in
 799          let quantifiers_rel_context =
 800           List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in
 801          let env = push_rel_context quantifiers_rel_context env in
 802          let find_relation_class t real_t =
 803           try
 804            let rel = find_relation_class t in
 805             rel, unify_relation_class_carrier_with_type env rel real_t
 806           with Not_found ->
 807            raise (ProofEngineTypes.Fail (lazy
 808             ("Not a valid signature: " ^ CicPp.ppterm t ^
 809              " is neither a registered relation nor the Leibniz " ^
 810              " equality.")))
 811          in
 812          let find_relation_class_v (variance,t) real_t =
 813           let relation,relation_instance = find_relation_class t real_t in
 814            match relation, variance with
 815               Leibniz _, None
 816             | Relation {rel_sym = Some _}, None
 817             | Relation {rel_sym = None}, Some _ ->
 818                (variance, relation), (variance, relation_instance)
 819             | Relation {rel_sym = None},None ->
 820                raise (ProofEngineTypes.Fail (lazy
 821                 ("You must specify the variance in each argument " ^
 822                  "whose relation is asymmetric.")))
 823             | Leibniz _, Some _
 824             | Relation {rel_sym = Some _}, Some _ ->
 825                raise (ProofEngineTypes.Fail (lazy
 826                 ("You cannot specify the variance of an argument " ^
 827                  "whose relation is symmetric.")))
 828          in
 829           let args, args_instance =
 830            List.split
 831             (List.map2 find_relation_class_v args real_args_ty) in
 832           let output,output_instance= find_relation_class output' real_output in
 833            args_ty_quantifiers_rev, args, args_instance, output, output_instance
 834         end
 835   in
 836    let argsconstr,outputconstr,lem =
 837     gen_compat_lemma_statement args_ty_quantifiers_rev output_instance
 838      args_instance (apply_to_rels m args_ty_quantifiers_rev) in
 839    (* "unfold make_compatibility_goal" *)
 840    let lem =
 841     Reductionops.clos_norm_flags
 842      (Closure.unfold_red (coq_make_compatibility_goal_eval_ref))
 843      env Evd.empty lem in
 844    (* "unfold make_compatibility_goal_aux" *)
 845    let lem =
 846     Reductionops.clos_norm_flags
 847      (Closure.unfold_red(coq_make_compatibility_goal_aux_eval_ref))
 848      env Evd.empty lem in
 849    (* "simpl" *)
 850    let lem = Tacred.nf env Evd.empty lem in
 851     if Lib.is_modtype () then
 852      begin
 853       ignore
 854        (Declare.declare_internal_constant id
 855         (ParameterEntry lem, IsAssumption Logical)) ;
 856       let mor_name = morphism_theory_id_of_morphism_proof_id id in
 857       let lemma_infos = Some (id,argsconstr,outputconstr) in
 858        add_morphism lemma_infos mor_name
 859         (m,args_ty_quantifiers_rev,args,output)
 860      end
 861     else
 862      begin
 863       new_edited id
 864        (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
 865       Pfedit.start_proof id (Global, Proof Lemma)
 866        (Declare.clear_proofs (Global.named_context ()))
 867        lem hook;
 868       Options.if_verbose msg (Printer.pr_open_subgoals ());
 869      end
 870 *) assert false
 871
 872 let morphism_hook _ ref =
 873 (*COQ
 874   let pf_id = id_of_global ref in
 875   let mor_id = morphism_theory_id_of_morphism_proof_id pf_id in
 876   let (m,quantifiers_rev,args,argsconstr,output,outputconstr) =
 877    what_edited pf_id in
 878   if (is_edited pf_id)
 879   then
 880    begin
 881     add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id
 882      (m,quantifiers_rev,args,output) ;
 883     no_more_edited pf_id
 884    end
 885 *) assert false
 886
 887 type morphism_signature =
 888  (bool option * Cic.term) list * Cic.term
 889
 890 let new_named_morphism id m sign =
 891  new_morphism m sign id morphism_hook
 892
 893 (************************** Adding a relation to the database *********************)
 894
 895 let check_a a =
 896 (*COQ
 897  let typ = Typing.type_of env Evd.empty a in
 898  let a_quantifiers_rev,_ = Reduction.dest_arity env typ in
 899   a_quantifiers_rev
 900 *) assert false
 901
 902 let check_eq a_quantifiers_rev a aeq =
 903 (*COQ
 904  let typ =
 905   Sign.it_mkProd_or_LetIn
 906    (Cic.Appl [coq_relation ; apply_to_rels a a_quantifiers_rev])
 907    a_quantifiers_rev in
 908  if
 909   not
 910    (is_conv env Evd.empty (Typing.type_of env Evd.empty aeq) typ)
 911  then
 912   raise (ProofEngineTypes.Fail (lazy
 913    (CicPp.ppterm aeq ^ " should have type (" ^ CicPp.ppterm typ ^ ")")))
 914 *) (assert false : unit)
 915
 916 let check_property a_quantifiers_rev a aeq strprop coq_prop t =
 917 (*COQ
 918  if
 919   not
 920    (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
 921     (Sign.it_mkProd_or_LetIn
 922      (Cic.Appl
 923        [coq_prop ;
 924         apply_to_rels a a_quantifiers_rev ;
 925         apply_to_rels aeq a_quantifiers_rev]) a_quantifiers_rev))
 926  then
 927   raise (ProofEngineTypes.Fail (lazy
 928    ("Not a valid proof of " ^ strprop ^ ".")))
 929 *) assert false
 930
 931 let check_refl a_quantifiers_rev a aeq refl =
 932  check_property a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl
 933
 934 let check_sym a_quantifiers_rev a aeq sym =
 935  check_property a_quantifiers_rev a aeq "symmetry" coq_symmetric sym
 936
 937 let check_trans a_quantifiers_rev a aeq trans =
 938  check_property a_quantifiers_rev a aeq "transitivity" coq_transitive trans
 939 ;;
 940
 941 let int_add_relation id a aeq refl sym trans =
 942 (*COQ
 943  let env = Global.env () in
 944 *)
 945  let a_quantifiers_rev = check_a a in
 946   check_eq a_quantifiers_rev a aeq  ;
 947   HExtlib.iter_option (check_refl a_quantifiers_rev a aeq) refl ;
 948   HExtlib.iter_option (check_sym a_quantifiers_rev a aeq) sym ;
 949   HExtlib.iter_option (check_trans a_quantifiers_rev a aeq) trans ;
 950   let quantifiers_no = List.length a_quantifiers_rev in
 951   let aeq_rel =
 952    { rel_a = a;
 953      rel_aeq = aeq;
 954      rel_refl = refl;
 955      rel_sym = sym;
 956      rel_trans = trans;
 957      rel_quantifiers_no = quantifiers_no;
 958      rel_X_relation_class = Cic.Sort Cic.Prop; (* dummy value, overwritten below *)
 959      rel_Xreflexive_relation_class = Cic.Sort Cic.Prop (* dummy value, overwritten below *)
 960    } in
 961   let x_relation_class =
 962    let subst =
 963     let len = List.length a_quantifiers_rev in
 964      list_map_i (fun i _ -> Cic.Rel (len - i + 2)) 0 a_quantifiers_rev in
 965    cic_relation_class_of_X_relation
 966     (Cic.Rel 2) (Cic.Rel 1) (apply_to_relation subst aeq_rel) in
 967   let _ =
 968 (*COQ
 969    Declare.declare_internal_constant id
 970     (DefinitionEntry
 971       {const_entry_body =
 972         Sign.it_mkLambda_or_LetIn x_relation_class
 973          ([ Name "v",None,Cic.Rel 1;
 974             Name "X",None,Cic.Sort (Cic.Type (CicUniv.fresh ()))] @
 975             a_quantifiers_rev);
 976        const_entry_type = None;
 977        const_entry_opaque = false;
 978        const_entry_boxed = Options.boxed_definitions()},
 979       IsDefinition Definition) in
 980 *) () in
 981   let id_precise = id ^ "_precise_relation_class" in
 982   let xreflexive_relation_class =
 983    let subst =
 984     let len = List.length a_quantifiers_rev in
 985      list_map_i (fun i _ -> Cic.Rel (len - i)) 0 a_quantifiers_rev
 986    in
 987     cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in
 988   let _ =
 989 (*COQ
 990    Declare.declare_internal_constant id_precise
 991     (DefinitionEntry
 992       {const_entry_body =
 993         Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev;
 994        const_entry_type = None;
 995        const_entry_opaque = false;
 996        const_entry_boxed = Options.boxed_definitions() },
 997       IsDefinition Definition) in
 998 *) () in
 999   let aeq_rel =
1000    { aeq_rel with
1001       rel_X_relation_class = current_constant id;
1002       rel_Xreflexive_relation_class = current_constant id_precise } in
1003   relation_to_obj (aeq, aeq_rel) ;
1004   prerr_endline (CicPp.ppterm aeq ^ " is registered as a relation");
1005   match trans with
1006      None -> ()
1007    | Some trans ->
1008       let mor_name = id ^ "_morphism" in
1009       let a_instance = apply_to_rels a a_quantifiers_rev in
1010       let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
1011       let sym_instance =
1012        HExtlib.map_option (fun x -> apply_to_rels x a_quantifiers_rev) sym in
1013       let refl_instance =
1014        HExtlib.map_option (fun x -> apply_to_rels x a_quantifiers_rev) refl in
1015       let trans_instance = apply_to_rels trans a_quantifiers_rev in
1016       let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output =
1017        match sym_instance, refl_instance with
1018           None, None ->
1019            (Some false, Relation aeq_rel),
1020            (Some true, Relation aeq_rel),
1021             Cic.Appl
1022              [coq_equality_morphism_of_asymmetric_areflexive_transitive_relation;
1023               a_instance ; aeq_instance ; trans_instance],
1024             coq_impl_relation
1025         | None, Some refl_instance ->
1026            (Some false, Relation aeq_rel),
1027            (Some true, Relation aeq_rel),
1028             Cic.Appl
1029              [coq_equality_morphism_of_asymmetric_reflexive_transitive_relation;
1030               a_instance ; aeq_instance ; refl_instance ; trans_instance],
1031             coq_impl_relation
1032         | Some sym_instance, None ->
1033            (None, Relation aeq_rel),
1034            (None, Relation aeq_rel),
1035             Cic.Appl
1036              [coq_equality_morphism_of_symmetric_areflexive_transitive_relation;
1037               a_instance ; aeq_instance ; sym_instance ; trans_instance],
1038             coq_iff_relation
1039         | Some sym_instance, Some refl_instance ->
1040            (None, Relation aeq_rel),
1041            (None, Relation aeq_rel),
1042             Cic.Appl
1043              [coq_equality_morphism_of_symmetric_reflexive_transitive_relation;
1044               a_instance ; aeq_instance ; refl_instance ; sym_instance ;
1045               trans_instance],
1046             coq_iff_relation in
1047       let _ =
1048 (*COQ
1049        Declare.declare_internal_constant mor_name
1050         (DefinitionEntry
1051           {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev;
1052            const_entry_type = None;
1053            const_entry_opaque = false;
1054           const_entry_boxed = Options.boxed_definitions()},
1055           IsDefinition Definition)
1056 *) ()
1057       in
1058        let a_quantifiers_rev =
1059         List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in
1060        add_morphism None mor_name
1061         (aeq,a_quantifiers_rev,[aeq_rel_class_and_var1; aeq_rel_class_and_var2],
1062           output)
1063
1064 (* The vernac command "Add Relation ..." *)
1065 let add_relation id a aeq refl sym trans =
1066  int_add_relation id a aeq refl sym trans
1067
1068 (****************************** The tactic itself *******************************)
1069
1070 type direction =
1071    Left2Right
1072  | Right2Left
1073
1074 let prdirection =
1075  function
1076     Left2Right -> "->"
1077   | Right2Left -> "<-"
1078
1079 type constr_with_marks =
1080   | MApp of Cic.term * morphism_class * constr_with_marks list * direction
1081   | ToReplace
1082   | ToKeep of Cic.term * relation relation_class * direction
1083
1084 let is_to_replace = function
1085  | ToKeep _ -> false
1086  | ToReplace -> true
1087  | MApp _ -> true
1088
1089 let get_mark a =
1090   List.fold_left (||) false (List.map is_to_replace a)
1091
1092 let cic_direction_of_direction =
1093  function
1094     Left2Right -> coq_Left2Right
1095   | Right2Left -> coq_Right2Left
1096
1097 let opposite_direction =
1098  function
1099     Left2Right -> Right2Left
1100   | Right2Left -> Left2Right
1101
1102 let direction_of_constr_with_marks hole_direction =
1103  function
1104     MApp (_,_,_,dir) -> cic_direction_of_direction dir
1105   | ToReplace -> hole_direction
1106   | ToKeep (_,_,dir) -> cic_direction_of_direction dir
1107
1108 type argument =
1109    Toapply of Cic.term         (* apply the function to the argument *)
1110  | Toexpand of Cic.name * Cic.term  (* beta-expand the function w.r.t. an argument
1111                                 of this type *)
1112 let beta_expand c args_rev =
1113  let rec to_expand =
1114   function
1115      [] -> []
1116    | (Toapply _)::tl -> to_expand tl
1117    | (Toexpand (name,s))::tl -> (name,s)::(to_expand tl) in
1118  let rec aux n =
1119   function
1120      [] -> []
1121    | (Toapply arg)::tl -> arg::(aux n tl)
1122    | (Toexpand _)::tl -> (Cic.Rel n)::(aux (n + 1) tl)
1123  in
1124   compose_lambda (to_expand args_rev)
1125    (Cic.Appl (c :: List.rev (aux 1 args_rev)))
1126
1127 exception Optimize (* used to fall-back on the tactic for Leibniz equality *)
1128
1129 let rec list_sep_last = function
1130   | [] -> assert false
1131   | hd::[] -> (hd,[])
1132   | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
1133
1134 let relation_class_that_matches_a_constr caller_name new_goals hypt =
1135  let heq, hargs =
1136   match hypt with
1137      Cic.Appl (heq::hargs) -> heq,hargs
1138    | _ -> hypt,[]
1139  in
1140  let rec get_all_but_last_two =
1141   function
1142      []
1143    | [_] ->
1144       raise (ProofEngineTypes.Fail (lazy (CicPp.ppterm hypt ^
1145        " is not a registered relation.")))
1146    | [_;_] -> []
1147    | he::tl -> he::(get_all_but_last_two tl) in
1148  let all_aeq_args = get_all_but_last_two hargs in
1149  let rec find_relation l subst =
1150   let aeq = Cic.Appl (heq::l) in
1151   try
1152    let rel = find_relation_class aeq in
1153    match rel,new_goals with
1154       Leibniz _,[] ->
1155        assert (subst = []);
1156        raise Optimize (* let's optimize the proof term size *)
1157     | Leibniz (Some _), _ ->
1158        assert (subst = []);
1159        rel
1160     | Leibniz None, _ ->
1161        (* for well-typedness reasons it should have been catched by the
1162           previous guard in the previous iteration. *)
1163        assert false
1164     | Relation rel,_ -> Relation (apply_to_relation subst rel)
1165   with Not_found ->
1166    if l = [] then
1167     raise (ProofEngineTypes.Fail (lazy
1168      (CicPp.ppterm (Cic.Appl (aeq::all_aeq_args)) ^
1169       " is not a registered relation.")))
1170    else
1171     let last,others = list_sep_last l in
1172     find_relation others (last::subst)
1173  in
1174   find_relation all_aeq_args []
1175
1176 (* rel1 is a subrelation of rel2 whenever
1177     forall x1 x2, rel1 x1 x2 -> rel2 x1 x2
1178    The Coq part of the tactic, however, needs rel1 == rel2.
1179    Hence the third case commented out.
1180    Note: accepting user-defined subtrelations seems to be the last
1181    useful generalization that does not go against the original spirit of
1182    the tactic.
1183 *)
1184 let subrelation gl rel1 rel2 =
1185  match rel1,rel2 with
1186     Relation {rel_aeq=rel_aeq1}, Relation {rel_aeq=rel_aeq2} ->
1187      (*COQ Tacmach.pf_conv_x gl rel_aeq1 rel_aeq2*) assert false
1188   | Leibniz (Some t1), Leibniz (Some t2) ->
1189      (*COQ Tacmach.pf_conv_x gl t1 t2*) assert false
1190   | Leibniz None, _
1191   | _, Leibniz None -> assert false
1192 (* This is the commented out case (see comment above)
1193   | Leibniz (Some t1), Relation {rel_a=t2; rel_refl = Some _} ->
1194      Tacmach.pf_conv_x gl t1 t2
1195 *)
1196   | _,_ -> false
1197
1198 (* this function returns the list of new goals opened by a constr_with_marks *)
1199 let rec collect_new_goals =
1200  function
1201    MApp (_,_,a,_) -> List.concat (List.map collect_new_goals a)
1202  | ToReplace
1203  | ToKeep (_,Leibniz _,_)
1204  | ToKeep (_,Relation {rel_refl=Some _},_) -> []
1205  | ToKeep (c,Relation {rel_aeq=aeq; rel_refl=None},_) -> [Cic.Appl[aeq;c;c]]
1206
1207 (* two marked_constr are equivalent if they produce the same set of new goals *)
1208 let marked_constr_equiv_or_more_complex to_marked_constr gl c1 c2 =
1209   let glc1 = collect_new_goals (to_marked_constr c1) in
1210   let glc2 = collect_new_goals (to_marked_constr c2) in
1211    List.for_all (fun c -> List.exists (fun c' -> (*COQ pf_conv_x gl c c'*) assert false) glc1) glc2
1212
1213 let pr_new_goals i c =
1214  let glc = collect_new_goals c in
1215   " " ^ string_of_int i ^ ") side conditions:" ^
1216    (if glc = [] then " no side conditions"
1217     else
1218      ("\n   " ^
1219        String.concat "\n   "
1220         (List.map (fun c -> " ... |- " ^ CicPp.ppterm c) glc)))
1221
1222 (* given a list of constr_with_marks, it returns the list where
1223    constr_with_marks than open more goals than simpler ones in the list
1224    are got rid of *)
1225 let elim_duplicates gl to_marked_constr =
1226  let rec aux =
1227   function
1228      [] -> []
1229    | he:: tl ->
1230       if List.exists
1231           (marked_constr_equiv_or_more_complex to_marked_constr gl he) tl
1232       then aux tl
1233       else he::aux tl
1234  in
1235   aux
1236
1237 let filter_superset_of_new_goals gl new_goals l =
1238  List.filter
1239   (fun (_,_,c) ->
1240     List.for_all
1241      (fun g -> List.exists ((*COQ pf_conv_x gl g*)assert false) (collect_new_goals c)) new_goals) l
1242
1243 (* given the list of lists [ l1 ; ... ; ln ] it returns the list of lists
1244    [ c1 ; ... ; cn ] that is the cartesian product of the sets l1, ..., ln *)
1245 let cartesian_product gl a =
1246  let rec aux =
1247   function
1248      [] -> assert false
1249    | [he] -> List.map (fun e -> [e]) he
1250    | he::tl ->
1251       let tl' = aux tl in
1252        List.flatten
1253         (List.map (function e -> List.map (function l -> e :: l) tl') he)
1254  in
1255   aux (List.map (elim_duplicates gl (fun x -> x)) a)
1256
1257 let does_not_occur n t = assert false
1258
1259 let mark_occur gl ~new_goals t in_c input_relation input_direction =
1260  let rec aux output_relation output_direction in_c =
1261   if t = in_c then
1262    if input_direction = output_direction
1263    && subrelation gl input_relation output_relation then
1264     [ToReplace]
1265    else []
1266   else
1267     match in_c with
1268       | Cic.Appl (c::al) ->
1269          let mors_and_cs_and_als =
1270           let mors_and_cs_and_als =
1271            let morphism_table_find c =
1272             try morphism_table_find c with Not_found -> [] in
1273            let rec aux acc =
1274             function
1275                [] ->
1276                 let c' = Cic.Appl (c::acc) in
1277                 let al' = [] in
1278                 List.map (fun m -> m,c',al') (morphism_table_find c')
1279              | (he::tl) as l ->
1280                 let c' = Cic.Appl (c::acc) in
1281                 let acc' = acc @ [he] in
1282                  (List.map (fun m -> m,c',l) (morphism_table_find c')) @
1283                   (aux acc' tl)
1284            in
1285             aux [] al in
1286           let mors_and_cs_and_als =
1287            List.map
1288             (function (m,c,al) ->
1289               relation_morphism_of_constr_morphism m, c, al)
1290              mors_and_cs_and_als in
1291           let mors_and_cs_and_als =
1292            List.fold_left
1293             (fun l (m,c,al) ->
1294                try (unify_morphism_with_arguments gl (c,al) m t) :: l
1295                with Impossible -> l
1296             ) [] mors_and_cs_and_als
1297           in
1298            List.filter
1299             (fun (mor,_,_) -> subrelation gl mor.output output_relation)
1300             mors_and_cs_and_als
1301          in
1302           (* First we look for well typed morphisms *)
1303           let res_mors =
1304            List.fold_left
1305             (fun res (mor,c,al) ->
1306               let a =
1307                let arguments = mor.args in
1308                let apply_variance_to_direction default_dir =
1309                 function
1310                    None -> default_dir
1311                  | Some true -> output_direction
1312                  | Some false -> opposite_direction output_direction
1313                in
1314                 List.map2
1315                  (fun a (variance,relation) ->
1316                    (aux relation
1317                      (apply_variance_to_direction Left2Right variance) a) @
1318                    (aux relation
1319                      (apply_variance_to_direction Right2Left variance) a)
1320                  ) al arguments
1321               in
1322                let a' = cartesian_product gl a in
1323                 (List.map
1324                   (function a ->
1325                     if not (get_mark a) then
1326                      ToKeep (in_c,output_relation,output_direction)
1327                     else
1328                      MApp (c,ACMorphism mor,a,output_direction)) a') @ res
1329             ) [] mors_and_cs_and_als in
1330           (* Then we look for well typed functions *)
1331           let res_functions =
1332            (* the tactic works only if the function type is
1333                made of non-dependent products only. However, here we
1334                can cheat a bit by partially istantiating c to match
1335                the requirement when the arguments to be replaced are
1336                bound by non-dependent products only. *)
1337             let typeofc = (*COQ Tacmach.pf_type_of gl c*) assert false in
1338             let typ = (*COQ nf_betaiota typeofc*) let _ = typeofc in assert false in
1339             let rec find_non_dependent_function context c c_args_rev typ
1340              f_args_rev a_rev
1341             =
1342              function
1343                 [] ->
1344                  if a_rev = [] then
1345                   [ToKeep (in_c,output_relation,output_direction)]
1346                  else
1347                   let a' =
1348                    cartesian_product gl (List.rev a_rev)
1349                   in
1350                    List.fold_left
1351                     (fun res a ->
1352                       if not (get_mark a) then
1353                        (ToKeep (in_c,output_relation,output_direction))::res
1354                       else
1355                        let err =
1356                         match output_relation with
1357                            Leibniz (Some typ') when (*COQ pf_conv_x gl typ typ'*) assert false ->
1358                             false
1359                          | Leibniz None -> assert false
1360                          | _ when output_relation = coq_iff_relation
1361                              -> false
1362                          | _ -> true
1363                        in
1364                         if err then res
1365                         else
1366                          let mor =
1367                           ACFunction{f_args=List.rev f_args_rev;f_output=typ} in
1368                          let func = beta_expand c c_args_rev in
1369                           (MApp (func,mor,a,output_direction))::res
1370                     ) [] a'
1371               | (he::tl) as a->
1372                  let typnf = (*COQ Reduction.whd_betadeltaiota env typ*) assert false in
1373                   match typnf with
1374                     Cic.Cast (typ,_) ->
1375                      find_non_dependent_function context c c_args_rev typ
1376                       f_args_rev a_rev a
1377                   | Cic.Prod (name,s,t) ->
1378                      let context' = Some (name, Cic.Decl s)::context in
1379                      let he =
1380                       (aux (Leibniz (Some s)) Left2Right he) @
1381                       (aux (Leibniz (Some s)) Right2Left he) in
1382                      if he = [] then []
1383                      else
1384                       let he0 = List.hd he in
1385                       begin
1386                        match does_not_occur 1 t, he0 with
1387                           _, ToKeep (arg,_,_) ->
1388                            (* invariant: if he0 = ToKeep (t,_,_) then every
1389                               element in he is = ToKeep (t,_,_) *)
1390                            assert
1391                             (List.for_all
1392                               (function
1393                                   ToKeep(arg',_,_) when (*COQpf_conv_x gl arg arg'*) assert false ->
1394                                     true
1395                                 | _ -> false) he) ;
1396                            (* generic product, to keep *)
1397                            find_non_dependent_function
1398                             context' c ((Toapply arg)::c_args_rev)
1399                             (CicSubstitution.subst arg t) f_args_rev a_rev tl
1400                         | true, _ ->
1401                            (* non-dependent product, to replace *)
1402                            find_non_dependent_function
1403                             context' c ((Toexpand (name,s))::c_args_rev)
1404                              (CicSubstitution.lift 1 t) (s::f_args_rev) (he::a_rev) tl
1405                         | false, _ ->
1406                            (* dependent product, to replace *)
1407                            (* This limitation is due to the reflexive
1408                              implementation and it is hard to lift *)
1409                            raise (ProofEngineTypes.Fail (lazy
1410                             ("Cannot rewrite in the argument of a " ^
1411                              "dependent product. If you need this " ^
1412                              "feature, please report to the author.")))
1413                       end
1414                   | _ -> assert false
1415             in
1416              find_non_dependent_function (*COQ (Tacmach.pf_env gl) ci vuole il contesto*)(assert false) c [] typ [] []
1417               al
1418           in
1419            elim_duplicates gl (fun x -> x) (res_functions @ res_mors)
1420       | Cic.Prod (_, c1, c2) ->
1421           if (*COQ (dependent (Cic.Rel 1) c2)*) assert false
1422           then
1423            raise (ProofEngineTypes.Fail (lazy
1424             ("Cannot rewrite in the type of a variable bound " ^
1425              "in a dependent product.")))
1426           else
1427            let typeofc1 = (*COQ Tacmach.pf_type_of gl c1*) assert false in
1428             if not (*COQ (Tacmach.pf_conv_x gl typeofc1 (Cic.Sort Cic.Prop))*) (assert false) then
1429              (* to avoid this error we should introduce an impl relation
1430                 whose first argument is Type instead of Prop. However,
1431                 the type of the new impl would be Type -> Prop -> Prop
1432                 that is no longer a Relation_Definitions.relation. Thus
1433                 the Coq part of the tactic should be heavily modified. *)
1434              raise (ProofEngineTypes.Fail (lazy
1435               ("Rewriting in a product A -> B is possible only when A " ^
1436                "is a proposition (i.e. A is of type Prop). The type " ^
1437                CicPp.ppterm c1 ^ " has type " ^ CicPp.ppterm typeofc1 ^
1438                " that is not convertible to Prop.")))
1439             else
1440              aux output_relation output_direction
1441               (Cic.Appl [coq_impl; c1 ; CicSubstitution.subst (Cic.Rel 1 (*dummy*)) c2])
1442       | _ ->
1443         if (*COQ occur_term t in_c*) assert false then
1444          raise (ProofEngineTypes.Fail (lazy
1445           ("Trying to replace " ^ CicPp.ppterm t ^ " in " ^ CicPp.ppterm in_c ^
1446            " that is not an applicative context.")))
1447         else
1448          [ToKeep (in_c,output_relation,output_direction)]
1449  in
1450   let aux2 output_relation output_direction =
1451    List.map
1452     (fun res -> output_relation,output_direction,res)
1453      (aux output_relation output_direction in_c) in
1454   let res =
1455    (aux2 coq_iff_relation Right2Left) @
1456    (* This is the case of a proposition of signature A ++> iff or B --> iff *)
1457    (aux2 coq_iff_relation Left2Right) @
1458    (aux2 coq_impl_relation Right2Left) in
1459   let res = elim_duplicates gl (function (_,_,t) -> t) res in
1460   let res' = filter_superset_of_new_goals gl new_goals res in
1461   match res' with
1462      [] when res = [] ->
1463       raise (ProofEngineTypes.Fail (lazy
1464        ("Either the term " ^ CicPp.ppterm t ^ " that must be " ^
1465         "rewritten occurs in a covariant position or the goal is not " ^
1466         "made of morphism applications only. You can replace only " ^
1467         "occurrences that are in a contravariant position and such that " ^
1468         "the context obtained by abstracting them is made of morphism " ^
1469         "applications only.")))
1470    | [] ->
1471       raise (ProofEngineTypes.Fail (lazy
1472        ("No generated set of side conditions is a superset of those " ^
1473         "requested by the user. The generated sets of side conditions " ^
1474         "are:\n" ^
1475          prlist_with_sepi "\n"
1476           (fun i (_,_,mc) -> pr_new_goals i mc) res)))
1477    | [he] -> he
1478    | he::_ ->
1479       prerr_endline
1480        ("Warning: The application of the tactic is subject to one of " ^
1481         "the \nfollowing set of side conditions that the user needs " ^
1482         "to prove:\n" ^
1483          prlist_with_sepi "\n"
1484           (fun i (_,_,mc) -> pr_new_goals i mc) res' ^
1485          "\nThe first set is randomly chosen. Use the syntax " ^
1486          "\"setoid_rewrite ... generate side conditions ...\" to choose " ^
1487          "a different set.") ;
1488       he
1489
1490 let cic_morphism_context_list_of_list hole_relation hole_direction out_direction
1491 =
1492  let check =
1493   function
1494      (None,dir,dir') ->
1495       Cic.Appl [coq_MSNone ; dir ; dir']
1496    | (Some true,dir,dir') ->
1497       assert (dir = dir');
1498       Cic.Appl [coq_MSCovariant ; dir]
1499    | (Some false,dir,dir') ->
1500       assert (dir <> dir');
1501       Cic.Appl [coq_MSContravariant ; dir] in
1502  let rec aux =
1503   function
1504      [] -> assert false
1505    | [(variance,out),(value,direction)] ->
1506       Cic.Appl [coq_singl ; coq_Argument_Class ; out],
1507       Cic.Appl
1508        [coq_fcl_singl;
1509         hole_relation; hole_direction ; out ;
1510         direction ; out_direction ;
1511         check (variance,direction,out_direction) ; value]
1512    | ((variance,out),(value,direction))::tl ->
1513       let outtl, valuetl = aux tl in
1514        Cic.Appl
1515         [coq_cons; coq_Argument_Class ; out ; outtl],
1516        Cic.Appl
1517         [coq_fcl_cons;
1518          hole_relation ; hole_direction ; out ; outtl ;
1519          direction ; out_direction ;
1520          check (variance,direction,out_direction) ;
1521          value ; valuetl]
1522  in aux
1523
1524 let rec cic_type_nelist_of_list =
1525  function
1526     [] -> assert false
1527   | [value] ->
1528       Cic.Appl [coq_singl; Cic.Sort (Cic.Type (CicUniv.fresh ())) ; value]
1529   | value::tl ->
1530      Cic.Appl
1531       [coq_cons; Cic.Sort (Cic.Type (CicUniv.fresh ())); value;
1532        cic_type_nelist_of_list tl]
1533
1534 let syntactic_but_representation_of_marked_but hole_relation hole_direction =
1535  let rec aux out (rel_out,precise_out,is_reflexive) =
1536   function
1537      MApp (f, m, args, direction) ->
1538       let direction = cic_direction_of_direction direction in
1539       let morphism_theory, relations =
1540        match m with
1541           ACMorphism { args = args ; morphism_theory = morphism_theory } ->
1542            morphism_theory,args
1543         | ACFunction { f_args = f_args ; f_output = f_output } ->
1544            let mt =
1545             if (*COQ eq_constr out (cic_relation_class_of_relation_class
1546               coq_iff_relation)*) assert false
1547             then
1548               Cic.Appl
1549                [coq_morphism_theory_of_predicate;
1550                 cic_type_nelist_of_list f_args; f]
1551             else
1552               Cic.Appl
1553                [coq_morphism_theory_of_function;
1554                 cic_type_nelist_of_list f_args; f_output; f]
1555            in
1556             mt,List.map (fun x -> None,Leibniz (Some x)) f_args in
1557       let cic_relations =
1558        List.map
1559         (fun (variance,r) ->
1560           variance,
1561           r,
1562           cic_relation_class_of_relation_class r,
1563           cic_precise_relation_class_of_relation_class r
1564         ) relations in
1565       let cic_args_relations,argst =
1566        cic_morphism_context_list_of_list hole_relation hole_direction direction
1567         (List.map2
1568          (fun (variance,trel,t,precise_t) v ->
1569            (variance,cic_argument_class_of_argument_class (variance,trel)),
1570              (aux t precise_t v,
1571                direction_of_constr_with_marks hole_direction v)
1572          ) cic_relations args)
1573       in
1574        Cic.Appl
1575         [coq_App;
1576          hole_relation ; hole_direction ;
1577          cic_args_relations ; out ; direction ;
1578          morphism_theory ; argst]
1579    | ToReplace ->
1580       Cic.Appl [coq_ToReplace ; hole_relation ; hole_direction]
1581    | ToKeep (c,_,direction) ->
1582       let direction = cic_direction_of_direction direction in
1583        if is_reflexive then
1584         Cic.Appl
1585          [coq_ToKeep ; hole_relation ; hole_direction ; precise_out ;
1586           direction ; c]
1587        else
1588         let c_is_proper =
1589          let typ = Cic.Appl [rel_out ; c ; c] in
1590           Cic.Cast ((*COQ Evarutil.mk_new_meta ()*)assert false, typ)
1591         in
1592          Cic.Appl
1593           [coq_ProperElementToKeep ;
1594            hole_relation ; hole_direction; precise_out ;
1595            direction; c ; c_is_proper]
1596  in aux
1597
1598 let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h)
1599  prop_direction m
1600 =
1601  let hole_relation = cic_relation_class_of_relation_class hole_relation in
1602  let hyp,hole_direction = h,cic_direction_of_direction direction in
1603  let cic_prop_relation = cic_relation_class_of_relation_class prop_relation in
1604  let precise_prop_relation =
1605   cic_precise_relation_class_of_relation_class prop_relation
1606  in
1607   Cic.Appl
1608    [coq_setoid_rewrite;
1609     hole_relation ; hole_direction ; cic_prop_relation ;
1610     prop_direction ; c1 ; c2 ;
1611     syntactic_but_representation_of_marked_but hole_relation hole_direction
1612     cic_prop_relation precise_prop_relation m ; hyp]
1613
1614 (*COQ
1615 let check_evar_map_of_evars_defs evd =
1616  let metas = Evd.meta_list evd in
1617  let check_freemetas_is_empty rebus =
1618   Evd.Metaset.iter
1619    (fun m ->
1620      if Evd.meta_defined evd m then () else
1621       raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
1622  in
1623   List.iter
1624    (fun (_,binding) ->
1625      match binding with
1626         Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) ->
1627          check_freemetas_is_empty rebus freemetas
1628       | Evd.Clval (_,{Evd.rebus=rebus1; Evd.freemetas=freemetas1},
1629                  {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) ->
1630          check_freemetas_is_empty rebus1 freemetas1 ;
1631          check_freemetas_is_empty rebus2 freemetas2
1632    ) metas
1633 *)
1634
1635 (* For a correct meta-aware "rewrite in", we split unification
1636    apart from the actual rewriting (Pierre L, 05/04/06) *)
1637
1638 (* [unification_rewrite] searchs a match for [c1] in [but] and then
1639    returns the modified objects (in particular [c1] and [c2]) *)
1640
1641 let unification_rewrite c1 c2 cl but gl =
1642 (*COQ
1643   let (env',c1) =
1644     try
1645       (* ~mod_delta:false to allow to mark occurences that must not be
1646          rewritten simply by replacing them with let-defined definitions
1647          in the context *)
1648       w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env
1649     with
1650         Pretype_errors.PretypeError _ ->
1651           (* ~mod_delta:true to make Ring work (since it really
1652              exploits conversion) *)
1653           w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.env
1654   in
1655   let cl' = {cl with env = env' } in
1656   let c2 = Clenv.clenv_nf_meta cl' c2 in
1657   check_evar_map_of_evars_defs env' ;
1658   env',Clenv.clenv_value cl', c1, c2
1659 *) assert false
1660
1661 (* no unification is performed in this function. [sigma] is the
1662  substitution obtained from an earlier unification. *)
1663
1664 let relation_rewrite_no_unif c1 c2 hyp ~new_goals sigma gl =
1665   let but = (*COQ pf_concl gl*) assert false in
1666   try
1667    let input_relation =
1668     relation_class_that_matches_a_constr "Setoid_rewrite"
1669      new_goals ((*COQTyping.mtype_of (pf_env gl) sigma (snd hyp)*) assert false) in
1670    let output_relation,output_direction,marked_but =
1671     mark_occur gl ~new_goals c1 but input_relation (fst hyp) in
1672    let cic_output_direction = cic_direction_of_direction output_direction in
1673    let if_output_relation_is_iff gl =
1674     let th =
1675      apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
1676       cic_output_direction marked_but
1677     in
1678      let new_but = (*COQ Termops.replace_term c1 c2 but*) assert false in
1679      let hyp1,hyp2,proj =
1680       match output_direction with
1681          Right2Left -> new_but, but, coq_proj1
1682        | Left2Right -> but, new_but, coq_proj2
1683      in
1684      let impl1 = Cic.Prod (Cic.Anonymous, hyp2, CicSubstitution.lift 1 hyp1) in
1685      let impl2 = Cic.Prod (Cic.Anonymous, hyp1, CicSubstitution.lift 1 hyp2) in
1686       let th' = Cic.Appl [proj; impl2; impl1; th] in
1687        (*COQ Tactics.refine
1688         (Cic.Appl [th'; mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)])
1689         gl*) let _ = th' in assert false in
1690    let if_output_relation_is_if gl =
1691     let th =
1692      apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
1693       cic_output_direction marked_but
1694     in
1695      let new_but = (*COQ Termops.replace_term c1 c2 but*) assert false in
1696       (*COQ Tactics.refine
1697        (Cic.Appl [th ; mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)])
1698        gl*) let _ = new_but,th in assert false in
1699    if output_relation = coq_iff_relation then
1700      if_output_relation_is_iff gl
1701    else
1702      if_output_relation_is_if gl
1703   with
1704     Optimize ->
1705       (*COQ !general_rewrite (fst hyp = Left2Right) (snd hyp) gl*) assert false
1706
1707 let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
1708  let (sigma,cl,c1,c2) = unification_rewrite c1 c2 cl ((*COQ pf_concl gl*) assert false) gl in
1709  relation_rewrite_no_unif c1 c2 (input_direction,cl) ~new_goals sigma gl
1710
1711 let analyse_hypothesis gl c =
1712  let ctype = (*COQ pf_type_of gl c*) assert false in
1713  let eqclause  = (*COQ Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings*) let _ = ctype in assert false in
1714  let (equiv, args) = (*COQ decompose_app (Clenv.clenv_type eqclause)*) assert false in
1715  let rec split_last_two = function
1716    | [c1;c2] -> [],(c1, c2)
1717    | x::y::z ->
1718       let l,res = split_last_two (y::z) in x::l, res
1719    | _ -> raise (ProofEngineTypes.Fail (lazy "The term provided is not an equivalence")) in
1720  let others,(c1,c2) = split_last_two args in
1721   eqclause,Cic.Appl (equiv::others),c1,c2
1722
1723 let general_s_rewrite lft2rgt c ~new_goals (*COQgl*) =
1724 (*COQ
1725   let eqclause,_,c1,c2 = analyse_hypothesis gl c in
1726   if lft2rgt then
1727     relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl
1728   else
1729     relation_rewrite c2 c1 (Right2Left,eqclause) ~new_goals gl
1730 *) assert false
1731
1732 let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl =
1733  let hyp = (*COQ pf_type_of gl (mkVar id)*) assert false in
1734  (* first, we find a match for c1 in the hyp *)
1735  let (sigma,cl,c1,c2) = unification_rewrite c1 c2 eqclause hyp gl in
1736  (* since we will actually rewrite in the opposite direction, we also need
1737     to replace every occurrence of c2 (resp. c1) in hyp with something that
1738     is convertible but not syntactically equal. To this aim we introduce a
1739     let-in and then we will use the intro tactic to get rid of it.
1740     Quite tricky to do properly since c1 can occur in c2 or vice-versa ! *)
1741  let mangled_new_hyp =
1742    let hyp = CicSubstitution.lift 2 hyp in
1743    (* first, we backup every occurences of c1 in newly allocated (Rel 1) *)
1744    let hyp = (*COQ Termops.replace_term (CicSubstitution.lift 2 c1) (Cic.Rel 1) hyp*) let _ = hyp in assert false in
1745    (* then, we factorize every occurences of c2 into (Rel 2) *)
1746    let hyp = (*COQ Termops.replace_term (CicSubstitution.lift 2 c2) (Cic.Rel 2) hyp*) let _ = hyp in assert false in
1747    (* Now we substitute (Rel 1) (i.e. c1) for c2 *)
1748    let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in
1749    (* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels,
1750       Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
1751    Cic.LetIn (Cic.Anonymous,c2,assert false,hyp)
1752  in
1753  let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in
1754  let oppdir = opposite_direction direction in
1755 (*COQ
1756  cut_replacing id new_hyp
1757    (tclTHENLAST
1758       (tclTHEN (change_in_concl None mangled_new_hyp)
1759          (tclTHEN intro
1760             (relation_rewrite_no_unif c2 c1 (oppdir,cl) ~new_goals sigma))))
1761    gl
1762 *) let _ = oppdir,new_hyp,mangled_new_hyp in assert false
1763
1764 let general_s_rewrite_in id lft2rgt c ~new_goals (*COQgl*) =
1765 (*COQ
1766   let eqclause,_,c1,c2 = analyse_hypothesis gl c in
1767   if lft2rgt then
1768     relation_rewrite_in id c1 c2 (Left2Right,eqclause) ~new_goals gl
1769   else
1770     relation_rewrite_in id c2 c1 (Right2Left,eqclause) ~new_goals gl
1771 *) assert false
1772
1773 let setoid_replace relation c1 c2 ~new_goals (*COQgl*) =
1774  try
1775   let relation =
1776    match relation with
1777       Some rel ->
1778        (try
1779          match find_relation_class rel with
1780             Relation sa -> sa
1781           | Leibniz _ -> raise Optimize
1782         with
1783          Not_found ->
1784           raise (ProofEngineTypes.Fail (lazy
1785            (CicPp.ppterm rel ^ " is not a registered relation."))))
1786     | None ->
1787        match default_relation_for_carrier ((*COQ pf_type_of gl c1*) assert false) with
1788           Relation sa -> sa
1789         | Leibniz _ -> raise Optimize
1790   in
1791    let eq_left_to_right = Cic.Appl [relation.rel_aeq; c1 ; c2] in
1792    let eq_right_to_left = Cic.Appl [relation.rel_aeq; c2 ; c1] in
1793 (*COQ
1794    let replace dir eq =
1795     tclTHENS (assert_tac false Cic.Anonymous eq)
1796       [onLastHyp (fun id ->
1797         tclTHEN
1798           (general_s_rewrite dir (mkVar id) ~new_goals)
1799           (clear [id]));
1800        Tacticals.tclIDTAC]
1801    in
1802     tclORELSE
1803      (replace true eq_left_to_right) (replace false eq_right_to_left) gl
1804 *) let _ = eq_left_to_right,eq_right_to_left in assert false
1805  with
1806   Optimize -> (*COQ (!replace c1 c2) gl*) assert false
1807
1808 let setoid_replace_in id relation c1 c2 ~new_goals (*COQgl*) =
1809 (*COQ
1810  let hyp = pf_type_of gl (mkVar id) in
1811  let new_hyp = Termops.replace_term c1 c2 hyp in
1812  cut_replacing id new_hyp
1813    (fun exact -> tclTHENLASTn
1814      (setoid_replace relation c2 c1 ~new_goals)
1815      [| exact; tclIDTAC |]) gl
1816 *) assert false
1817
1818 (* [setoid_]{reflexivity,symmetry,transitivity} tactics *)
1819
1820 let setoid_reflexivity_tac =
1821  let tac ((proof,goal) as status) =
1822   let (_,metasenv,_subst,_,_, _) = proof in
1823   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1824    try
1825     let relation_class =
1826      relation_class_that_matches_a_constr "Setoid_reflexivity" [] ty in
1827     match relation_class with
1828        Leibniz _ -> assert false (* since [] is empty *)
1829      | Relation rel ->
1830         match rel.rel_refl with
1831            None ->
1832             raise (ProofEngineTypes.Fail (lazy
1833              ("The relation " ^ prrelation rel ^ " is not reflexive.")))
1834          | Some refl ->
1835             ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac refl)
1836              status
1837    with
1838     Optimize ->
1839      ProofEngineTypes.apply_tactic EqualityTactics.reflexivity_tac status
1840  in
1841   ProofEngineTypes.mk_tactic tac
1842
1843 let setoid_symmetry  =
1844  let tac status =
1845   try
1846    let relation_class =
1847     relation_class_that_matches_a_constr "Setoid_symmetry"
1848      [] ((*COQ pf_concl gl*) assert false) in
1849    match relation_class with
1850       Leibniz _ -> assert false (* since [] is empty *)
1851     | Relation rel ->
1852        match rel.rel_sym with
1853           None ->
1854            raise (ProofEngineTypes.Fail (lazy
1855             ("The relation " ^ prrelation rel ^ " is not symmetric.")))
1856         | Some sym -> (*COQ apply sym gl*) assert false
1857   with
1858    Optimize -> (*COQ symmetry gl*) assert false
1859  in
1860   ProofEngineTypes.mk_tactic tac
1861
1862 let setoid_symmetry_in id (*COQgl*) =
1863 (*COQ
1864  let new_hyp =
1865   let _,he,c1,c2 = analyse_hypothesis gl (mkVar id) in
1866    Cic.Appl [he ; c2 ; c1]
1867  in
1868  cut_replacing id new_hyp (tclTHEN setoid_symmetry) gl
1869 *) assert false
1870
1871 let setoid_transitivity c (*COQgl*) =
1872  try
1873   let relation_class =
1874    relation_class_that_matches_a_constr "Setoid_transitivity"
1875     [] ((*COQ pf_concl gl*) assert false) in
1876   match relation_class with
1877      Leibniz _ -> assert false (* since [] is empty *)
1878    | Relation rel ->
1879 (*COQ
1880       let ctyp = pf_type_of gl c in
1881       let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in
1882        match rel'.rel_trans with
1883           None ->
1884            raise (ProofEngineTypes.Fail (lazy
1885             ("The relation " ^ prrelation rel ^ " is not transitive.")))
1886         | Some trans ->
1887            let transty = nf_betaiota (pf_type_of gl trans) in
1888            let argsrev, _ =
1889             Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in
1890            let binder =
1891             match List.rev argsrev with
1892                _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2
1893              | _ -> assert false
1894            in
1895             apply_with_bindings
1896              (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
1897 *) assert false
1898  with
1899   Optimize -> (*COQ transitivity c gl*) assert false
1900 ;;
1901
1902 (*COQ
1903 Tactics.register_setoid_reflexivity setoid_reflexivity;;
1904 Tactics.register_setoid_symmetry setoid_symmetry;;
1905 Tactics.register_setoid_symmetry_in setoid_symmetry_in;;
1906 Tactics.register_setoid_transitivity setoid_transitivity;;
1907 *)