(* $Id: setoid_replace.ml 8900 2006-06-06 14:40:27Z letouzey $ *)
+module T = Tacticals
+module RT = ReductionTactics
+module PET = ProofEngineTypes
+
let default_eq () =
match LibraryObjects.eq_URI () with
Some uri -> uri
(*COQ
let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s
-*) let constant dir s = assert false
+*) let constant dir s = Cic.Implicit None
(*COQ
let gen_constant dir s = Coqlib.gen_constant "Setoid_replace" dir s
-*) let gen_constant dir s = assert false
+*) let gen_constant dir s = Cic.Implicit None
(*COQ
let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s
let eval_reference dir s = EvalConstRef (destConst (constant dir s))
-*) let eval_reference dir s = assert false
+*) let eval_reference dir s = Cic.Implicit None
(*COQ
let eval_init_reference dir s = EvalConstRef (destConst (gen_constant ("Init"::dir) s))
*)
try
global_reference id
with Not_found ->
- anomaly ("Setoid: cannot find " ^ (string_of_id id))
+ anomaly ("Setoid: cannot find " ^ id)
*) let current_constant id = assert false
(* From Setoid.v *)
(*COQ
let coq_iff_relation = lazy (find_relation_class (Lazy.force coq_iff))
let coq_impl_relation = lazy (find_relation_class (Lazy.force coq_impl))
-*) let coq_iff_relation = assert false let coq_impl_relation = assert false
+*) let coq_iff_relation = Obj.magic 0 let coq_impl_relation = Obj.magic 0
let relation_morphism_of_constr_morphism =
let relation_relation_class_of_constr_relation_class =
(* Declare a new type of object in the environment : "relation-theory". *)
-(*COQ
-let (relation_to_obj, obj_to_relation)=
- let cache_set (_,(s, th)) =
+let relation_to_obj (s, th) =
let th' =
if relation_table_mem s then
begin
{th with rel_sym =
match th.rel_sym with
None -> old_relation.rel_sym
- | Some t -> Some t} in
-(*COQ
+ | Some t -> Some t}
+ in
prerr_endline
("Warning: The relation " ^ prrelation th' ^
" is redeclared. The new declaration" ^
(if old_relation.rel_refl <> None && old_relation.rel_sym <> None
then ")" else "") ^
".");
-*)
th'
end
else
th
in
relation_table_add (s,th')
- and export_set x = Some x
- in
- declare_object {(default_object "relation-theory") with
- cache_function = cache_set;
- load_function = (fun i o -> cache_set o);
- subst_function = subst_set;
- classify_function = (fun (_,x) -> Substitute x);
- export_function = export_set}
-*)
(******************************* Table of declared morphisms ********************)
let argsno = List.length args' - rel.rel_quantifiers_no in
let args1 = list_sub args' 0 argsno in
let args2 = list_sub args' argsno rel.rel_quantifiers_no in
- if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1)) CicUniv.empty_ugraph) then
+ if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1))
+ CicUniv.oblivion_ugraph) then
args2
else
raise_error rel.rel_quantifiers_no
| _ ->
- if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] rel.rel_a t CicUniv.empty_ugraph) then
+ if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible []
+ rel.rel_a t CicUniv.oblivion_ugraph) then
[]
else
begin
(*COQ
let evars,args,instantiated_rel_a =
- let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a CicUniv.empty_ugraph in
+ let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a
+ CicUniv.oblivion_ugraph in
let evd = Evd.create_evar_defs Evd.empty in
let evars,args,concl =
Clenv.clenv_environments_evars env evd
let unify_relation_class_carrier_with_type env rel t =
match rel with
Leibniz (Some t') ->
- if fst (CicReduction.are_convertible [] t t' CicUniv.empty_ugraph) then
+ if fst (CicReduction.are_convertible [] t t' CicUniv.oblivion_ugraph) then
rel
else
raise (ProofEngineTypes.Fail (lazy
(************************** Adding a relation to the database *********************)
+let check_a a =
(*COQ
-let check_a env a =
let typ = Typing.type_of env Evd.empty a in
let a_quantifiers_rev,_ = Reduction.dest_arity env typ in
a_quantifiers_rev
+*) assert false
-let check_eq env a_quantifiers_rev a aeq =
+let check_eq a_quantifiers_rev a aeq =
+(*COQ
let typ =
Sign.it_mkProd_or_LetIn
(Cic.Appl [coq_relation ; apply_to_rels a a_quantifiers_rev])
then
raise (ProofEngineTypes.Fail (lazy
(CicPp.ppterm aeq ^ " should have type (" ^ CicPp.ppterm typ ^ ")")))
+*) (assert false : unit)
-let check_property env a_quantifiers_rev a aeq strprop coq_prop t =
+let check_property a_quantifiers_rev a aeq strprop coq_prop t =
+(*COQ
if
not
(is_conv env Evd.empty (Typing.type_of env Evd.empty t)
then
raise (ProofEngineTypes.Fail (lazy
("Not a valid proof of " ^ strprop ^ ".")))
+*) assert false
-let check_refl env a_quantifiers_rev a aeq refl =
- check_property env a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl
+let check_refl a_quantifiers_rev a aeq refl =
+ check_property a_quantifiers_rev a aeq "reflexivity" coq_reflexive refl
-let check_sym env a_quantifiers_rev a aeq sym =
- check_property env a_quantifiers_rev a aeq "symmetry" coq_symmetric sym
+let check_sym a_quantifiers_rev a aeq sym =
+ check_property a_quantifiers_rev a aeq "symmetry" coq_symmetric sym
-let check_trans env a_quantifiers_rev a aeq trans =
- check_property env a_quantifiers_rev a aeq "transitivity" coq_transitive trans
+let check_trans a_quantifiers_rev a aeq trans =
+ check_property a_quantifiers_rev a aeq "transitivity" coq_transitive trans
+;;
let int_add_relation id a aeq refl sym trans =
+(*COQ
let env = Global.env () in
- let a_quantifiers_rev = check_a env a in
- check_eq env a_quantifiers_rev a aeq ;
- option_iter (check_refl env a_quantifiers_rev a aeq) refl ;
- option_iter (check_sym env a_quantifiers_rev a aeq) sym ;
- option_iter (check_trans env a_quantifiers_rev a aeq) trans ;
+*)
+ let a_quantifiers_rev = check_a a in
+ check_eq a_quantifiers_rev a aeq ;
+ HExtlib.iter_option (check_refl a_quantifiers_rev a aeq) refl ;
+ HExtlib.iter_option (check_sym a_quantifiers_rev a aeq) sym ;
+ HExtlib.iter_option (check_trans a_quantifiers_rev a aeq) trans ;
let quantifiers_no = List.length a_quantifiers_rev in
let aeq_rel =
{ rel_a = a;
rel_X_relation_class = Cic.Sort Cic.Prop; (* dummy value, overwritten below *)
rel_Xreflexive_relation_class = Cic.Sort Cic.Prop (* dummy value, overwritten below *)
} in
- let x_relation_class =
+ let _x_relation_class =
let subst =
let len = List.length a_quantifiers_rev in
list_map_i (fun i _ -> Cic.Rel (len - i + 2)) 0 a_quantifiers_rev in
cic_relation_class_of_X_relation
(Cic.Rel 2) (Cic.Rel 1) (apply_to_relation subst aeq_rel) in
let _ =
+(*COQ
Declare.declare_internal_constant id
(DefinitionEntry
{const_entry_body =
Sign.it_mkLambda_or_LetIn x_relation_class
- ([ Name (id_of_string "v"),None,Cic.Rel 1;
- Name (id_of_string "X"),None,Cic.Sort (Cic.Type (CicUniv.fresh ()))] @
+ ([ Name "v",None,Cic.Rel 1;
+ Name "X",None,Cic.Sort (Cic.Type (CicUniv.fresh ()))] @
a_quantifiers_rev);
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()},
IsDefinition Definition) in
- let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in
- let xreflexive_relation_class =
+*) () in
+ let id_precise = id ^ "_precise_relation_class" in
+ let _xreflexive_relation_class =
let subst =
let len = List.length a_quantifiers_rev in
list_map_i (fun i _ -> Cic.Rel (len - i)) 0 a_quantifiers_rev
in
cic_precise_relation_class_of_relation (apply_to_relation subst aeq_rel) in
let _ =
+(*COQ
Declare.declare_internal_constant id_precise
(DefinitionEntry
{const_entry_body =
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions() },
IsDefinition Definition) in
+*) () in
let aeq_rel =
{ aeq_rel with
rel_X_relation_class = current_constant id;
rel_Xreflexive_relation_class = current_constant id_precise } in
- Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ;
- Options.if_verbose prerr_endline (CicPp.ppterm aeq ^ " is registered as a relation");
+ relation_to_obj (aeq, aeq_rel) ;
+ prerr_endline (CicPp.ppterm aeq ^ " is registered as a relation");
match trans with
None -> ()
| Some trans ->
- let mor_name = id_of_string (string_of_id id ^ "_morphism") in
+ let mor_name = id ^ "_morphism" in
let a_instance = apply_to_rels a a_quantifiers_rev in
let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
let sym_instance =
trans_instance],
coq_iff_relation in
let _ =
+(*COQ
Declare.declare_internal_constant mor_name
(DefinitionEntry
{const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()},
IsDefinition Definition)
+*) ()
in
let a_quantifiers_rev =
List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in
add_morphism None mor_name
(aeq,a_quantifiers_rev,[aeq_rel_class_and_var1; aeq_rel_class_and_var2],
output)
-*)
(* The vernac command "Add Relation ..." *)
let add_relation id a aeq refl sym trans =
-(*COQ
- int_add_relation id (constr_of a) (constr_of aeq) (HExtlib.map_option constr_of refl)
- (HExtlib.map_option constr_of sym) (HExtlib.map_option constr_of trans)
-*) assert false
+ int_add_relation id a aeq refl sym trans
(****************************** The tactic itself *******************************)
let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in
(* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels,
Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
- Cic.LetIn (Cic.Anonymous,c2,hyp)
+ Cic.LetIn (Cic.Anonymous,c2,assert false,hyp)
in
let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in
let oppdir = opposite_direction direction in
(* [setoid_]{reflexivity,symmetry,transitivity} tactics *)
-let setoid_reflexivity (*COQgl*) =
- try
- let relation_class =
- relation_class_that_matches_a_constr "Setoid_reflexivity"
- [] ((*COQ pf_concl gl*) assert false) in
- match relation_class with
- Leibniz _ -> assert false (* since [] is empty *)
- | Relation rel ->
- match rel.rel_refl with
- None ->
- raise (ProofEngineTypes.Fail (lazy
- ("The relation " ^ prrelation rel ^ " is not reflexive.")))
- | Some refl -> (*COQ apply refl gl*) assert false
- with
- Optimize -> (*COQ reflexivity gl*) assert false
+let setoid_reflexivity_tac =
+ let tac ((proof,goal) as status) =
+ let (_,metasenv,_subst,_,_, _) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ try
+ let relation_class =
+ relation_class_that_matches_a_constr "Setoid_reflexivity" [] ty in
+ match relation_class with
+ Leibniz _ -> assert false (* since [] is empty *)
+ | Relation rel ->
+ match rel.rel_refl with
+ None ->
+ raise (ProofEngineTypes.Fail (lazy
+ ("The relation " ^ prrelation rel ^ " is not reflexive.")))
+ | Some refl ->
+ ProofEngineTypes.apply_tactic (PrimitiveTactics.apply_tac refl)
+ status
+ with
+ Optimize ->
+ ProofEngineTypes.apply_tactic EqualityTactics.reflexivity_tac status
+ in
+ ProofEngineTypes.mk_tactic tac
-let setoid_symmetry (*COQgl*) =
- try
- let relation_class =
- relation_class_that_matches_a_constr "Setoid_symmetry"
- [] ((*COQ pf_concl gl*) assert false) in
- match relation_class with
- Leibniz _ -> assert false (* since [] is empty *)
- | Relation rel ->
- match rel.rel_sym with
- None ->
- raise (ProofEngineTypes.Fail (lazy
- ("The relation " ^ prrelation rel ^ " is not symmetric.")))
- | Some sym -> (*COQ apply sym gl*) assert false
- with
- Optimize -> (*COQ symmetry gl*) assert false
+let setoid_reflexivity_tac =
+ let start_tac = RT.whd_tac ~pattern:(PET.conclusion_pattern None) in
+ let fail_tac = T.then_ ~start:start_tac ~continuation:setoid_reflexivity_tac in
+ T.if_ ~start:setoid_reflexivity_tac ~continuation:T.id_tac ~fail:fail_tac
+
+let setoid_symmetry =
+ let tac status =
+ try
+ let relation_class =
+ relation_class_that_matches_a_constr "Setoid_symmetry"
+ [] ((*COQ pf_concl gl*) assert false) in
+ match relation_class with
+ Leibniz _ -> assert false (* since [] is empty *)
+ | Relation rel ->
+ match rel.rel_sym with
+ None ->
+ raise (ProofEngineTypes.Fail (lazy
+ ("The relation " ^ prrelation rel ^ " is not symmetric.")))
+ | Some sym -> (*COQ apply sym gl*) assert false
+ with
+ Optimize -> (*COQ symmetry gl*) assert false
+ in
+ ProofEngineTypes.mk_tactic tac
let setoid_symmetry_in id (*COQgl*) =
(*COQ
projects / helm.git / blobdiff