helm/software/components/tactics/setoids.ml

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