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