From 13d449a37131f69ae9fce6c230974b926d579d28 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 1 Jan 2009 09:24:56 +0000 Subject: Switched to "standardized" names for the properties of eq and identity. Add notations for compatibility and support for understanding these notations in the ml files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 3 +++ contrib/fourier/fourierR.ml | 2 +- contrib/ring/ring.ml | 2 +- interp/coqlib.ml | 25 +++++++++++++++---------- interp/coqlib.mli | 2 +- interp/syntax_def.ml | 14 +++++++++----- interp/syntax_def.mli | 4 +++- library/nametab.ml | 3 ++- library/nametab.mli | 3 ++- tactics/equality.ml | 2 +- theories/FSets/FSetFullAVL.v | 2 -- theories/Init/Datatypes.v | 4 ++-- theories/Init/Logic.v | 39 +++++++++++++++++++++++---------------- theories/Init/Logic_Type.v | 21 +++++++++++++-------- 14 files changed, 76 insertions(+), 50 deletions(-) diff --git a/CHANGES b/CHANGES index 85ed627e1..cd8ac1562 100644 --- a/CHANGES +++ b/CHANGES @@ -304,6 +304,9 @@ Tactics - New tactic "instantiate" (without argument). - Tactic firstorder "with" and "using" options have their meaning swapped for consistency with auto/eauto (source of incompatibility). +- Tactic "intuition" now preserves inner "iff" (exceptional source of + incompatibilities solvable by redefining "intuition" as + "unfold iff in *; intuition". - Tactic "generalize" now supports "at" options to specify occurrences and "as" options to name the quantified hypotheses. - New tactic "specialize H with a" or "specialize (H a)" allows to transform diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index ef0ff426d..908267700 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -281,7 +281,7 @@ let constant = Coqlib.gen_constant "Fourier" (* Standard library *) open Coqlib -let coq_sym_eqT = lazy (build_coq_sym_eq ()) +let coq_sym_eqT = lazy (build_coq_eq_sym ()) let coq_False = lazy (build_coq_False ()) let coq_not = lazy (build_coq_not ()) let coq_eq = lazy (build_coq_eq ()) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index bb6aaea7d..eac109cae 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -837,7 +837,7 @@ let raw_polynom th op lc gl = (tclORELSE (tclORELSE (h_exact c'i_eq_c''i) - (h_exact (mkApp(build_coq_sym_eq (), + (h_exact (mkApp(build_coq_eq_sym (), [|th.th_a; c'''i; ci; c'i_eq_c''i |])))) (tclTHENS (elim_type diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 845707f9e..43c774707 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -15,6 +15,7 @@ open Term open Libnames open Pattern open Nametab +open Syntax_def (************************************************************************) (* Generic functions to find Coq objects *) @@ -25,10 +26,8 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (id_of_string s) in - try - Nametab.absolute_reference sp - with Not_found -> - anomaly (locstr^": cannot find "^(string_of_path sp)) + try global_of_extended_global (Nametab.extended_absolute_reference sp) + with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp)) let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s) @@ -40,10 +39,14 @@ let has_suffix_in_dirs dirs ref = let dir = dirpath (sp_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs +let global_of_extended q = + try Some (global_of_extended_global q) with Not_found -> None + let gen_constant_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let id = id_of_string s in - let all = Nametab.locate_all (make_short_qualid id) in + let all = Nametab.extended_locate_all (make_short_qualid id) in + let all = list_uniquize (list_map_filter global_of_extended all) in let these = List.filter (has_suffix_in_dirs dirs) all in match these with | [x] -> constr_of_global x @@ -195,12 +198,12 @@ let lazy_init_constant dir id = lazy (init_constant dir id) (* Equality on Set *) let coq_eq_eq = lazy_init_constant ["Logic"] "eq" -let coq_eq_refl = lazy_init_constant ["Logic"] "refl_equal" +let coq_eq_refl = lazy_init_constant ["Logic"] "eq_refl" let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind" 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"] "sym_eq" +let coq_eq_sym = lazy_init_constant ["Logic"] "eq_sym" let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2" let build_coq_eq_data () = @@ -214,9 +217,11 @@ let build_coq_eq_data () = sym = Lazy.force coq_eq_sym } let build_coq_eq () = Lazy.force coq_eq_eq -let build_coq_sym_eq () = Lazy.force coq_eq_sym +let build_coq_eq_sym () = Lazy.force coq_eq_sym let build_coq_f_equal2 () = Lazy.force coq_f_equal2 +let build_coq_sym_eq = build_coq_eq_sym (* compatibility *) + (* Specif *) let coq_sumbool = lazy_init_constant ["Specif"] "sumbool" @@ -228,8 +233,8 @@ let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity" let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind" 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"] "congr_id" -let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id" +let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr" +let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym" let build_coq_identity_data () = { eq = Lazy.force coq_identity_eq; diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 038cf94ff..a4751f6e7 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -117,7 +117,7 @@ val build_coq_eq_data : coq_leibniz_eq_data delayed val build_coq_identity_data : coq_leibniz_eq_data delayed val build_coq_eq : constr delayed (* = [(build_coq_eq_data()).eq] *) -val build_coq_sym_eq : constr delayed (* = [(build_coq_eq_data()).sym] *) +val build_coq_eq_sym : constr delayed (* = [(build_coq_eq_data()).sym] *) val build_coq_f_equal2 : constr delayed (* Specif *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 8f303ea61..bb8d68323 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -83,15 +83,19 @@ let declare_syntactic_definition local id onlyparse pat = let search_syntactic_definition loc kn = out_pat (KNmap.find kn !syntax_table) -let locate_global_with_alias (loc,qid) = - match Nametab.extended_locate qid with +let global_of_extended_global = function | TrueGlobal ref -> ref | SyntacticDef kn -> match search_syntactic_definition dummy_loc kn with | [],ARef ref -> ref - | _ -> - user_err_loc (loc,"",pr_qualid qid ++ - str " is bound to a notation that does not denote a reference") + | _ -> raise Not_found + +let locate_global_with_alias (loc,qid) = + let ref = Nametab.extended_locate qid in + try global_of_extended_global ref + with Not_found -> + user_err_loc (loc,"",pr_qualid qid ++ + str " is bound to a notation that does not denote a reference") let inductive_of_reference_with_alias r = match locate_global_with_alias (qualid_of_reference r) with diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 1599e844b..39583d856 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -32,9 +32,11 @@ val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation val locate_global_with_alias : qualid located -> global_reference +(* Extract a global_reference from a reference that can be an "alias" *) +val global_of_extended_global : extended_global_reference -> global_reference + (* Locate a reference taking into account possible "alias" notations *) val global_with_alias : reference -> global_reference (* The same for inductive types *) val inductive_of_reference_with_alias : reference -> inductive - diff --git a/library/nametab.ml b/library/nametab.ml index ac6c61116..5bb21b3e5 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -419,12 +419,13 @@ let locate_mind qid = | TrueGlobal (IndRef (kn,0)) -> kn | _ -> raise Not_found - let absolute_reference sp = match SpTab.find sp !the_ccitab with | TrueGlobal ref -> ref | _ -> raise Not_found +let extended_absolute_reference sp = SpTab.find sp !the_ccitab + let locate_in_absolute_module dir id = absolute_reference (make_path dir id) diff --git a/library/nametab.mli b/library/nametab.mli index eab86db1d..225a8b080 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -116,9 +116,10 @@ val locate_module : qualid -> module_path (* A variant looking up a [section_path] *) val absolute_reference : section_path -> global_reference +val extended_absolute_reference : section_path -> extended_global_reference -(*s These function tell if the given absolute name is already taken *) +(*s These functions tell if the given absolute name is already taken *) val exists_cci : section_path -> bool val exists_modtype : section_path -> bool diff --git a/tactics/equality.ml b/tactics/equality.ml index 259f51ad1..884a04e8f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -267,7 +267,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = and t2 = pf_apply get_type_of gl c2 in if unsafe or (pf_conv_x gl t1 t2) then let e = build_coq_eq () in - let sym = build_coq_sym_eq () in + let sym = build_coq_eq_sym () in let eq = applist (e, [t1;c1;c2]) in tclTHENS (assert_as false None eq) [onLastHyp (fun id -> diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v index ac8800923..64d5eb8af 100644 --- a/theories/FSets/FSetFullAVL.v +++ b/theories/FSets/FSetFullAVL.v @@ -522,8 +522,6 @@ Ltac ocaml_union_tac := rewrite H; simpl; romega with * end. -Import Logic. (* Unhide eq, otherwise Function complains. *) - Function ocaml_union (s : t * t) { measure cardinal2 s } : t := match s with | (Leaf, Leaf) => s#2 diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index cb96f3f60..73e4924aa 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -114,8 +114,8 @@ Inductive Empty_set : Set :=. sole inhabitant is denoted [refl_identity A a] *) Inductive identity (A:Type) (a:A) : A -> Type := - refl_identity : identity (A:=A) a a. -Hint Resolve refl_identity: core. + identity_refl : identity a a. +Hint Resolve identity_refl: core. Implicit Arguments identity_ind [A]. Implicit Arguments identity_rec [A]. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index a91fd0480..ede73ebf1 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -243,7 +243,7 @@ End universal_quantification. [A] which is true of [x] is also true of [y] *) Inductive eq (A:Type) (x:A) : A -> Prop := - refl_equal : x = x :>A + eq_refl : x = x :>A where "x = y :> A" := (@eq A x y) : type_scope. @@ -255,7 +255,7 @@ Implicit Arguments eq_ind [A]. Implicit Arguments eq_rec [A]. Implicit Arguments eq_rect [A]. -Hint Resolve I conj or_introl or_intror refl_equal: core. +Hint Resolve I conj or_introl or_intror eq_refl: core. Hint Resolve ex_intro ex_intro2: core. Section Logic_lemmas. @@ -271,17 +271,17 @@ Section Logic_lemmas. Variable f : A -> B. Variables x y z : A. - Theorem sym_eq : x = y -> y = x. + Theorem eq_sym : x = y -> y = x. Proof. destruct 1; trivial. Defined. - Opaque sym_eq. + Opaque eq_sym. - Theorem trans_eq : x = y -> y = z -> x = z. + Theorem eq_trans : x = y -> y = z -> x = z. Proof. destruct 2; trivial. Defined. - Opaque trans_eq. + Opaque eq_trans. Theorem f_equal : x = y -> f x = f y. Proof. @@ -289,30 +289,26 @@ Section Logic_lemmas. Defined. Opaque f_equal. - Theorem sym_not_eq : x <> y -> y <> x. + Theorem not_eq_sym : x <> y -> y <> x. Proof. red in |- *; intros h1 h2; apply h1; destruct h2; trivial. Qed. - Definition sym_equal := sym_eq. - Definition sym_not_equal := sym_not_eq. - Definition trans_equal := trans_eq. - End equality. Definition eq_ind_r : forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y. - intros A x P H y H0; elim sym_eq with (1 := H0); assumption. + intros A x P H y H0; elim eq_sym with (1 := H0); assumption. Defined. Definition eq_rec_r : forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y. - intros A x P H y H0; elim sym_eq with (1 := H0); assumption. + intros A x P H y H0; elim eq_sym with (1 := H0); assumption. Defined. Definition eq_rect_r : forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y. - intros A x P H y H0; elim sym_eq with (1 := H0); assumption. + intros A x P H y H0; elim eq_sym with (1 := H0); assumption. Defined. End Logic_lemmas. @@ -349,7 +345,18 @@ Proof. destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity. Qed. -Hint Immediate sym_eq sym_not_eq: core. +(* Aliases *) + +Notation sym_eq := eq_sym (only parsing). +Notation trans_eq := eq_trans (only parsing). +Notation sym_not_eq := not_eq_sym (only parsing). + +Notation refl_equal := eq_refl (only parsing). +Notation sym_equal := eq_sym (only parsing). +Notation trans_equal := eq_trans (only parsing). +Notation sym_not_equal := not_eq_sym (only parsing). + +Hint Immediate eq_sym not_eq_sym: core. (** Basic definitions about relations and properties *) @@ -411,7 +418,7 @@ intros A x y z H1 H2. rewrite <- H2; exact H1. Qed. Declare Left Step eq_stepl. -Declare Right Step trans_eq. +Declare Right Step eq_trans. Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B). Proof. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index f5cee92c7..bdec651da 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -29,22 +29,22 @@ Section identity_is_a_congruence. Variables x y z : A. - Lemma sym_id : identity x y -> identity y x. + Lemma identity_sym : identity x y -> identity y x. Proof. destruct 1; trivial. Defined. - Lemma trans_id : identity x y -> identity y z -> identity x z. + Lemma identity_trans : identity x y -> identity y z -> identity x z. Proof. destruct 2; trivial. Defined. - Lemma congr_id : identity x y -> identity (f x) (f y). + Lemma identity_congr : identity x y -> identity (f x) (f y). Proof. destruct 1; trivial. Defined. - Lemma sym_not_id : notT (identity x y) -> notT (identity y x). + Lemma not_identity_sym : notT (identity x y) -> notT (identity y x). Proof. red in |- *; intros H H'; apply H; destruct H'; trivial. Qed. @@ -53,17 +53,22 @@ End identity_is_a_congruence. Definition identity_ind_r : forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y. - intros A x P H y H0; case sym_id with (1 := H0); trivial. + intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. Definition identity_rec_r : forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y. - intros A x P H y H0; case sym_id with (1 := H0); trivial. + intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. Definition identity_rect_r : forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y. - intros A x P H y H0; case sym_id with (1 := H0); trivial. + intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. -Hint Immediate sym_id sym_not_id: core v62. +Hint Immediate identity_sym not_identity_sym: core v62. + +Notation refl_id := identity_refl (only parsing). +Notation sym_id := identity_sym (only parsing). +Notation trans_id := identity_trans (only parsing). +Notation sym_not_id := not_identity_sym (only parsing). -- cgit v1.2.3