From 3fe4912b568916676644baeb982a3e10c592d887 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 25 Sep 2014 00:12:26 +0200 Subject: Keyed unification option, compiling the whole standard library (but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on. --- library/impargs.ml | 15 +---- library/keys.ml | 100 ++++++++++++++++++++-------- library/keys.mli | 7 +- plugins/micromega/ZCoeff.v | 1 + plugins/micromega/ZMicromega.v | 10 +-- plugins/setoid_ring/Field_theory.v | 9 ++- plugins/setoid_ring/Ncring_initial.v | 1 + plugins/setoid_ring/Ring_polynom.v | 8 ++- pretyping/unification.ml | 16 +++-- tactics/extratactics.ml4 | 16 +++++ test-suite/bugs/opened/1596.v | 10 ++- test-suite/success/keyedrewrite.v | 23 ++++++- theories/FSets/FMapFullAVL.v | 2 + theories/FSets/FSetCompat.v | 2 + theories/FSets/FSetPositive.v | 3 + theories/MSets/MSetGenTree.v | 2 + theories/Numbers/Cyclic/Abstract/NZCyclic.v | 4 +- theories/Numbers/Natural/BigN/NMake_gen.ml | 5 ++ theories/Numbers/Natural/BigN/Nbasic.v | 1 + theories/Numbers/Rational/BigQ/BigQ.v | 2 + theories/Reals/Binomial.v | 7 +- theories/Reals/Rlimit.v | 2 + 22 files changed, 174 insertions(+), 72 deletions(-) diff --git a/library/impargs.ml b/library/impargs.ml index cbbb2cea9..d88d6f106 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -542,17 +542,9 @@ let discharge_implicits (_,(req,l)) = | ImplInteractive (ref,flags,exp) -> (try let vars = section_segment_of_reference ref in - (* let isproj = *) - (* match ref with *) - (* | ConstRef cst -> is_projection cst (Global.env ()) *) - (* | _ -> false *) - (* in *) let ref' = if isVarRef ref then ref else pop_global_reference ref in let extra_impls = impls_of_context vars in - let l' = - (* if isproj then [ref',snd (List.hd l)] *) - (* else *) - [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in + let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in Some (ImplInteractive (ref',flags,exp),l') with Not_found -> (* ref not defined in this section *) Some (req,l)) | ImplConstant (con,flags) -> @@ -560,10 +552,7 @@ let discharge_implicits (_,(req,l)) = let con' = pop_con con in let vars,_,_ = section_segment_of_constant con in let extra_impls = impls_of_context vars in - let newimpls = - (* if is_projection con (Global.env()) then (snd (List.hd l)) *) - (* else *) List.map (add_section_impls vars extra_impls) (snd (List.hd l)) - in + let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in let l' = [ConstRef con',newimpls] in Some (ImplConstant (con',flags),l') with Not_found -> (* con not defined in this section *) Some (req,l)) diff --git a/library/keys.ml b/library/keys.ml index c661e67fb..e4af0380b 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -1,8 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Keyset.add v vs) m + with Not_found -> Keymap.add k (Keyset.singleton v) m -let add_keys k v = KeyUF.union k v keys +let add_keys k v = + keys := add_kv k v (add_kv v k !keys) let equiv_keys k k' = - k == k' || KeyUF.find k keys == KeyUF.find k' keys + k == k' || KeyOrdered.equal k k' || + try Keyset.mem k' (Keymap.find k !keys) + with Not_found -> false (** Registration of keys as an object *) @@ -79,8 +95,8 @@ let subst_keys (subst,(k,k')) = (subst_key subst k, subst_key subst k') let discharge_key = function - | KGlob (VarRef _) -> None - | KGlob g -> Some (KGlob (pop_global_reference g)) + | KGlob g when Lib.is_in_section g -> + if isVarRef g then None else Some (KGlob (pop_global_reference g)) | x -> Some x let discharge_keys (_,(k,k')) = @@ -101,26 +117,54 @@ let inKeys : key_obj -> obj = discharge_function = discharge_keys; rebuild_function = rebuild_keys } -let declare_keys ref ref' = +let declare_equiv_keys ref ref' = Lib.add_anonymous_leaf (inKeys (ref,ref')) -let rec constr_key c = +let constr_key c = let open Globnames in - match kind_of_term c with - | Const (c, _) -> KGlob (ConstRef c) - | Ind (i, u) -> KGlob (IndRef i) - | Construct (c,u) -> KGlob (ConstructRef c) - | Var id -> KGlob (VarRef id) - | App (f, _) -> constr_key f - | Proj (p, _) -> KGlob (ConstRef p) - | Cast (p, _, _) -> constr_key p - | Lambda _ -> KLam - | Prod _ -> KProd - | Case _ -> KCase - | Fix _ -> KFix - | CoFix _ -> KCoFix - | Rel _ -> KRel - | Meta _ -> KMeta - | Evar _ -> KEvar - | Sort _ -> KSort - | LetIn _ -> KLet + try + let rec aux k = + match kind_of_term k with + | Const (c, _) -> KGlob (ConstRef c) + | Ind (i, u) -> KGlob (IndRef i) + | Construct (c,u) -> KGlob (ConstructRef c) + | Var id -> KGlob (VarRef id) + | App (f, _) -> aux f + | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p)) + | Cast (p, _, _) -> aux p + | Lambda _ -> KLam + | Prod _ -> KProd + | Case _ -> KCase + | Fix _ -> KFix + | CoFix _ -> KCoFix + | Rel _ -> KRel + | Meta _ -> raise Not_found + | Evar _ -> raise Not_found + | Sort _ -> KSort + | LetIn _ -> KLet + in Some (aux c) + with Not_found -> None + +open Pp + +let pr_key pr_global = function + | KGlob gr -> pr_global gr + | KLam -> str"Lambda" + | KLet -> str"Let" + | KProd -> str"Product" + | KSort -> str"Sort" + | KEvar -> str"Evar" + | KCase -> str"Case" + | KFix -> str"Fix" + | KCoFix -> str"CoFix" + | KRel -> str"Rel" + | KMeta -> str"Meta" + +let pr_keyset pr_global v = + prlist_with_sep spc (pr_key pr_global) (Keyset.elements v) + +let pr_mapping pr_global k v = + pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v + +let pr_keys pr_global = + Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt()) diff --git a/library/keys.mli b/library/keys.mli index 87ba45558..36789c83b 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -10,11 +10,14 @@ open Globnames type key -val declare_keys : key -> key -> unit +val declare_equiv_keys : key -> key -> unit (** Declare two keys as being equivalent. *) val equiv_keys : key -> key -> bool (** Check equivalence of keys. *) -val constr_key : Term.constr -> key +val constr_key : Term.constr -> key option (** Compute the head key of a term. *) + +val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds +(** Pretty-print the mapping *) diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index d65c60167..50197872c 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -93,6 +93,7 @@ Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption. Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption. Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp. +Declare Equivalent Keys gen_order_phi_Z gen_phiZ. Notation phi_pos := (gen_phiPOS 1 rplus rtimes). Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes). diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 78837d4cd..c982db393 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -155,12 +155,16 @@ Proof. Qed. Definition psub := psub Z0 Z.add Z.sub Z.opp Zeq_bool. +Declare Equivalent Keys psub RingMicromega.psub. Definition padd := padd Z0 Z.add Zeq_bool. +Declare Equivalent Keys padd RingMicromega.padd. Definition norm := norm 0 1 Z.add Z.mul Z.sub Z.opp Zeq_bool. +Declare Equivalent Keys norm RingMicromega.norm. Definition eval_pol := eval_pol Z.add Z.mul (fun x => x). +Declare Equivalent Keys eval_pol RingMicromega.eval_pol. Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) = eval_pol env lhs - eval_pol env rhs. Proof. @@ -202,11 +206,10 @@ Definition normalise (t:Formula Z) : cnf (NFormula Z) := Lemma normalise_correct : forall env t, eval_cnf eval_nformula env (normalise t) <-> Zeval_formula env t. Proof. - Opaque padd. - unfold normalise, xnormalise ; simpl; intros env t. + unfold normalise, xnormalise; cbn -[padd]; intros env t. rewrite Zeval_formula_compat. unfold eval_cnf, eval_clause. - destruct t as [lhs o rhs]; case_eq o; simpl; + destruct t as [lhs o rhs]; case_eq o; cbn -[padd]; repeat rewrite eval_pol_sub; repeat rewrite eval_pol_add; repeat rewrite <- eval_pol_norm ; simpl in *; @@ -216,7 +219,6 @@ Proof. generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst; intuition (auto with zarith). - Transparent padd. Qed. Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z) := diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index ad7fbd871..16f9b9723 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1168,7 +1168,8 @@ induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; assert (U2 := split_ok_r (num F1) (num F2) l). assert (U3 := split_ok_l (denum F1) (denum F2) l). assert (U4 := split_ok_r (denum F1) (denum F2) l). - rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4; apply rdiv7b; + rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4. + simpl in U2, U3, U4. apply rdiv7b; rewrite <- ?U2, <- ?U3, <- ?U4; try apply Pcond_Fnorm; trivial. - rewrite !NPEpow_ok. simpl. rewrite !rpow_pow, (IHfe Hc). @@ -1274,6 +1275,9 @@ Qed. (* simplify a field equation : generate the crossproduct and simplify polynomials *) +(** This allows rewriting modulo the simplification of PEeval on PMul *) +Declare Equivalent Keys PEeval rmul. + Theorem Field_simplify_eq_correct : forall n l lpe fe1 fe2, Ninterp_PElist l lpe -> @@ -1294,8 +1298,7 @@ rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3. simpl. rewrite !rmul_assoc. apply rmul_ext; trivial. -rewrite - (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl), +rewrite (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl), (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl). rewrite Hlmp. apply Hcrossprod. diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 528ad4f17..40748c044 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -192,6 +192,7 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x]. Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y]. Proof. intros;subst;reflexivity. Qed. +Declare Equivalent Keys bracket gen_phiZ. (*proof that [.] satisfies morphism specifications*) Global Instance gen_phiZ_morph : (@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*) diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 5ec73950b..3e0e931b6 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1033,16 +1033,18 @@ Section POWER. now destruct pe. Qed. + Arguments norm_aux !pe : simpl nomatch. + Lemma norm_aux_spec l pe : PEeval l pe == (norm_aux pe)@l. Proof. intros. - induction pe. - - now rewrite (morph0 CRmorph). + induction pe; cbn. + - now rewrite (morph0 CRmorph). - now rewrite (morph1 CRmorph). - reflexivity. - apply mkX_ok. - - simpl PEeval. rewrite IHpe1, IHpe2. + - rewrite IHpe1, IHpe2. assert (H1 := norm_aux_PEopp pe1). assert (H2 := norm_aux_PEopp pe2). rewrite norm_aux_PEadd. diff --git a/pretyping/unification.ml b/pretyping/unification.ml index efa64ca1e..735d4b68a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1457,11 +1457,17 @@ let make_abstraction env evd ccl abs = make_abstraction_core name (make_eq_test env evd c) (evd,c) ty occs check_occs env ccl -let keyed_unify env evd kop cl = - if not !keyed_unification then true - else - let k2 = Keys.constr_key cl in - Keys.equiv_keys kop k2 +let keyed_unify env evd kop = + if not !keyed_unification then fun cl -> true + else + match kop with + | None -> fun _ -> true + | Some kop -> + fun cl -> + let kc = Keys.constr_key cl in + match kc with + | None -> false + | Some kc -> Keys.equiv_keys kop kc (* Tries to find an instance of term [cl] in term [op]. Unifies [cl] to every subterm of [op] until it finds a match. diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0647fa813..ffd164d16 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -994,3 +994,19 @@ let decompose l c = TACTIC EXTEND decompose | [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] END + +(** library/keys *) + +VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF +| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ + let it c = snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c) in + let k1 = Keys.constr_key (it c) in + let k2 = Keys.constr_key (it c') in + match k1, k2 with + | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2 + | _ -> () ] +END + +VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY +| [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ] +END diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 91cd09910..7c5dc4167 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -1,10 +1,11 @@ - Require Import Relations. Require Import FSets. Require Import Arith. Require Import Omega. Unset Standard Proposition Elimination Names. +Set Keyed Unification. + Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false. destruct b;try tauto. Qed. @@ -255,9 +256,6 @@ n). induction m;simpl;intro. elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros. apply SynInc;apply H.mem_2;trivial. - - Fail rewrite H in H0. (* !! impossible here !! *) -Abort. -(* discriminate H0. - Qed.*) + rewrite H in H0. discriminate. (* !! impossible here !! *) + Qed. End B. \ No newline at end of file diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index 438613b44..c99b16e2b 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -1 +1,22 @@ -Lemma foo : \ No newline at end of file +Section foo. +Variable f : nat -> nat. + +Definition g := f. + +Variable lem : g 0 = 0. + +Goal f 0 = 0. +Proof. + Fail rewrite lem. +Abort. + +Declare Equivalent Keys @g @f. +(** Now f and g are considered equivalent heads for subterm selection *) +Goal f 0 = 0. +Proof. + rewrite lem. + reflexivity. +Qed. + +Print Equivalent Keys. +End foo. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index dea23d68c..a7be32328 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -674,6 +674,8 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Definition cardinal_e_2 ee := (cardinal_e (fst ee) + cardinal_e (snd ee))%nat. + Local Unset Keyed Unification. + Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t) { measure cardinal_e_2 ee } : comparison := match ee with diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index 6b3d86d39..b1769da3d 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -283,6 +283,8 @@ Module Update_WSets Lemma is_empty_spec : is_empty s = true <-> Empty s. Proof. intros; symmetry; apply MF.is_empty_iff. Qed. + + Declare Equivalent Keys In M.In. Lemma add_spec : In y (add x s) <-> E.eq y x \/ In y s. Proof. intros. rewrite MF.add_iff. intuition. Qed. diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index 88011ff1c..7398c6d65 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -306,6 +306,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. Notation "s [<=] t" := (Subset s t) (at level 70, no associativity). Definition eq := Equal. + + Declare Equivalent Keys Equal eq. + Definition lt m m' := compare_fun m m' = Lt. (** Specification of [In] *) diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 901574235..d1d9897fb 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -970,6 +970,8 @@ Definition lt (s1 s2 : tree) : Prop := exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2' /\ L.lt (elements s1') (elements s2'). +Declare Equivalent Keys L.eq equivlistA. + Instance lt_strorder : StrictOrder lt. Proof. split. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 1d5b78ec4..c9f3a774d 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -126,9 +126,7 @@ Let B (n : Z) := A (ZnZ.of_Z n). Lemma B0 : B 0. Proof. -unfold B. -setoid_replace (ZnZ.of_Z 0) with zero. assumption. -red; zify. apply ZnZ.of_Z_correct. auto using gt_wB_0 with zarith. +unfold B. apply A0. Qed. Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1). diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 8df4b7c64..dc35d087b 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -961,6 +961,11 @@ pr " end."; pr ""; pr " Ltac unfold_red := unfold reduce, %s." (iter_name 1 size "reduce_" ","); +pr ""; +for i = 0 to size do +pr " Declare Equivalent Keys reduce reduce_%i." i; +done; +pr " Declare Equivalent Keys reduce_n reduce_%i." (size + 1); pr " Ltac solve_red := diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index 161f523ca..e8a9940bd 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -320,6 +320,7 @@ Section CompareRec. Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n := (spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos). + Declare Equivalent Keys compare0_mn compare0_m. Lemma spec_compare0_mn: forall n x, compare0_mn n x = (0 ?= double_to_Z n x). diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index e866a52d6..b304b339b 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -88,6 +88,8 @@ exact BigQ.add_opp_diag_r. exact BigQ.neq_1_0. exact BigQ.div_mul_inv. exact BigQ.mul_inv_diag_l. Qed. +Declare Equivalent Keys pow_N pow_pos. + Lemma BigQpowerth : power_theory 1 BigQ.mul BigQ.eq Z.of_N BigQ.power. Proof. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index ad076c488..16f2661fe 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -172,13 +172,12 @@ Proof. apply sum_eq. intros; apply H1. unfold N; apply le_lt_trans with n; [ assumption | apply lt_n_Sn ]. - intros; unfold Bn, Cn. - replace (S N - S i)%nat with (N - i)%nat; reflexivity. + reflexivity. unfold An; fold N; rewrite <- minus_n_n; rewrite H0; simpl; ring. apply sum_eq. - intros; unfold An, Bn; replace (S N - S i)%nat with (N - i)%nat; - [ idtac | reflexivity ]. + intros; unfold An, Bn. + change (S N - S i)%nat with (N - i)%nat. rewrite <- pascal; [ ring | apply le_lt_trans with n; [ assumption | unfold N; apply lt_n_Sn ] ]. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 375cc2752..cf7b91af8 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -174,6 +174,8 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X') Definition R_met : Metric_Space := Build_Metric_Space R R_dist R_dist_pos R_dist_sym R_dist_refl R_dist_tri. +Declare Equivalent Keys dist R_dist. + (*******************************) (** * Limit 1 arg *) (*******************************) -- cgit v1.2.3