aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--ide/coq.ml6
-rw-r--r--interp/coqlib.ml88
-rw-r--r--interp/coqlib.mli20
-rw-r--r--parsing/g_tactic.ml43
-rw-r--r--parsing/pptactic.ml3
-rw-r--r--parsing/q_coqast.ml42
-rw-r--r--plugins/field/field.ml410
-rw-r--r--plugins/interface/depends.ml3
-rw-r--r--plugins/interface/xlate.ml3
-rw-r--r--plugins/ring/ring.ml20
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--tactics/equality.ml79
-rw-r--r--tactics/hiddentac.ml3
-rw-r--r--tactics/hiddentac.mli2
-rw-r--r--tactics/hipattern.ml467
-rw-r--r--tactics/hipattern.mli22
-rw-r--r--tactics/rewrite.ml416
-rw-r--r--tactics/tacinterp.ml6
-rw-r--r--tactics/tactics.ml176
-rw-r--r--tactics/tactics.mli34
-rw-r--r--theories/Logic/JMeq.v59
-rw-r--r--toplevel/coqcompat.ml4
23 files changed, 379 insertions, 251 deletions
diff --git a/CHANGES b/CHANGES
index 4c2ed82b8..0688f5246 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,8 @@ Tactics
variables and "**" for introducing all quantified variables and hypotheses.
- Pattern Unification for existential variables activated in tactics and
new option "Unset Tactic Evars Pattern Unification" to deactivate it.
+- New tactic "etransitivity".
+- Support of JMeq for "injection" and "discriminate".
Tactic Language
diff --git a/ide/coq.ml b/ide/coq.ml
index d81bb42f2..35feb59ed 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -523,14 +523,14 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
pr_ast
^".") ] @
- (if is_equation ast then
+ (if is_equality_type ast then
[ "discriminate "^ident, "discriminate "^ident^".";
"injection "^ident, "injection "^ident^"." ]
else
[]) @
(let _,t = splay_prod env sigma ast in
- if is_equation t then
+ if is_equality_type t then
[ "rewrite "^ident, "rewrite "^ident^".";
"rewrite <- "^ident, "rewrite <- "^ident^"." ]
else
@@ -546,7 +546,7 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
("inversion_clear "^ident^".")]
let concl_menu (_,_,concl,_) =
- let is_eq = is_equation concl in
+ let is_eq = is_equality_type concl in
["intro", "intro.";
"intros", "intros.";
"intuition","intuition." ] @
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 087a51982..e110ad00a 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -82,6 +82,8 @@ let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s
let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s
+let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s
+
let arith_dir = ["Coq";"Arith"]
let arith_modules = [arith_dir]
@@ -107,9 +109,18 @@ let datatypes_id = id_of_string "Datatypes"
let logic_module_name = ["Coq";"Init";"Logic"]
let logic_module = make_dir logic_module_name
-let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
-let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
-let arith_module = make_dir ["Coq";"Arith";"Arith"]
+
+let logic_type_module_name = ["Coq";"Init";"Logic_Type"]
+let logic_type_module = make_dir logic_type_module_name
+
+let datatypes_module_name = ["Coq";"Init";"Datatypes"]
+let datatypes_module = make_dir datatypes_module_name
+
+let arith_module_name = ["Coq";"Arith";"Arith"]
+let arith_module = make_dir arith_module_name
+
+let jmeq_module_name = ["Coq";"Logic";"JMeq"]
+let jmeq_module = make_dir jmeq_module_name
(* TODO: temporary hack *)
let make_kn dir id = Libnames.encode_kn dir id
@@ -145,9 +156,14 @@ let glob_false = ConstructRef path_of_false
(** Equality *)
let eq_kn = make_kn logic_module (id_of_string "eq")
-
let glob_eq = IndRef (eq_kn,0)
+let identity_kn = make_kn datatypes_module (id_of_string "identity")
+let glob_identity = IndRef (identity_kn,0)
+
+let jmeq_kn = make_kn jmeq_module (id_of_string "JMeq")
+let glob_jmeq = IndRef (jmeq_kn,0)
+
type coq_sigma_data = {
proj1 : constr;
proj2 : constr;
@@ -185,18 +201,24 @@ let build_prod () =
typ = init_constant ["Datatypes"] "prod" }
(* Equalities *)
-type coq_leibniz_eq_data = {
+type coq_eq_data = {
eq : constr;
- refl : constr;
ind : constr;
+ refl : constr;
+ sym : constr;
+ trans: constr;
+ congr: constr }
+
+type coq_rewrite_data = {
rrec : constr option;
- rect : constr option;
- congr: constr;
- sym : constr }
+ rect : constr option
+}
let lazy_init_constant dir id = lazy (init_constant dir id)
+let lazy_logic_constant dir id = lazy (logic_constant dir id)
+
+(* Leibniz equality on Type *)
-(* Equality on Set *)
let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl"
let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
@@ -204,17 +226,17 @@ let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym"
+let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans"
let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
let build_coq_eq_data () =
let _ = check_required_library logic_module_name in {
eq = Lazy.force coq_eq_eq;
- refl = Lazy.force coq_eq_refl;
ind = Lazy.force coq_eq_ind;
- rrec = Some (Lazy.force coq_eq_rec);
- rect = Some (Lazy.force coq_eq_rect);
- congr = Lazy.force coq_eq_congr;
- sym = Lazy.force coq_eq_sym }
+ refl = Lazy.force coq_eq_refl;
+ sym = Lazy.force coq_eq_sym;
+ trans = Lazy.force coq_eq_trans;
+ congr = Lazy.force coq_eq_congr }
let build_coq_eq () = Lazy.force coq_eq_eq
let build_coq_eq_sym () = Lazy.force coq_eq_sym
@@ -222,6 +244,26 @@ let build_coq_f_equal2 () = Lazy.force coq_f_equal2
let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
+(* Heterogenous equality on Type *)
+
+let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq"
+let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl"
+let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind"
+let coq_jmeq_rec = lazy_logic_constant ["JMeq"] "JMeq_rec"
+let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect"
+let coq_jmeq_sym = lazy_logic_constant ["JMeq"] "JMeq_sym"
+let coq_jmeq_congr = lazy_logic_constant ["JMeq"] "JMeq_congr"
+let coq_jmeq_trans = lazy_logic_constant ["JMeq"] "JMeq_trans"
+
+let build_coq_jmeq_data () =
+ let _ = check_required_library jmeq_module_name in {
+ eq = Lazy.force coq_jmeq_eq;
+ ind = Lazy.force coq_jmeq_ind;
+ refl = Lazy.force coq_jmeq_refl;
+ sym = Lazy.force coq_jmeq_sym;
+ trans = Lazy.force coq_jmeq_trans;
+ congr = Lazy.force coq_jmeq_congr }
+
(* Specif *)
let coq_sumbool = lazy_init_constant ["Specif"] "sumbool"
@@ -235,15 +277,16 @@ let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec"
let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr"
let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym"
+let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans"
-let build_coq_identity_data () = {
+let build_coq_identity_data () =
+ let _ = check_required_library datatypes_module_name in {
eq = Lazy.force coq_identity_eq;
- refl = Lazy.force coq_identity_refl;
ind = Lazy.force coq_identity_ind;
- rrec = Some (Lazy.force coq_identity_rec);
- rect = Some (Lazy.force coq_identity_rect);
- congr = Lazy.force coq_identity_congr;
- sym = Lazy.force coq_identity_sym }
+ refl = Lazy.force coq_identity_refl;
+ sym = Lazy.force coq_identity_sym;
+ trans = Lazy.force coq_identity_trans;
+ congr = Lazy.force coq_identity_congr }
(* The False proposition *)
let coq_False = lazy_init_constant ["Logic"] "False"
@@ -281,7 +324,8 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
(* The following is less readable but does not depend on parsing *)
let coq_eq_ref = lazy (init_reference ["Logic"] "eq")
-let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
+let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
+let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
let coq_existS_ref = lazy (anomaly "use coq_existT_ref")
let coq_existT_ref = lazy (init_reference ["Specif"] "existT")
let coq_not_ref = lazy (init_reference ["Logic"] "not")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 7e13b1b1e..5b550a86b 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -76,6 +76,8 @@ val glob_false : global_reference
(* Equality *)
val glob_eq : global_reference
+val glob_identity : global_reference
+val glob_jmeq : global_reference
(*s Constructions and patterns related to Coq initial state are unknown
at compile time. Therefore, we can only provide methods to build
@@ -104,22 +106,23 @@ val build_sigma_type : coq_sigma_data delayed
(* Non-dependent pairs in Set from Datatypes *)
val build_prod : coq_sigma_data delayed
-type coq_leibniz_eq_data = {
+type coq_eq_data = {
eq : constr;
- refl : constr;
ind : constr;
- rrec : constr option;
- rect : constr option;
- congr: constr;
- sym : constr }
+ refl : constr;
+ sym : constr;
+ trans: constr;
+ congr: constr }
-val build_coq_eq_data : coq_leibniz_eq_data delayed
-val build_coq_identity_data : coq_leibniz_eq_data delayed
+val build_coq_eq_data : coq_eq_data delayed
+val build_coq_identity_data : coq_eq_data delayed
+val build_coq_jmeq_data : coq_eq_data delayed
val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *)
val build_coq_eq_sym : constr delayed (* = [(build_coq_eq_data()).sym] *)
val build_coq_f_equal2 : constr delayed
+
(* Specif *)
val build_coq_sumbool : constr delayed
@@ -150,6 +153,7 @@ val build_coq_ex : constr delayed
val coq_eq_ref : global_reference lazy_t
val coq_identity_ref : global_reference lazy_t
+val coq_jmeq_ref : global_reference lazy_t
val coq_existS_ref : global_reference lazy_t
val coq_existT_ref : global_reference lazy_t
val coq_not_ref : global_reference lazy_t
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c0a3f2e77..d5d32ce5b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -616,7 +616,8 @@ GEXTEND Gram
(* Equivalence relations *)
| IDENT "reflexivity" -> TacReflexivity
| IDENT "symmetry"; cl = clause_dft_concl -> TacSymmetry cl
- | IDENT "transitivity"; c = constr -> TacTransitivity c
+ | IDENT "transitivity"; c = constr -> TacTransitivity (Some c)
+ | IDENT "etransitivity" -> TacTransitivity None
(* Equality and inversion *)
| IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 357a572be..bdd9241e3 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -844,7 +844,8 @@ and pr_atom1 = function
(* Equivalence relations *)
| TacReflexivity as x -> pr_atom0 x
| TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls
- | TacTransitivity c -> str "transitivity" ++ pr_constrarg c
+ | TacTransitivity (Some c) -> str "transitivity" ++ pr_constrarg c
+ | TacTransitivity None -> str "etransitivity"
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a494738f9..606b652c2 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -413,7 +413,7 @@ let rec mlexpr_of_atomic_tactic = function
(* Equivalence relations *)
| Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>
| Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
- | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >>
+ | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
(* Automation tactics *)
| Tacexpr.TacAuto (n,lems,l) ->
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 93de6118b..c9b993690 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -154,10 +154,12 @@ END
(* Guesses the type and calls field_gen with the right theory *)
let field g =
Coqlib.check_required_library ["Coq";"field";"LegacyField"];
- let typ =
- match Hipattern.match_with_equation (pf_concl g) with
- | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t
- | _ -> error "The statement is not built from Leibniz' equality" in
+ let typ =
+ try match Hipattern.match_with_equation (pf_concl g) with
+ | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t
+ | _ -> raise Exit
+ with Hipattern.NoEquationFound | Exit ->
+ error "The statement is not built from Leibniz' equality" in
let th = VConstr (lookup (pf_env g) typ) in
(interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
<:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index 445b193f8..9e649a5a2 100644
--- a/plugins/interface/depends.ml
+++ b/plugins/interface/depends.ml
@@ -357,7 +357,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
(* Equivalence relations *)
| TacReflexivity
| TacSymmetry _ -> acc
- | TacTransitivity c -> depends_of_'constr c acc
+ | TacTransitivity (Some c) -> depends_of_'constr c acc
+ | TacTransitivity None -> acc
(* Equality and inversion *)
| TacRewrite (_,cbl,_,_) -> list_union_map (o depends_of_'constr_with_bindings (fun (_,_,x)->x)) cbl acc
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index bff8cae26..9629fa923 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -1066,7 +1066,8 @@ and xlate_tac =
(out_gen (wit_list1 rawwit_ident) l)))
| TacReflexivity -> CT_reflexivity
| TacSymmetry cls -> CT_symmetry(xlate_clause cls)
- | TacTransitivity c -> CT_transitivity (xlate_formula c)
+ | TacTransitivity (Some c) -> CT_transitivity (xlate_formula c)
+ | TacTransitivity None -> xlate_error "TODO: etransitivity"
| TacAssumption -> CT_assumption
| TacExact c -> CT_exact (xlate_formula c)
| TacExactNoCheck c -> CT_exact_no_check (xlate_formula c)
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index adcf51fe8..6dcc1e872 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -892,16 +892,18 @@ let polynom lc gl =
do "Ring c1 c2 ... cn" and then try to apply the simplification
theorems declared for the relation *)
| [] ->
- (match Hipattern.match_with_equation (pf_concl gl) with
- | Some (eq,t::args) ->
+ (try
+ match Hipattern.match_with_equation (pf_concl gl) with
+ | _,_,Hipattern.PolymorphicLeibnizEq (t,c1,c2) ->
let th = guess_theory t in
- if List.exists
- (fun c1 -> not (safe_pf_conv_x gl t (pf_type_of gl c1))) args
- then
- errorlabstrm "Ring :"
- (str" All terms must have the same type");
- (tclTHEN (raw_polynom th None args) (guess_eq_tac th)) gl
- | _ -> (match match_with_equiv (pf_concl gl) with
+ (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
+ | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2)
+ when safe_pf_conv_x gl t1 t2 ->
+ let th = guess_theory t1 in
+ (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
+ | _ -> raise Exit
+ with Hipattern.NoEquationFound | Exit ->
+ (match match_with_equiv (pf_concl gl) with
| Some (equiv, c1::args) ->
let t = (pf_type_of gl c1) in
let th = (guess_theory t) in
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 6b153fa10..65b330c3d 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -208,7 +208,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
(* Equivalence relations *)
| TacReflexivity
| TacSymmetry of 'id gclause
- | TacTransitivity of 'constr
+ | TacTransitivity of 'constr option
(* Equality and inversion *)
| TacRewrite of
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ce0677cae..101e7ef8c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -632,10 +632,9 @@ let apply_on_clause (f,t) clause =
| _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
clenv_fchain argmv f_clause clause
-let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
+let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
let e = next_ident_away eq_baseid (ids_of_context env) in
let e_env = push_named (e,None,t) env in
- let eqn = mkApp(lbeq.eq,[|t;t1;t2|]) in
let discriminator =
build_discriminator sigma e_env dirn (mkVar e) sort cpath in
let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
@@ -645,8 +644,8 @@ let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
tclTHENS (cut_intro absurd_term)
[onLastHypId gen_absurdity; refine pf]
-let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
- let sigma = eq_clause.evd in
+let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause gls =
+ let sigma = eq_clause.evd in
let env = pf_env gls in
match find_positions env sigma t1 t2 with
| Inr _ ->
@@ -655,19 +654,26 @@ let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
let sort = pf_apply get_type_of gls (pf_concl gls) in
discr_positions env sigma u eq_clause cpath dirn sort gls
+let extract_main_eq_args gl = function
+ | MonomorphicLeibnizEq (e1,e2) -> let t = pf_type_of gl e1 in (t,e1,e2)
+ | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
+ | HeterogenousEq (t1,e1,t2,e2) ->
+ if pf_conv_x gl t1 t2 then (t1,e1,e2)
+ else error"Don't know what to do with JMeq on arguments not of same type."
+
let onEquality with_evars tac (c,lbindc) gls =
let t = pf_type_of gls c in
let t' = try snd (pf_reduce_to_quantified_ind gls t) with UserError _ -> t in
let eq_clause = make_clenv_binding gls (c,t') lbindc in
let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
let eqn = clenv_type eq_clause' in
- let eq =
+ let eq,eq_args =
try find_eq_data_decompose eqn
with PatternMatchingFailure ->
errorlabstrm "" (str"No primitive equality found.") in
tclTHEN
(Refiner.tclEVARS eq_clause'.evd)
- (tac eq eq_clause') gls
+ (tac (eq,eqn,extract_main_eq_args gls eq_args) eq_clause') gls
let onNegatedEquality with_evars tac gls =
let ccl = pf_concl gls in
@@ -688,7 +694,9 @@ let discr with_evars = onEquality with_evars discrEq
let discrClause with_evars = onClause (discrSimpleClause with_evars)
let discrEverywhere with_evars =
+(*
tclORELSE
+*)
(if !discr_do_intro then
(tclTHEN
(tclREPEAT introf)
@@ -696,9 +704,9 @@ let discrEverywhere with_evars =
(fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
else (* <= 8.2 compat *)
Tacticals.tryAllHypsAndConcl (discrSimpleClause with_evars))
- (fun gls ->
+(* (fun gls ->
errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
-
+*)
let discr_tac with_evars = function
| None -> discrEverywhere with_evars
| Some c -> onInductionArg (discr with_evars) c
@@ -926,7 +934,7 @@ let simplify_args env sigma t =
| eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
| _ -> t
-let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
+let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns =
let e = next_ident_away eq_baseid (ids_of_context env) in
let e_env = push_named (e,None,t) env in
let injectors =
@@ -951,8 +959,8 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
exception Not_dep_pair
-let injEq ipats (eq,(t,t1,t2)) eq_clause =
- let sigma = eq_clause.evd in
+let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
+ let sigma = eq_clause.evd in
let env = eq_clause.env in
match find_positions env sigma t1 t2 with
| Inl _ ->
@@ -1000,7 +1008,7 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause =
) else (raise Not_dep_pair)
) with _ ->
tclTHEN
- (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns)
+ (inject_at_positions env sigma u eq_clause posns)
(intros_pattern no_move ipats)
let inj ipats with_evars = onEquality with_evars (injEq ipats)
@@ -1012,7 +1020,7 @@ let injClause ipats with_evars = function
let injConcl gls = injClause [] false None gls
let injHyp id gls = injClause [] false (Some (ElimOnIdent (dummy_loc,id))) gls
-let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
+let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
let sort = pf_apply get_type_of gls (pf_concl gls) in
let sigma = clause.evd in
let env = pf_env gls in
@@ -1023,8 +1031,7 @@ let decompEqThen ntac (lbeq,(t,t1,t2) as u) clause gls =
ntac 0 gls
| Inr posns ->
tclTHEN
- (inject_at_positions env sigma (lbeq,(t,t1,t2)) clause
- (List.rev posns))
+ (inject_at_positions env sigma u clause (List.rev posns))
(ntac (List.length posns))
gls
@@ -1034,14 +1041,26 @@ let dEqThen with_evars ntac = function
let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
+let swap_equality_args = function
+ | MonomorphicLeibnizEq (e1,e2) -> [e2;e1]
+ | PolymorphicLeibnizEq (t,e1,e2) -> [t;e2;e1]
+ | HeterogenousEq (t1,e1,t2,e2) -> [t2;e2;t1;e1]
+
+let get_equality_args = function
+ | MonomorphicLeibnizEq (e1,e2) -> [e1;e2]
+ | PolymorphicLeibnizEq (t,e1,e2) -> [t;e1;e2]
+ | HeterogenousEq (t1,e1,t2,e2) -> [t1;e1;t2;e2]
+
let swap_equands gls eqn =
- let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in
- applist(lbeq.eq,[t;e2;e1])
+ let (lbeq,eq_args) = find_eq_data_decompose eqn in
+ applist(lbeq.eq,swap_equality_args eq_args)
let swapEquandsInConcl gls =
- let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in
+ let (lbeq,eq_args) = find_eq_data_decompose (pf_concl gls) in
let sym_equal = lbeq.sym in
- refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
+ refine
+ (applist(sym_equal,(swap_equality_args eq_args@[Evarutil.mk_new_meta()])))
+ gls
(* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
@@ -1102,12 +1121,13 @@ let subst_tuple_term env sigma dep_pair b =
(fun (e,t) body -> lambda_create env (t,subst_term e body)) e_list b in
beta_applist(abst_B,proj_list)
-(* Comme "replace" mais decompose les egalites dependantes *)
+(* Like "replace" but decompose dependent equalities *)
exception NothingToRewrite
let cutSubstInConcl_RL eqn gls =
- let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in
+ let (lbeq,eq_args) = find_eq_data_decompose eqn in
+ let (t,e1,e2 as eq) = extract_main_eq_args gls eq_args in
let body = pf_apply subst_tuple_term gls e2 (pf_concl gls) in
if not (dependent (mkRel 1) body) then raise NothingToRewrite;
bareRevSubstInConcl lbeq body eq gls
@@ -1125,7 +1145,8 @@ let cutSubstInConcl_LR eqn gls =
let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL
let cutSubstInHyp_LR eqn id gls =
- let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose eqn in
+ let (lbeq,eq_args) = find_eq_data_decompose eqn in
+ let (t,e1,e2 as eq) = extract_main_eq_args gls eq_args in
let body = pf_apply subst_tuple_term gls e1 (pf_get_hyp_typ gls id) in
if not (dependent (mkRel 1) body) then raise NothingToRewrite;
cut_replacing id (subst1 e2 body)
@@ -1208,9 +1229,9 @@ let unfold_body x gl =
exception FoundHyp of (identifier * constr * bool)
(* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *)
-let is_eq_x x (id,_,c) =
+let is_eq_x gl x (id,_,c) =
try
- let (_,lhs,rhs) = snd (find_eq_data_decompose c) in
+ let (_,lhs,rhs) = extract_main_eq_args gl (snd(find_eq_data_decompose c)) in
if (x = lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
if (x = rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
with PatternMatchingFailure ->
@@ -1226,7 +1247,7 @@ let subst_one x gl =
(* Find a non-recursive definition for x *)
let (hyp,rhs,dir) =
try
- let test hyp _ = is_eq_x varx hyp in
+ let test hyp _ = is_eq_x gl varx hyp in
Sign.fold_named_context test ~init:() hyps;
errorlabstrm "Subst"
(str "Cannot find any non-recursive equality over " ++ pr_id x ++
@@ -1274,7 +1295,7 @@ let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids)
let subst_all gl =
let test (_,c) =
try
- let (_,x,y) = snd (find_eq_data_decompose c) in
+ let (_,x,y) = extract_main_eq_args gl (snd (find_eq_data_decompose c)) in
(* J.F.: added to prevent failure on goal containing x=x as an hyp *)
if eq_constr x y then failwith "caught";
match kind_of_term x with Var x -> x | _ ->
@@ -1291,19 +1312,19 @@ let subst_all gl =
let cond_eq_term_left c t gl =
try
- let (_,x,_) = snd (find_eq_data_decompose t) in
+ let (_,x,_) = extract_main_eq_args gl (snd (find_eq_data_decompose t)) in
if pf_conv_x gl c x then true else failwith "not convertible"
with PatternMatchingFailure -> failwith "not an equality"
let cond_eq_term_right c t gl =
try
- let (_,_,x) = snd (find_eq_data_decompose t) in
+ let (_,_,x) = extract_main_eq_args gl (snd (find_eq_data_decompose t)) in
if pf_conv_x gl c x then false else failwith "not convertible"
with PatternMatchingFailure -> failwith "not an equality"
let cond_eq_term c t gl =
try
- let (_,x,y) = snd (find_eq_data_decompose t) in
+ let (_,x,y) = extract_main_eq_args gl (snd (find_eq_data_decompose t)) in
if pf_conv_x gl c x then true
else if pf_conv_x gl c y then false
else failwith "not convertible"
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b85491c57..65a56100b 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -128,7 +128,8 @@ let h_change oc c cl =
let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity
let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c)
let h_transitivity c =
- abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c)
+ abstract_tactic (TacTransitivity (Option.map inj_open c))
+ (intros_transitivity c)
let h_simplest_apply c = h_apply false false [inj_open c,NoBindings]
let h_simplest_eapply c = h_apply false true [inj_open c,NoBindings]
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 5aafb91a0..f5b2dbb55 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -113,7 +113,7 @@ val h_change :
(* Equivalence relations *)
val h_reflexivity : tactic
val h_symmetry : Tacticals.clause -> tactic
-val h_transitivity : constr -> tactic
+val h_transitivity : constr option -> tactic
val h_simplest_apply : constr -> tactic
val h_simplest_eapply : constr -> tactic
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 7086e4421..0b81a492a 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -219,28 +219,47 @@ let is_unit_type t =
inductive binary relation R, so that R has only one constructor
establishing its reflexivity. *)
-let coq_refl_rel1_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ]
-let coq_refl_rel2_pattern = PATTERN [ forall x:_, _ x x ]
-let coq_refl_reljm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ]
+type equation_kind =
+ | MonomorphicLeibnizEq of constr * constr
+ | PolymorphicLeibnizEq of constr * constr * constr
+ | HeterogenousEq of constr * constr * constr * constr
+
+exception NoEquationFound
+
+let coq_refl_leibniz1_pattern = PATTERN [ forall x:_, _ x x ]
+let coq_refl_leibniz2_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ]
+let coq_refl_jm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ]
+
+open Libnames
let match_with_equation t =
- let (hdapp,args) = decompose_app t in
- match (kind_of_term hdapp) with
- | Ind ind ->
+ if not (isApp t) then raise NoEquationFound;
+ let (hdapp,args) = destApp t in
+ match kind_of_term hdapp with
+ | Ind ind ->
+ if IndRef ind = glob_eq then
+ Some (build_coq_eq_data()),hdapp,
+ PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ else if IndRef ind = glob_identity then
+ Some (build_coq_identity_data()),hdapp,
+ PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ else if IndRef ind = glob_jmeq then
+ Some (build_coq_jmeq_data()),hdapp,
+ HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+ else
let (mib,mip) = Global.lookup_inductive ind in
let constr_types = mip.mind_nf_lc in
let nconstr = Array.length mip.mind_consnames in
- if nconstr = 1 &&
- (is_matching coq_refl_rel1_pattern constr_types.(0) ||
- is_matching coq_refl_rel2_pattern constr_types.(0) ||
- is_matching coq_refl_reljm_pattern constr_types.(0))
- then
- Some (hdapp,args)
- else
- None
- | _ -> None
-
-let is_equation t = op2bool (match_with_equation t)
+ if nconstr = 1 then
+ if is_matching coq_refl_leibniz1_pattern constr_types.(0) then
+ None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
+ else if is_matching coq_refl_leibniz2_pattern constr_types.(0) then
+ None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+ else if is_matching coq_refl_jm_pattern constr_types.(0) then
+ None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+ else raise NoEquationFound
+ else raise NoEquationFound
+ | _ -> raise NoEquationFound
let match_with_equality_type t =
let (hdapp,args) = decompose_app t in
@@ -255,6 +274,8 @@ let match_with_equality_type t =
None
| _ -> None
+let is_equality_type t = op2bool (match_with_equality_type t)
+
let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
let match_arrow_pattern t =
@@ -333,16 +354,22 @@ let rec first_match matcher = function
let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
+let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
let match_eq eqn eq_pat =
- match matches (Lazy.force eq_pat) eqn with
+ let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
+ match matches pat eqn with
| [(m1,t);(m2,x);(m3,y)] ->
assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
- (t,x,y)
- | _ -> anomaly "match_eq: an eq pattern should match 3 terms"
+ PolymorphicLeibnizEq (t,x,y)
+ | [(m1,t);(m2,x);(m3,t');(m4,x')] ->
+ assert (m1 = meta1 & m2 = meta2 & m3 = meta3 & m4 = meta4);
+ HeterogenousEq (t,x,t',x')
+ | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms"
let equalities =
[coq_eq_pattern, build_coq_eq_data;
+ coq_jmeq_pattern, build_coq_jmeq_data;
coq_identity_pattern, build_coq_identity_data]
let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3418dd208..5be8b2026 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -16,6 +16,7 @@ open Sign
open Evd
open Pattern
open Proof_trees
+open Coqlib
(*i*)
(*s Given a term with second-order variables in it,
@@ -81,11 +82,9 @@ val is_unit_or_eq_type : testing_function
(* type with only one constructor and no arguments, no indices *)
val is_unit_type : testing_function
-val match_with_equation : (constr * constr list) matching_function
-val is_equation : testing_function
-
(* type with only one constructor, no arguments and at least one dependency *)
val match_with_equality_type : (constr * constr list) matching_function
+val is_equality_type : testing_function
val match_with_nottype : (constr * constr) matching_function
val is_nottype : testing_function
@@ -110,14 +109,23 @@ val is_nodep_ind : testing_function
val match_with_sigma_type : (constr * constr list) matching_function
val is_sigma_type : testing_function
-(***** Destructing patterns bound to some theory *)
+(* Recongnize inductive relation defined by reflexivity *)
-open Coqlib
+type equation_kind =
+ | MonomorphicLeibnizEq of constr * constr
+ | PolymorphicLeibnizEq of constr * constr * constr
+ | HeterogenousEq of constr * constr * constr * constr
+
+exception NoEquationFound
+
+val match_with_equation:
+ constr -> coq_eq_data option * constr * equation_kind
+
+(***** Destructing patterns bound to some theory *)
(* Match terms [(eq A t u)] or [(identity A t u)] *)
(* Returns associated lemmas and [A,t,u] *)
-val find_eq_data_decompose : constr ->
- coq_leibniz_eq_data * (constr * constr * constr)
+val find_eq_data_decompose : constr -> coq_eq_data * equation_kind
(* Match a term of the form [(existT A P t p)] *)
(* Returns associated lemmas and [A,P,t,p] *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 52f10d46c..43ae99203 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1390,9 +1390,8 @@ let setoid_proof gl ty fn fallback =
let evm, car = project gl, pf_type_of gl args.(0) in
fn env evm car rel gl
with e ->
- match fallback gl with
- | Some tac -> tac gl
- | None ->
+ try fallback gl
+ with Hipattern.NoEquationFound ->
match e with
| Not_found ->
let rel, args = relation_of_constr env (pf_concl gl) in
@@ -1412,9 +1411,11 @@ let setoid_symmetry gl =
let setoid_transitivity c gl =
setoid_proof gl "transitive"
(fun env evm car rel ->
- apply_with_bindings
- ((get_transitive_proof env evm car rel),
- Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]))
+ let proof = get_transitive_proof env evm car rel in
+ match c with
+ | None -> eapply proof
+ | Some c ->
+ apply_with_bindings (proof,Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]))
(transitivity_red true c)
let setoid_symmetry_in id gl =
@@ -1450,7 +1451,8 @@ TACTIC EXTEND setoid_reflexivity
END
TACTIC EXTEND setoid_transitivity
-[ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ]
+ [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
+| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
END
let implify id gl =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 41ec5dc07..e436fc90f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -798,7 +798,7 @@ let rec intern_atomic lf ist x =
| TacReflexivity -> TacReflexivity
| TacSymmetry idopt ->
TacSymmetry (clause_app (intern_hyp_location ist) idopt)
- | TacTransitivity c -> TacTransitivity (intern_constr ist c)
+ | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c)
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
@@ -2338,7 +2338,7 @@ and interp_atomic ist gl = function
(* Equivalence relations *)
| TacReflexivity -> h_reflexivity
| TacSymmetry c -> h_symmetry (interp_clause ist gl c)
- | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
+ | TacTransitivity c -> h_transitivity (Option.map (pf_interp_constr ist gl) c)
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
@@ -2652,7 +2652,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Equivalence relations *)
| TacReflexivity | TacSymmetry _ as x -> x
- | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
+ | TacTransitivity c -> TacTransitivity (Option.map (subst_rawconstr subst) c)
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e96806de1..0224da6c8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -905,16 +905,13 @@ let eapply_with_bindings (c,bl) =
let apply c =
apply_with_ebindings (inj_open c,NoBindings)
+let eapply c =
+ eapply_with_ebindings (inj_open c,NoBindings)
+
let apply_list = function
| c::l -> apply_with_bindings (c,ImplicitBindings l)
| _ -> assert false
-(* Resolution with no reduction on the type (used ?) *)
-
-let apply_without_reduce c gl =
- let clause = mk_clenv_type_of gl c in
- res_pf clause gl
-
(* [apply_in hyp c] replaces
hyp : forall y1, ti -> t hyp : rho(u)
@@ -2116,9 +2113,6 @@ let mkHRefl t x =
(* mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep_intro", *)
(* [| ty; mkApp (Lazy.force id, [|ty|]); t; x |]) *)
-let mkCoe a x p px y eq =
- mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |])
-
let lift_togethern n l =
let l', _ =
List.fold_right
@@ -3059,13 +3053,11 @@ let reflexivity_red allowred gl =
else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
in
match match_with_equality_type concl with
- | None -> None
- | Some _ -> Some (one_constructor 1 NoBindings)
+ | None -> raise NoEquationFound
+ | Some _ -> one_constructor 1 NoBindings gl
-let reflexivity gl =
- match reflexivity_red false gl with
- | None -> !setoid_reflexivity gl
- | Some tac -> tac gl
+let reflexivity gl =
+ try reflexivity_red false gl with NoEquationFound -> !setoid_reflexivity gl
let intros_reflexivity = (tclTHEN intros reflexivity)
@@ -3079,41 +3071,35 @@ let intros_reflexivity = (tclTHEN intros reflexivity)
let setoid_symmetry = ref (fun _ -> assert false)
let register_setoid_symmetry f = setoid_symmetry := f
+(* This is probably not very useful any longer *)
+let prove_symmetry hdcncl eq_kind =
+ let symc =
+ match eq_kind with
+ | MonomorphicLeibnizEq (c1,c2) -> mkApp(hdcncl,[|c2;c1|])
+ | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp(hdcncl,[|typ;c2;c1|])
+ | HeterogenousEq (t1,c1,t2,c2) -> mkApp(hdcncl,[|t2;c2;t1;c1|]) in
+ tclTHENFIRST (cut symc)
+ (tclTHENLIST
+ [ intro;
+ onLastHyp simplest_case;
+ one_constructor 1 NoBindings ])
+
let symmetry_red allowred gl =
(* PL: usual symmetry don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
- let concl = if not allowred then pf_concl gl
- else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
+ let concl =
+ if not allowred then pf_concl gl else pf_whd_betadeltaiota gl (pf_concl gl)
in
- match match_with_equation concl with
- | None -> None
- | Some (hdcncl,args) -> Some (fun gl ->
- let hdcncls = string_of_inductive hdcncl in
- begin
- try
- tclTHEN
- (convert_concl_no_check concl DEFAULTcast)
- (apply (pf_parse_const gl ("sym_"^hdcncls))) gl
- with _ ->
- let symc = match args with
- | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |])
- | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |])
- | [c1;c2] -> mkApp (hdcncl, [| c2; c1 |])
- | _ -> assert false
- in
- tclTHENFIRST (cut symc)
- (tclTHENLIST
- [ intro;
- onLastHyp simplest_case;
- one_constructor 1 NoBindings ])
- gl
- end)
-
-let symmetry gl =
- match symmetry_red false gl with
- | None -> !setoid_symmetry gl
- | Some tac -> tac gl
+ match match_with_equation concl with
+ | Some eq_data,_,_ ->
+ tclTHEN
+ (convert_concl_no_check concl DEFAULTcast)
+ (apply eq_data.sym) gl
+ | None,eq,eq_kind -> prove_symmetry eq eq_kind gl
+
+let symmetry gl =
+ try symmetry_red false gl with NoEquationFound -> !setoid_symmetry gl
let setoid_symmetry_in = ref (fun _ _ -> assert false)
let register_setoid_symmetry_in f = setoid_symmetry_in := f
@@ -3121,18 +3107,17 @@ let register_setoid_symmetry_in f = setoid_symmetry_in := f
let symmetry_in id gl =
let ctype = pf_type_of gl (mkVar id) in
let sign,t = decompose_prod_assum ctype in
- match match_with_equation t with
- | None -> !setoid_symmetry_in id gl
- | Some (hdcncl,args) ->
- let symccl = match args with
- | [t1; c1; t2; c2] -> mkApp (hdcncl, [| t2; c2; t1; c1 |])
- | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |])
- | [c1;c2] -> mkApp (hdcncl, [| c2; c1 |])
- | _ -> assert false in
- tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
- [ intro_replacing id;
- tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
- gl
+ try
+ let _,hdcncl,eq = match_with_equation t in
+ let symccl = match eq with
+ | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |])
+ | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |])
+ | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in
+ tclTHENS (cut (it_mkProd_or_LetIn symccl sign))
+ [ intro_replacing id;
+ tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
+ gl
+ with NoEquationFound -> !setoid_symmetry_in id gl
let intros_symmetry =
onClause
@@ -3155,47 +3140,52 @@ let intros_symmetry =
let setoid_transitivity = ref (fun _ _ -> assert false)
let register_setoid_transitivity f = setoid_transitivity := f
+(* This is probably not very useful any longer *)
+let prove_transitivity hdcncl eq_kind t gl =
+ let eq1,eq2 =
+ match eq_kind with
+ | MonomorphicLeibnizEq (c1,c2) ->
+ (mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]))
+ | PolymorphicLeibnizEq (typ,c1,c2) ->
+ (mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]))
+ | HeterogenousEq (typ1,c1,typ2,c2) ->
+ let typt = pf_type_of gl t in
+ (mkApp(hdcncl, [| typ1; c1; typt ;t |]),
+ mkApp(hdcncl, [| typt; t; typ2; c2 |])) in
+ tclTHENFIRST (cut eq2)
+ (tclTHENFIRST (cut eq1)
+ (tclTHENLIST
+ [ tclDO 2 intro;
+ onLastHyp simplest_case;
+ assumption ])) gl
+
let transitivity_red allowred t gl =
(* PL: usual transitivity don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
- let concl = if not allowred then pf_concl gl
- else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl)
- in
+ let concl =
+ if not allowred then pf_concl gl else pf_whd_betadeltaiota gl (pf_concl gl)
+ in
match match_with_equation concl with
- | None -> None
- | Some (hdcncl,args) -> Some (fun gl ->
- let hdcncls = string_of_inductive hdcncl in
- begin
- try
- apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl
- with _ ->
- let eq1, eq2 = match args with
- | [typ1;c1;typ2;c2] -> let typt = pf_type_of gl t in
- ( mkApp(hdcncl, [| typ1; c1; typt ;t |]),
- mkApp(hdcncl, [| typt; t; typ2; c2 |]) )
- | [typ;c1;c2] ->
- ( mkApp (hdcncl, [| typ; c1; t |]),
- mkApp (hdcncl, [| typ; t; c2 |]) )
- | [c1;c2] ->
- ( mkApp (hdcncl, [| c1; t|]),
- mkApp (hdcncl, [| t; c2 |]) )
- | _ -> assert false
- in
- tclTHENFIRST (cut eq2)
- (tclTHENFIRST (cut eq1)
- (tclTHENLIST
- [ tclDO 2 intro;
- onLastHyp simplest_case;
- assumption ])) gl
- end)
-
-let transitivity t gl =
- match transitivity_red false t gl with
- | None -> !setoid_transitivity t gl
- | Some tac -> tac gl
-
-let intros_transitivity n = tclTHEN intros (transitivity n)
+ | Some eq_data,_,_ ->
+ tclTHEN
+ (convert_concl_no_check concl DEFAULTcast)
+ (match t with
+ | None -> eapply eq_data.trans
+ | Some t -> apply_list [eq_data.trans;t]) gl
+ | None,eq,eq_kind ->
+ match t with
+ | None -> error "etransitivity not supported for this relation."
+ | Some t -> prove_transitivity eq eq_kind t gl
+
+let transitivity_gen t gl =
+ try transitivity_red false t gl
+ with NoEquationFound -> !setoid_transitivity t gl
+
+let etransitivity = transitivity_gen None
+let transitivity t = transitivity_gen (Some t)
+
+let intros_transitivity n = tclTHEN intros (transitivity_gen n)
(* tactical to save as name a subproof such that the generalisation of
the current goal, abstracted with respect to the local signature,
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 355380a74..40740c3a8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -176,10 +176,9 @@ val apply_type : constr -> constr list -> tactic
val apply_term : constr -> constr list -> tactic
val bring_hyps : named_context -> tactic
-val apply : constr -> tactic
-val apply_without_reduce : constr -> tactic
-val apply_list : constr list -> tactic
-
+val apply : constr -> tactic
+val eapply : constr -> tactic
+
val apply_with_ebindings_gen :
advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic
@@ -271,8 +270,8 @@ val simple_induct : quantified_hypothesis -> tactic
val new_induct : evars_flag -> constr with_ebindings induction_arg list ->
constr with_ebindings option ->
- intro_pattern_expr located option * intro_pattern_expr located option ->
- clause option -> tactic
+ intro_pattern_expr located option * intro_pattern_expr located option ->
+ clause option -> tactic
(*s Case analysis tactics. *)
@@ -282,16 +281,16 @@ val simplest_case : constr -> tactic
val simple_destruct : quantified_hypothesis -> tactic
val new_destruct : evars_flag -> constr with_ebindings induction_arg list ->
constr with_ebindings option ->
- intro_pattern_expr located option * intro_pattern_expr located option ->
- clause option -> tactic
+ intro_pattern_expr located option * intro_pattern_expr located option ->
+ clause option -> tactic
(*s Generic case analysis / induction tactics. *)
val induction_destruct : evars_flag -> rec_flag ->
(constr with_ebindings induction_arg list *
- constr with_ebindings option *
- (intro_pattern_expr located option * intro_pattern_expr located option) *
- clause option) list ->
+ constr with_ebindings option *
+ (intro_pattern_expr located option * intro_pattern_expr located option) *
+ clause option) list ->
tactic
(*s Eliminations giving the type instead of the proof. *)
@@ -312,7 +311,7 @@ val dorE : bool -> clause ->tactic
(*s Introduction tactics. *)
val constructor_tac : evars_flag -> int option -> int ->
- open_constr bindings -> tactic
+ open_constr bindings -> tactic
val any_constructor : evars_flag -> tactic option -> tactic
val one_constructor : int -> open_constr bindings -> tactic
@@ -331,21 +330,22 @@ val simplest_split : tactic
(*s Logical connective tactics. *)
val register_setoid_reflexivity : tactic -> unit
-val reflexivity_red : bool -> goal sigma -> tactic option
+val reflexivity_red : bool -> tactic
val reflexivity : tactic
val intros_reflexivity : tactic
val register_setoid_symmetry : tactic -> unit
-val symmetry_red : bool -> goal sigma -> tactic option
+val symmetry_red : bool -> tactic
val symmetry : tactic
val register_setoid_symmetry_in : (identifier -> tactic) -> unit
val symmetry_in : identifier -> tactic
val intros_symmetry : clause -> tactic
-val register_setoid_transitivity : (constr -> tactic) -> unit
-val transitivity_red : bool -> constr -> goal sigma -> tactic option
+val register_setoid_transitivity : (constr option -> tactic) -> unit
+val transitivity_red : bool -> constr option -> tactic
val transitivity : constr -> tactic
-val intros_transitivity : constr -> tactic
+val etransitivity : tactic
+val intros_transitivity : constr option -> tactic
val cut : constr -> tactic
val cut_intro : constr -> tactic
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 1211d3327..7d9e11296 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -28,44 +28,61 @@ Set Elimination Schemes.
Hint Resolve JMeq_refl.
-Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
+Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
+Proof.
destruct 1; trivial.
Qed.
-Hint Immediate sym_JMeq.
+Hint Immediate JMeq_sym.
-Lemma trans_JMeq :
+Lemma JMeq_trans :
forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
-destruct 1; trivial.
+Proof.
+destruct 2; trivial.
Qed.
Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
-Lemma JMeq_ind : forall (A:Type) (x y:A) (P:A -> Prop), P x -> JMeq x y -> P y.
-intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
+Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
+ P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.
-Lemma JMeq_rec : forall (A:Type) (x y:A) (P:A -> Set), P x -> JMeq x y -> P y.
-intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
+Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set),
+ P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.
-Lemma JMeq_rect : forall (A:Type) (x y:A) (P:A->Type), P x -> JMeq x y -> P y.
-intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
+Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type),
+ P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.
-Lemma JMeq_ind_r :
- forall (A:Type) (x y:A) (P:A -> Prop), P y -> JMeq x y -> P x.
-intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
+Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
+ P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.
-Lemma JMeq_rec_r :
- forall (A:Type) (x y:A) (P:A -> Set), P y -> JMeq x y -> P x.
-intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
+Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set),
+ P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
+Qed.
+
+Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type),
+ P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.
-Lemma JMeq_rect_r :
- forall (A:Type) (x y:A) (P:A -> Type), P y -> JMeq x y -> P x.
-intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
+Lemma JMeq_congr :
+ forall (A B:Type) (f:A->B) (x y:A), JMeq x y -> JMeq (f x) (f y).
+Proof.
+intros A B f x y H; case JMeq_eq with (1 := H); trivial.
Qed.
(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)
@@ -107,3 +124,7 @@ intro H.
assert (true=false) by (destruct H; reflexivity).
discriminate.
Qed.
+
+(* Compatibility *)
+Notation sym_JMeq := JMeq_sym (only parsing).
+Notation trans_JMeq := JMeq_trans (only parsing).
diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml
index 8bf1e9bd0..59dca330c 100644
--- a/toplevel/coqcompat.ml
+++ b/toplevel/coqcompat.ml
@@ -24,10 +24,10 @@ let set_compat_options = function
set_bool_option_value ["Intuition";"Iff";"Unfolding"] true
| "8.1" ->
- warning "Compatibility with versions 8.1 not supported."
+ warning "Compatibility with version 8.1 not supported."
| "8.0" ->
- warning "Compatibility with versions 8.0 not supported."
+ warning "Compatibility with version 8.0 not supported."
| s ->
error ("Unknown compatibility version \""^s^"\".")
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:57:16 +0000