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)) CicUniv.empty_ugraph) then
 650         args2
 651        else
 652         raise_error rel.rel_quantifiers_no
 653    | _  ->
 654      if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] rel.rel_a t CicUniv.empty_ugraph) then
 655       []
 656      else
 657       begin
 658 (*COQ
 659         let evars,args,instantiated_rel_a =
 660          let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a CicUniv.empty_ugraph in
 661          let evd = Evd.create_evar_defs Evd.empty in
 662          let evars,args,concl =
 663           Clenv.clenv_environments_evars env evd
 664            (Some rel.rel_quantifiers_no) ty
 665          in
 666           evars, args,
 667           nf_betaiota
 668            (match args with [] -> rel.rel_a | _ -> applist (rel.rel_a,args))
 669         in
 670          let evars' =
 671           w_unify true (*??? or false? *) env Reduction.CONV (*??? or cumul? *)
 672            ~mod_delta:true (*??? or true? *) t instantiated_rel_a evars in
 673          let args' =
 674           List.map (Reductionops.nf_evar (Evd.evars_of evars')) args
 675          in
 676           args'
 677 *) assert false
 678       end
 679  in
 680   apply_to_relation args rel
 681
 682 let unify_relation_class_carrier_with_type env rel t =
 683  match rel with
 684     Leibniz (Some t') ->
 685      if fst (CicReduction.are_convertible [] t t' CicUniv.empty_ugraph) then
 686       rel
 687      else
 688       raise (ProofEngineTypes.Fail (lazy
 689        ("One morphism argument or its output has type " ^ CicPp.ppterm t ^
 690         " but the signature requires an argument of type " ^
 691         CicPp.ppterm t')))
 692   | Leibniz None -> Leibniz (Some t)
 693   | Relation rel -> Relation (unify_relation_carrier_with_type env rel t)
 694
 695 exception Impossible
 696
 697 (*COQ
 698 (* first order matching with a bit of conversion *)
 699 (* Note: the type checking operations performed by the function could  *)
 700 (* be done once and for all abstracting the morphism structure using   *)
 701 (* the quantifiers. Would the new structure be more suited than the    *)
 702 (* existent one for other tasks to? (e.g. pretty printing would expose *)
 703 (* much more information: is it ok or is it too much information?)     *)
 704 let unify_morphism_with_arguments gl (c,al)
 705      {args=args; output=output; lem=lem; morphism_theory=morphism_theory} t
 706 =
 707  let allen = List.length al in
 708  let argsno = List.length args in
 709  if allen < argsno then raise Impossible; (* partial application *)
 710  let quantifiers,al' = Util.list_chop (allen - argsno) al in
 711  let c' = Cic.Appl (c::quantifiers) in
 712  if dependent t c' then raise Impossible;
 713  (* these are pf_type_of we could avoid *)
 714  let al'_type = List.map (Tacmach.pf_type_of gl) al' in
 715  let args' =
 716    List.map2
 717      (fun (var,rel) ty ->
 718         var,unify_relation_class_carrier_with_type (pf_env gl) rel ty)
 719      args al'_type in
 720  (* this is another pf_type_of we could avoid *)
 721  let ty = Tacmach.pf_type_of gl (Cic.Appl (c::al)) in
 722  let output' = unify_relation_class_carrier_with_type (pf_env gl) output ty in
 723  let lem' = Cic.Appl (lem::quantifiers) in
 724  let morphism_theory' = Cic.Appl (morphism_theory::quantifiers) in
 725  ({args=args'; output=output'; lem=lem'; morphism_theory=morphism_theory'},
 726   c',al')
 727 *) let unify_morphism_with_arguments _ _ _ _ = assert false
 728
 729 let new_morphism m signature id hook =
 730 (*COQ
 731  if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
 732   raise (ProofEngineTypes.Fail (lazy (pr_id id ^ " already exists")))
 733  else
 734   let env = Global.env() in
 735   let typeofm = Typing.type_of env Evd.empty m in
 736   let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm in
 737   let argsrev, output =
 738    match signature with
 739       None -> decompose_prod typ
 740     | Some (_,output') ->
 741        (* the carrier of the relation output' can be a Prod ==>
 742           we must uncurry on the fly output.
 743           E.g: A -> B -> C vs        A -> (B -> C)
 744                 args   output     args     output
 745        *)
 746        let rel = find_relation_class output' in
 747        let rel_a,rel_quantifiers_no =
 748         match rel with
 749            Relation rel -> rel.rel_a, rel.rel_quantifiers_no
 750          | Leibniz (Some t) -> t, 0
 751          | Leibniz None -> assert false in
 752        let rel_a_n =
 753         clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in
 754        try
 755         let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in
 756         let argsrev,_ = decompose_prod output_rel_a_n in
 757         let n = List.length argsrev in
 758         let argsrev',_ = decompose_prod typ in
 759         let m = List.length argsrev' in
 760          decompose_prod_n (m - n) typ
 761        with UserError(_,_) ->
 762         (* decompose_lam_n failed. This may happen when rel_a is an axiom,
 763            a constructor, an inductive type, etc. *)
 764         decompose_prod typ
 765   in
 766   let args_ty = List.rev argsrev in
 767   let args_ty_len = List.length (args_ty) in
 768   let args_ty_quantifiers_rev,args,args_instance,output,output_instance =
 769    match signature with
 770       None ->
 771        if args_ty = [] then
 772         raise (ProofEngineTypes.Fail (lazy
 773          ("The term " ^ CicPp.ppterm m ^ " has type " ^
 774           CicPp.ppterm typeofm ^ " that is not a product."))) ;
 775        ignore (check_is_dependent 0 args_ty output) ;
 776        let args =
 777         List.map
 778          (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in
 779        let output = default_relation_for_carrier output in
 780         [],args,args,output,output
 781     | Some (args,output') ->
 782        assert (args <> []);
 783        let number_of_arguments = List.length args in
 784        let number_of_quantifiers = args_ty_len - number_of_arguments in
 785        if number_of_quantifiers < 0 then
 786         raise (ProofEngineTypes.Fail (lazy
 787          ("The morphism " ^ CicPp.ppterm m ^ " has type " ^
 788           CicPp.ppterm typeofm ^ " that attends at most " ^ int args_ty_len ^
 789           " arguments. The signature that you specified requires " ^
 790           int number_of_arguments ^ " arguments.")))
 791        else
 792         begin
 793          (* the real_args_ty returned are already delifted *)
 794          let args_ty_quantifiers_rev, real_args_ty, real_output =
 795           check_is_dependent number_of_quantifiers args_ty output in
 796          let quantifiers_rel_context =
 797           List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in
 798          let env = push_rel_context quantifiers_rel_context env in
 799          let find_relation_class t real_t =
 800           try
 801            let rel = find_relation_class t in
 802             rel, unify_relation_class_carrier_with_type env rel real_t
 803           with Not_found ->
 804            raise (ProofEngineTypes.Fail (lazy
 805             ("Not a valid signature: " ^ CicPp.ppterm t ^
 806              " is neither a registered relation nor the Leibniz " ^
 807              " equality.")))
 808          in
 809          let find_relation_class_v (variance,t) real_t =
 810           let relation,relation_instance = find_relation_class t real_t in
 811            match relation, variance with
 812               Leibniz _, None
 813             | Relation {rel_sym = Some _}, None
 814             | Relation {rel_sym = None}, Some _ ->
 815                (variance, relation), (variance, relation_instance)
 816             | Relation {rel_sym = None},None ->
 817                raise (ProofEngineTypes.Fail (lazy
 818                 ("You must specify the variance in each argument " ^
 819                  "whose relation is asymmetric.")))
 820             | Leibniz _, Some _
 821             | Relation {rel_sym = Some _}, Some _ ->
 822                raise (ProofEngineTypes.Fail (lazy
 823                 ("You cannot specify the variance of an argument " ^
 824                  "whose relation is symmetric.")))
 825          in
 826           let args, args_instance =
 827            List.split
 828             (List.map2 find_relation_class_v args real_args_ty) in
 829           let output,output_instance= find_relation_class output' real_output in
 830            args_ty_quantifiers_rev, args, args_instance, output, output_instance
 831         end
 832   in
 833    let argsconstr,outputconstr,lem =
 834     gen_compat_lemma_statement args_ty_quantifiers_rev output_instance
 835      args_instance (apply_to_rels m args_ty_quantifiers_rev) in
 836    (* "unfold make_compatibility_goal" *)
 837    let lem =
 838     Reductionops.clos_norm_flags
 839      (Closure.unfold_red (coq_make_compatibility_goal_eval_ref))
 840      env Evd.empty lem in
 841    (* "unfold make_compatibility_goal_aux" *)
 842    let lem =
 843     Reductionops.clos_norm_flags
 844      (Closure.unfold_red(coq_make_compatibility_goal_aux_eval_ref))
 845      env Evd.empty lem in
 846    (* "simpl" *)
 847    let lem = Tacred.nf env Evd.empty lem in
 848     if Lib.is_modtype () then
 849      begin
 850       ignore
 851        (Declare.declare_internal_constant id
 852         (ParameterEntry lem, IsAssumption Logical)) ;
 853       let mor_name = morphism_theory_id_of_morphism_proof_id id in
 854       let lemma_infos = Some (id,argsconstr,outputconstr) in
 855        add_morphism lemma_infos mor_name
 856         (m,args_ty_quantifiers_rev,args,output)
 857      end
 858     else
 859      begin
 860       new_edited id
 861        (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
 862       Pfedit.start_proof id (Global, Proof Lemma)
 863        (Declare.clear_proofs (Global.named_context ()))
 864        lem hook;
 865       Options.if_verbose msg (Printer.pr_open_subgoals ());
 866      end
 867 *) assert false
 868
 869 let morphism_hook _ ref =
 870 (*COQ
 871   let pf_id = id_of_global ref in
 872   let mor_id = morphism_theory_id_of_morphism_proof_id pf_id in
 873   let (m,quantifiers_rev,args,argsconstr,output,outputconstr) =
 874    what_edited pf_id in
 875   if (is_edited pf_id)
 876   then
 877    begin
 878     add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id
 879      (m,quantifiers_rev,args,output) ;
 880     no_more_edited pf_id
 881    end
 882 *) assert false
 883
 884 type morphism_signature =
 885  (bool option * Cic.term) list * Cic.term
 886
 887 let new_named_morphism id m sign =
 888  new_morphism m sign id morphism_hook
 889
 890 (************************** Adding a relation to the database *********************)
 891
 892 let check_a a =
 893 (*COQ
 894  let typ = Typing.type_of env Evd.empty a in
 895  let a_quantifiers_rev,_ = Reduction.dest_arity env typ in
 896   a_quantifiers_rev
 897 *) assert false
 898
 899 let check_eq a_quantifiers_rev a aeq =
 900 (*COQ
 901  let typ =
 902   Sign.it_mkProd_or_LetIn
 903    (Cic.Appl [coq_relation ; apply_to_rels a a_quantifiers_rev])
 904    a_quantifiers_rev in
 905  if
 906   not
 907    (is_conv env Evd.empty (Typing.type_of env Evd.empty aeq) typ)
 908  then
 909   raise (ProofEngineTypes.Fail (lazy
 910    (CicPp.ppterm aeq ^ " should have type (" ^ CicPp.ppterm typ ^ ")")))
 911 *) (assert false : unit)
 912
 913 let check_property a_quantifiers_rev a aeq strprop coq_prop t =
 914 (*COQ
 915  if
 916   not
 917    (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
 918     (Sign.it_mkProd_or_LetIn
 919      (Cic.Appl
 920        [coq_prop ;
 921         apply_to_rels a a_quantifiers_rev ;
 922         apply_to_rels aeq a_quantifiers_rev]) a_quantifiers_rev))
 923  then
 924   raise (ProofEngineTypes.Fail (lazy
 925    ("Not a valid proof of " ^ strprop ^ ".")))
 926 *) assert false
 927
 928 let check_refl a_quantifiers_rev a aeq refl =
 929  check_property a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl
 930
 931 let check_sym a_quantifiers_rev a aeq sym =
 932  check_property a_quantifiers_rev a aeq "symmetry" coq_symmetric sym
 933
 934 let check_trans a_quantifiers_rev a aeq trans =
 935  check_property a_quantifiers_rev a aeq "transitivity" coq_transitive trans
 936 ;;
 937
 938 let int_add_relation id a aeq refl sym trans =
 939 (*COQ
 940  let env = Global.env () in
 941 *)
 942  let a_quantifiers_rev = check_a a in
 943   check_eq a_quantifiers_rev a aeq  ;
 944   HExtlib.iter_option (check_refl a_quantifiers_rev a aeq) refl ;
 945   HExtlib.iter_option (check_sym a_quantifiers_rev a aeq) sym ;
 946   HExtlib.iter_option (check_trans a_quantifiers_rev a aeq) trans ;
 947   let quantifiers_no = List.length a_quantifiers_rev in
 948   let aeq_rel =
 949    { rel_a = a;
 950      rel_aeq = aeq;
 951      rel_refl = refl;
 952      rel_sym = sym;
 953      rel_trans = trans;
 954      rel_quantifiers_no = quantifiers_no;
 955      rel_X_relation_class = Cic.Sort Cic.Prop; (* dummy value, overwritten below *)
 956      rel_Xreflexive_relation_class = Cic.Sort Cic.Prop (* dummy value, overwritten below *)
 957    } in
 958   let x_relation_class =
 959    let subst =
 960     let len = List.length a_quantifiers_rev in
 961      list_map_i (fun i _ -> Cic.Rel (len - i + 2)) 0 a_quantifiers_rev in
 962    cic_relation_class_of_X_relation
 963     (Cic.Rel 2) (Cic.Rel 1) (apply_to_relation subst aeq_rel) in
 964   let _ =
 965 (*COQ
 966    Declare.declare_internal_constant id
 967     (DefinitionEntry
 968       {const_entry_body =
 969         Sign.it_mkLambda_or_LetIn x_relation_class
 970          ([ Name "v",None,Cic.Rel 1;
 971             Name "X",None,Cic.Sort (Cic.Type (CicUniv.fresh ()))] @
 972             a_quantifiers_rev);
 973        const_entry_type = None;
 974        const_entry_opaque = false;
 975        const_entry_boxed = Options.boxed_definitions()},
 976       IsDefinition Definition) in
 977 *) () in
 978   let id_precise = id ^ "_precise_relation_class" in
 979   let xreflexive_relation_class =
 980    let subst =
 981     let len = List.length a_quantifiers_rev in
 982      list_map_i (fun i _ -> Cic.Rel (len - i)) 0 a_quantifiers_rev
 983    in
 984     cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in
 985   let _ =
 986 (*COQ
 987    Declare.declare_internal_constant id_precise
 988     (DefinitionEntry
 989       {const_entry_body =
 990         Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev;
 991        const_entry_type = None;
 992        const_entry_opaque = false;
 993        const_entry_boxed = Options.boxed_definitions() },
 994       IsDefinition Definition) in
 995 *) () in
 996   let aeq_rel =
 997    { aeq_rel with
 998       rel_X_relation_class = current_constant id;
 999       rel_Xreflexive_relation_class = current_constant id_precise } in
1000   relation_to_obj (aeq, aeq_rel) ;
1001   prerr_endline (CicPp.ppterm aeq ^ " is registered as a relation");
1002   match trans with
1003      None -> ()
1004    | Some trans ->
1005       let mor_name = id ^ "_morphism" in
1006       let a_instance = apply_to_rels a a_quantifiers_rev in
1007       let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
1008       let sym_instance =
1009        HExtlib.map_option (fun x -> apply_to_rels x a_quantifiers_rev) sym in
1010       let refl_instance =
1011        HExtlib.map_option (fun x -> apply_to_rels x a_quantifiers_rev) refl in
1012       let trans_instance = apply_to_rels trans a_quantifiers_rev in
1013       let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output =
1014        match sym_instance, refl_instance with
1015           None, None ->
1016            (Some false, Relation aeq_rel),
1017            (Some true, Relation aeq_rel),
1018             Cic.Appl
1019              [coq_equality_morphism_of_asymmetric_areflexive_transitive_relation;
1020               a_instance ; aeq_instance ; trans_instance],
1021             coq_impl_relation
1022         | None, Some refl_instance ->
1023            (Some false, Relation aeq_rel),
1024            (Some true, Relation aeq_rel),
1025             Cic.Appl
1026              [coq_equality_morphism_of_asymmetric_reflexive_transitive_relation;
1027               a_instance ; aeq_instance ; refl_instance ; trans_instance],
1028             coq_impl_relation
1029         | Some sym_instance, None ->
1030            (None, Relation aeq_rel),
1031            (None, Relation aeq_rel),
1032             Cic.Appl
1033              [coq_equality_morphism_of_symmetric_areflexive_transitive_relation;
1034               a_instance ; aeq_instance ; sym_instance ; trans_instance],
1035             coq_iff_relation
1036         | Some sym_instance, Some refl_instance ->
1037            (None, Relation aeq_rel),
1038            (None, Relation aeq_rel),
1039             Cic.Appl
1040              [coq_equality_morphism_of_symmetric_reflexive_transitive_relation;
1041               a_instance ; aeq_instance ; refl_instance ; sym_instance ;
1042               trans_instance],
1043             coq_iff_relation in
1044       let _ =
1045 (*COQ
1046        Declare.declare_internal_constant mor_name
1047         (DefinitionEntry
1048           {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev;
1049            const_entry_type = None;
1050            const_entry_opaque = false;
1051           const_entry_boxed = Options.boxed_definitions()},
1052           IsDefinition Definition)
1053 *) ()
1054       in
1055        let a_quantifiers_rev =
1056         List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in
1057        add_morphism None mor_name
1058         (aeq,a_quantifiers_rev,[aeq_rel_class_and_var1; aeq_rel_class_and_var2],
1059           output)
1060
1061 (* The vernac command "Add Relation ..." *)
1062 let add_relation id a aeq refl sym trans =
1063  int_add_relation id a aeq refl sym trans
1064
1065 (****************************** The tactic itself *******************************)
1066
1067 type direction =
1068    Left2Right
1069  | Right2Left
1070
1071 let prdirection =
1072  function
1073     Left2Right -> "->"
1074   | Right2Left -> "<-"
1075
1076 type constr_with_marks =
1077   | MApp of Cic.term * morphism_class * constr_with_marks list * direction
1078   | ToReplace
1079   | ToKeep of Cic.term * relation relation_class * direction
1080
1081 let is_to_replace = function
1082  | ToKeep _ -> false
1083  | ToReplace -> true
1084  | MApp _ -> true
1085
1086 let get_mark a =
1087   List.fold_left (||) false (List.map is_to_replace a)
1088
1089 let cic_direction_of_direction =
1090  function
1091     Left2Right -> coq_Left2Right
1092   | Right2Left -> coq_Right2Left
1093
1094 let opposite_direction =
1095  function
1096     Left2Right -> Right2Left
1097   | Right2Left -> Left2Right
1098
1099 let direction_of_constr_with_marks hole_direction =
1100  function
1101     MApp (_,_,_,dir) -> cic_direction_of_direction dir
1102   | ToReplace -> hole_direction
1103   | ToKeep (_,_,dir) -> cic_direction_of_direction dir
1104
1105 type argument =
1106    Toapply of Cic.term         (* apply the function to the argument *)
1107  | Toexpand of Cic.name * Cic.term  (* beta-expand the function w.r.t. an argument
1108                                 of this type *)
1109 let beta_expand c args_rev =
1110  let rec to_expand =
1111   function
1112      [] -> []
1113    | (Toapply _)::tl -> to_expand tl
1114    | (Toexpand (name,s))::tl -> (name,s)::(to_expand tl) in
1115  let rec aux n =
1116   function
1117      [] -> []
1118    | (Toapply arg)::tl -> arg::(aux n tl)
1119    | (Toexpand _)::tl -> (Cic.Rel n)::(aux (n + 1) tl)
1120  in
1121   compose_lambda (to_expand args_rev)
1122    (Cic.Appl (c :: List.rev (aux 1 args_rev)))
1123
1124 exception Optimize (* used to fall-back on the tactic for Leibniz equality *)
1125
1126 let rec list_sep_last = function
1127   | [] -> assert false
1128   | hd::[] -> (hd,[])
1129   | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
1130
1131 let relation_class_that_matches_a_constr caller_name new_goals hypt =
1132  let heq, hargs =
1133   match hypt with
1134      Cic.Appl (heq::hargs) -> heq,hargs
1135    | _ -> hypt,[]
1136  in
1137  let rec get_all_but_last_two =
1138   function
1139      []
1140    | [_] ->
1141       raise (ProofEngineTypes.Fail (lazy (CicPp.ppterm hypt ^
1142        " is not a registered relation.")))
1143    | [_;_] -> []
1144    | he::tl -> he::(get_all_but_last_two tl) in
1145  let all_aeq_args = get_all_but_last_two hargs in
1146  let rec find_relation l subst =
1147   let aeq = Cic.Appl (heq::l) in
1148   try
1149    let rel = find_relation_class aeq in
1150    match rel,new_goals with
1151       Leibniz _,[] ->
1152        assert (subst = []);
1153        raise Optimize (* let's optimize the proof term size *)
1154     | Leibniz (Some _), _ ->
1155        assert (subst = []);
1156        rel
1157     | Leibniz None, _ ->
1158        (* for well-typedness reasons it should have been catched by the
1159           previous guard in the previous iteration. *)
1160        assert false
1161     | Relation rel,_ -> Relation (apply_to_relation subst rel)
1162   with Not_found ->
1163    if l = [] then
1164     raise (ProofEngineTypes.Fail (lazy
1165      (CicPp.ppterm (Cic.Appl (aeq::all_aeq_args)) ^
1166       " is not a registered relation.")))
1167    else
1168     let last,others = list_sep_last l in
1169     find_relation others (last::subst)
1170  in
1171   find_relation all_aeq_args []
1172
1173 (* rel1 is a subrelation of rel2 whenever
1174     forall x1 x2, rel1 x1 x2 -> rel2 x1 x2
1175    The Coq part of the tactic, however, needs rel1 == rel2.
1176    Hence the third case commented out.
1177    Note: accepting user-defined subtrelations seems to be the last
1178    useful generalization that does not go against the original spirit of
1179    the tactic.
1180 *)
1181 let subrelation gl rel1 rel2 =
1182  match rel1,rel2 with
1183     Relation {rel_aeq=rel_aeq1}, Relation {rel_aeq=rel_aeq2} ->
1184      (*COQ Tacmach.pf_conv_x gl rel_aeq1 rel_aeq2*) assert false
1185   | Leibniz (Some t1), Leibniz (Some t2) ->
1186      (*COQ Tacmach.pf_conv_x gl t1 t2*) assert false
1187   | Leibniz None, _
1188   | _, Leibniz None -> assert false
1189 (* This is the commented out case (see comment above)
1190   | Leibniz (Some t1), Relation {rel_a=t2; rel_refl = Some _} ->
1191      Tacmach.pf_conv_x gl t1 t2
1192 *)
1193   | _,_ -> false
1194
1195 (* this function returns the list of new goals opened by a constr_with_marks *)
1196 let rec collect_new_goals =
1197  function
1198    MApp (_,_,a,_) -> List.concat (List.map collect_new_goals a)
1199  | ToReplace
1200  | ToKeep (_,Leibniz _,_)
1201  | ToKeep (_,Relation {rel_refl=Some _},_) -> []
1202  | ToKeep (c,Relation {rel_aeq=aeq; rel_refl=None},_) -> [Cic.Appl[aeq;c;c]]
1203
1204 (* two marked_constr are equivalent if they produce the same set of new goals *)
1205 let marked_constr_equiv_or_more_complex to_marked_constr gl c1 c2 =
1206   let glc1 = collect_new_goals (to_marked_constr c1) in
1207   let glc2 = collect_new_goals (to_marked_constr c2) in
1208    List.for_all (fun c -> List.exists (fun c' -> (*COQ pf_conv_x gl c c'*) assert false) glc1) glc2
1209
1210 let pr_new_goals i c =
1211  let glc = collect_new_goals c in
1212   " " ^ string_of_int i ^ ") side conditions:" ^
1213    (if glc = [] then " no side conditions"
1214     else
1215      ("\n   " ^
1216        String.concat "\n   "
1217         (List.map (fun c -> " ... |- " ^ CicPp.ppterm c) glc)))
1218
1219 (* given a list of constr_with_marks, it returns the list where
1220    constr_with_marks than open more goals than simpler ones in the list
1221    are got rid of *)
1222 let elim_duplicates gl to_marked_constr =
1223  let rec aux =
1224   function
1225      [] -> []
1226    | he:: tl ->
1227       if List.exists
1228           (marked_constr_equiv_or_more_complex to_marked_constr gl he) tl
1229       then aux tl
1230       else he::aux tl
1231  in
1232   aux
1233
1234 let filter_superset_of_new_goals gl new_goals l =
1235  List.filter
1236   (fun (_,_,c) ->
1237     List.for_all
1238      (fun g -> List.exists ((*COQ pf_conv_x gl g*)assert false) (collect_new_goals c)) new_goals) l
1239
1240 (* given the list of lists [ l1 ; ... ; ln ] it returns the list of lists
1241    [ c1 ; ... ; cn ] that is the cartesian product of the sets l1, ..., ln *)
1242 let cartesian_product gl a =
1243  let rec aux =
1244   function
1245      [] -> assert false
1246    | [he] -> List.map (fun e -> [e]) he
1247    | he::tl ->
1248       let tl' = aux tl in
1249        List.flatten
1250         (List.map (function e -> List.map (function l -> e :: l) tl') he)
1251  in
1252   aux (List.map (elim_duplicates gl (fun x -> x)) a)
1253
1254 let does_not_occur n t = assert false
1255
1256 let mark_occur gl ~new_goals t in_c input_relation input_direction =
1257  let rec aux output_relation output_direction in_c =
1258   if t = in_c then
1259    if input_direction = output_direction
1260    && subrelation gl input_relation output_relation then
1261     [ToReplace]
1262    else []
1263   else
1264     match in_c with
1265       | Cic.Appl (c::al) ->
1266          let mors_and_cs_and_als =
1267           let mors_and_cs_and_als =
1268            let morphism_table_find c =
1269             try morphism_table_find c with Not_found -> [] in
1270            let rec aux acc =
1271             function
1272                [] ->
1273                 let c' = Cic.Appl (c::acc) in
1274                 let al' = [] in
1275                 List.map (fun m -> m,c',al') (morphism_table_find c')
1276              | (he::tl) as l ->
1277                 let c' = Cic.Appl (c::acc) in
1278                 let acc' = acc @ [he] in
1279                  (List.map (fun m -> m,c',l) (morphism_table_find c')) @
1280                   (aux acc' tl)
1281            in
1282             aux [] al in
1283           let mors_and_cs_and_als =
1284            List.map
1285             (function (m,c,al) ->
1286               relation_morphism_of_constr_morphism m, c, al)
1287              mors_and_cs_and_als in
1288           let mors_and_cs_and_als =
1289            List.fold_left
1290             (fun l (m,c,al) ->
1291                try (unify_morphism_with_arguments gl (c,al) m t) :: l
1292                with Impossible -> l
1293             ) [] mors_and_cs_and_als
1294           in
1295            List.filter
1296             (fun (mor,_,_) -> subrelation gl mor.output output_relation)
1297             mors_and_cs_and_als
1298          in
1299           (* First we look for well typed morphisms *)
1300           let res_mors =
1301            List.fold_left
1302             (fun res (mor,c,al) ->
1303               let a =
1304                let arguments = mor.args in
1305                let apply_variance_to_direction default_dir =
1306                 function
1307                    None -> default_dir
1308                  | Some true -> output_direction
1309                  | Some false -> opposite_direction output_direction
1310                in
1311                 List.map2
1312                  (fun a (variance,relation) ->
1313                    (aux relation
1314                      (apply_variance_to_direction Left2Right variance) a) @
1315                    (aux relation
1316                      (apply_variance_to_direction Right2Left variance) a)
1317                  ) al arguments
1318               in
1319                let a' = cartesian_product gl a in
1320                 (List.map
1321                   (function a ->
1322                     if not (get_mark a) then
1323                      ToKeep (in_c,output_relation,output_direction)
1324                     else
1325                      MApp (c,ACMorphism mor,a,output_direction)) a') @ res
1326             ) [] mors_and_cs_and_als in
1327           (* Then we look for well typed functions *)
1328           let res_functions =
1329            (* the tactic works only if the function type is
1330                made of non-dependent products only. However, here we
1331                can cheat a bit by partially istantiating c to match
1332                the requirement when the arguments to be replaced are
1333                bound by non-dependent products only. *)
1334             let typeofc = (*COQ Tacmach.pf_type_of gl c*) assert false in
1335             let typ = (*COQ nf_betaiota typeofc*) let _ = typeofc in assert false in
1336             let rec find_non_dependent_function context c c_args_rev typ
1337              f_args_rev a_rev
1338             =
1339              function
1340                 [] ->
1341                  if a_rev = [] then
1342                   [ToKeep (in_c,output_relation,output_direction)]
1343                  else
1344                   let a' =
1345                    cartesian_product gl (List.rev a_rev)
1346                   in
1347                    List.fold_left
1348                     (fun res a ->
1349                       if not (get_mark a) then
1350                        (ToKeep (in_c,output_relation,output_direction))::res
1351                       else
1352                        let err =
1353                         match output_relation with
1354                            Leibniz (Some typ') when (*COQ pf_conv_x gl typ typ'*) assert false ->
1355                             false
1356                          | Leibniz None -> assert false
1357                          | _ when output_relation = coq_iff_relation
1358                              -> false
1359                          | _ -> true
1360                        in
1361                         if err then res
1362                         else
1363                          let mor =
1364                           ACFunction{f_args=List.rev f_args_rev;f_output=typ} in
1365                          let func = beta_expand c c_args_rev in
1366                           (MApp (func,mor,a,output_direction))::res
1367                     ) [] a'
1368               | (he::tl) as a->
1369                  let typnf = (*COQ Reduction.whd_betadeltaiota env typ*) assert false in
1370                   match typnf with
1371                     Cic.Cast (typ,_) ->
1372                      find_non_dependent_function context c c_args_rev typ
1373                       f_args_rev a_rev a
1374                   | Cic.Prod (name,s,t) ->
1375                      let context' = Some (name, Cic.Decl s)::context in
1376                      let he =
1377                       (aux (Leibniz (Some s)) Left2Right he) @
1378                       (aux (Leibniz (Some s)) Right2Left he) in
1379                      if he = [] then []
1380                      else
1381                       let he0 = List.hd he in
1382                       begin
1383                        match does_not_occur 1 t, he0 with
1384                           _, ToKeep (arg,_,_) ->
1385                            (* invariant: if he0 = ToKeep (t,_,_) then every
1386                               element in he is = ToKeep (t,_,_) *)
1387                            assert
1388                             (List.for_all
1389                               (function
1390                                   ToKeep(arg',_,_) when (*COQpf_conv_x gl arg arg'*) assert false ->
1391                                     true
1392                                 | _ -> false) he) ;
1393                            (* generic product, to keep *)
1394                            find_non_dependent_function
1395                             context' c ((Toapply arg)::c_args_rev)
1396                             (CicSubstitution.subst arg t) f_args_rev a_rev tl
1397                         | true, _ ->
1398                            (* non-dependent product, to replace *)
1399                            find_non_dependent_function
1400                             context' c ((Toexpand (name,s))::c_args_rev)
1401                              (CicSubstitution.lift 1 t) (s::f_args_rev) (he::a_rev) tl
1402                         | false, _ ->
1403                            (* dependent product, to replace *)
1404                            (* This limitation is due to the reflexive
1405                              implementation and it is hard to lift *)
1406                            raise (ProofEngineTypes.Fail (lazy
1407                             ("Cannot rewrite in the argument of a " ^
1408                              "dependent product. If you need this " ^
1409                              "feature, please report to the author.")))
1410                       end
1411                   | _ -> assert false
1412             in
1413              find_non_dependent_function (*COQ (Tacmach.pf_env gl) ci vuole il contesto*)(assert false) c [] typ [] []
1414               al
1415           in
1416            elim_duplicates gl (fun x -> x) (res_functions @ res_mors)
1417       | Cic.Prod (_, c1, c2) ->
1418           if (*COQ (dependent (Cic.Rel 1) c2)*) assert false
1419           then
1420            raise (ProofEngineTypes.Fail (lazy
1421             ("Cannot rewrite in the type of a variable bound " ^
1422              "in a dependent product.")))
1423           else
1424            let typeofc1 = (*COQ Tacmach.pf_type_of gl c1*) assert false in
1425             if not (*COQ (Tacmach.pf_conv_x gl typeofc1 (Cic.Sort Cic.Prop))*) (assert false) then
1426              (* to avoid this error we should introduce an impl relation
1427                 whose first argument is Type instead of Prop. However,
1428                 the type of the new impl would be Type -> Prop -> Prop
1429                 that is no longer a Relation_Definitions.relation. Thus
1430                 the Coq part of the tactic should be heavily modified. *)
1431              raise (ProofEngineTypes.Fail (lazy
1432               ("Rewriting in a product A -> B is possible only when A " ^
1433                "is a proposition (i.e. A is of type Prop). The type " ^
1434                CicPp.ppterm c1 ^ " has type " ^ CicPp.ppterm typeofc1 ^
1435                " that is not convertible to Prop.")))
1436             else
1437              aux output_relation output_direction
1438               (Cic.Appl [coq_impl; c1 ; CicSubstitution.subst (Cic.Rel 1 (*dummy*)) c2])
1439       | _ ->
1440         if (*COQ occur_term t in_c*) assert false then
1441          raise (ProofEngineTypes.Fail (lazy
1442           ("Trying to replace " ^ CicPp.ppterm t ^ " in " ^ CicPp.ppterm in_c ^
1443            " that is not an applicative context.")))
1444         else
1445          [ToKeep (in_c,output_relation,output_direction)]
1446  in
1447   let aux2 output_relation output_direction =
1448    List.map
1449     (fun res -> output_relation,output_direction,res)
1450      (aux output_relation output_direction in_c) in
1451   let res =
1452    (aux2 coq_iff_relation Right2Left) @
1453    (* This is the case of a proposition of signature A ++> iff or B --> iff *)
1454    (aux2 coq_iff_relation Left2Right) @
1455    (aux2 coq_impl_relation Right2Left) in
1456   let res = elim_duplicates gl (function (_,_,t) -> t) res in
1457   let res' = filter_superset_of_new_goals gl new_goals res in
1458   match res' with
1459      [] when res = [] ->
1460       raise (ProofEngineTypes.Fail (lazy
1461        ("Either the term " ^ CicPp.ppterm t ^ " that must be " ^
1462         "rewritten occurs in a covariant position or the goal is not " ^
1463         "made of morphism applications only. You can replace only " ^
1464         "occurrences that are in a contravariant position and such that " ^
1465         "the context obtained by abstracting them is made of morphism " ^
1466         "applications only.")))
1467    | [] ->
1468       raise (ProofEngineTypes.Fail (lazy
1469        ("No generated set of side conditions is a superset of those " ^
1470         "requested by the user. The generated sets of side conditions " ^
1471         "are:\n" ^
1472          prlist_with_sepi "\n"
1473           (fun i (_,_,mc) -> pr_new_goals i mc) res)))
1474    | [he] -> he
1475    | he::_ ->
1476       prerr_endline
1477        ("Warning: The application of the tactic is subject to one of " ^
1478         "the \nfollowing set of side conditions that the user needs " ^
1479         "to prove:\n" ^
1480          prlist_with_sepi "\n"
1481           (fun i (_,_,mc) -> pr_new_goals i mc) res' ^
1482          "\nThe first set is randomly chosen. Use the syntax " ^
1483          "\"setoid_rewrite ... generate side conditions ...\" to choose " ^
1484          "a different set.") ;
1485       he
1486
1487 let cic_morphism_context_list_of_list hole_relation hole_direction out_direction
1488 =
1489  let check =
1490   function
1491      (None,dir,dir') ->
1492       Cic.Appl [coq_MSNone ; dir ; dir']
1493    | (Some true,dir,dir') ->
1494       assert (dir = dir');
1495       Cic.Appl [coq_MSCovariant ; dir]
1496    | (Some false,dir,dir') ->
1497       assert (dir <> dir');
1498       Cic.Appl [coq_MSContravariant ; dir] in
1499  let rec aux =
1500   function
1501      [] -> assert false
1502    | [(variance,out),(value,direction)] ->
1503       Cic.Appl [coq_singl ; coq_Argument_Class ; out],
1504       Cic.Appl
1505        [coq_fcl_singl;
1506         hole_relation; hole_direction ; out ;
1507         direction ; out_direction ;
1508         check (variance,direction,out_direction) ; value]
1509    | ((variance,out),(value,direction))::tl ->
1510       let outtl, valuetl = aux tl in
1511        Cic.Appl
1512         [coq_cons; coq_Argument_Class ; out ; outtl],
1513        Cic.Appl
1514         [coq_fcl_cons;
1515          hole_relation ; hole_direction ; out ; outtl ;
1516          direction ; out_direction ;
1517          check (variance,direction,out_direction) ;
1518          value ; valuetl]
1519  in aux
1520
1521 let rec cic_type_nelist_of_list =
1522  function
1523     [] -> assert false
1524   | [value] ->
1525       Cic.Appl [coq_singl; Cic.Sort (Cic.Type (CicUniv.fresh ())) ; value]
1526   | value::tl ->
1527      Cic.Appl
1528       [coq_cons; Cic.Sort (Cic.Type (CicUniv.fresh ())); value;
1529        cic_type_nelist_of_list tl]
1530
1531 let syntactic_but_representation_of_marked_but hole_relation hole_direction =
1532  let rec aux out (rel_out,precise_out,is_reflexive) =
1533   function
1534      MApp (f, m, args, direction) ->
1535       let direction = cic_direction_of_direction direction in
1536       let morphism_theory, relations =
1537        match m with
1538           ACMorphism { args = args ; morphism_theory = morphism_theory } ->
1539            morphism_theory,args
1540         | ACFunction { f_args = f_args ; f_output = f_output } ->
1541            let mt =
1542             if (*COQ eq_constr out (cic_relation_class_of_relation_class
1543               coq_iff_relation)*) assert false
1544             then
1545               Cic.Appl
1546                [coq_morphism_theory_of_predicate;
1547                 cic_type_nelist_of_list f_args; f]
1548             else
1549               Cic.Appl
1550                [coq_morphism_theory_of_function;
1551                 cic_type_nelist_of_list f_args; f_output; f]
1552            in
1553             mt,List.map (fun x -> None,Leibniz (Some x)) f_args in
1554       let cic_relations =
1555        List.map
1556         (fun (variance,r) ->
1557           variance,
1558           r,
1559           cic_relation_class_of_relation_class r,
1560           cic_precise_relation_class_of_relation_class r
1561         ) relations in
1562       let cic_args_relations,argst =
1563        cic_morphism_context_list_of_list hole_relation hole_direction direction
1564         (List.map2
1565          (fun (variance,trel,t,precise_t) v ->
1566            (variance,cic_argument_class_of_argument_class (variance,trel)),
1567              (aux t precise_t v,
1568                direction_of_constr_with_marks hole_direction v)
1569          ) cic_relations args)
1570       in
1571        Cic.Appl
1572         [coq_App;
1573          hole_relation ; hole_direction ;
1574          cic_args_relations ; out ; direction ;
1575          morphism_theory ; argst]
1576    | ToReplace ->
1577       Cic.Appl [coq_ToReplace ; hole_relation ; hole_direction]
1578    | ToKeep (c,_,direction) ->
1579       let direction = cic_direction_of_direction direction in
1580        if is_reflexive then
1581         Cic.Appl
1582          [coq_ToKeep ; hole_relation ; hole_direction ; precise_out ;
1583           direction ; c]
1584        else
1585         let c_is_proper =
1586          let typ = Cic.Appl [rel_out ; c ; c] in
1587           Cic.Cast ((*COQ Evarutil.mk_new_meta ()*)assert false, typ)
1588         in
1589          Cic.Appl
1590           [coq_ProperElementToKeep ;
1591            hole_relation ; hole_direction; precise_out ;
1592            direction; c ; c_is_proper]
1593  in aux
1594
1595 let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h)
1596  prop_direction m
1597 =
1598  let hole_relation = cic_relation_class_of_relation_class hole_relation in
1599  let hyp,hole_direction = h,cic_direction_of_direction direction in
1600  let cic_prop_relation = cic_relation_class_of_relation_class prop_relation in
1601  let precise_prop_relation =
1602   cic_precise_relation_class_of_relation_class prop_relation
1603  in
1604   Cic.Appl
1605    [coq_setoid_rewrite;
1606     hole_relation ; hole_direction ; cic_prop_relation ;
1607     prop_direction ; c1 ; c2 ;
1608     syntactic_but_representation_of_marked_but hole_relation hole_direction
1609     cic_prop_relation precise_prop_relation m ; hyp]
1610
1611 (*COQ
1612 let check_evar_map_of_evars_defs evd =
1613  let metas = Evd.meta_list evd in
1614  let check_freemetas_is_empty rebus =
1615   Evd.Metaset.iter
1616    (fun m ->
1617      if Evd.meta_defined evd m then () else
1618       raise (Logic.RefinerError (Logic.OccurMetaGoal rebus)))
1619  in
1620   List.iter
1621    (fun (_,binding) ->
1622      match binding with
1623         Evd.Cltyp (_,{Evd.rebus=rebus; Evd.freemetas=freemetas}) ->
1624          check_freemetas_is_empty rebus freemetas
1625       | Evd.Clval (_,{Evd.rebus=rebus1; Evd.freemetas=freemetas1},
1626                  {Evd.rebus=rebus2; Evd.freemetas=freemetas2}) ->
1627          check_freemetas_is_empty rebus1 freemetas1 ;
1628          check_freemetas_is_empty rebus2 freemetas2
1629    ) metas
1630 *)
1631
1632 (* For a correct meta-aware "rewrite in", we split unification
1633    apart from the actual rewriting (Pierre L, 05/04/06) *)
1634
1635 (* [unification_rewrite] searchs a match for [c1] in [but] and then
1636    returns the modified objects (in particular [c1] and [c2]) *)
1637
1638 let unification_rewrite c1 c2 cl but gl =
1639 (*COQ
1640   let (env',c1) =
1641     try
1642       (* ~mod_delta:false to allow to mark occurences that must not be
1643          rewritten simply by replacing them with let-defined definitions
1644          in the context *)
1645       w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env
1646     with
1647         Pretype_errors.PretypeError _ ->
1648           (* ~mod_delta:true to make Ring work (since it really
1649              exploits conversion) *)
1650           w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.env
1651   in
1652   let cl' = {cl with env = env' } in
1653   let c2 = Clenv.clenv_nf_meta cl' c2 in
1654   check_evar_map_of_evars_defs env' ;
1655   env',Clenv.clenv_value cl', c1, c2
1656 *) assert false
1657
1658 (* no unification is performed in this function. [sigma] is the
1659  substitution obtained from an earlier unification. *)
1660
1661 let relation_rewrite_no_unif c1 c2 hyp ~new_goals sigma gl =
1662   let but = (*COQ pf_concl gl*) assert false in
1663   try
1664    let input_relation =
1665     relation_class_that_matches_a_constr "Setoid_rewrite"
1666      new_goals ((*COQTyping.mtype_of (pf_env gl) sigma (snd hyp)*) assert false) in
1667    let output_relation,output_direction,marked_but =
1668     mark_occur gl ~new_goals c1 but input_relation (fst hyp) in
1669    let cic_output_direction = cic_direction_of_direction output_direction in
1670    let if_output_relation_is_iff gl =
1671     let th =
1672      apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
1673       cic_output_direction marked_but
1674     in
1675      let new_but = (*COQ Termops.replace_term c1 c2 but*) assert false in
1676      let hyp1,hyp2,proj =
1677       match output_direction with
1678          Right2Left -> new_but, but, coq_proj1
1679        | Left2Right -> but, new_but, coq_proj2
1680      in
1681      let impl1 = Cic.Prod (Cic.Anonymous, hyp2, CicSubstitution.lift 1 hyp1) in
1682      let impl2 = Cic.Prod (Cic.Anonymous, hyp1, CicSubstitution.lift 1 hyp2) in
1683       let th' = Cic.Appl [proj; impl2; impl1; th] in
1684        (*COQ Tactics.refine
1685         (Cic.Appl [th'; mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)])
1686         gl*) let _ = th' in assert false in
1687    let if_output_relation_is_if gl =
1688     let th =
1689      apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
1690       cic_output_direction marked_but
1691     in
1692      let new_but = (*COQ Termops.replace_term c1 c2 but*) assert false in
1693       (*COQ Tactics.refine
1694        (Cic.Appl [th ; mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)])
1695        gl*) let _ = new_but,th in assert false in
1696    if output_relation = coq_iff_relation then
1697      if_output_relation_is_iff gl
1698    else
1699      if_output_relation_is_if gl
1700   with
1701     Optimize ->
1702       (*COQ !general_rewrite (fst hyp = Left2Right) (snd hyp) gl*) assert false
1703
1704 let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
1705  let (sigma,cl,c1,c2) = unification_rewrite c1 c2 cl ((*COQ pf_concl gl*) assert false) gl in
1706  relation_rewrite_no_unif c1 c2 (input_direction,cl) ~new_goals sigma gl
1707
1708 let analyse_hypothesis gl c =
1709  let ctype = (*COQ pf_type_of gl c*) assert false in
1710  let eqclause  = (*COQ Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings*) let _ = ctype in assert false in
1711  let (equiv, args) = (*COQ decompose_app (Clenv.clenv_type eqclause)*) assert false in
1712  let rec split_last_two = function
1713    | [c1;c2] -> [],(c1, c2)
1714    | x::y::z ->
1715       let l,res = split_last_two (y::z) in x::l, res
1716    | _ -> raise (ProofEngineTypes.Fail (lazy "The term provided is not an equivalence")) in
1717  let others,(c1,c2) = split_last_two args in
1718   eqclause,Cic.Appl (equiv::others),c1,c2
1719
1720 let general_s_rewrite lft2rgt c ~new_goals (*COQgl*) =
1721 (*COQ
1722   let eqclause,_,c1,c2 = analyse_hypothesis gl c in
1723   if lft2rgt then
1724     relation_rewrite c1 c2 (Left2Right,eqclause) ~new_goals gl
1725   else
1726     relation_rewrite c2 c1 (Right2Left,eqclause) ~new_goals gl
1727 *) assert false
1728
1729 let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl =
1730  let hyp = (*COQ pf_type_of gl (mkVar id)*) assert false in
1731  (* first, we find a match for c1 in the hyp *)
1732  let (sigma,cl,c1,c2) = unification_rewrite c1 c2 eqclause hyp gl in
1733  (* since we will actually rewrite in the opposite direction, we also need
1734     to replace every occurrence of c2 (resp. c1) in hyp with something that
1735     is convertible but not syntactically equal. To this aim we introduce a
1736     let-in and then we will use the intro tactic to get rid of it.
1737     Quite tricky to do properly since c1 can occur in c2 or vice-versa ! *)
1738  let mangled_new_hyp =
1739    let hyp = CicSubstitution.lift 2 hyp in
1740    (* first, we backup every occurences of c1 in newly allocated (Rel 1) *)
1741    let hyp = (*COQ Termops.replace_term (CicSubstitution.lift 2 c1) (Cic.Rel 1) hyp*) let _ = hyp in assert false in
1742    (* then, we factorize every occurences of c2 into (Rel 2) *)
1743    let hyp = (*COQ Termops.replace_term (CicSubstitution.lift 2 c2) (Cic.Rel 2) hyp*) let _ = hyp in assert false in
1744    (* Now we substitute (Rel 1) (i.e. c1) for c2 *)
1745    let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in
1746    (* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels,
1747       Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
1748    Cic.LetIn (Cic.Anonymous,c2,assert false,hyp)
1749  in
1750  let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in
1751  let oppdir = opposite_direction direction in
1752 (*COQ
1753  cut_replacing id new_hyp
1754    (tclTHENLAST
1755       (tclTHEN (change_in_concl None mangled_new_hyp)
1756          (tclTHEN intro
1757             (relation_rewrite_no_unif c2 c1 (oppdir,cl) ~new_goals sigma))))
1758    gl
1759 *) let _ = oppdir,new_hyp,mangled_new_hyp in assert false
1760
1761 let general_s_rewrite_in id lft2rgt c ~new_goals (*COQgl*) =
1762 (*COQ
1763   let eqclause,_,c1,c2 = analyse_hypothesis gl c in
1764   if lft2rgt then
1765     relation_rewrite_in id c1 c2 (Left2Right,eqclause) ~new_goals gl
1766   else
1767     relation_rewrite_in id c2 c1 (Right2Left,eqclause) ~new_goals gl
1768 *) assert false
1769
1770 let setoid_replace relation c1 c2 ~new_goals (*COQgl*) =
1771  try
1772   let relation =
1773    match relation with
1774       Some rel ->
1775        (try
1776          match find_relation_class rel with
1777             Relation sa -> sa
1778           | Leibniz _ -> raise Optimize
1779         with
1780          Not_found ->
1781           raise (ProofEngineTypes.Fail (lazy
1782            (CicPp.ppterm rel ^ " is not a registered relation."))))
1783     | None ->
1784        match default_relation_for_carrier ((*COQ pf_type_of gl c1*) assert false) with
1785           Relation sa -> sa
1786         | Leibniz _ -> raise Optimize
1787   in
1788    let eq_left_to_right = Cic.Appl [relation.rel_aeq; c1 ; c2] in
1789    let eq_right_to_left = Cic.Appl [relation.rel_aeq; c2 ; c1] in
1790 (*COQ
1791    let replace dir eq =
1792     tclTHENS (assert_tac false Cic.Anonymous eq)
1793       [onLastHyp (fun id ->
1794         tclTHEN
1795           (general_s_rewrite dir (mkVar id) ~new_goals)
1796           (clear [id]));
1797        Tacticals.tclIDTAC]
1798    in
1799     tclORELSE
1800      (replace true eq_left_to_right) (replace false eq_right_to_left) gl
1801 *) let _ = eq_left_to_right,eq_right_to_left in assert false
1802  with
1803   Optimize -> (*COQ (!replace c1 c2) gl*) assert false
1804
1805 let setoid_replace_in id relation c1 c2 ~new_goals (*COQgl*) =
1806 (*COQ
1807  let hyp = pf_type_of gl (mkVar id) in
1808  let new_hyp = Termops.replace_term c1 c2 hyp in
1809  cut_replacing id new_hyp
1810    (fun exact -> tclTHENLASTn
1811      (setoid_replace relation c2 c1 ~new_goals)
1812      [| exact; tclIDTAC |]) gl
1813 *) assert false
1814
1815 (* [setoid_]{reflexivity,symmetry,transitivity} tactics *)
1816
1817 let setoid_reflexivity_tac =
1818  let tac ((proof,goal) as status) =
1819   let (_,metasenv,_subst,_,_, _) = proof in
1820   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1821    try
1822     let relation_class =
1823      relation_class_that_matches_a_constr "Setoid_reflexivity" [] ty in
1824     match relation_class with
1825        Leibniz _ -> assert false (* since [] is empty *)
1826      | Relation rel ->
1827         match rel.rel_refl with
1828            None ->
1829             raise (ProofEngineTypes.Fail (lazy
1830              ("The relation " ^ prrelation rel ^ " is not reflexive.")))
1831          | Some refl ->
1832             ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac refl)
1833              status
1834    with
1835     Optimize ->
1836      ProofEngineTypes.apply_tactic EqualityTactics.reflexivity_tac status
1837  in
1838   ProofEngineTypes.mk_tactic tac
1839
1840 let setoid_symmetry  =
1841  let tac status =
1842   try
1843    let relation_class =
1844     relation_class_that_matches_a_constr "Setoid_symmetry"
1845      [] ((*COQ pf_concl gl*) assert false) in
1846    match relation_class with
1847       Leibniz _ -> assert false (* since [] is empty *)
1848     | Relation rel ->
1849        match rel.rel_sym with
1850           None ->
1851            raise (ProofEngineTypes.Fail (lazy
1852             ("The relation " ^ prrelation rel ^ " is not symmetric.")))
1853         | Some sym -> (*COQ apply sym gl*) assert false
1854   with
1855    Optimize -> (*COQ symmetry gl*) assert false
1856  in
1857   ProofEngineTypes.mk_tactic tac
1858
1859 let setoid_symmetry_in id (*COQgl*) =
1860 (*COQ
1861  let new_hyp =
1862   let _,he,c1,c2 = analyse_hypothesis gl (mkVar id) in
1863    Cic.Appl [he ; c2 ; c1]
1864  in
1865  cut_replacing id new_hyp (tclTHEN setoid_symmetry) gl
1866 *) assert false
1867
1868 let setoid_transitivity c (*COQgl*) =
1869  try
1870   let relation_class =
1871    relation_class_that_matches_a_constr "Setoid_transitivity"
1872     [] ((*COQ pf_concl gl*) assert false) in
1873   match relation_class with
1874      Leibniz _ -> assert false (* since [] is empty *)
1875    | Relation rel ->
1876 (*COQ
1877       let ctyp = pf_type_of gl c in
1878       let rel' = unify_relation_carrier_with_type (pf_env gl) rel ctyp in
1879        match rel'.rel_trans with
1880           None ->
1881            raise (ProofEngineTypes.Fail (lazy
1882             ("The relation " ^ prrelation rel ^ " is not transitive.")))
1883         | Some trans ->
1884            let transty = nf_betaiota (pf_type_of gl trans) in
1885            let argsrev, _ =
1886             Reductionops.decomp_n_prod (pf_env gl) Evd.empty 2 transty in
1887            let binder =
1888             match List.rev argsrev with
1889                _::(Name n2,None,_)::_ -> Rawterm.NamedHyp n2
1890              | _ -> assert false
1891            in
1892             apply_with_bindings
1893              (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
1894 *) assert false
1895  with
1896   Optimize -> (*COQ transitivity c gl*) assert false
1897 ;;
1898
1899 (*COQ
1900 Tactics.register_setoid_reflexivity setoid_reflexivity;;
1901 Tactics.register_setoid_symmetry setoid_symmetry;;
1902 Tactics.register_setoid_symmetry_in setoid_symmetry_in;;
1903 Tactics.register_setoid_transitivity setoid_transitivity;;
1904 *)