aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/setoid_replace.ml679
-rw-r--r--tactics/setoid_replace.mli7
2 files changed, 448 insertions, 238 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 0a35282b74..44203278b3 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -30,19 +30,46 @@ open Nametab
open Decl_kinds
open Constrintern
+let replace = ref (fun _ _ -> assert false)
+let register_replace f = replace := f
+
type setoid =
{ set_a : constr;
set_aeq : constr;
set_th : constr
}
-type morphism =
+type 'a setoid_class =
+ ACSetoid of 'a (*the equivalence relation of the setoid or the setoid*)
+ | ACLeibniz of constr (*the carrier of the setoid*)
+
+type 'a morphism =
{ lem : constr;
- profil : bool list;
- arg_types : constr list;
+ args : 'a setoid_class list;
+ output : 'a setoid_class;
lem2 : constr option
}
+type funct =
+ { f_args : constr list;
+ f_output : constr
+ }
+
+type morphism_class =
+ ACMorphism of setoid morphism
+ | ACFunction of funct
+
+let subst_mps_in_setoid_class subst =
+ function
+ ACSetoid t -> ACSetoid (subst_mps subst t)
+ | ACLeibniz t -> ACLeibniz (subst_mps subst t)
+
+let constr_setoid_class_of_setoid_setoid_class =
+ function
+ ACSetoid setoid -> ACSetoid setoid.set_aeq
+ | ACLeibniz t -> ACLeibniz t
+
+
let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s
@@ -53,7 +80,7 @@ let current_constant id =
try
global_reference id
with Not_found ->
- anomaly ("Setoid: cannot find "^(string_of_id id))
+ anomaly ("Setoid: cannot find " ^ (string_of_id id))
(* Setoid_theory *)
@@ -67,6 +94,8 @@ let coq_fleche = lazy(constant ["Setoid"] "fleche")
(* Coq constants *)
+let coqiff = lazy(global_constant ["Logic"] "iff")
+
let coqeq = lazy(global_constant ["Logic"] "eq")
let coqconj = lazy(global_constant ["Logic"] "conj")
@@ -79,14 +108,56 @@ let coqproj2 = lazy(global_constant ["Logic"] "proj2")
(* Setoids are stored in a table which is synchronised with the Reset mechanism. *)
-module Cmap = Map.Make(struct type t = constr let compare = compare end)
-
let setoid_table = ref Gmap.empty
let setoid_table_add (s,th) = setoid_table := Gmap.add s th !setoid_table
let setoid_table_find s = Gmap.find s !setoid_table
let setoid_table_mem s = Gmap.mem s !setoid_table
+let prsetoid s =
+ str "(" ++ prterm s.set_a ++ str "," ++ prterm s.set_aeq ++ str ")"
+
+let prsetoid_class =
+ function
+ ACSetoid eq ->
+ (try prsetoid (setoid_table_find eq)
+ with Not_found ->
+ str "[[ Error: setoid on equality " ++ prterm eq ++ str " not found! ]]")
+ | ACLeibniz ty -> prterm ty
+
+let prmorphism k m =
+ prterm k ++ str ": " ++
+ prlist_with_sep (fun () -> str " -> ") prsetoid_class m.args ++
+ str " -> " ++ prsetoid_class m.output
+
+
+(* A function that gives back the only setoid on a given carrier *)
+(*CSC: this implementation is really inefficient. I should define a new
+ map to make it efficient. However, is this really worth of? *)
+let default_setoid_for_carrier a =
+ let rng = Gmap.rng !setoid_table in
+ match List.filter (fun {set_a=set_a} -> set_a = a) rng with
+ [] -> ACLeibniz a
+ | setoid::tl ->
+ if tl <> [] then
+ msg_warning
+ (str "There are several setoids whose carrier is " ++ prterm a ++
+ str ". The setoid " ++ prsetoid setoid ++
+ str " is randomly chosen.") ;
+ ACSetoid setoid
+
+let setoid_morphism_of_constr_morphism =
+ let setoid_setoid_class_of_constr_setoid_class =
+ function
+ ACLeibniz t -> ACLeibniz t
+ | ACSetoid aeq ->
+ ACSetoid (try setoid_table_find aeq with Not_found -> assert false)
+ in
+ function mor ->
+ let args' = List.map setoid_setoid_class_of_constr_setoid_class mor.args in
+ let output' = setoid_setoid_class_of_constr_setoid_class mor.output in
+ {mor with args=args' ; output=output'}
+
let subst_setoid subst setoid =
let set_a' = subst_mps subst setoid.set_a in
let set_aeq' = subst_mps subst setoid.set_aeq in
@@ -109,13 +180,23 @@ let _ =
{ Summary.freeze_function = (fun () -> !setoid_table);
Summary.unfreeze_function = (fun t -> setoid_table := t);
Summary.init_function = (fun () -> setoid_table := Gmap .empty);
- Summary.survive_module = false;
+ Summary.survive_module = true;
Summary.survive_section = false }
(* Declare a new type of object in the environment : "setoid-theory". *)
let (setoid_to_obj, obj_to_setoid)=
- let cache_set (_,(s, th)) = setoid_table_add (s,th)
+ let cache_set (_,(s, th)) =
+ if setoid_table_mem s then
+ begin
+ let old_setoid = setoid_table_find s in
+ msg_warning
+ (str "The setoid " ++ prsetoid th ++ str " is redeclared. " ++
+ str "The new declaration justified by " ++
+ prterm th.set_th ++ str " replaces the old declaration justified by "++
+ prterm old_setoid.set_th ++ str ".")
+ end ;
+ setoid_table_add (s,th)
and subst_set (_,subst,(s,th as obj)) =
let s' = subst_mps subst s in
let th' = subst_setoid subst th in
@@ -125,7 +206,7 @@ let (setoid_to_obj, obj_to_setoid)=
in
declare_object {(default_object "setoid-theory") with
cache_function = cache_set;
- open_function = (fun i o -> if i=1 then cache_set o);
+ load_function = (fun i o -> cache_set o);
subst_function = subst_set;
classify_function = (fun (_,x) -> Substitute x);
export_function = export_set}
@@ -136,24 +217,63 @@ let (setoid_to_obj, obj_to_setoid)=
let morphism_table = ref Gmap.empty
-let morphism_table_add (m,c) = morphism_table := Gmap.add m c !morphism_table
let morphism_table_find m = Gmap.find m !morphism_table
-let morphism_table_mem m = Gmap.mem m !morphism_table
+let morphism_table_add (m,c) =
+ let old =
+ try
+ morphism_table_find m
+ with
+ Not_found -> []
+ in
+ try
+ let old_morph =
+ List.find
+ (function mor -> mor.args = c.args && mor.output = c.output) old
+ in
+ msg_warning
+ (str "The morphism " ++ prmorphism m old_morph ++ str " is redeclared. " ++
+ str "The new declaration whose compatibility is granted by " ++
+ prterm c.lem ++
+ (match c.lem2 with None -> str "" | Some t-> str " and " ++ prterm t)
+ ++ str " replaces the old declaration whose" ++
+ str " compatibility was granted by " ++
+ prterm old_morph.lem ++
+ (match old_morph.lem2 with
+ None -> str ""
+ | Some t-> str " and "++ prterm t) ++ str ".")
+ with
+ Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table
+
+let find_morphism_fleche () =
+ let fleche_constr = (Lazy.force coq_fleche) in
+ try
+ let mor =
+ List.find
+ (function {args=args; output=output} as morphism ->
+ output = ACSetoid (Lazy.force coqiff) &&
+ List.for_all (function c -> c = ACSetoid (Lazy.force coqiff)) args)
+ (morphism_table_find fleche_constr)
+ in
+ setoid_morphism_of_constr_morphism mor
+ with
+ Not_found -> assert false
let subst_morph subst morph =
let lem' = subst_mps subst morph.lem in
- let arg_types' = list_smartmap (subst_mps subst) morph.arg_types in
+ let args' = list_smartmap (subst_mps_in_setoid_class subst) morph.args in
+ let output' = subst_mps_in_setoid_class subst morph.output in
let lem2' = option_smartmap (subst_mps subst) morph.lem2 in
if lem' == morph.lem
- && arg_types' == morph.arg_types
+ && args' == morph.args
+ && output' == morph.output
&& lem2' == morph.lem2
then
morph
else
{ lem = lem' ;
- profil = morph.profil ;
- arg_types = arg_types' ;
- lem2 = lem2' ;
+ args = args' ;
+ output = output' ;
+ lem2 = lem2'
}
@@ -162,7 +282,7 @@ let _ =
{ Summary.freeze_function = (fun () -> !morphism_table);
Summary.unfreeze_function = (fun t -> morphism_table := t);
Summary.init_function = (fun () -> morphism_table := Gmap .empty);
- Summary.survive_module = false;
+ Summary.survive_module = true;
Summary.survive_section = false }
(* Declare a new type of object in the environment : "morphism-definition". *)
@@ -178,26 +298,34 @@ let (morphism_to_obj, obj_to_morphism)=
in
declare_object {(default_object "morphism-definition") with
cache_function = cache_set;
- open_function = (fun i o -> if i=1 then cache_set o);
+ load_function = (fun i o -> cache_set o);
subst_function = subst_set;
classify_function = (fun (_,x) -> Substitute x);
export_function = export_set}
-(************************** Adding a setoid to the database *********************)
+(************************** Printing setoids and morphisms **********************)
+
+let print_setoids () =
+ Gmap.iter
+ (fun k setoid ->
+ assert (k=setoid.set_aeq) ;
+ ppnl (str"Setoid " ++ prsetoid setoid ++ str"; equivalence relation properties granted by " ++
+ prterm setoid.set_th))
+ !setoid_table ;
+ Gmap.iter
+ (fun k l ->
+ List.iter
+ (fun ({lem=lem ; lem2=lem2} as mor) ->
+ ppnl (str "Morphism " ++ prmorphism k mor ++
+ str ". Compatibility granted by " ++
+ prterm lem ++
+ (match lem2 with None -> str"" | Some t -> str " and " ++ prterm t) ++
+ str "."))
+ l) !morphism_table
+;;
-(* Find the setoid theory associated with a given type A.
-This implies that only one setoid theory can be declared for
-a given type A. *)
+(************************** Adding a setoid to the database *********************)
-let find_theory a =
- try
- setoid_table_find a
- with Not_found ->
- errorlabstrm "Setoid"
- (str "No Declared Setoid Theory for " ++
- prterm a ++ fnl () ++
- str "Use Add Setoid to declare it")
-
(* Add a Setoid to the database after a type verification. *)
let eq_lem_common_sign env a eq =
@@ -264,15 +392,12 @@ let gen_eq_lem_name =
make_ident "setoid_eq_ext" (Some !i)
let add_setoid a aeq th =
- if setoid_table_mem a
- then errorlabstrm "Add Setoid"
- (str "A Setoid Theory is already declared for " ++ prterm a)
- else let env = Global.env () in
+ let env = Global.env () in
if (is_conv env Evd.empty (Typing.type_of env Evd.empty th)
(mkApp ((Lazy.force coq_Setoid_Theory), [| a; aeq |])))
then (Lib.add_anonymous_leaf
(setoid_to_obj
- (a, { set_a = a;
+ (aeq, { set_a = a;
set_aeq = aeq;
set_th = th}));
let sym = mkApp ((Lazy.force coq_seq_sym), [|a; aeq; th|]) in
@@ -295,10 +420,10 @@ let add_setoid a aeq th =
let eqmorph = (current_constant eq_ext_name) in
let eqmorph2 = (current_constant eq_ext_name2) in
(Lib.add_anonymous_leaf
- (morphism_to_obj (aeq,
+ (morphism_to_obj (aeq,
{ lem = eqmorph;
- profil = [true; true];
- arg_types = [a;a];
+ args = [ACSetoid aeq; ACSetoid aeq];
+ output = ACSetoid (Lazy.force coqiff);
lem2 = (Some eqmorph2)})));
Options.if_verbose ppnl (prterm aeq ++str " is registered as a morphism"))
else errorlabstrm "Add Setoid" (str "Not a valid setoid theory")
@@ -314,8 +439,8 @@ let add_setoid a aeq th =
let edited = ref Gmap.empty
-let new_edited id m profil =
- edited := Gmap.add id (m,profil) !edited
+let new_edited id m =
+ edited := Gmap.add id m !edited
let is_edited id =
Gmap.mem id !edited
@@ -341,182 +466,175 @@ let gen_lem_name m = match kind_of_term m with
(id_of_label (label kn)) ((string_of_int i)^(string_of_int j)^"_ext")
| _ -> errorlabstrm "New Morphism" (str "The term " ++ prterm m ++ str "is not a known name")
-let gen_lemma_tail m lisset body n =
- let l = (List.length lisset) in
+let gen_lemma_tail m args body n =
+ let l = (List.length args) in
let a1 = Array.create l (mkRel 0) in
let a2 = Array.create l (mkRel 0) in
let rec aux i n = function
- | true::q ->
+ | (ACSetoid _)::tl ->
a1.(i) <- (mkRel n);
a2.(i) <- (mkRel (n-1));
- aux (i+1) (n-2) q
- | false::q ->
+ aux (i+1) (n-2) tl
+ | (ACLeibniz _)::tl ->
a1.(i) <- (mkRel n);
a2.(i) <- (mkRel n);
- aux (i+1) (n-1) q
+ aux (i+1) (n-1) tl
| [] -> () in
- aux 0 n lisset;
- if (eq_constr body mkProp)
+ aux 0 n args;
+ if (match body with ACSetoid setoid when setoid.set_aeq = Lazy.force coqiff -> true | _ -> false)
then mkArrow (mkApp (m,a1)) (lift 1 (mkApp (m, a2)))
- else if (setoid_table_mem body)
- then mkApp ((setoid_table_find body).set_aeq, [|(mkApp (m, a1)); (mkApp (m, a2))|])
- else mkApp ((Lazy.force coqeq), [|body; (mkApp (m, a1)); (mkApp (m, a2))|])
-
-let gen_lemma_middle m larg lisset body n =
- let rec aux la li i n = match (la, li) with
- | ([], []) -> gen_lemma_tail m lisset body n
- | (t::q, true::lq) ->
- mkArrow (mkApp ((setoid_table_find t).set_aeq,
- [|(mkRel i); (mkRel (i-1))|])) (aux q lq (i-1) (n+1))
- | (t::q, false::lq) -> aux q lq (i-1) n
- | _ -> assert false
- in aux larg lisset n n
-
-let gen_compat_lemma env m body larg lisset =
- let rec aux la li n = match (la, li) with
- | (t::q, true::lq) ->
- prod_create env (t,(prod_create env (t, (aux q lq (n+2)))))
- | (t::q, false::lq) ->
- prod_create env (t, (aux q lq (n+1)))
- | ([],[]) -> gen_lemma_middle m larg lisset body n
- | _ -> assert false
- in aux larg lisset 0
+ else
+ match body with
+ ACSetoid setoid ->
+ mkApp (setoid.set_aeq, [|(mkApp (m, a1)); (mkApp (m, a2))|])
+ | ACLeibniz t ->
+ mkApp ((Lazy.force coqeq), [|t; (mkApp (m, a1)); (mkApp (m, a2))|])
+
+let gen_lemma_middle m args body n =
+ let rec aux i n =
+ function
+ | [] -> gen_lemma_tail m args body n
+ | (ACSetoid setoid)::tl ->
+ let t = setoid.set_a in
+ mkArrow (mkApp (setoid.set_aeq,
+ [|(mkRel i); (mkRel (i-1))|])) (aux (i-1) (n+1) tl)
+ | (ACLeibniz t)::tl -> aux (i-1) n tl
+ in aux n n args
+
+let gen_compat_lemma env m body args =
+ let rec aux n =
+ function
+ (ACSetoid setoid)::tl ->
+ let t = setoid.set_a in
+ prod_create env (t,(prod_create env (t, (aux (n+2) tl))))
+ | (ACLeibniz t)::tl ->
+ prod_create env (t, (aux (n+1) tl))
+ | [] -> gen_lemma_middle m args body n
+ in aux 0 args
let new_morphism m id hook =
- if morphism_table_mem m
- then errorlabstrm "New Morphism"
- (str "The term " ++ prterm m ++ str " is already declared as a morphism")
- else
- let env = Global.env() in
- let typeofm = (Typing.type_of env Evd.empty m) in
- let typ = (nf_betaiota typeofm) in (* nf_bdi avant, mais bug *)
- let (argsrev, body) = (decompose_prod typ) in
- let args = (List.rev argsrev) in
- if (args=[])
- then errorlabstrm "New Morphism"
- (str "The term " ++ prterm m ++ str " is not a product")
- else if (check_is_dependent typ (List.length args))
- then errorlabstrm "New Morphism"
- (str "The term " ++ prterm m ++ str " should not be a dependent product")
- else (
- let args_t = (List.map snd args) in
- let poss = (List.map setoid_table_mem args_t) in
- let lem = (gen_compat_lemma env m body args_t poss) in
- new_edited id m poss;
- Pfedit.start_proof id (IsGlobal (Proof Lemma))
- (Declare.clear_proofs (Global.named_context ()))
- lem hook;
- (Options.if_verbose msg (Pfedit.pr_open_subgoals ())))
-
-let rec sub_bool l1 n = function
+ let env = Global.env() in
+ let typeofm = (Typing.type_of env Evd.empty m) in
+ let typ = (nf_betaiota typeofm) in (* nf_bdi avant, mais bug *)
+ let (argsrev, output) = (decompose_prod typ) in
+ let args_ty = (List.map snd (List.rev argsrev)) in
+ if (args_ty=[])
+ then errorlabstrm "New Morphism"
+ (str "The term " ++ prterm m ++ str " is not a product")
+ else if (check_is_dependent typ (List.length args_ty))
+ then errorlabstrm "New Morphism"
+ (str "The term " ++ prterm m ++ str" should not be a dependent product")
+ else (
+ let args = List.map default_setoid_for_carrier args_ty in
+ let output = default_setoid_for_carrier output in
+ let lem = (gen_compat_lemma env m output args) in
+ new_edited id (m,args,output);
+ Pfedit.start_proof id (IsGlobal (Proof Lemma))
+ (Declare.clear_proofs (Global.named_context ()))
+ lem hook;
+ (Options.if_verbose msg (Pfedit.pr_open_subgoals ())))
+
+let rec sub_bool n = function
| [] -> []
- | true::q -> ((List.hd l1), n)::(sub_bool (List.tl l1) (n-2) q)
- | false::q -> (sub_bool (List.tl l1) (n-1) q)
+ | (ACSetoid setoid)::tl -> (setoid, n)::(sub_bool (n-2) tl)
+ | (ACLeibniz _)::tl -> (sub_bool (n-1) tl)
-let gen_lemma_iff_tail m mext larg lisset n k =
+let gen_lemma_iff_tail m mext args n k =
let a1 = Array.create k (mkRel 0) in
let a2 = Array.create k (mkRel 0) in
- let nb = List.length lisset in
+ let nb = List.length args in
let b1 = Array.create nb (mkRel 0) in
let b2 = Array.create nb (mkRel 0) in
let rec aux i j = function
|[] -> ()
- |true::q ->
+ |(ACSetoid _)::tl ->
(a1.(i) <- (mkRel j);
a1.(i+1) <- (mkRel (j-1));
a2.(i) <- (mkRel (j-1));
a2.(i+1) <- (mkRel j);
- aux (i+2) (j-2) q)
- |false::q ->
+ aux (i+2) (j-2) tl)
+ |(ACLeibniz _)::tl ->
(a1.(i) <- (mkRel j);
a2.(i) <- (mkRel j);
- aux (i+1) (j-1) q) in
+ aux (i+1) (j-1) tl) in
let rec aux2 i j = function
- | (t,p)::q ->
- let th = (setoid_table_find t).set_th
- and equiv = (setoid_table_find t).set_aeq in
- a1.(i) <- (mkRel j);
- a2.(i) <- mkApp ((Lazy.force coq_seq_sym),
- [|t; equiv; th; (mkRel p); (mkRel (p-1)); (mkRel j)|]);
- aux2 (i+1) (j-1) q
+ | ({set_a=a; set_th=th; set_aeq=aeq},p)::tl ->
+ a1.(i) <- (mkRel j);
+ a2.(i) <- mkApp ((Lazy.force coq_seq_sym),
+ [|a; aeq; th; (mkRel p); (mkRel (p-1)); (mkRel j)|]);
+ aux2 (i+1) (j-1) tl
| [] -> () in
let rec aux3 i j = function
- | true::q ->
+ | (ACSetoid _)::tl ->
b1.(i) <- (mkRel j);
b2.(i) <- (mkRel (j-1));
- aux3 (i+1) (j-2) q
- | false::q ->
+ aux3 (i+1) (j-2) tl
+ | (ACLeibniz _)::tl ->
b1.(i) <- (mkRel j);
b2.(i) <- (mkRel j);
- aux3 (i+1) (j-1) q
+ aux3 (i+1) (j-1) tl
| [] -> () in
- aux 0 k lisset;
- aux2 n (k-n) (sub_bool larg k lisset);
- aux3 0 k lisset;
+ aux 0 k args;
+ aux2 n (k-n) (sub_bool k args);
+ aux3 0 k args;
mkApp ((Lazy.force coqconj),
[|(mkArrow (mkApp (m,b1)) (lift 1 (mkApp (m, b2))));
(mkArrow (mkApp (m,b2)) (lift 1 (mkApp (m, b1))));
(mkApp (mext, a1));(mkApp (mext, a2))|])
-let gen_lemma_iff_middle env m mext larg lisset n =
- let rec aux la li i k = match (la, li) with
- | ([], []) -> gen_lemma_iff_tail m mext larg lisset n k
- | (t::q, true::lq) ->
- lambda_create env ((mkApp ((setoid_table_find t).set_aeq, [|(mkRel i); (mkRel (i-1))|])),
- (aux q lq (i-1) (k+1)))
- | (t::q, false::lq) -> aux q lq (i-1) k
- | _ -> assert false
- in aux larg lisset n n
-
-let gen_lem_iff env m mext larg lisset =
- let rec aux la li n = match (la, li) with
- | (t::q, true::lq) ->
- lambda_create env (t,(lambda_create env (t, (aux q lq (n+2)))))
- | (t::q, false::lq) ->
- lambda_create env (t, (aux q lq (n+1)))
- | ([],[]) -> gen_lemma_iff_middle env m mext larg lisset n
- | _ -> assert false
- in aux larg lisset 0
-
-let add_morphism lem_name (m,profil) =
- if morphism_table_mem m
- then errorlabstrm "New Morphism"
- (str "The term " ++ prterm m ++ str " is already declared as a morpism")
- else
- let env = Global.env() in
- let mext = (current_constant lem_name) in
- let typeofm = (Typing.type_of env Evd.empty m) in
- let typ = (nf_betaiota typeofm) in
- let (argsrev, body) = (decompose_prod typ) in
- let args = List.rev argsrev in
- let args_t = (List.map snd args) in
- let poss = (List.map setoid_table_mem args_t) in
- let _ = assert (poss=profil) in
- (if (eq_constr body mkProp)
- then
- (let lem_2 = gen_lem_iff env m mext args_t poss in
- let lem2_name = add_suffix lem_name "2" in
- let _ = Declare.declare_constant lem2_name
- ((DefinitionEntry {const_entry_body = lem_2;
- const_entry_type = None;
- const_entry_opaque = true}),
- IsProof Lemma) in
- let lem2 = (current_constant lem2_name) in
+let gen_lemma_iff_middle env m mext args n =
+ let rec aux i k =
+ function
+ [] -> gen_lemma_iff_tail m mext args n k
+ | (ACSetoid setoid)::tl ->
+ lambda_create env
+ ((mkApp (setoid.set_aeq, [|(mkRel i); (mkRel (i-1))|])),
+ (aux (i-1) (k+1) tl))
+ | (ACLeibniz t)::tl -> aux (i-1) k tl
+ in aux n n args
+
+let gen_lem_iff env m mext args =
+ let rec aux n =
+ function
+ (ACSetoid setoid)::tl ->
+ let t = setoid.set_a in
+ lambda_create env (t,(lambda_create env (t, (aux (n+2) tl))))
+ | (ACLeibniz t)::tl ->
+ lambda_create env (t, (aux (n+1) tl))
+ | [] -> gen_lemma_iff_middle env m mext args n
+ in aux 0 args
+
+let add_morphism lem_name (m,args,output) =
+ let env = Global.env() in
+ let mext = (current_constant lem_name) in
+ let args_constr= List.map constr_setoid_class_of_setoid_setoid_class args in
+ let output_constr = constr_setoid_class_of_setoid_setoid_class output in
+ (if (match output with ACSetoid setoid when setoid.set_aeq = Lazy.force coqiff -> true | _ -> false)
+ then
+ (let lem_2 = gen_lem_iff env m mext args in
+ let lem2_name = add_suffix lem_name "2" in
+ let _ = Declare.declare_constant lem2_name
+ ((DefinitionEntry {const_entry_body = lem_2;
+ const_entry_type = None;
+ const_entry_opaque = true}),
+ IsProof Lemma) in
+ let lem2 = (current_constant lem2_name) in
(Lib.add_anonymous_leaf
(morphism_to_obj (m,
{ lem = mext;
- profil = poss;
- arg_types = args_t;
+ args = args_constr;
+ output = output_constr;
lem2 = (Some lem2)})));
Options.if_verbose message ((string_of_id lem2_name) ^ " is defined"))
- else
- (Lib.add_anonymous_leaf
- (morphism_to_obj (m,
- { lem = mext;
- profil = poss;
- arg_types = args_t;
- lem2 = None}))));
+ else
+ (Lib.add_anonymous_leaf
+ (morphism_to_obj (m,
+ { lem = mext;
+ args = args_constr;
+ output = output_constr;
+ lem2 = None}))));
Options.if_verbose ppnl (prterm m ++str " is registered as a morphism")
+
let morphism_hook stre ref =
let pf_id = id_of_global ref in
if (is_edited pf_id)
@@ -528,117 +646,199 @@ let new_named_morphism id m = new_morphism (constr_of m) id morphism_hook
(****************************** The tactic itself *******************************)
type constr_with_marks =
- | MApp of constr_with_marks array
- | Toreplace
+ | MApp of morphism_class Lazy.t * constr_with_marks array
+ | Toreplace of setoid
| Tokeep
| Mimp of constr_with_marks * constr_with_marks
let is_to_replace = function
- | Tokeep -> false
- | Toreplace -> true
- | MApp _ -> true
- | Mimp _ -> true
+ | Tokeep -> false
+ | Toreplace _ -> true
+ | MApp _ -> true
+ | Mimp _ -> true
let get_mark a =
Array.fold_left (||) false (Array.map is_to_replace a)
-let rec mark_occur t in_c =
- if (eq_constr t in_c) then Toreplace else
+exception Use_replace
+
+let mark_occur gl hyp =
+ let rec aux t in_c =
+ if (eq_constr t in_c) then
+ let sa =
+ match hyp with
+ None ->
+ (match default_setoid_for_carrier (pf_type_of gl t) with
+ ACSetoid sa -> sa
+ | ACLeibniz _ -> raise Use_replace)
+ | Some h ->
+ let hypt = pf_type_of gl h in
+ let (heq, hargs) = decompose_app hypt in
+ let rec get_all_but_last_two =
+ function
+ []
+ | [_] -> assert false
+ | [_;_] -> []
+ | he::tl -> he::(get_all_but_last_two tl) in
+ let aeq = mkApp (heq,(Array.of_list (get_all_but_last_two hargs))) in
+ try setoid_table_find aeq with Not_found -> assert false
+ in
+ Toreplace sa
+ else
match kind_of_term in_c with
| App (c,al) ->
- let a = Array.map (mark_occur t) al
- in if (get_mark a) then (MApp a) else Tokeep
+ let a = Array.map (aux t) al in
+ let mor =
+ lazy
+ (try
+ begin
+ match morphism_table_find c with
+ [] -> assert false
+ | morphism::tl ->
+ if tl <> [] then
+ msg_warning
+ (str "There are several morphisms declared for " ++
+ prterm c ++
+ str ". The morphism " ++ prmorphism c morphism ++
+ str " is randomly chosen.") ;
+ ACMorphism (setoid_morphism_of_constr_morphism morphism)
+ end
+ with Not_found ->
+ let env = Global.env() in
+ let typeofc = (Typing.type_of env Evd.empty c) in
+ let typ = nf_betaiota typeofc in
+ let (argsrev, output) = decompose_prod typ in
+ ACFunction
+ {f_args=List.rev (List.map snd argsrev); f_output=output})
+ in
+ if (get_mark a) then MApp (mor,a) else Tokeep
| Prod (_, c1, c2) ->
if (dependent (mkRel 1) c2)
then Tokeep
else
- let c1m = mark_occur t c1 in
- let c2m = mark_occur t c2 in
+ let c1m = aux t c1 in
+ let c2m = aux t c2 in
if ((is_to_replace c1m)||(is_to_replace c2m))
then (Mimp (c1m, c2m))
else Tokeep
| _ -> Tokeep
+ in aux
-let create_args ca ma bl c1 c2 =
+let create_args ca ma args c1 c2 =
let rec aux i = function
| [] -> []
- | true::q ->
- if (is_to_replace ma.(i))
- then (replace_term c1 c2 ca.(i))::ca.(i)::(aux (i+1) q)
- else ca.(i)::ca.(i)::(aux (i+1) q)
- | false::q -> ca.(i)::(aux (i+1) q)
+ | (ACSetoid _)::tl ->
+ if is_to_replace ma.(i)
+ then (replace_term c1 c2 ca.(i))::ca.(i)::(aux (i+1) tl)
+ else ca.(i)::ca.(i)::(aux (i+1) tl)
+ | (ACLeibniz _)::tl ->
+ if is_to_replace ma.(i)
+ then
+ let newarg = replace_term c1 c2 ca.(i) in
+ newarg::(aux (i+1) tl)
+ else ca.(i)::(aux (i+1) tl)
in
- aux 0 bl
-
+ aux 0 args
-let res_tac c a hyp =
- let sa = setoid_table_find a in
+let res_tac sa c hyp glll =
let fin = match hyp with
| None -> Auto.full_trivial
| Some h ->
tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0 ""))
(tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0 ""))
- Auto.full_trivial) in
+ Auto.full_trivial)
+ in
tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0 ""))
(tclORELSE assumption
(tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|])))) assumption)
fin))
-let id_res_tac c a =
- let sa = setoid_table_find a in
- (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th; c|]))))
+let id_res_tac (*c*) sa =
+ (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th(*; c*)|])))
(* An exception to catchs errors *)
exception Nothing_found of constr;;
-let rec create_tac_list i a al c1 c2 hyp args_t = function
+(* special case of replace_where_needed_gen where all the arguments
+ are of class (ACLeibniz _) *)
+let rec replace_where_needed hyp ca ma c1 c2 =
+ let rec aux i = function
+ | [] -> tclIDTAC
+ | he::tl ->
+ if is_to_replace he then
+ let dummy = mkProp in (* dummy will never be used *)
+ tclTHENS
+ (!replace ca.(i) (replace_term c1 c2 ca.(i)))
+ [aux (i+1) tl; zapply (Some(ACLeibniz dummy)) false ca.(i) he c1 c2 hyp]
+ else
+ (aux (i+1) tl)
+ in
+ aux 0 ma
+and replace_where_needed_gen hyp ca ma args c1 c2 =
+ let rec aux i = function
+ | [] -> tclIDTAC
+ | ((ACLeibniz _) as he)::tl ->
+ if is_to_replace ma.(i) then
+ tclTHENS
+ (!replace ca.(i) (replace_term c1 c2 ca.(i)))
+ [aux (i+1) tl ; zapply (Some he) false ca.(i) ma.(i) c1 c2 hyp ]
+ else
+ aux (i+1) tl
+ | (ACSetoid _)::tl -> aux (i+1) tl
+ in
+ aux 0 args
+and create_tac_list i a al c1 c2 hyp = function
| [] -> []
- | false::q -> create_tac_list (i+1) a al c1 c2 hyp args_t q
- | true::q ->
+ | (ACLeibniz _)::tl -> create_tac_list (i+1) a al c1 c2 hyp tl
+ | ((ACSetoid setoid) as he)::tl ->
if (is_to_replace a.(i))
- then (zapply false al.(i) a.(i) c1 c2 hyp)::(create_tac_list (i+1) a al c1 c2 hyp args_t q)
- else (id_res_tac al.(i) (List.nth args_t i))::(create_tac_list (i+1) a al c1 c2 hyp args_t q)
-(* else tclIDTAC::(create_tac_list (i+1) a al c1 c2 hyp q) *)
-
-and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
- | ((App (c,al)),(MApp a)) -> (
- try
- let m = morphism_table_find c in
- let args = Array.of_list (create_args al a m.profil c1 c2) in
- if is_r
- then tclTHENS (apply (mkApp (m.lem, args)))
- ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])
- else (match m.lem2 with
- | None ->
- tclTHENS (apply (mkApp (m.lem, args))) (create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)
- | Some xom ->
- tclTHENS (apply (mkApp (xom, args))) (create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil))
- with Not_found -> errorlabstrm "Setoid_replace"
- (str "The term " ++ prterm c ++ str " has not been declared as a morphism"))
+ then (zapply (Some he) false al.(i) a.(i) c1 c2 hyp)::(create_tac_list (i+1) a al c1 c2 hyp tl)
+ else (id_res_tac (*al.(i)*) setoid)::(create_tac_list (i+1) a al c1 c2 hyp tl)
+
+and zapply close is_r gl gl_m c1 c2 hyp glll =
+ (match ((kind_of_term gl), gl_m) with
+ | ((App (c,al)),(MApp (m,a))) ->
+ (match Lazy.force m with
+ ACMorphism m ->
+ let args = Array.of_list (create_args al a m.args c1 c2) in
+ tclTHENS
+ (replace_where_needed_gen hyp al a m.args c1 c2)
+ [if is_r
+ then tclTHENS (apply (mkApp (m.lem, args)))
+ ((create_tac_list 0 a al c1 c2 hyp m.args)@[tclIDTAC])
+ else
+ match m.lem2 with
+ None ->
+ tclTHENS (apply (mkApp (m.lem, args)))
+ (create_tac_list 0 a al c1 c2 hyp m.args)
+ | Some xom ->
+ tclTHENS (apply (mkApp (xom, args)))
+ (create_tac_list 0 a al c1 c2 hyp m.args)]
+ | ACFunction f ->
+ tclTHENS
+ (replace_where_needed hyp al (Array.to_list a) c1 c2)
+ [match close with
+ None -> tclIDTAC
+ | Some (ACLeibniz _) -> reflexivity
+ | Some (ACSetoid setoid) -> id_res_tac setoid])
| ((Prod (_,hh, cc)),(Mimp (hhm, ccm))) ->
let al = [|hh; cc|] in
let a = [|hhm; ccm|] in
let fleche_constr = (Lazy.force coq_fleche) in
let fleche_cp = destConst fleche_constr in
let new_concl = (mkApp (fleche_constr, al)) in
+ let m = find_morphism_fleche () in
if is_r
then
- let m = morphism_table_find fleche_constr in
- let args = Array.of_list (create_args al a m.profil c1 c2) in
+ let args = Array.of_list (create_args al a m.args c1 c2) in
tclTHEN (change_in_concl None new_concl)
(tclTHENS (apply (mkApp (m.lem, args)))
- ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[unfold_constr (ConstRef fleche_cp)]))
-(* ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])) *)
- else (zapply is_r new_concl (MApp a) c1 c2 hyp)
-(* let args = Array.of_list (create_args [|hh; cc|] [|hhm; ccm|] [true;true] c1 c2) in
- if is_r
- then tclTHENS (apply (mkApp ((Lazy.force coq_fleche_ext), args)))
- ((create_tac_list 0 [|hhm; ccm|] [|hh; cc|] c1 c2 hyp [mkProp; mkProp] [true;true])@[tclIDTAC])
- else tclTHENS (apply (mkApp ((Lazy.force coq_fleche_ext2), args)))
- ((create_tac_list 0 [|hhm; ccm|] [|hh; cc|] c1 c2 hyp [mkProp; mkProp] [true;true])@[tclIDTAC])
-*)
- | (_, Toreplace) ->
+ ((create_tac_list 0 a al c1 c2 hyp m.args)@[unfold_constr (ConstRef fleche_cp)]))
+ else
+ (zapply (Some m.output) is_r new_concl
+ (MApp (lazy (ACMorphism m),a)) c1 c2 hyp)
+ | (_, Toreplace setoid) ->
if is_r
then (match hyp with
| None -> errorlabstrm "Setoid_replace"
@@ -657,17 +857,20 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
else
apply (mkApp (Lazy.force coqproj1,[|(mkArrow hc1 hc2);(mkArrow hc2 hc1);h|]))
)
- else (res_tac gl (pf_type_of glll gl) hyp) (* tclORELSE Auto.full_trivial tclIDTAC *)
+ else (res_tac setoid gl hyp glll)
| (_, Tokeep) -> (match hyp with
| None -> errorlabstrm "Setoid_replace"
(str "No replacable occurence of " ++ prterm c1 ++ str " found")
| Some _ ->errorlabstrm "Setoid_replace"
(str "No rewritable occurence of " ++ prterm c1 ++ str " found"))
- | _ -> anomaly ("Bug in Setoid_replace")) glll
+ | _ -> assert false) glll
let setoid_replace c1 c2 hyp gl =
let but = (pf_concl gl) in
- (zapply true but (mark_occur c1 but) c1 c2 hyp) gl
+ try
+ (zapply None true but (mark_occur gl hyp c1 but) c1 c2 hyp) gl
+ with
+ Use_replace -> (!replace c1 c2) gl
let general_s_rewrite lft2rgt c gl =
let ctype = pf_type_of gl c in
@@ -681,6 +884,8 @@ let general_s_rewrite lft2rgt c gl =
then setoid_replace c1 c2 (Some c) gl
else setoid_replace c2 c1 (Some c) gl
+let setoid_replace c1 c2 = setoid_replace c1 c2 None
+
let setoid_rewriteLR = general_s_rewrite true
let setoid_rewriteRL = general_s_rewrite false
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 059a25010f..02046c55b3 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -12,9 +12,14 @@ open Term
open Proof_type
open Topconstr
+
+val register_replace : (constr -> constr -> tactic) -> unit
+
+val print_setoids : unit -> unit
+
val equiv_list : unit -> constr list
-val setoid_replace : constr -> constr -> constr option -> tactic
+val setoid_replace : constr -> constr -> tactic
val setoid_rewriteLR : constr -> tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 03:18:25 +0000