From bf4fdaa1836a17e4d36d38ba47959d1f50155a7b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 29 May 2018 23:07:02 +0200 Subject: [ssr] under: rewrite takes an optional bool arg * If this flag under=true: enable flag with_evars of refine_with to create evar(s) if the "under lemma" has non-inferable args. * Backward compatibility of ssr rewrite is kept. * Fix test-suite/ssr/dependent_type_err.v --- plugins/ssr/ssrequality.ml | 21 ++++++++++----------- plugins/ssr/ssrequality.mli | 1 + test-suite/prerequisite/ssr_mini_mathcomp.v | 2 ++ 3 files changed, 13 insertions(+), 11 deletions(-) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 5abbc214de..ccd0203b17 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -327,7 +327,7 @@ let rule_id = mk_internal_id "rewrite rule" exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option -let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = +let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (* ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *) let env = pf_env gl in let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in @@ -357,7 +357,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = in ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with - ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl + ~first_goes_last:(not !ssroldreworder) ~with_evars:under (sigma, proof) gl with _ -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with @@ -385,7 +385,7 @@ let is_construct_ref sigma c r = EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r -let rwcltac cl rdx dir sr gl = +let rwcltac ?under cl rdx dir sr gl = let sr = let sigma, r = sr in let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in @@ -405,7 +405,7 @@ let rwcltac cl rdx dir sr gl = match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in - pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl + pirrel_rewrite ?under cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl | _ -> let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in @@ -547,7 +547,7 @@ let rwprocess_rule dir rule gl = in r_sigma, rules -let rwrxtac occ rdx_pat dir rule gl = +let rwrxtac ?under occ rdx_pat dir rule gl = let env = pf_env gl in let r_sigma, rules = rwprocess_rule dir rule gl in let find_rule rdx = @@ -585,7 +585,7 @@ let rwrxtac occ rdx_pat dir rule gl = let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in - rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl + rwcltac ?under (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl ;; let ssrinstancesofrule ist dir arg gl = @@ -614,7 +614,7 @@ let ssrinstancesofrule ist dir arg gl = let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl -let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = +let rwargtac ?under ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = let fail = ref false in let interp_rpattern gl gc = try interp_rpattern gl gc @@ -628,7 +628,7 @@ let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt - | RWeq -> rwrxtac occ rx dir t) gl in + | RWeq -> rwrxtac ?under occ rx dir t) gl in let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl @@ -638,8 +638,8 @@ let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = (** The "rewrite" tactic *) -let ssrrewritetac ist rwargs = - tclTHENLIST (List.map (rwargtac ist) rwargs) +let ssrrewritetac ?under ist rwargs = + tclTHENLIST (List.map (rwargtac ?under ist) rwargs) (** The "unlock" tactic *) @@ -660,4 +660,3 @@ let unlocktac ist args gl = (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in tclTHENLIST (List.map utac args @ ktacs) gl - diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index bbcd6b900a..2f95d3f22b 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -49,6 +49,7 @@ val ssrinstancesofrule : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val ssrrewritetac : + ?under:bool -> Ltac_plugin.Tacinterp.interp_sign -> ((Ssrast.ssrdir * (int * Ssrast.ssrmmod)) * (((Ssrast.ssrhyps option * Ssrmatching.occ) * diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index cb2c56736c..ca360f65a7 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -427,6 +427,8 @@ Lemma leqnSn n : n <= n.+1. Proof. by elim: n. Qed. Lemma leq_trans n m p : m <= n -> n <= p -> m <= p. Admitted. +Lemma leq_ltn_trans n m p : m <= n -> n < p -> m < p. +Admitted. Lemma leqW m n : m <= n -> m <= n.+1. Admitted. Hint Resolve leqnSn. -- cgit v1.2.3 From 3a10b4d89d3d0ba3cdc8f85fbe3b66e8653da117 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 31 May 2018 16:08:59 +0200 Subject: [ssr] move is_ind/constructor_ref to ssrcommon --- plugins/ssr/ssrcommon.ml | 4 ++++ plugins/ssr/ssrcommon.mli | 3 +++ plugins/ssr/ssrequality.ml | 7 +------ 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 2a84469af0..ec9a937f80 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1540,5 +1540,9 @@ let get g = end +let is_construct_ref sigma c r = + EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r +let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r + (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 9662daa7c7..585db41de0 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -482,3 +482,6 @@ module MakeState(S : StateType) : sig val get : Proofview.Goal.t -> S.state end + +val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool +val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ccd0203b17..f55ece7d09 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -19,7 +19,6 @@ open Context open Vars open Locus open Printer -open Globnames open Termops open Tacinterp @@ -381,10 +380,6 @@ let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) ;; -let is_construct_ref sigma c r = - EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r -let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r - let rwcltac ?under cl rdx dir sr gl = let sr = let sigma, r = sr in @@ -403,7 +398,7 @@ let rwcltac ?under cl rdx dir sr gl = let sigma, c_ty = Typing.type_of env sigma c in ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with - | AtomicType(e, a) when is_ind_ref sigma e c_eq -> + | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in pirrel_rewrite ?under cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl | _ -> -- cgit v1.2.3 From 0e38043fc616a8a5dac3cdace8f7bed8f1e295ce Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 31 May 2018 16:09:28 +0200 Subject: [ssr] clean up type declaration of ssrrewritetac --- plugins/ssr/ssrequality.mli | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 2f95d3f22b..008c1d457c 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -51,11 +51,7 @@ val ssrinstancesofrule : val ssrrewritetac : ?under:bool -> Ltac_plugin.Tacinterp.interp_sign -> - ((Ssrast.ssrdir * (int * Ssrast.ssrmmod)) * - (((Ssrast.ssrhyps option * Ssrmatching.occ) * - Ssrmatching.rpattern option) * - (ssrwkind * Ssrast.ssrterm))) - list -> Tacmach.tactic + ssrrwarg list -> Tacmach.tactic val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic -- cgit v1.2.3 From cb7f2a54e6a1e8430f74bb9a02c24b22556b2287 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 31 May 2018 16:11:52 +0200 Subject: [ssr] fix implementation of refine ~first_goes_last --- plugins/ssr/ssrcommon.ml | 27 +++++++++++++-------------- plugins/ssr/ssrcommon.mli | 1 + 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index ec9a937f80..0b3bfab366 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -973,7 +973,7 @@ let dependent_apply_error = * * Refiner.refiner that does not handle metas with a non ground type but works * with dependently typed higher order metas. *) -let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = +let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t gl = if with_evars then let refine gl = let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in @@ -985,8 +985,11 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = pf_partial_solution gl t gs in Proofview.(V82.of_tactic - (tclTHEN (V82.tactic refine) - (if with_shelve then shelve_unifiable else tclUNIT ()))) gl + (Tacticals.New.tclTHENLIST [ + V82.tactic refine; + (if with_shelve then shelve_unifiable else tclUNIT ()); + (if first_goes_last then cycle 1 else tclUNIT ()) + ])) gl else let t, gl = if n = 0 then t, gl else let sigma, si = project gl, sig_it gl in @@ -1001,21 +1004,17 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); - Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl + Proofview.(V82.of_tactic + (Tacticals.New.tclTHENLIST [ + V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t)); + (if first_goes_last then cycle 1 else tclUNIT ()) + ])) gl let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = - let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in let uct = Evd.evar_universe_context (fst oc) in - let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.Unsafe.to_constr (snd oc)) in + let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in let gl = pf_unsafe_merge_uc uct gl in - let oc = if not first_goes_last || n <= 1 then oc else - let l, c = decompose_lam oc in - if not (List.for_all_i (fun i (_,t) -> Vars.closedn ~-i t) (1-n) l) then oc else - compose_lam (let xs,y = List.chop (n-1) l in y @ xs) - (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n))) - in - pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc)); - try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl + try applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error (* We wipe out all the keywords generated by the grammar rules we defined. *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 585db41de0..3049f67f87 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -312,6 +312,7 @@ val applyn : with_evars:bool -> ?beta:bool -> ?with_shelve:bool -> + ?first_goes_last:bool -> int -> EConstr.t -> v82tac exception NotEnoughProducts -- cgit v1.2.3 From 2b2b70d2f0487994db7effc7ced89a658c0cf4f3 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 24 Feb 2019 19:01:46 +0100 Subject: [ssr] under: Add opaque modules for tagging and notation support (Note: coq notations cannot contain \n) Co-authored-by: Enrico Tassi --- plugins/ssr/ssreflect.v | 50 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 4721e19a8b..e0b775f07b 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -500,3 +500,53 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. Lemma abstract_context T (P : T -> Type) x : (forall Q, Q = P -> Q x) -> P x. Proof. by move=> /(_ P); apply. Qed. + +(*****************************************************************************) +(* Syntax proposal for the under tactic: + +under i: eq_bigr by []. (* renaming *) + +under i: eq_bigr. + by rewrite addnC over. +(* oneliner version *) +under i: eq_bigr by rewrite adnnC. + +under i: lem => /andP [H1 H2]. + by rewrite addnC over. +(* oneliner version *) +under i: lem by move => /andP [H1 H2]; rewrite addnC. + +(* 2-var version *) +under i j: {2}[in RHS]eq_mx. +(* ... *) + +(* nested version *) +under i: eq_bigr=> ?; under j: eq_bigl. + *) + +Module Type UNDER. +Parameter Under : + forall (R : Type), R -> R -> Prop. +Parameter Under_from_eq : + forall (T : Type) (x y : T), + @Under T x y -> x = y. +Parameter over : + forall (T : Type) (x : T), + @Under T x x <-> True. +Notation "''Under[' x ]" := (@Under _ x _) + (at level 8, format "''Under[' x ]"). +End UNDER. + +Module Export Under : UNDER. +Definition Under := @eq. +Definition Under_done := @refl_equal. +Lemma Under_from_eq (T : Type) (x y : T) : + @Under T x y -> x = y. +Proof. easy. Qed. +Lemma over (T : Type) (x : T) : + @Under T x x <-> True. +Proof. easy. Qed. +End Under. + +Register Under as plugins.ssreflect.Under. +Register Under_from_eq as plugins.ssreflect.Under_from_eq. -- cgit v1.2.3 From 717f77bbaf479ae1e8335ce226ad71c2c88df644 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 31 May 2018 16:12:33 +0200 Subject: [ssr] implement "under i: ext_lemma" by rewrite rule Still to do: renaming the bound variables afterwards --- plugins/ssr/ssrfwd.ml | 63 +++++++++++++++++++++++++++++++++++++++++++++++ plugins/ssr/ssrfwd.mli | 3 +++ plugins/ssr/ssrparser.mlg | 5 ++++ test-suite/ssr/under.v | 29 ++++++++++++++++++++++ 4 files changed, 100 insertions(+) create mode 100644 test-suite/ssr/under.v diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 3cadc92bcc..ff7b891319 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -319,3 +319,66 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in basecuttac "ssr_suff" ty gl in Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))] + +open Proofview.Notations + +let is_app_evar sigma t = + match EConstr.kind sigma t with + | Constr.Evar _ -> true + | Constr.App(t,_) -> + begin match EConstr.kind sigma t with + | Constr.Evar _ -> true + | _ -> false end + | _ -> false + +let tmp = ref 0 + +let rec intro_lock names = Proofview.Goal.enter begin fun gl -> + let c = Proofview.Goal.concl gl in + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let rec aux c = + match EConstr.kind_of_type sigma c with + | Term.SortType _ -> Proofview.tclUNIT () + | ( Term.ProdType ({ Context.binder_name = name },_,t) + | Term.LetInType ({ Context.binder_name = name },_,_,t) ) -> + begin match names with + | n :: names -> Ssripats.(tclIPAT @@ [Ssripats.IOpId n]) <*> intro_lock names + | [] -> + (* after quell intro patterns, use IpatTemp *) + let id = + match name with + | Name.Anonymous -> Id.of_string (Printf.sprintf "_under_%d_" !tmp) + | Name.Name n -> n in + incr tmp; + Ssripats.tclIPAT [ + Ssripats.IOpId id; + Ssripats.IOpEqGen (intro_lock names); + Ssripats.IOpEqGen (Tactics.revert [id])] + end + | Term.CastType (t,_) -> aux t + | Term.AtomicType _ -> + let t = Reductionops.whd_all env sigma c in + match EConstr.kind_of_type sigma t with + | Term.AtomicType(hd, args) when + Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && + Array.length args = 3 && is_app_evar sigma args.(2) -> + Tactics.New.refine ~typecheck:true (fun sigma -> + let sigma, under = + Ssrcommon.mkSsrConst "Under" env sigma in + let sigma, under_from_eq = + Ssrcommon.mkSsrConst "Under_from_eq" env sigma in + let ty = EConstr.mkApp (under,args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|])) + | _ -> Proofview.tclUNIT () + in + aux c + +end + +let undertac ist varnames ((dir,mult),_ as rule) = + if mult <> Ssrequality.nomult then + Ssrcommon.errorstrm Pp.(str"Multiplicity not supported"); + Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ist [rule]) <*> + intro_lock varnames diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 35e89dbcea..fe7d84871e 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -57,3 +57,6 @@ val sufftac : (bool * Tacinterp.Value.t option list)) -> Tacmach.tactic +val undertac : + Ltac_plugin.Tacinterp.interp_sign -> + Names.Id.t list -> Ssrequality.ssrrwarg -> unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 0ec5f1673a..e63d1e5562 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -2650,6 +2650,11 @@ TACTIC EXTEND ssrgenhave2 V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) } END +TACTIC EXTEND under + | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ] -> + { Ssrfwd.undertac ist names r } +END + { (* We wipe out all the keywords generated by the grammar rules we defined. *) diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v new file mode 100644 index 0000000000..43d319737a --- /dev/null +++ b/test-suite/ssr/under.v @@ -0,0 +1,29 @@ +Require Import ssreflect. + +Inductive body := + mk_body : bool -> nat -> nat -> body. + +Axiom big : (nat -> body) -> nat. + +Axiom eq_big : + forall P Q F G, +(forall x, P x = Q x :> bool) -> + (forall x, (P x =true -> F x = G x : Type)) -> + big (fun x => mk_body (P x) (F x) x) = big (fun toto => mk_body (Q toto) (F toto) toto). + +Axiom leb : nat -> nat -> bool. + +Axiom admit : False. + +Lemma test : + (big (fun x => mk_body (leb x 3) (S x + x) x)) + = 3. +Proof. + + under i : {1}eq_big. + { by apply over. } + { move=> Pi. by apply over. } + rewrite /=. + + case: admit. +Qed. -- cgit v1.2.3 From 8b8ab996552d79ac070af80eb0978b523d929833 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Jun 2018 10:51:48 +0200 Subject: [ssr] rewrite takes optional function to make the new valued of the redex --- plugins/ssr/ssrequality.ml | 32 ++++++++++++++++---------------- plugins/ssr/ssrequality.mli | 5 +++++ 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index f55ece7d09..921dce4689 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -326,15 +326,15 @@ let rule_id = mk_internal_id "rewrite rule" exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option -let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = +let id_map_redex _ sigma ~before:_ ~after = sigma, after + +let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = (* ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *) let env = pf_env gl in let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in - let sigma, p = - let sigma = Evd.create_evar_defs sigma in - let (sigma, ev) = Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in - (sigma, ev) - in + let sigma, new_rdx = map_redex env sigma ~before:rdx ~after:new_rdx in + let sigma, p = (* The resulting goal *) + Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in let elim, gl = let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in @@ -354,7 +354,8 @@ let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te))) | e when CErrors.noncritical e -> raise (PRtype_error None) in - ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty)); + ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); + ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with ~first_goes_last:(not !ssroldreworder) ~with_evars:under (sigma, proof) gl with _ -> @@ -380,7 +381,7 @@ let pirrel_rewrite ?(under=false) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty)) ;; -let rwcltac ?under cl rdx dir sr gl = +let rwcltac ?under ?map_redex cl rdx dir sr gl = let sr = let sigma, r = sr in let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in @@ -400,7 +401,7 @@ let rwcltac ?under cl rdx dir sr gl = match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> let new_rdx = if dir = L2R then a.(2) else a.(1) in - pirrel_rewrite ?under cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl + pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl | _ -> let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in @@ -434,7 +435,6 @@ let rwcltac ?under cl rdx dir sr gl = in tclTHEN cvtac' rwtac gl - [@@@ocaml.warning "-3"] let lz_coq_prod = let prod = lazy (Coqlib.build_prod ()) in fun () -> Lazy.force prod @@ -542,7 +542,7 @@ let rwprocess_rule dir rule gl = in r_sigma, rules -let rwrxtac ?under occ rdx_pat dir rule gl = +let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl = let env = pf_env gl in let r_sigma, rules = rwprocess_rule dir rule gl in let find_rule rdx = @@ -580,7 +580,7 @@ let rwrxtac ?under occ rdx_pat dir rule gl = let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in - rwcltac ?under (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl + rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl ;; let ssrinstancesofrule ist dir arg gl = @@ -609,7 +609,7 @@ let ssrinstancesofrule ist dir arg gl = let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl -let rwargtac ?under ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = +let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = let fail = ref false in let interp_rpattern gl gc = try interp_rpattern gl gc @@ -623,7 +623,7 @@ let rwargtac ?under ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt - | RWeq -> rwrxtac ?under occ rx dir t) gl in + | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) gl in let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl @@ -633,8 +633,8 @@ let rwargtac ?under ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = (** The "rewrite" tactic *) -let ssrrewritetac ?under ist rwargs = - tclTHENLIST (List.map (rwargtac ?under ist) rwargs) +let ssrrewritetac ?under ?map_redex ist rwargs = + tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs) (** The "unlock" tactic *) diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 008c1d457c..601968d511 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -48,8 +48,13 @@ val ssrinstancesofrule : Ssrast.ssrterm -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma +(* map_redex (by default the identity on after) is called on the + * redex (before) and its replacement (after). It is used to + * "rename" binders by the under tactic *) val ssrrewritetac : ?under:bool -> + ?map_redex:(Environ.env -> Evd.evar_map -> + before:EConstr.t -> after:EConstr.t -> Evd.evar_map * EConstr.t) -> Ltac_plugin.Tacinterp.interp_sign -> ssrrwarg list -> Tacmach.tactic -- cgit v1.2.3 From 964779322e0358dc821b03a67b4a7dd0b3b6d11e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 2 Apr 2019 21:48:40 +0200 Subject: [ssr] under: Rename bound variables a posteriori for cosmetic purpose Rename the bound variables of the last (lambda) argument of the redex w.r.t. the varnames specified by the user. Co-authored-by: Erik Martin-Dorel --- plugins/ssr/ssrfwd.ml | 40 +++++++++++++++++++++++++++++++++++++++- test-suite/ssr/under.v | 2 +- 2 files changed, 40 insertions(+), 2 deletions(-) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index ff7b891319..29983e7504 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -377,8 +377,46 @@ let rec intro_lock names = Proofview.Goal.enter begin fun gl -> end +let rec pretty_rename evar_map term = function + | [] -> term + | varname :: varnames -> + try begin + match EConstr.destLambda evar_map term + with ({ Context.binder_relevance = r }, types, body) -> + let res = pretty_rename evar_map body varnames in + let name = Names.Name.mk_name varname in + (* Note: we don't explicitly check name \notin free_vars(res) here *) + EConstr.mkLambda (Context.make_annot name r, types, res) + end + with + | DestKO -> + ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda")); + term + let undertac ist varnames ((dir,mult),_ as rule) = if mult <> Ssrequality.nomult then Ssrcommon.errorstrm Pp.(str"Multiplicity not supported"); - Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ist [rule]) <*> + + let map_redex env evar_map ~before:_ ~after:t = + ppdebug(lazy Pp.(str("under vars: " ^ + (List.fold_right (fun e r -> Names.Id.to_string e ^ " " ^ r) varnames "")))); + ppdebug(lazy Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map t)); + + let evar_map, ty = Typing.type_of env evar_map t in + let new_t = (* pretty-rename the bound variables *) + try begin match EConstr.destApp evar_map t with (f, ar) -> + let lam = Array.last ar in + let new_lam = pretty_rename evar_map lam varnames in + let new_ar, len1 = Array.copy ar, pred (Array.length ar) in + new_ar.(len1) <- new_lam; + EConstr.mkApp (f, new_ar) + end with + | DestKO -> + ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp")); + t + in + ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); + evar_map, new_t + in + Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*> intro_lock varnames diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 43d319737a..9947d2bf4c 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -19,7 +19,7 @@ Lemma test : (big (fun x => mk_body (leb x 3) (S x + x) x)) = 3. Proof. - + Set Debug Ssreflect. under i : {1}eq_big. { by apply over. } { move=> Pi. by apply over. } -- cgit v1.2.3 From 2fed7b9a1870c7b921255ec055f0511ef530749d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 1 Jun 2018 15:37:17 +0200 Subject: [ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over" Both can be use to close the "under goals", in rewrite style or in closing-tactic style. Contrarily to the previous implementation that assumed "over : forall (T : Type) (x : T), @Under T x x <-> True" this new design won't require the Setoid library. Extend the test-suite (in test-suite/ssr/under.v) --- plugins/ssr/ssreflect.v | 42 +++++++++++++---- test-suite/ssr/under.v | 120 ++++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 148 insertions(+), 14 deletions(-) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index e0b775f07b..d2b44a869a 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -528,25 +528,49 @@ Module Type UNDER. Parameter Under : forall (R : Type), R -> R -> Prop. Parameter Under_from_eq : - forall (T : Type) (x y : T), - @Under T x y -> x = y. + forall (T : Type) (x y : T), @Under T x y -> x = y. + +(** [Over, over, over_done]: for "by rewrite over" *) +Parameter Over : + forall (R : Type), R -> R -> Prop. Parameter over : - forall (T : Type) (x : T), - @Under T x x <-> True. + forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y. +Parameter over_done : + forall (T : Type) (x : T), @Over T x x. +(* We need both hints below, otherwise the test-suite does not pass *) +Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core. +(* => for test_under_eq_big *) +Hint Resolve over_done : core. +(* => for test_over_1_1 *) + +(** [under_done]: for Ltac-style over *) +Parameter under_done : + forall (T : Type) (x : T), @Under T x x. Notation "''Under[' x ]" := (@Under _ x _) (at level 8, format "''Under[' x ]"). End UNDER. Module Export Under : UNDER. Definition Under := @eq. -Definition Under_done := @refl_equal. Lemma Under_from_eq (T : Type) (x y : T) : @Under T x y -> x = y. -Proof. easy. Qed. -Lemma over (T : Type) (x : T) : - @Under T x x <-> True. -Proof. easy. Qed. +Proof. by []. Qed. +Definition Over := Under. +Lemma over : + forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y. +Proof. by []. Qed. +Lemma over_done : + forall (T : Type) (x : T), @Over T x x. +Proof. by []. Qed. +Lemma under_done : + forall (T : Type) (x : T), @Under T x x. +Proof. by []. Qed. End Under. Register Under as plugins.ssreflect.Under. Register Under_from_eq as plugins.ssreflect.Under_from_eq. + +Ltac over := + by apply Under.under_done. +(* [exact: Under.under_done] woud be more satisfying, + but issue with 2-var test-suite (test_over_2_2) *) diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 9947d2bf4c..67e4316ba8 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -1,5 +1,75 @@ Require Import ssreflect. +Axiom admit : False. + +(** Testing over for the 1-var case *) +Lemma test_over_1_1 : forall i : nat, False. +intros. +evar (I : Type); evar (R : Type); evar (x2 : I -> R). +assert (H : i + 2 * i - i = x2 i). + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold I in *; clear I. + apply Under_from_eq. + Fail done. + + over. + case: admit. +Qed. + +Lemma test_over_1_2 : forall i : nat, False. +intros. +evar (I : Type); evar (R : Type); evar (x2 : I -> R). +assert (H : i + 2 * i - i = x2 i). + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold I in *; clear I. + apply Under_from_eq. + Fail done. + + by rewrite over. + case: admit. +Qed. + +(** Testing over for the 2-var case *) + +Lemma test_over_2_1 : forall i j : nat, False. +intros. +evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). +assert (H : i + 2 * j - i = x2 i j). + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold J in *; clear J; + unfold I in *; clear I. + apply Under_from_eq. + Fail done. + + Fail over. (* Bug: doesn't work so we have to make a beta-expansion by hand *) + rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *) + over. + case: admit. +Qed. + +Lemma test_over_2_2 : forall i j : nat, False. +intros. +evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). +assert (H : i + 2 * j - i = x2 i j). + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold J in *; clear J; + unfold I in *; clear I. + apply Under_from_eq. + Fail done. + + rewrite over. + Fail done. (* Bug: doesn't work so we have to make a beta-expansion by hand *) + rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *) + done. + case: admit. +Qed. + +(** Testing under for the 1-var case *) + Inductive body := mk_body : bool -> nat -> nat -> body. @@ -13,17 +83,57 @@ Axiom eq_big : Axiom leb : nat -> nat -> bool. -Axiom admit : False. +Axiom addnC : forall p q : nat, p + q = q + p. -Lemma test : +Lemma test_under_eq_big : (big (fun x => mk_body (leb x 3) (S x + x) x)) = 3. Proof. Set Debug Ssreflect. - under i : {1}eq_big. - { by apply over. } - { move=> Pi. by apply over. } + under i : {1}[in LHS]eq_big. + + { over. } + { move=> Pi; by rewrite addnC over. } + rewrite /=. case: admit. Qed. +Unset Debug Ssreflect. + +(** 2-var test + +Erik: Note that this axiomatization does not faithfully follow that of +mathcomp’s implementation of matrices. We may want to refine this test +once [eq_mx] has been integrated in mathcomp. *) + +Axiom I_ : nat -> Type. + +(* Inductive matrix (R : Type) (m n : nat) : Type := Matrix (_ : list (I_ m * I_ n * R)). *) +Inductive matrix (R : Type) (m n : nat) : Type := Matrix (_ : I_ m -> I_ n -> R). + +Axiom mx_of_fun : forall (R : Type) (m n : nat), + unit -> (I_ m -> I_ n -> R) -> matrix R m n. + +Axiom eq_mx : forall (R : Type) m n (k : unit) (F1 F2 : I_ m -> I_ n -> R), + (forall foo bar, F1 foo bar = F2 foo bar) -> + (mx_of_fun R m n k (fun a b => F1 a b)) = (mx_of_fun R m n k (fun c d => F2 c d)). +Arguments eq_mx [R m n k F1] F2 _. + +Definition fun_of_mx (R : Type) (m n : nat) (M : matrix R m n) := + let: Matrix _ _ _ F := M in F. + +Coercion fun_of_mx : matrix >-> Funclass. + +Definition addmx : forall (m n : nat) (A B : matrix nat m n), matrix nat m n := + fun m n A B => mx_of_fun nat m n tt (fun x y => A x y + B x y). +Arguments addmx [m n]. + +Lemma test_under_eq_mx (m n : nat) (A B C : matrix nat m n) : + addmx (addmx A B) C = addmx C (addmx A B). +Proof. +(* Set Debug Ssreflect. *) +under i j : [addmx C _ in RHS]eq_mx. + by rewrite addnC over. +done. +Qed. -- cgit v1.2.3 From 062dcd9c32e900242751a1ab84886f6aacac04d8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 1 Jun 2018 16:06:08 +0200 Subject: [ide] update coq-ssreflect.lang wrt under tactic --- ide/coq-ssreflect.lang | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang index bd9cb4bfa2..fc7bc64a68 100644 --- a/ide/coq-ssreflect.lang +++ b/ide/coq-ssreflect.lang @@ -73,11 +73,13 @@ suffices suff transitivity + under without loss wlog by + over exact reflexivity -- cgit v1.2.3 From 527e6a97d1429a58273ddc6b4ce2826df0dba1c6 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 24 Feb 2019 16:08:36 +0100 Subject: [ssr] over: also works on universally quantified goals --- plugins/ssr/ssreflect.v | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index d2b44a869a..e705942c36 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -571,6 +571,14 @@ Register Under as plugins.ssreflect.Under. Register Under_from_eq as plugins.ssreflect.Under_from_eq. Ltac over := - by apply Under.under_done. -(* [exact: Under.under_done] woud be more satisfying, - but issue with 2-var test-suite (test_over_2_2) *) + solve [ apply Under.under_done | by rewrite over ]. + +(* The 2 variants below wouldn't work for the [test_over_2_1] test + (2-var case with evars) + +Ltac over := + exact: Under.under_done. + +Ltac over := + by rewrite over. + *) -- cgit v1.2.3 From 1a5a4c9c8cacea6e6ed7ced8766cadb0195655d9 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 24 Feb 2019 18:30:00 +0100 Subject: [ssr] under: Add support for one-liners "under (…) by [tac1|tac2]." Supported syntax: under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created *) under i: eq_big by [rewrite adnnC | rewrite addnC]. (* 2 Under subgoals *) Equivalent, expanded form: under i: eq_bigr; [rewrite adnnC; over | idtac]. under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | idtac]. --- plugins/ssr/ssrfwd.ml | 18 +++++++++++++++--- plugins/ssr/ssrfwd.mli | 3 ++- plugins/ssr/ssrparser.mlg | 4 ++-- 3 files changed, 19 insertions(+), 6 deletions(-) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 29983e7504..570b5a8c61 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -393,7 +393,9 @@ let rec pretty_rename evar_map term = function ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda")); term -let undertac ist varnames ((dir,mult),_ as rule) = +let overtac gl = ssr_n_tac "over" ~-1 gl + +let undertac ist varnames ((dir,mult),_ as rule) hint = if mult <> Ssrequality.nomult then Ssrcommon.errorstrm Pp.(str"Multiplicity not supported"); @@ -418,5 +420,15 @@ let undertac ist varnames ((dir,mult),_ as rule) = ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); evar_map, new_t in - Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*> - intro_lock varnames + let undertacs = + if hint = nohint then + Proofview.tclUNIT () + else + Proofview.tclDISPATCH + ((List.map (function None -> Proofview.V82.tactic overtac + | Some e -> ssrevaltac ist e <*> + Proofview.V82.tactic overtac) + (if hint = nullhint then [None] else snd hint)) @ [Proofview.tclUNIT ()]) + in + (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*> + intro_lock varnames <*> undertacs) diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index fe7d84871e..63df8f5349 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -59,4 +59,5 @@ val sufftac : val undertac : Ltac_plugin.Tacinterp.interp_sign -> - Names.Id.t list -> Ssrequality.ssrrwarg -> unit Proofview.tactic + Names.Id.t list -> Ssrequality.ssrrwarg -> + Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index e63d1e5562..507cf8db70 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -2651,8 +2651,8 @@ TACTIC EXTEND ssrgenhave2 END TACTIC EXTEND under - | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ] -> - { Ssrfwd.undertac ist names r } + | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ssrhint(hint) ] -> + { Ssrfwd.undertac ist names r hint } END { -- cgit v1.2.3 From e22d8f725bae56550fed8cab8640447953cd3a47 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 25 Feb 2019 00:04:44 +0100 Subject: [ssr] under: generate missing Under subgoal for eq_bigl/eq_big in the particular case where the side-condition is phrased (_ : @eqfun bool I P1 P2) instead of (_ : forall x : I, P1 x = P2 x) --- plugins/ssr/ssrfwd.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 570b5a8c61..491d6cfb33 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -360,6 +360,7 @@ let rec intro_lock names = Proofview.Goal.enter begin fun gl -> | Term.AtomicType _ -> let t = Reductionops.whd_all env sigma c in match EConstr.kind_of_type sigma t with + | Term.ProdType _ -> aux t | Term.AtomicType(hd, args) when Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && Array.length args = 3 && is_app_evar sigma args.(2) -> -- cgit v1.2.3 From 8279f7673c89254139869ac3a3688e12658db471 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 24 Feb 2019 22:21:15 +0100 Subject: [ssr] under: Extend the test-suite to exemplify most use cases --- plugins/ssr/ssreflect.v | 30 +---- test-suite/ssr/over.v | 70 ++++++++++++ test-suite/ssr/under.v | 295 ++++++++++++++++++++++++++++-------------------- 3 files changed, 249 insertions(+), 146 deletions(-) create mode 100644 test-suite/ssr/over.v diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index e705942c36..229f6ceb1a 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -502,27 +502,7 @@ Lemma abstract_context T (P : T -> Type) x : Proof. by move=> /(_ P); apply. Qed. (*****************************************************************************) -(* Syntax proposal for the under tactic: - -under i: eq_bigr by []. (* renaming *) - -under i: eq_bigr. - by rewrite addnC over. -(* oneliner version *) -under i: eq_bigr by rewrite adnnC. - -under i: lem => /andP [H1 H2]. - by rewrite addnC over. -(* oneliner version *) -under i: lem by move => /andP [H1 H2]; rewrite addnC. - -(* 2-var version *) -under i j: {2}[in RHS]eq_mx. -(* ... *) - -(* nested version *) -under i: eq_bigr=> ?; under j: eq_bigl. - *) +(* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *) Module Type UNDER. Parameter Under : @@ -539,9 +519,9 @@ Parameter over_done : forall (T : Type) (x : T), @Over T x x. (* We need both hints below, otherwise the test-suite does not pass *) Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core. -(* => for test_under_eq_big *) +(* => for [test-suite/ssr/under.v:test_big_nested_1] *) Hint Resolve over_done : core. -(* => for test_over_1_1 *) +(* => for [test-suite/ssr/over.v:test_over_1_1] *) (** [under_done]: for Ltac-style over *) Parameter under_done : @@ -573,8 +553,8 @@ Register Under_from_eq as plugins.ssreflect.Under_from_eq. Ltac over := solve [ apply Under.under_done | by rewrite over ]. -(* The 2 variants below wouldn't work for the [test_over_2_1] test - (2-var case with evars) +(* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1] + (2-var test case with evars). Ltac over := exact: Under.under_done. diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v new file mode 100644 index 0000000000..c6bccd1d77 --- /dev/null +++ b/test-suite/ssr/over.v @@ -0,0 +1,70 @@ +Require Import ssreflect. + +Axiom daemon : False. Ltac myadmit := case: daemon. + +(** Testing over for the 1-var case *) + +Lemma test_over_1_1 : forall i : nat, False. +intros. +evar (I : Type); evar (R : Type); evar (x2 : I -> R). +assert (H : i + 2 * i - i = x2 i). + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold I in *; clear I. + apply Under_from_eq. + Fail done. + + over. + myadmit. +Qed. + +Lemma test_over_1_2 : forall i : nat, False. +intros. +evar (I : Type); evar (R : Type); evar (x2 : I -> R). +assert (H : i + 2 * i - i = x2 i). + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold I in *; clear I. + apply Under_from_eq. + Fail done. + + by rewrite over. + myadmit. +Qed. + +(** Testing over for the 2-var case *) + +Lemma test_over_2_1 : forall i j : nat, False. +intros. +evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). +assert (H : i + 2 * j - i = x2 i j). + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold J in *; clear J; + unfold I in *; clear I. + apply Under_from_eq. + Fail done. + + Fail over. (* Bug: doesn't work so we have to make a beta-expansion by hand *) + rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *) + over. + myadmit. +Qed. + +Lemma test_over_2_2 : forall i j : nat, False. +intros. +evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). +assert (H : i + 2 * j - i = x2 i j). + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold J in *; clear J; + unfold I in *; clear I. + apply Under_from_eq. + Fail done. + + rewrite over. + Fail done. (* Bug: doesn't work so we have to make a beta-expansion by hand *) + rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *) + done. + myadmit. +Qed. diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 67e4316ba8..066f89cfcf 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -1,139 +1,192 @@ Require Import ssreflect. -Axiom admit : False. - -(** Testing over for the 1-var case *) -Lemma test_over_1_1 : forall i : nat, False. -intros. -evar (I : Type); evar (R : Type); evar (x2 : I -> R). -assert (H : i + 2 * i - i = x2 i). - unfold x2 in *; clear x2; - unfold R in *; clear R; - unfold I in *; clear I. - apply Under_from_eq. - Fail done. +(* under : {occs}[patt]. + under : {occs}[patt] by tac1. + under : {occs}[patt] by [tac1 | ...]. + *) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Axiom daemon : False. Ltac myadmit := case: daemon. + +Module Mocks. + +(* Mock bigop.v definitions to test the behavior of under with bigops + without requiring mathcomp *) + +Variant bigbody (R I : Type) : Type := + BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I. + +Parameter bigop : + forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R. + +Definition eqfun := + fun (A B : Type) (f g : forall _ : B, A) => forall x : B, @eq A (f x) (g x). + +Definition pred := fun T : Type => forall _ : T, bool. + +Section Defix. +Variables (T : Type) (n : nat) (f : forall _ : T, T) (x : T). +Fixpoint loop (m : nat) : T := + match m return T with + | O => x + | S i => f (loop i) + end. +Definition iter := loop n. +End Defix. + +Definition addn := nosimpl plus. +Definition subn := nosimpl minus. +Definition muln := nosimpl mult. + +Fixpoint seq_iota (m n : nat) {struct n} : list nat := + match n return (list nat) with + | O => @nil nat + | S n' => @cons nat m (seq_iota (S m) n') + end. + +Definition index_iota := fun m n : nat => seq_iota m (subn n m). + +Parameter eq_bigl : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P1 P2 : pred I) (F : forall _ : I, R) (_ : @eqfun bool I P1 P2), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P1 i) (F i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P2 i) (F i))). + +Parameter eq_big : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P1 P2 : pred I) (F1 F2 : forall _ : I, R) (_ : @eqfun bool I P1 P2) + (_ : forall (i : I) (_ : is_true (P1 i)), @eq R (F1 i) (F2 i)), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P1 i) (F1 i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P2 i) (F2 i))). + +Parameter eq_bigr : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P : pred I) (F1 F2 : forall _ : I, R) + (_ : forall (i : I) (_ : is_true (P i)), @eq R (F1 i) (F2 i)), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P i) (F1 i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P i) (F2 i))). + +Parameter big_const_nat : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (m n : nat) (x : R), + @eq R (@bigop R nat idx (index_iota m n) (fun i : nat => @BigBody R nat i op true x)) + (@iter R (subn n m) (op x) idx). + +Delimit Scope bool_scope with B. +Open Scope bool_scope. + +Delimit Scope N_scope with num. +Delimit Scope nat_scope with N. + +Delimit Scope big_scope with BIG. +Open Scope big_scope. + +Reserved Notation "~~ b" (at level 35, right associativity). +Notation "~~ b" := (negb b) : bool_scope. + +Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" + (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50, + format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'"). +Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F" + (at level 36, F at level 36, op, idx at level 10, i, m, n at level 50, + format "'[' \big [ op / idx ]_ ( m <= i < n ) '/ ' F ']'"). + +Reserved Notation "\sum_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\sum_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n ) '/ ' F ']'"). + +Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" := + (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%B F)) + : big_scope. +Notation "\big [ op / idx ]_ ( m <= i < n ) F" := + (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F)) + : big_scope. + +Local Notation "+%N" := addn (at level 0, only parsing). +Notation "\sum_ ( m <= i < n | P ) F" := + (\big[+%N/0%N]_(m <= i < n | P%B) F%N) : nat_scope. +Notation "\sum_ ( m <= i < n ) F" := + (\big[+%N/0%N]_(m <= i < n) F%N) : nat_scope. + +Fixpoint odd n := if n is S n' then ~~ odd n' else false. + +Parameter addnC : forall m n : nat, m + n = n + m. +Parameter mulnC : forall m n : nat, m * n = n * m. +Parameter addnA : forall x y z : nat, x + (y + z) = ((x + y) + z). +Parameter mulnA : forall x y z : nat, x * (y * z) = ((x * y) * z). + +Parameter iter_addn_0 : forall m n : nat, @eq nat (@iter nat n (addn m) O) (muln m n). + +Notation "x == y" := (Nat.eqb x y) + (at level 70, no associativity) : bool_scope. +End Mocks. + +Import Mocks. + +(*****************************************************************************) + +Lemma test_big_nested_1 (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). +Proof. +(* in interactive mode *) +under i Hi: eq_bigr. + under j Hj: eq_big. + { by rewrite mulnC /= addnC /= over. } + { by rewrite addnC over. } over. - case: admit. +done. Qed. -Lemma test_over_1_2 : forall i : nat, False. -intros. -evar (I : Type); evar (R : Type); evar (x2 : I -> R). -assert (H : i + 2 * i - i = x2 i). - unfold x2 in *; clear x2; - unfold R in *; clear R; - unfold I in *; clear I. - apply Under_from_eq. - Fail done. - - by rewrite over. - case: admit. +Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). +Proof. +(* in one-liner mode *) +under i I: eq_bigr by under j J: eq_big by [rewrite mulnC /= addnC|rewrite addnC]. +done. Qed. -(** Testing over for the 2-var case *) - -Lemma test_over_2_1 : forall i j : nat, False. -intros. -evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). -assert (H : i + 2 * j - i = x2 i j). - unfold x2 in *; clear x2; - unfold R in *; clear R; - unfold J in *; clear J; - unfold I in *; clear I. - apply Under_from_eq. - Fail done. - - Fail over. (* Bug: doesn't work so we have to make a beta-expansion by hand *) - rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *) +Lemma test_big_patt1 (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0. +Proof. +under i Hi: [in RHS]eq_bigr. + rewrite addnC. over. - case: admit. +done. Qed. -Lemma test_over_2_2 : forall i j : nat, False. -intros. -evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). -assert (H : i + 2 * j - i = x2 i j). - unfold x2 in *; clear x2; - unfold R in *; clear R; - unfold J in *; clear J; - unfold I in *; clear I. - apply Under_from_eq. - Fail done. - - rewrite over. - Fail done. (* Bug: doesn't work so we have to make a beta-expansion by hand *) - rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *) - done. - case: admit. +Lemma test_big_patt2 (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (F i + F i) = + \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2). +Proof. +under i Hi: [X in _ = _ + X]eq_bigr. + (* the proof is not idiomatic as mathcomp lemmas are not available here *) + rewrite mulnC /= addnA -plus_n_O. + over. +by rewrite big_const_nat iter_addn_0. Qed. -(** Testing under for the 1-var case *) - -Inductive body := - mk_body : bool -> nat -> nat -> body. - -Axiom big : (nat -> body) -> nat. - -Axiom eq_big : - forall P Q F G, -(forall x, P x = Q x :> bool) -> - (forall x, (P x =true -> F x = G x : Type)) -> - big (fun x => mk_body (P x) (F x) x) = big (fun toto => mk_body (Q toto) (F toto) toto). - -Axiom leb : nat -> nat -> bool. - -Axiom addnC : forall p q : nat, p + q = q + p. - -Lemma test_under_eq_big : - (big (fun x => mk_body (leb x 3) (S x + x) x)) - = 3. +Lemma test_big_occs (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0). Proof. - Set Debug Ssreflect. - under i : {1}[in LHS]eq_big. - - { over. } - { move=> Pi; by rewrite addnC over. } - - rewrite /=. - - case: admit. +under i Hi: {2}[in RHS]eq_bigr. + by rewrite mulnC /= over. +by rewrite big_const_nat iter_addn_0. Qed. -Unset Debug Ssreflect. - -(** 2-var test - -Erik: Note that this axiomatization does not faithfully follow that of -mathcomp’s implementation of matrices. We may want to refine this test -once [eq_mx] has been integrated in mathcomp. *) - -Axiom I_ : nat -> Type. - -(* Inductive matrix (R : Type) (m n : nat) : Type := Matrix (_ : list (I_ m * I_ n * R)). *) -Inductive matrix (R : Type) (m n : nat) : Type := Matrix (_ : I_ m -> I_ n -> R). -Axiom mx_of_fun : forall (R : Type) (m n : nat), - unit -> (I_ m -> I_ n -> R) -> matrix R m n. - -Axiom eq_mx : forall (R : Type) m n (k : unit) (F1 F2 : I_ m -> I_ n -> R), - (forall foo bar, F1 foo bar = F2 foo bar) -> - (mx_of_fun R m n k (fun a b => F1 a b)) = (mx_of_fun R m n k (fun c d => F2 c d)). -Arguments eq_mx [R m n k F1] F2 _. - -Definition fun_of_mx (R : Type) (m n : nat) (M : matrix R m n) := - let: Matrix _ _ _ F := M in F. - -Coercion fun_of_mx : matrix >-> Funclass. - -Definition addmx : forall (m n : nat) (A B : matrix nat m n), matrix nat m n := - fun m n A B => mx_of_fun nat m n tt (fun x y => A x y + B x y). -Arguments addmx [m n]. - -Lemma test_under_eq_mx (m n : nat) (A B C : matrix nat m n) : - addmx (addmx A B) C = addmx C (addmx A B). +(* Solely used, one such renaming is useless in practice, but it works anyway *) +Lemma test_big_cosmetic (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). Proof. -(* Set Debug Ssreflect. *) -under i j : [addmx C _ in RHS]eq_mx. - by rewrite addnC over. -done. +under a A: [RHS]eq_bigr by under b B: eq_bigr by []. (* renaming bound vars *) +simpl. +myadmit. Qed. -- cgit v1.2.3 From 540a581a42114d7cf19b0135d7ad3702fa7cdaca Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 25 Feb 2019 01:52:27 +0100 Subject: [ssr] under: Strenghten over & Add test_big_andb * Rely on a new tactic unify_helper that workarounds the fact [apply Under.under_done] cannot unify (?G i...) with (expr i...) in [|- @Under T (expr i...) (?G i...)] when expr is a constant expression, or has more than one var (i...). Idea: massage the expression with Ltac to obtain a beta redex. * Simplify test-suite/ssr/under.v by using TestSuite.ssr_mini_mathcomp and add a test-case [test_big_andb]. * Summary of commands to quickly test [under]: $ cd .../coq $ make plugins/ssr/ssreflect.vo plugins/ssr/ssrfun.vo plugins/ssr/ssrbool.vo $ cd test-suite $ touch prerequisite/ssr_mini_mathcomp.v $ make $ emacs under.v --- plugins/ssr/ssreflect.v | 27 ++++++++++++++++- test-suite/ssr/over.v | 5 ++-- test-suite/ssr/under.v | 77 ++++++++++++------------------------------------- 3 files changed, 46 insertions(+), 63 deletions(-) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 229f6ceb1a..7e2c1c913f 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -550,8 +550,33 @@ End Under. Register Under as plugins.ssreflect.Under. Register Under_from_eq as plugins.ssreflect.Under_from_eq. +Ltac beta_expand c e := + match e with + | ?G ?z => + let T := type of z in + match c with + | context f [z] => + let b := constr:(fun x : T => ltac:(let r := context f [x] in refine r)) in + rewrite -{1}[c]/(b z); beta_expand b G + | (* constante *) _ => + let b := constr:(fun x : T => ltac:(exact c)) in + rewrite -{1}[c]/(b z); beta_expand b G + end + | ?G => idtac + end. + +Ltac unify_helper := + move=> *; + lazymatch goal with + | [ |- @Under _ ?c ?e ] => + beta_expand c e + end. + Ltac over := - solve [ apply Under.under_done | by rewrite over ]. + solve [ apply Under.under_done + | by rewrite over + | unify_helper; eapply Under.under_done + ]. (* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1] (2-var test case with evars). diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v index c6bccd1d77..3bb5c03e08 100644 --- a/test-suite/ssr/over.v +++ b/test-suite/ssr/over.v @@ -45,8 +45,6 @@ assert (H : i + 2 * j - i = x2 i j). apply Under_from_eq. Fail done. - Fail over. (* Bug: doesn't work so we have to make a beta-expansion by hand *) - rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *) over. myadmit. Qed. @@ -64,7 +62,8 @@ assert (H : i + 2 * j - i = x2 i j). rewrite over. Fail done. (* Bug: doesn't work so we have to make a beta-expansion by hand *) - rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). (* todo: automate? *) + rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). + (* cf. [plugins/ssr/ssreflect.v:unify_helper] *) done. myadmit. Qed. diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 066f89cfcf..cc85b96a3a 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -1,4 +1,6 @@ Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. +Global Unset SsrOldRewriteGoalsOrder. (* under : {occs}[patt]. under : {occs}[patt] by tac1. @@ -16,17 +18,9 @@ Module Mocks. (* Mock bigop.v definitions to test the behavior of under with bigops without requiring mathcomp *) -Variant bigbody (R I : Type) : Type := - BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I. - -Parameter bigop : - forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R. - Definition eqfun := fun (A B : Type) (f g : forall _ : B, A) => forall x : B, @eq A (f x) (g x). -Definition pred := fun T : Type => forall _ : T, bool. - Section Defix. Variables (T : Type) (n : nat) (f : forall _ : T, T) (x : T). Fixpoint loop (m : nat) : T := @@ -37,18 +31,6 @@ Fixpoint loop (m : nat) : T := Definition iter := loop n. End Defix. -Definition addn := nosimpl plus. -Definition subn := nosimpl minus. -Definition muln := nosimpl mult. - -Fixpoint seq_iota (m n : nat) {struct n} : list nat := - match n return (list nat) with - | O => @nil nat - | S n' => @cons nat m (seq_iota (S m) n') - end. - -Definition index_iota := fun m n : nat => seq_iota m (subn n m). - Parameter eq_bigl : forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) (r : list I) (P1 P2 : pred I) (F : forall _ : I, R) (_ : @eqfun bool I P1 P2), @@ -74,25 +56,9 @@ Parameter big_const_nat : @eq R (@bigop R nat idx (index_iota m n) (fun i : nat => @BigBody R nat i op true x)) (@iter R (subn n m) (op x) idx). -Delimit Scope bool_scope with B. -Open Scope bool_scope. - Delimit Scope N_scope with num. Delimit Scope nat_scope with N. -Delimit Scope big_scope with BIG. -Open Scope big_scope. - -Reserved Notation "~~ b" (at level 35, right associativity). -Notation "~~ b" := (negb b) : bool_scope. - -Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" - (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50, - format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'"). -Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F" - (at level 36, F at level 36, op, idx at level 10, i, m, n at level 50, - format "'[' \big [ op / idx ]_ ( m <= i < n ) '/ ' F ']'"). - Reserved Notation "\sum_ ( m <= i < n | P ) F" (at level 41, F at level 41, i, m, n at level 50, format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). @@ -100,31 +66,15 @@ Reserved Notation "\sum_ ( m <= i < n ) F" (at level 41, F at level 41, i, m, n at level 50, format "'[' \sum_ ( m <= i < n ) '/ ' F ']'"). -Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" := - (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%B F)) - : big_scope. -Notation "\big [ op / idx ]_ ( m <= i < n ) F" := - (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F)) - : big_scope. - Local Notation "+%N" := addn (at level 0, only parsing). Notation "\sum_ ( m <= i < n | P ) F" := - (\big[+%N/0%N]_(m <= i < n | P%B) F%N) : nat_scope. + (\big[+%N/0%N]_(m <= i < n | P%B) F%N) : (*nat_scope*) big_scope. Notation "\sum_ ( m <= i < n ) F" := - (\big[+%N/0%N]_(m <= i < n) F%N) : nat_scope. - -Fixpoint odd n := if n is S n' then ~~ odd n' else false. - -Parameter addnC : forall m n : nat, m + n = n + m. -Parameter mulnC : forall m n : nat, m * n = n * m. -Parameter addnA : forall x y z : nat, x + (y + z) = ((x + y) + z). -Parameter mulnA : forall x y z : nat, x * (y * z) = ((x * y) * z). + (\big[+%N/0%N]_(m <= i < n) F%N) : (*nat_scope*) big_scope. Parameter iter_addn_0 : forall m n : nat, @eq nat (@iter nat n (addn m) O) (muln m n). -Notation "x == y" := (Nat.eqb x y) - (at level 70, no associativity) : bool_scope. End Mocks. Import Mocks. @@ -138,7 +88,7 @@ Proof. (* in interactive mode *) under i Hi: eq_bigr. under j Hj: eq_big. - { by rewrite mulnC /= addnC /= over. } + { by rewrite muln1 over. } { by rewrite addnC over. } over. done. @@ -149,7 +99,7 @@ Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) : \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). Proof. (* in one-liner mode *) -under i I: eq_bigr by under j J: eq_big by [rewrite mulnC /= addnC|rewrite addnC]. +under i Hi: eq_bigr by under j Hj: eq_big by [rewrite muln1 | rewrite addnC]. done. Qed. @@ -167,8 +117,7 @@ Lemma test_big_patt2 (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2). Proof. under i Hi: [X in _ = _ + X]eq_bigr. - (* the proof is not idiomatic as mathcomp lemmas are not available here *) - rewrite mulnC /= addnA -plus_n_O. + rewrite mulnS muln1. over. by rewrite big_const_nat iter_addn_0. Qed. @@ -177,7 +126,7 @@ Lemma test_big_occs (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0). Proof. under i Hi: {2}[in RHS]eq_bigr. - by rewrite mulnC /= over. + by rewrite muln0 /= over. by rewrite big_const_nat iter_addn_0. Qed. @@ -190,3 +139,13 @@ under a A: [RHS]eq_bigr by under b B: eq_bigr by []. (* renaming bound vars *) simpl. myadmit. Qed. + +Lemma test_big_andb (F : nat -> nat) (m n : nat) : + \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1. +Proof. +under i: eq_bigl by rewrite andb_idl; first by move/eqP->. +simpl. +under i: eq_bigr by move/eqP=>{1}->. (* the 2nd occ should not be touched *) +simpl. +myadmit. +Qed. -- cgit v1.2.3 From 0a00a122a04ed9afdaccc2dae85e61d51d5d7a89 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 25 Feb 2019 02:05:40 +0100 Subject: [ssr] under: Move {beta_expand, unify_helper} in the module type (qualify them) --- plugins/ssr/ssreflect.v | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 7e2c1c913f..f8d761b088 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -528,27 +528,6 @@ Parameter under_done : forall (T : Type) (x : T), @Under T x x. Notation "''Under[' x ]" := (@Under _ x _) (at level 8, format "''Under[' x ]"). -End UNDER. - -Module Export Under : UNDER. -Definition Under := @eq. -Lemma Under_from_eq (T : Type) (x y : T) : - @Under T x y -> x = y. -Proof. by []. Qed. -Definition Over := Under. -Lemma over : - forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y. -Proof. by []. Qed. -Lemma over_done : - forall (T : Type) (x : T), @Over T x x. -Proof. by []. Qed. -Lemma under_done : - forall (T : Type) (x : T), @Under T x x. -Proof. by []. Qed. -End Under. - -Register Under as plugins.ssreflect.Under. -Register Under_from_eq as plugins.ssreflect.Under_from_eq. Ltac beta_expand c e := match e with @@ -571,6 +550,27 @@ Ltac unify_helper := | [ |- @Under _ ?c ?e ] => beta_expand c e end. +End UNDER. + +Module Export Under : UNDER. +Definition Under := @eq. +Lemma Under_from_eq (T : Type) (x y : T) : + @Under T x y -> x = y. +Proof. by []. Qed. +Definition Over := Under. +Lemma over : + forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y. +Proof. by []. Qed. +Lemma over_done : + forall (T : Type) (x : T), @Over T x x. +Proof. by []. Qed. +Lemma under_done : + forall (T : Type) (x : T), @Under T x x. +Proof. by []. Qed. +End Under. + +Register Under as plugins.ssreflect.Under. +Register Under_from_eq as plugins.ssreflect.Under_from_eq. Ltac over := solve [ apply Under.under_done -- cgit v1.2.3 From d8b8893f7700e17700ca40c52b69a0a554b2da2f Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 25 Feb 2019 02:25:31 +0100 Subject: [ssr] under: Add a fancy test with several kinds of side-conditions --- test-suite/ssr/under.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index cc85b96a3a..190277aa31 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -149,3 +149,22 @@ under i: eq_bigr by move/eqP=>{1}->. (* the 2nd occ should not be touched *) simpl. myadmit. Qed. + +Lemma test_foo (f1 f2 : nat -> nat) (f_eq : forall n, f1 n = f2 n) + (G : (nat -> nat) -> nat) + (Lem : forall f1 f2 : nat -> nat, + True -> + (forall n, f1 n = f2 n) -> + False = False -> + G f1 = G f2) : + G f1 = G f2. +Proof. +(* +under x: Lem. +- done. +- rewrite f_eq; over. +- done. + *) +under x: Lem by [done|rewrite f_eq|done]. +done. +Qed. -- cgit v1.2.3 From d9db4dec813a18b205f1cd9bccca54aa23524706 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 25 Feb 2019 02:58:45 +0100 Subject: [ssr] under: Change the style of a few tests (over tactic vs. lemma) --- plugins/ssr/ssreflect.v | 2 +- test-suite/ssr/under.v | 14 +++++--------- 2 files changed, 6 insertions(+), 10 deletions(-) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index f8d761b088..c78381d3cc 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -519,7 +519,7 @@ Parameter over_done : forall (T : Type) (x : T), @Over T x x. (* We need both hints below, otherwise the test-suite does not pass *) Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core. -(* => for [test-suite/ssr/under.v:test_big_nested_1] *) +(* => for [test-suite/ssr/under.v:test_big_patt1] *) Hint Resolve over_done : core. (* => for [test-suite/ssr/over.v:test_over_1_1] *) diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 190277aa31..7db2f2a982 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -88,8 +88,8 @@ Proof. (* in interactive mode *) under i Hi: eq_bigr. under j Hj: eq_big. - { by rewrite muln1 over. } - { by rewrite addnC over. } + { rewrite muln1. over. } + { rewrite addnC. over. } over. done. Qed. @@ -107,8 +107,7 @@ Lemma test_big_patt1 (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0. Proof. under i Hi: [in RHS]eq_bigr. - rewrite addnC. - over. + by rewrite addnC over. done. Qed. @@ -116,17 +115,14 @@ Lemma test_big_patt2 (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (F i + F i) = \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2). Proof. -under i Hi: [X in _ = _ + X]eq_bigr. - rewrite mulnS muln1. - over. +under i Hi: [X in _ = _ + X]eq_bigr by rewrite mulnS muln1. by rewrite big_const_nat iter_addn_0. Qed. Lemma test_big_occs (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0). Proof. -under i Hi: {2}[in RHS]eq_bigr. - by rewrite muln0 /= over. +under i Hi: {2}[in RHS]eq_bigr by rewrite muln0. by rewrite big_const_nat iter_addn_0. Qed. -- cgit v1.2.3 From 605d0e3e79fe1f654150c5ba14a1cbe3b5a0d78a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 25 Feb 2019 13:16:45 +0100 Subject: [ssr] under(one-liner version): Do nf_betaiota in the last goal As a result, the following: under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created *) under i: eq_big by [rewrite adnnC | rewrite addnC]. (* 2 Under subgoals *) amounts to: under i: eq_bigr; [rewrite adnnC; over | cbv beta iota]. under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | cbv beta iota]. --- plugins/ssr/ssrfwd.ml | 4 +++- test-suite/ssr/under.v | 3 --- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 491d6cfb33..be2732513f 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -425,11 +425,13 @@ let undertac ist varnames ((dir,mult),_ as rule) hint = if hint = nohint then Proofview.tclUNIT () else + let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in Proofview.tclDISPATCH ((List.map (function None -> Proofview.V82.tactic overtac | Some e -> ssrevaltac ist e <*> Proofview.V82.tactic overtac) - (if hint = nullhint then [None] else snd hint)) @ [Proofview.tclUNIT ()]) + (if hint = nullhint then [None] else snd hint)) + @ [betaiota]) in (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*> intro_lock varnames <*> undertacs) diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 7db2f2a982..9ce249124d 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -132,7 +132,6 @@ Lemma test_big_cosmetic (F G : nat -> nat) (m n : nat) : \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). Proof. under a A: [RHS]eq_bigr by under b B: eq_bigr by []. (* renaming bound vars *) -simpl. myadmit. Qed. @@ -140,9 +139,7 @@ Lemma test_big_andb (F : nat -> nat) (m n : nat) : \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1. Proof. under i: eq_bigl by rewrite andb_idl; first by move/eqP->. -simpl. under i: eq_bigr by move/eqP=>{1}->. (* the 2nd occ should not be touched *) -simpl. myadmit. Qed. -- cgit v1.2.3 From 19e3ce970fd8f6d9922006aa30620a2b9db1cd06 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 25 Feb 2019 14:46:17 +0100 Subject: [ssr] under: Check that the number of hints and focused goals match --- plugins/ssr/ssrfwd.ml | 26 ++++++++++++++++++++------ 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index be2732513f..6d0b6de40d 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -396,6 +396,18 @@ let rec pretty_rename evar_map term = function let overtac gl = ssr_n_tac "over" ~-1 gl +let check_numgoals ?(minus = 0) nh = + Proofview.numgoals >>= fun ng -> + if nh <> ng then + let errmsg = + str"Incorrect number of hints" ++ spc() ++ + str"(expected "++int (ng - minus)++str(String.plural ng " tactic") ++ + str", was given "++ int (nh - minus)++str")." + in + CErrors.user_err errmsg + else + Proofview.tclUNIT () + let undertac ist varnames ((dir,mult),_ as rule) hint = if mult <> Ssrequality.nomult then Ssrcommon.errorstrm Pp.(str"Multiplicity not supported"); @@ -426,12 +438,14 @@ let undertac ist varnames ((dir,mult),_ as rule) hint = Proofview.tclUNIT () else let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in - Proofview.tclDISPATCH - ((List.map (function None -> Proofview.V82.tactic overtac - | Some e -> ssrevaltac ist e <*> - Proofview.V82.tactic overtac) - (if hint = nullhint then [None] else snd hint)) - @ [betaiota]) + let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in + check_numgoals ~minus:1 nh <*> + Proofview.tclDISPATCH + ((List.map (function None -> Proofview.V82.tactic overtac + | Some e -> ssrevaltac ist e <*> + Proofview.V82.tactic overtac) + (if hint = nullhint then [None] else snd hint)) + @ [betaiota]) in (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*> intro_lock varnames <*> undertacs) -- cgit v1.2.3 From adbb10dc627faa199bc4164b45740f62af8dc3fc Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 25 Feb 2019 18:12:06 +0100 Subject: [ssr] over: Add Ssrfwd.overtac in the .mli --- plugins/ssr/ssrfwd.mli | 3 +++ 1 file changed, 3 insertions(+) diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 63df8f5349..d57884c3ec 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -61,3 +61,6 @@ val undertac : Ltac_plugin.Tacinterp.interp_sign -> Names.Id.t list -> Ssrequality.ssrrwarg -> Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic + +val overtac : + Tacmach.tactic -- cgit v1.2.3 From f294fe1684e03f63871864def0f82190da087ebe Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 27 Feb 2019 18:53:11 +0100 Subject: [ssr] under: Fix rewrite goals order when called from under * "under"-specific behavior: the order of goals is kept even if one issues Global Set SsrOldRewriteGoalsOrder. * href: https://github.com/math-comp/math-comp/blob/mathcomp-1.7.0/mathcomp/ssreflect/ssreflect.v --- plugins/ssr/ssrequality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 921dce4689..ff6dd8f75a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -357,7 +357,7 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try refine_with - ~first_goes_last:(not !ssroldreworder) ~with_evars:under (sigma, proof) gl + ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl with _ -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with -- cgit v1.2.3 From 01b5e6e64b2af828b18fa6ee7037a7b7055f026e Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 1 Mar 2019 16:06:14 +0100 Subject: [ssr] Remove the unify_helper tactic that appears unnecessary It was only required in the (not realistic) test case "test_over_2_2", which happened to introduce evars after the context variables. --- plugins/ssr/ssreflect.v | 23 ----------------------- test-suite/ssr/over.v | 23 ++++++++++++----------- 2 files changed, 12 insertions(+), 34 deletions(-) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index c78381d3cc..e1e4d25ced 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -528,28 +528,6 @@ Parameter under_done : forall (T : Type) (x : T), @Under T x x. Notation "''Under[' x ]" := (@Under _ x _) (at level 8, format "''Under[' x ]"). - -Ltac beta_expand c e := - match e with - | ?G ?z => - let T := type of z in - match c with - | context f [z] => - let b := constr:(fun x : T => ltac:(let r := context f [x] in refine r)) in - rewrite -{1}[c]/(b z); beta_expand b G - | (* constante *) _ => - let b := constr:(fun x : T => ltac:(exact c)) in - rewrite -{1}[c]/(b z); beta_expand b G - end - | ?G => idtac - end. - -Ltac unify_helper := - move=> *; - lazymatch goal with - | [ |- @Under _ ?c ?e ] => - beta_expand c e - end. End UNDER. Module Export Under : UNDER. @@ -575,7 +553,6 @@ Register Under_from_eq as plugins.ssreflect.Under_from_eq. Ltac over := solve [ apply Under.under_done | by rewrite over - | unify_helper; eapply Under.under_done ]. (* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1] diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v index 3bb5c03e08..cd6b196eeb 100644 --- a/test-suite/ssr/over.v +++ b/test-suite/ssr/over.v @@ -4,10 +4,11 @@ Axiom daemon : False. Ltac myadmit := case: daemon. (** Testing over for the 1-var case *) -Lemma test_over_1_1 : forall i : nat, False. +Lemma test_over_1_1 : False. intros. evar (I : Type); evar (R : Type); evar (x2 : I -> R). -assert (H : i + 2 * i - i = x2 i). +assert (H : forall i : nat, i + 2 * i - i = x2 i). + intros i. unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. @@ -18,10 +19,11 @@ assert (H : i + 2 * i - i = x2 i). myadmit. Qed. -Lemma test_over_1_2 : forall i : nat, False. +Lemma test_over_1_2 : False. intros. evar (I : Type); evar (R : Type); evar (x2 : I -> R). -assert (H : i + 2 * i - i = x2 i). +assert (H : forall i : nat, i + 2 * i - i = x2 i). + intros i. unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. @@ -34,10 +36,11 @@ Qed. (** Testing over for the 2-var case *) -Lemma test_over_2_1 : forall i j : nat, False. +Lemma test_over_2_1 : False. intros. evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). -assert (H : i + 2 * j - i = x2 i j). +assert (H : forall i j, i + 2 * j - i = x2 i j). + intros i j. unfold x2 in *; clear x2; unfold R in *; clear R; unfold J in *; clear J; @@ -49,10 +52,11 @@ assert (H : i + 2 * j - i = x2 i j). myadmit. Qed. -Lemma test_over_2_2 : forall i j : nat, False. +Lemma test_over_2_2 : False. intros. evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). -assert (H : i + 2 * j - i = x2 i j). +assert (H : forall i j : nat, i + 2 * j - i = x2 i j). + intros i j. unfold x2 in *; clear x2; unfold R in *; clear R; unfold J in *; clear J; @@ -61,9 +65,6 @@ assert (H : i + 2 * j - i = x2 i j). Fail done. rewrite over. - Fail done. (* Bug: doesn't work so we have to make a beta-expansion by hand *) - rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). - (* cf. [plugins/ssr/ssreflect.v:unify_helper] *) done. myadmit. Qed. -- cgit v1.2.3 From c02ac6657863ba08b4c5f52dddf770d864ee6d4c Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 1 Mar 2019 17:07:41 +0100 Subject: [ssr] over: Expose the new type of tactic for Ssrfwd.overtac --- plugins/ssr/ssrfwd.ml | 6 +++--- plugins/ssr/ssrfwd.mli | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 6d0b6de40d..757a7968ca 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -394,7 +394,7 @@ let rec pretty_rename evar_map term = function ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda")); term -let overtac gl = ssr_n_tac "over" ~-1 gl +let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1) let check_numgoals ?(minus = 0) nh = Proofview.numgoals >>= fun ng -> @@ -441,9 +441,9 @@ let undertac ist varnames ((dir,mult),_ as rule) hint = let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in check_numgoals ~minus:1 nh <*> Proofview.tclDISPATCH - ((List.map (function None -> Proofview.V82.tactic overtac + ((List.map (function None -> overtac | Some e -> ssrevaltac ist e <*> - Proofview.V82.tactic overtac) + overtac) (if hint = nullhint then [None] else snd hint)) @ [betaiota]) in diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index d57884c3ec..745560da03 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -63,4 +63,4 @@ val undertac : Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic val overtac : - Tacmach.tactic + unit Proofview.tactic -- cgit v1.2.3 From f13c55b0c031b6ef92f28a3297ccfa0f7dde869d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 1 Mar 2019 17:33:21 +0100 Subject: [ssr] under: Add comment to justify the need for check_numgoals --- plugins/ssr/ssrfwd.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 757a7968ca..8bca62a4ff 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -400,7 +400,7 @@ let check_numgoals ?(minus = 0) nh = Proofview.numgoals >>= fun ng -> if nh <> ng then let errmsg = - str"Incorrect number of hints" ++ spc() ++ + str"Incorrect number of tactics" ++ spc() ++ str"(expected "++int (ng - minus)++str(String.plural ng " tactic") ++ str", was given "++ int (nh - minus)++str")." in @@ -439,6 +439,9 @@ let undertac ist varnames ((dir,mult),_ as rule) hint = else let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in + (* Usefulness of check_numgoals: tclDISPATCH would be enough, + except for the error message w.r.t. the number of + provided/expected tactics, as the last one is implied *) check_numgoals ~minus:1 nh <*> Proofview.tclDISPATCH ((List.map (function None -> overtac -- cgit v1.2.3 From c9454e2f4a083006d7145389beabcf8e4b10caa9 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Fri, 1 Mar 2019 19:47:41 +0100 Subject: [ssr] under: Add doc for {under, over} & Add entry in CHANGES.md * For better uniformity, replace "intro-pattern" with "intro pattern" in the ssr doc. --- CHANGES.md | 10 + .../proof-engine/ssreflect-proof-language.rst | 239 ++++++++++++++++++++- 2 files changed, 245 insertions(+), 4 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 7f4f9a232b..c420caa04b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -266,12 +266,22 @@ Misc SSReflect +- New tactic `under` to rewrite under binders, given an extensionality lemma: + - interactive mode: `under lem`, associated terminator: `over` + - one-liner mode: `under lem do [tac1 | ...]` + + It can take occurrence switches, contextual patterns, and intro patterns: + `under {2}[in RHS]eq_big => [i|i ?] do ...`. + + See the reference manual for the actual documentation. + - New intro patterns: - temporary introduction: `=> +` - block introduction: `=> [^ prefix ] [^~ suffix ]` - fast introduction: `=> >` - tactics as views: `=> /ltac:mytac` - replace hypothesis: `=> {}H` + See the reference manual for the actual documentation. - Clear discipline made consistent across the entire proof language. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index b240cef40c..a4ab038314 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1737,9 +1737,8 @@ Intro patterns for each :token:`ident`. Its type has to be fixed later on by using the ``abstract`` tactic. Before then the type displayed is ````. - Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for -destructing intro-patterns. +destructing intro patterns. Clear switch ```````````` @@ -3626,7 +3625,7 @@ corresponding new goals will be generated. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. - .. coqtop:: all + .. coqtop:: all abort Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. rewrite insubT. @@ -3637,6 +3636,230 @@ rewriting rule is stated using Leibniz equality (as opposed to setoid relations). It will be extended to other rewriting relations in the future. +.. _under_over_ssr: + +A convenience under tactic +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Goals involving objects defined with higher-order functions often +require "rewriting under binders". While setoid rewriting is a +possible approach in this case, it is common to use regular rewriting +along with dedicated extensionality lemmas. This may cause some +practical issues during the development of the corresponding scripts, +notably as we might be forced to provide the rewrite tactic with +complete terms, as shown by the simple example below. + +.. example:: + + .. coqtop:: reset none + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + + .. coqtop:: in + + Axiom subnn : forall n : nat, n - n = 0. + Parameter G : (nat -> nat) -> nat -> nat. + Axiom eq_G : + forall F1 F2 : nat -> nat, + (forall n : nat, F1 n = F2 n) -> + forall n : nat, G F1 n = G F2 n. + + .. coqtop:: all + + Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. + + In this context, one cannot directly use ``eq_G``: + + .. coqtop:: all fail + + rewrite eq_G. + + as we need to explicitly provide the non-inferable argument ``F2``, + which corresponds here to the term we want to obtain *after* the + rewriting step. We can thus do: + + .. coqtop:: all abort + + rewrite (@eq_G _ (fun _ : nat => 0)); last first. + by move=> m; rewrite subnn. + + Otherwise, a more convenient approach consists in relying on the + :tacn:`under` tactic that alleviates this bookkeeping: + + .. coqtop:: all abort + + Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. + under m: eq_G by rewrite subnn. + + ``(* FIXME: replace with do... *)`` + +.. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) } + :name: under + + Rewrite under :token:`term`. We distinguish two modes, + :ref:`interactive mode ` without a ``do`` clause, and + :ref:`one-liner mode ` with a ``do`` clause, + which are explained in more detail below. + + .. exn:: Incorrect number of tactics (expected N tactics, was given N'). + + This error can occur when using the version with a ``do`` clause. + +.. _under_interactive: + +Interactive mode +```````````````` +The execution of the Ltac expression: +:n:`under {@occ_switch}[@r_pattern]@term => [i|j].` +involves the following steps: + ++ It performs a full-blown :n:`rewrite {@occ_switch}[@r_pattern]@term`, + without failing like in the above example with ``eq_G``, but + creating evars. ++ As a 2-branches intro pattern is provided, it checks that 3 subgoals + have been created (the last one being the initial, main subgoal that + now contains some evars). ++ In the first 2 subgoals, it introduces ``i``, resp. ``j``, and tests + whether these 2 subgoals are (quantified) equalities involving + an evar. For example: ``some_expr(i) = ?Goal i``. ++ If this is the case, the subgoal is manipulated to get the + provably equivalent goal ``Under _ (some_expr i) (?Goal i)``, + pretty-printed as ``Under[ some_expr i ]``. + This change avoids instantiating the evar by accident (e.g., if one + uses a proof script such as: :n:`rewrite lem1 // lem2`). ++ Finally, a post-processing step is performed in the main (here, 3rd) + subgoal to try keeping (in the object after the rewrite) the same + bound variables as the identifers provided in the first + intro pattern branch (here, ``i``). + +If the intro pattern is omitted, the Ltac expression: +:n:`under {@occ_switch}[@r_pattern]@term.` defaults to: +:n:`under {@occ_switch}[@r_pattern]@term => *.` + +Two equivalent facilities (a terminator and a lemma) are provided to +close intermediate subgoal ``Under[ … ]`` and instantiate the +corresponding evar: + +.. tacn:: over + :name: over + + This terminator tactic allows one to close goals of the form + ``Under[ … ]``. + +.. tacv:: by rewrite over + + This is a variant of :tacn:`over` in order to close ``Under[ … ]`` + goals, relying on the ``over`` lemma. + +Let us focus again on the simple example involving an extensionality +lemma ``eq_G``, but this time in interactive mode: + +.. example:: + + .. coqtop:: all abort + + Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. + under m: eq_G. + rewrite subnn. + over. + + ``(* FIXME: replace with do... *)`` + +.. _under_one_liner: + +One-liner mode +`````````````` + +The Ltac expression: +:n:`under {@occ_switch}[@r_pattern]@term => [i|j] do [tac1|tac2]` +can be viewed as a shorter form for the following Ltac expression: +:n:`under {@occ_switch}[@r_pattern]@term => [i|j]; [tac1; over | tac2; over | cbv beta iota].` + +Here, the ``beta-iota`` reduction is useful to get rid of the beta +redexes that will typically be introduced after the substitution of +the evars by the :tacn:`under` tactic. + +Note that the provided tactics (e.g., ``tac1``) can just as well +involve other :tacn:`under` tactics. See below for a typical example +involving the `bigop` theory from the Mathematical Components library. + +If there is only one tactic, the brackets are optional, i.e.: +:n:`under @term => i do [tac1]` can be +shortened to: :n:`under @term => i do tac1.` + +.. example:: + + .. coqtop:: reset none + + From Coq Require Import ssreflect. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. + + Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" + (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50, + format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'"). + Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F" + (at level 36, F at level 36, op, idx at level 10, i, m, n at level 50, + format "'[' \big [ op / idx ]_ ( m <= i < n ) '/ ' F ']'"). + + Variant bigbody (R I : Type) : Type := + BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I. + + Parameter bigop : + forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R. + + Axiom eq_bigr : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P : I -> bool) (F1 F2 : I -> R), + (forall x : I, P x = true -> F1 x = F2 x) -> + bigop idx r (fun i : I => BigBody i op (P i) (F1 i)) = + bigop idx r (fun i : I => BigBody i op (P i) (F2 i)). + + Axiom eq_big : + forall (R : Type) (idx : R) (op : R -> R -> R) (I : Type) (r : list I) + (P1 P2 : I -> bool) (F1 F2 : I -> R), + (forall x : I, P1 x = P2 x) -> + (forall i : I, is_true (P1 i) -> F1 i = F2 i) -> + bigop idx r (fun i : I => BigBody i op (P1 i) (F1 i)) = + bigop idx r (fun i : I => BigBody i op (P2 i) (F2 i)). + + Reserved Notation "\sum_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). + Reserved Notation "\sum_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n ) '/ ' F ']'"). + + Parameter index_iota : nat -> nat -> list nat. + + Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" := + (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%bool F)). + Notation "\big [ op / idx ]_ ( m <= i < n ) F" := + (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F)). + + Notation "\sum_ ( m <= i < n | P ) F" := + (\big[plus/O]_(m <= i < n | P%bool) F%nat). + Notation "\sum_ ( m <= i < n ) F" := + (\big[plus/O]_(m <= i < n) F%nat). + + .. coqtop:: in + + Parameter addnC : forall m n : nat, m + n = n + m. + Parameter muln1 : forall n : nat, n * 1 = n. + Parameter odd : nat -> bool. + + .. coqtop:: all + + Lemma test_big_nested (F G : nat -> nat) (m n : nat) : + \sum_(0 <= a < m) \sum_(0 <= j < n | odd (j * 1)) (a + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). + under i I: eq_bigr by under j J: eq_big by [rewrite muln1|rewrite addnC]. + + ``(* FIXME: replace with do... *)`` .. _locking_ssr: @@ -5373,7 +5596,15 @@ respectively. .. tacn:: rewrite {+ @r_step } - rewrite (see :ref:`rewriting_ssr`) + rewrite (see :ref:`rewriting_ssr`) + +.. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] )} + + under (see :ref:`under_over_ssr`) + +.. tacn:: over + + over (see :ref:`under_over_ssr`) .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } -- cgit v1.2.3 From 600fef9a1c9cd15ad43196b7750ba15922c01752 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 3 Mar 2019 01:07:19 +0100 Subject: [ssr] under: Simplify the over tactic * Use ssr `by […|…]` and `apply:` --- plugins/ssr/ssreflect.v | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index e1e4d25ced..37390e1af7 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -551,16 +551,6 @@ Register Under as plugins.ssreflect.Under. Register Under_from_eq as plugins.ssreflect.Under_from_eq. Ltac over := - solve [ apply Under.under_done - | by rewrite over - ]. - -(* The 2 variants below wouldn't work on [test-suite/ssr/over.v:test_over_2_1] - (2-var test case with evars). - -Ltac over := - exact: Under.under_done. - -Ltac over := - by rewrite over. - *) + by [ apply: Under.under_done + | rewrite over + ]. -- cgit v1.2.3 From e68bccba9344c1b3d77d3e815af6cce1ce50b731 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Mar 2019 10:08:29 +0100 Subject: [ssr] new syntax for the under tactic --- .../proof-engine/ssreflect-proof-language.rst | 10 +- plugins/ssr/ssrfwd.ml | 144 +++++++++++---------- plugins/ssr/ssrfwd.mli | 2 +- plugins/ssr/ssrparser.mlg | 47 ++++++- test-suite/ssr/under.v | 23 ++-- 5 files changed, 135 insertions(+), 91 deletions(-) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index a4ab038314..cb529bd68e 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3692,9 +3692,7 @@ complete terms, as shown by the simple example below. .. coqtop:: all abort Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. - under m: eq_G by rewrite subnn. - - ``(* FIXME: replace with do... *)`` + under eq_G => n do rewrite subnn. .. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) } :name: under @@ -3762,7 +3760,7 @@ lemma ``eq_G``, but this time in interactive mode: .. coqtop:: all abort Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. - under m: eq_G. + under eq_G => m. rewrite subnn. over. @@ -3857,9 +3855,7 @@ shortened to: :n:`under @term => i do tac1.` Lemma test_big_nested (F G : nat -> nat) (m n : nat) : \sum_(0 <= a < m) \sum_(0 <= j < n | odd (j * 1)) (a + j) = \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). - under i I: eq_bigr by under j J: eq_big by [rewrite muln1|rewrite addnC]. - - ``(* FIXME: replace with do... *)`` + under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1|rewrite addnC]. .. _locking_ssr: diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 8bca62a4ff..349f0082e1 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -331,68 +331,53 @@ let is_app_evar sigma t = | _ -> false end | _ -> false -let tmp = ref 0 - -let rec intro_lock names = Proofview.Goal.enter begin fun gl -> - let c = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in - let env = Proofview.Goal.env gl in - let rec aux c = - match EConstr.kind_of_type sigma c with - | Term.SortType _ -> Proofview.tclUNIT () - | ( Term.ProdType ({ Context.binder_name = name },_,t) - | Term.LetInType ({ Context.binder_name = name },_,_,t) ) -> - begin match names with - | n :: names -> Ssripats.(tclIPAT @@ [Ssripats.IOpId n]) <*> intro_lock names - | [] -> - (* after quell intro patterns, use IpatTemp *) - let id = - match name with - | Name.Anonymous -> Id.of_string (Printf.sprintf "_under_%d_" !tmp) - | Name.Name n -> n in - incr tmp; - Ssripats.tclIPAT [ - Ssripats.IOpId id; - Ssripats.IOpEqGen (intro_lock names); - Ssripats.IOpEqGen (Tactics.revert [id])] - end - | Term.CastType (t,_) -> aux t - | Term.AtomicType _ -> - let t = Reductionops.whd_all env sigma c in - match EConstr.kind_of_type sigma t with - | Term.ProdType _ -> aux t - | Term.AtomicType(hd, args) when - Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && - Array.length args = 3 && is_app_evar sigma args.(2) -> - Tactics.New.refine ~typecheck:true (fun sigma -> - let sigma, under = - Ssrcommon.mkSsrConst "Under" env sigma in - let sigma, under_from_eq = - Ssrcommon.mkSsrConst "Under_from_eq" env sigma in - let ty = EConstr.mkApp (under,args) in - let sigma, t = Evarutil.new_evar env sigma ty in - sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|])) - | _ -> Proofview.tclUNIT () +let intro_lock ipats = + let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ -> + Proofview.tclORELSE + (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())]) + (fun _exn -> Proofview.Goal.enter begin fun gl -> + let c = Proofview.Goal.concl gl in + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let t = Reductionops.whd_all env sigma c in + match EConstr.kind_of_type sigma t with + | Term.AtomicType(hd, args) when + Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && + Array.length args = 3 && is_app_evar sigma args.(2) -> + Tactics.New.refine ~typecheck:true (fun sigma -> + let sigma, under = + Ssrcommon.mkSsrConst "Under" env sigma in + let sigma, under_from_eq = + Ssrcommon.mkSsrConst "Under_from_eq" env sigma in + let ty = EConstr.mkApp (under,args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|])) + | _ -> + ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); + + Proofview.tclUNIT () + end) + end in - aux c - -end - -let rec pretty_rename evar_map term = function - | [] -> term - | varname :: varnames -> - try begin - match EConstr.destLambda evar_map term - with ({ Context.binder_relevance = r }, types, body) -> - let res = pretty_rename evar_map body varnames in - let name = Names.Name.mk_name varname in - (* Note: we don't explicitly check name \notin free_vars(res) here *) - EConstr.mkLambda (Context.make_annot name r, types, res) - end - with - | DestKO -> - ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda")); - term + Ssripats.tclIPATssr ipats <*> lock_eq () + +let pretty_rename evar_map term varnames = + let rec aux term vars = + try + match vars with + | [] -> term + | Names.Name.Anonymous :: varnames -> + let name, types, body = EConstr.destLambda evar_map term in + let res = aux body varnames in + EConstr.mkLambda (name, types, res) + | Names.Name.Name _ as name :: varnames -> + let { Context.binder_relevance = r }, types, body = + EConstr.destLambda evar_map term in + let res = aux body varnames in + EConstr.mkLambda (Context.make_annot name r, types, res) + with DestKO -> term + in + aux term varnames let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1) @@ -408,19 +393,37 @@ let check_numgoals ?(minus = 0) nh = else Proofview.tclUNIT () -let undertac ist varnames ((dir,mult),_ as rule) hint = - if mult <> Ssrequality.nomult then - Ssrcommon.errorstrm Pp.(str"Multiplicity not supported"); +let undertac ist ipats ((dir,_),_ as rule) hint = + + let varnames = + let rec aux acc = function + | IPatId id :: rest -> aux (Names.Name.Name id :: acc) rest + | IPatClear _ :: rest -> aux acc rest + | IPatSimpl _ :: rest -> aux acc rest + | IPatAnon (One _ | Drop) :: rest -> + aux (Names.Name.Anonymous :: acc) rest + | _ -> List.rev acc in + aux [] (Option.default [] ipats) in + + (* If we find a "=> [|]" we add 1 | to get "=> [||]" for the extra + * goal (the one that is left once we run over) *) + let ipats = + match ipats with + | None -> [IPatNoop] + | Some (IPatCase(Regular []) :: _ as ipats) -> ipats + | Some (IPatCase(Regular l) :: rest) -> IPatCase(Regular(l @ [[]])) :: rest + | Some (IPatCase(Block _) :: _ as l) -> l + | Some l -> [IPatCase(Regular [l;[]])] in let map_redex env evar_map ~before:_ ~after:t = - ppdebug(lazy Pp.(str("under vars: " ^ - (List.fold_right (fun e r -> Names.Id.to_string e ^ " " ^ r) varnames "")))); - ppdebug(lazy Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map t)); + ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames)); let evar_map, ty = Typing.type_of env evar_map t in let new_t = (* pretty-rename the bound variables *) try begin match EConstr.destApp evar_map t with (f, ar) -> let lam = Array.last ar in + ppdebug(lazy Pp.(str"under: mapping:" ++ + pr_econstr_env env evar_map lam)); let new_lam = pretty_rename evar_map lam varnames in let new_ar, len1 = Array.copy ar, pred (Array.length ar) in new_ar.(len1) <- new_lam; @@ -450,5 +453,8 @@ let undertac ist varnames ((dir,mult),_ as rule) hint = (if hint = nullhint then [None] else snd hint)) @ [betaiota]) in - (Proofview.V82.tactic (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) <*> - intro_lock varnames <*> undertacs) + let rew = + Proofview.V82.tactic + (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule]) + in + rew <*> intro_lock ipats <*> undertacs diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 745560da03..6f7cc6d445 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -59,7 +59,7 @@ val sufftac : val undertac : Ltac_plugin.Tacinterp.interp_sign -> - Names.Id.t list -> Ssrequality.ssrrwarg -> + Ssrast.ssripats option -> Ssrequality.ssrrwarg -> Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic val overtac : diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 507cf8db70..2c46947658 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -741,15 +741,33 @@ let pushIPatNoop = function | pats :: orpat -> (IPatNoop :: pats) :: orpat | [] -> [] +let test_ident_no_do strm = + match Util.stream_nth 0 strm with + | Tok.IDENT s when s <> "do" -> () + | _ -> raise Stream.Failure + +let test_ident_no_do = + Pcoq.Entry.of_parser "test_ident_no_do" test_ident_no_do + } +ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print } +| [ "YouShouldNotTypeThis" ident(id) ] -> { id } +END + + +GRAMMAR EXTEND Gram + GLOBAL: ident_no_do; + ident_no_do: [ [ test_ident_no_do; id = IDENT -> { Id.of_string id } ] ]; +END + ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } INTERPRETED BY { interp_ipats } GLOBALIZED BY { intern_ipats } | [ "_" ] -> { [IPatAnon Drop] } | [ "*" ] -> { [IPatAnon All] } | [ ">" ] -> { [IPatFastNondep] } - | [ ident(id) ] -> { [IPatId id] } + | [ ident_no_do(id) ] -> { [IPatId id] } | [ "?" ] -> { [IPatAnon (One None)] } | [ "+" ] -> { [IPatAnon Temporary] } | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] } @@ -2650,9 +2668,32 @@ TACTIC EXTEND ssrgenhave2 V82.tactic (wlogtac ist pats fwd hint false (`Gen id)) } END +{ + +let check_under_arg ((_dir,mult),((_occ,_rpattern),_rule)) = + if mult <> nomult then + CErrors.user_err Pp.(str"under does not support multipliers") + +} + + TACTIC EXTEND under - | [ "under" ne_ident_list(names) ":" ssrrwarg(r) ssrhint(hint) ] -> - { Ssrfwd.undertac ist names r hint } + | [ "under" ssrrwarg(arg) ] -> { + check_under_arg arg; + Ssrfwd.undertac ist None arg nohint + } + | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) ] -> { + check_under_arg arg; + Ssrfwd.undertac ist (Some ipats) arg nohint + } + | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhintarg(h) ] -> { + check_under_arg arg; + Ssrfwd.undertac ist (Some ipats) arg h + } + | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> *" *) + check_under_arg arg; + Ssrfwd.undertac ist (Some [IPatAnon All]) arg h + } END { diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 9ce249124d..5f27858d17 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -86,12 +86,13 @@ Lemma test_big_nested_1 (F G : nat -> nat) (m n : nat) : \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). Proof. (* in interactive mode *) -under i Hi: eq_bigr. - under j Hj: eq_big. +under eq_bigr => i Hi. + under eq_big => [j|j Hj]. { rewrite muln1. over. } { rewrite addnC. over. } +(* MISSING BETA *) over. -done. +by []. Qed. Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) : @@ -99,14 +100,14 @@ Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) : \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). Proof. (* in one-liner mode *) -under i Hi: eq_bigr by under j Hj: eq_big by [rewrite muln1 | rewrite addnC]. +under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1 | rewrite addnC ]. done. Qed. Lemma test_big_patt1 (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0. Proof. -under i Hi: [in RHS]eq_bigr. +under [in RHS]eq_bigr => i Hi. by rewrite addnC over. done. Qed. @@ -115,14 +116,14 @@ Lemma test_big_patt2 (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (F i + F i) = \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2). Proof. -under i Hi: [X in _ = _ + X]eq_bigr by rewrite mulnS muln1. +under [X in _ = _ + X]eq_bigr => i Hi do rewrite mulnS muln1. by rewrite big_const_nat iter_addn_0. Qed. Lemma test_big_occs (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0). Proof. -under i Hi: {2}[in RHS]eq_bigr by rewrite muln0. +under {2}[in RHS]eq_bigr => i Hi do rewrite muln0. by rewrite big_const_nat iter_addn_0. Qed. @@ -131,15 +132,15 @@ Lemma test_big_cosmetic (F G : nat -> nat) (m n : nat) : \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). Proof. -under a A: [RHS]eq_bigr by under b B: eq_bigr by []. (* renaming bound vars *) +under [RHS]eq_bigr => a A do under eq_bigr => b B do []. (* renaming bound vars *) myadmit. Qed. Lemma test_big_andb (F : nat -> nat) (m n : nat) : \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1. Proof. -under i: eq_bigl by rewrite andb_idl; first by move/eqP->. -under i: eq_bigr by move/eqP=>{1}->. (* the 2nd occ should not be touched *) +under eq_bigl => i do rewrite andb_idl; first by move/eqP->. +under eq_bigr => i do move/eqP=>{1}->. (* the 2nd occ should not be touched *) myadmit. Qed. @@ -158,6 +159,6 @@ under x: Lem. - rewrite f_eq; over. - done. *) -under x: Lem by [done|rewrite f_eq|done]. +under Lem => [|x|] do [done|rewrite f_eq|done]. done. Qed. -- cgit v1.2.3 From 7c598f9f1f6da2cecc70557f9f436392322fc6d9 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 2 Apr 2019 01:47:11 +0200 Subject: [ssr] under: use varnames from the 1st ipat with multi-goal under lemmas In particular, this enhances support for lemma eq_big (with 2 side-conditions). --- plugins/ssr/ssrfwd.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 349f0082e1..b5082582c9 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -403,7 +403,10 @@ let undertac ist ipats ((dir,_),_ as rule) hint = | IPatAnon (One _ | Drop) :: rest -> aux (Names.Name.Anonymous :: acc) rest | _ -> List.rev acc in - aux [] (Option.default [] ipats) in + aux [] @@ match ipats with + | None -> [] + | Some (IPatCase(Regular (l :: _)) :: _) -> l + | Some l -> l in (* If we find a "=> [|]" we add 1 | to get "=> [||]" for the extra * goal (the one that is left once we run over) *) -- cgit v1.2.3 From bb6dc2355bcd027a3a89c40629b82eb2019eff6a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 4 Mar 2019 01:25:39 +0100 Subject: [ssr] under: Add iff support in side-conditions --- plugins/ssr/ssrcommon.ml | 9 ++++++--- plugins/ssr/ssrcommon.mli | 3 ++- plugins/ssr/ssreflect.v | 42 ++++++++++++++++++++++++++++++++++++++++++ plugins/ssr/ssrequality.ml | 4 ++-- plugins/ssr/ssrfwd.ml | 13 +++++++++++++ test-suite/ssr/under.v | 34 ++++++++++++++++++++++++++++++++++ 6 files changed, 99 insertions(+), 6 deletions(-) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 0b3bfab366..a05b1e3d81 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -828,10 +828,12 @@ let view_error s gv = open Locus (****************************** tactics ***********************************) -let rewritetac dir c = +let rewritetac ?(under=false) dir c = (* Due to the new optional arg ?tac, application shouldn't be too partial *) + let open Proofview.Notations in Proofview.V82.of_tactic begin - Equality.general_rewrite (dir = L2R) AllOccurrences true false c + Equality.general_rewrite (dir = L2R) AllOccurrences true false c <*> + if under then Proofview.cycle 1 else Proofview.tclUNIT () end (**********************`:********* hooks ************************************) @@ -1542,6 +1544,7 @@ end let is_construct_ref sigma c r = EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r - +let is_const_ref sigma c r = + EConstr.isConst sigma c && GlobRef.equal (ConstRef (fst(EConstr.destConst sigma c))) r (* vim: set filetype=ocaml foldmethod=marker: *) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 3049f67f87..58ce84ecb3 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -349,7 +349,7 @@ val resolve_typeclasses : (*********************** Wrapped Coq tactics *****************************) -val rewritetac : ssrdir -> EConstr.t -> tactic +val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic type name_hint = (int * EConstr.types array) option ref @@ -486,3 +486,4 @@ end val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool +val is_const_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 37390e1af7..94e0b2a724 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -550,7 +550,49 @@ End Under. Register Under as plugins.ssreflect.Under. Register Under_from_eq as plugins.ssreflect.Under_from_eq. +Module Type UNDER_IFF. +Parameter Under_iff : Prop -> Prop -> Prop. +Parameter Under_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y. + +(** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *) +Parameter Over_iff : Prop -> Prop -> Prop. +Parameter over_iff : + forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y. +Parameter over_iff_done : + forall (x : Prop), @Over_iff x x. +Hint Extern 0 (@Over_iff _ _) => solve [ apply over_iff_done ] : core. +Hint Resolve over_iff_done : core. + +(** [under_iff_done]: for Ltac-style over *) +Parameter under_iff_done : + forall (x : Prop), @Under_iff x x. +Notation "''Under_iff[' x ]" := (@Under_iff x _) + (at level 8, format "''Under_iff[' x ]"). +End UNDER_IFF. + +Module Export Under_iff : UNDER_IFF. +Definition Under_iff := iff. +Lemma Under_from_iff (x y : Prop) : + @Under_iff x y -> x <-> y. +Proof. by []. Qed. +Definition Over_iff := Under_iff. +Lemma over_iff : + forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y. +Proof. by []. Qed. +Lemma over_iff_done : + forall (x : Prop), @Over_iff x x. +Proof. by []. Qed. +Lemma under_iff_done : + forall (x : Prop), @Under_iff x x. +Proof. by []. Qed. +End Under_iff. + +Register Under_iff as plugins.ssreflect.Under_iff. +Register Under_from_iff as plugins.ssreflect.Under_from_iff. + Ltac over := by [ apply: Under.under_done | rewrite over + | apply: Under_iff.under_iff_done + | rewrite over_iff ]. diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ff6dd8f75a..842e4feecf 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in let gl = pf_merge_uc_of sigma gl in - Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl + Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl else let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = @@ -417,7 +417,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in let itacs = [introid pattern_id; introid rule_id] in let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in - let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in + let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl in let cvtac' _ = diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index b5082582c9..2bac69b5b7 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -339,6 +339,19 @@ let intro_lock ipats = let c = Proofview.Goal.concl gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in + match EConstr.kind_of_type sigma c with + | Term.AtomicType(hd, args) when + Ssrcommon.is_const_ref sigma hd (Coqlib.lib_ref "core.iff.type") && + Array.length args = 2 && is_app_evar sigma args.(1) -> + Tactics.New.refine ~typecheck:true (fun sigma -> + let sigma, under_iff = + Ssrcommon.mkSsrConst "Under_iff" env sigma in + let sigma, under_from_iff = + Ssrcommon.mkSsrConst "Under_from_iff" env sigma in + let ty = EConstr.mkApp (under_iff,args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|])) + | _ -> let t = Reductionops.whd_all env sigma c in match EConstr.kind_of_type sigma t with | Term.AtomicType(hd, args) when diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 5f27858d17..1e3b0f678b 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -162,3 +162,37 @@ under x: Lem. under Lem => [|x|] do [done|rewrite f_eq|done]. done. Qed. + + +(* Inspired From Coquelicot.Lub. *) +(* http://coquelicot.saclay.inria.fr/html/Coquelicot.Lub.html#Lub_Rbar_eqset *) + +Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar). +Parameter Rbar_le : Rbar -> Rbar -> Prop. +Parameter Lub_Rbar : (R -> Prop) -> Rbar. +Parameter Lub_Rbar_eqset : + forall E1 E2 : R -> Prop, + (forall x : R, E1 x <-> E2 x) -> + Lub_Rbar E1 = Lub_Rbar E2. + +Lemma test_Lub_Rbar (E : R -> Prop) : + Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)). +Proof. +under Lub_Rbar_eqset => r. +by rewrite over. +Abort. + + +Lemma ex_iff R (P1 P2 : R -> Prop) : + (forall x : R, P1 x <-> P2 x) -> ((exists x, P1 x) <-> (exists x, P2 x)). +Proof. +by move=> H; split; move=> [x Hx]; exists x; apply H. +Qed. + +Arguments ex_iff [R P1] P2 iffP12. + +Require Import Setoid. +Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True. +under ex_iff => n. +by rewrite over. +Abort. -- cgit v1.2.3 From 96513a4a8bb361aee6034b1f76127acaf613415a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 2 Apr 2019 15:49:12 +0200 Subject: [ssr] under: Fix and extend the documentation --- .../proof-engine/ssreflect-proof-language.rst | 74 +++++++++++++--------- 1 file changed, 44 insertions(+), 30 deletions(-) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index cb529bd68e..0df0f937a6 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3683,7 +3683,7 @@ complete terms, as shown by the simple example below. .. coqtop:: all abort - rewrite (@eq_G _ (fun _ : nat => 0)); last first. + rewrite (@eq_G _ (fun _ : nat => 0)). by move=> m; rewrite subnn. Otherwise, a more convenient approach consists in relying on the @@ -3692,7 +3692,7 @@ complete terms, as shown by the simple example below. .. coqtop:: all abort Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. - under eq_G => n do rewrite subnn. + under eq_G => m do rewrite subnn. .. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) } :name: under @@ -3714,28 +3714,39 @@ The execution of the Ltac expression: :n:`under {@occ_switch}[@r_pattern]@term => [i|j].` involves the following steps: -+ It performs a full-blown :n:`rewrite {@occ_switch}[@r_pattern]@term`, - without failing like in the above example with ``eq_G``, but - creating evars. -+ As a 2-branches intro pattern is provided, it checks that 3 subgoals - have been created (the last one being the initial, main subgoal that - now contains some evars). -+ In the first 2 subgoals, it introduces ``i``, resp. ``j``, and tests - whether these 2 subgoals are (quantified) equalities involving - an evar. For example: ``some_expr(i) = ?Goal i``. -+ If this is the case, the subgoal is manipulated to get the - provably equivalent goal ``Under _ (some_expr i) (?Goal i)``, - pretty-printed as ``Under[ some_expr i ]``. - This change avoids instantiating the evar by accident (e.g., if one - uses a proof script such as: :n:`rewrite lem1 // lem2`). -+ Finally, a post-processing step is performed in the main (here, 3rd) - subgoal to try keeping (in the object after the rewrite) the same - bound variables as the identifers provided in the first - intro pattern branch (here, ``i``). - -If the intro pattern is omitted, the Ltac expression: -:n:`under {@occ_switch}[@r_pattern]@term.` defaults to: -:n:`under {@occ_switch}[@r_pattern]@term => *.` +1. It performs a full-blown :n:`rewrite {@occ_switch}[@r_pattern]@term`, + without failing like in the above example with ``eq_G``, but + creating evars. + +2. As a 2-branches intro pattern is provided, it checks that 3 subgoals + have been created (the last one being the initial, main subgoal that + now contains some evars). + +3. In the first 2 subgoals, it introduces ``i``, resp. ``j``, and tests + whether these 2 subgoals are (quantified) equalities involving + an evar. For example: ``some_expr(i) = ?Goal i``. + +4. If this is the case, the subgoal is manipulated to get the + provably equivalent goal ``Under _ (some_expr i) (?Goal i)``, + pretty-printed as ``'Under[ some_expr i ]``. + This change avoids instantiating the evar by accident (e.g., if one + uses a proof script such as: :n:`rewrite lem1 // lem2`). + +5. Finally, a post-processing step is performed in the main (here, 3rd) + subgoal to try keeping (in the object after the rewrite) the same + bound variables as the identifers provided in the first + intro pattern branch (here, ``i``). + +Notes: + ++ For the steps 3. and 4. above, the :tacn:`under` tactic also + supports subgoals of the form ``some_expr(i) <-> ?Goal i``, which + are "protected" in the form ``Under_iff (some_expr i) (?Goal i)``, + itself pretty-printed as ``'Under_iff[ some_expr i ]``. + ++ If the intro pattern is omitted, the Ltac expression: + :n:`under {@occ_switch}[@r_pattern]@term.` defaults to: + :n:`under {@occ_switch}[@r_pattern]@term => *.` Two equivalent facilities (a terminator and a lemma) are provided to close intermediate subgoal ``Under[ … ]`` and instantiate the @@ -3745,13 +3756,18 @@ corresponding evar: :name: over This terminator tactic allows one to close goals of the form - ``Under[ … ]``. + ``'Under[ … ]`` or ``'Under_iff[ … ]``. .. tacv:: by rewrite over This is a variant of :tacn:`over` in order to close ``Under[ … ]`` goals, relying on the ``over`` lemma. +.. tacv:: by rewrite over_iff + + This is a variant of :tacn:`over` in order to close ``Under_iff[ … ]`` + goals, relying on the ``over_iff`` lemma. + Let us focus again on the simple example involving an extensionality lemma ``eq_G``, but this time in interactive mode: @@ -3764,8 +3780,6 @@ lemma ``eq_G``, but this time in interactive mode: rewrite subnn. over. - ``(* FIXME: replace with do... *)`` - .. _under_one_liner: One-liner mode @@ -3774,11 +3788,11 @@ One-liner mode The Ltac expression: :n:`under {@occ_switch}[@r_pattern]@term => [i|j] do [tac1|tac2]` can be viewed as a shorter form for the following Ltac expression: -:n:`under {@occ_switch}[@r_pattern]@term => [i|j]; [tac1; over | tac2; over | cbv beta iota].` +:n:`under {@occ_switch}[@r_pattern]@term => [i|j|]; [tac1; over | tac2; over | cbv beta iota].` Here, the ``beta-iota`` reduction is useful to get rid of the beta -redexes that will typically be introduced after the substitution of -the evars by the :tacn:`under` tactic. +redexes that could be introduced after the substitution of the evars +by the :tacn:`under` tactic. Note that the provided tactics (e.g., ``tac1``) can just as well involve other :tacn:`under` tactics. See below for a typical example -- cgit v1.2.3 From 6835590f6e0a8e96719c7f37ef6f8bb789bd349b Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Apr 2019 01:07:11 +0200 Subject: [ssr] Add small output test for "under eq_G => m do rewrite subnn" --- test-suite/output/ssr_under.out | 2 ++ test-suite/output/ssr_under.v | 15 +++++++++++++++ 2 files changed, 17 insertions(+) create mode 100644 test-suite/output/ssr_under.out create mode 100644 test-suite/output/ssr_under.v diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out new file mode 100644 index 0000000000..8532b62a54 --- /dev/null +++ b/test-suite/output/ssr_under.out @@ -0,0 +1,2 @@ +'Under[ m - m ] +(G (fun _ : nat => 0) n >= 0) diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v new file mode 100644 index 0000000000..b11dd1509c --- /dev/null +++ b/test-suite/output/ssr_under.v @@ -0,0 +1,15 @@ +From Coq Require Import ssreflect. + +Axiom subnn : forall n : nat, n - n = 0. +Parameter G : (nat -> nat) -> nat -> nat. +Axiom eq_G : + forall F1 F2 : nat -> nat, + (forall n : nat, F1 n = F2 n) -> + forall n : nat, G F1 n = G F2 n. + +Ltac show := match goal with [|-?g] => idtac g end. + +Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. +under eq_G => m do show; rewrite subnn. +show. +Abort. -- cgit v1.2.3 From 04da1739139c8d96469a2b86280e520e532beb39 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Apr 2019 01:08:38 +0200 Subject: [ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc * Add tests accordingly. --- .../proof-engine/ssreflect-proof-language.rst | 32 ++++++++++--------- plugins/ssr/ssrfwd.ml | 15 +++++++-- plugins/ssr/ssrfwd.mli | 6 ++++ plugins/ssr/ssrparser.mlg | 4 +-- test-suite/ssr/under.v | 36 ++++++++++++++++++++++ 5 files changed, 75 insertions(+), 18 deletions(-) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 0df0f937a6..c32788c9da 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3737,17 +3737,13 @@ involves the following steps: bound variables as the identifers provided in the first intro pattern branch (here, ``i``). -Notes: +Note: + For the steps 3. and 4. above, the :tacn:`under` tactic also supports subgoals of the form ``some_expr(i) <-> ?Goal i``, which are "protected" in the form ``Under_iff (some_expr i) (?Goal i)``, itself pretty-printed as ``'Under_iff[ some_expr i ]``. -+ If the intro pattern is omitted, the Ltac expression: - :n:`under {@occ_switch}[@r_pattern]@term.` defaults to: - :n:`under {@occ_switch}[@r_pattern]@term => *.` - Two equivalent facilities (a terminator and a lemma) are provided to close intermediate subgoal ``Under[ … ]`` and instantiate the corresponding evar: @@ -3790,17 +3786,25 @@ The Ltac expression: can be viewed as a shorter form for the following Ltac expression: :n:`under {@occ_switch}[@r_pattern]@term => [i|j|]; [tac1; over | tac2; over | cbv beta iota].` -Here, the ``beta-iota`` reduction is useful to get rid of the beta -redexes that could be introduced after the substitution of the evars -by the :tacn:`under` tactic. +Notes: + ++ The ``beta-iota`` reduction here is useful to get rid of the beta + redexes that could be introduced after the substitution of the evars + by the :tacn:`under` tactic. + ++ Note that the provided tactics (e.g., ``tac1``) can just as well + involve other :tacn:`under` tactics. See below for a typical example + involving the `bigop` theory from the Mathematical Components library. -Note that the provided tactics (e.g., ``tac1``) can just as well -involve other :tacn:`under` tactics. See below for a typical example -involving the `bigop` theory from the Mathematical Components library. ++ If there is only one tactic, the brackets are optional, i.e.: + :n:`under @term => [i] do [tac1]` is equivalent to: + :n:`under @term => i do tac1.` and that shorter form should be + preferred. -If there is only one tactic, the brackets are optional, i.e.: -:n:`under @term => i do [tac1]` can be -shortened to: :n:`under @term => i do tac1.` ++ If the ``do`` clause is provided but the intro pattern is omitted, + the Ltac expression: + :n:`under {@occ_switch}[@r_pattern]@term do [tac1|tac2]` defaults to: + :n:`under {@occ_switch}[@r_pattern]@term => [*|*] do [tac1|tac2].` .. example:: diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 2bac69b5b7..d60e3857b1 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -406,7 +406,15 @@ let check_numgoals ?(minus = 0) nh = else Proofview.tclUNIT () -let undertac ist ipats ((dir,_),_ as rule) hint = +let rec ncons n e = match n with + | 0 -> [] + | n when n > 0 -> e :: ncons (n - 1) e + | _ -> failwith "ncons" + +let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = + + (* total number of implied hints *) + let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in let varnames = let rec aux acc = function @@ -426,7 +434,11 @@ let undertac ist ipats ((dir,_),_ as rule) hint = let ipats = match ipats with | None -> [IPatNoop] + | Some l when pad_intro -> (* typically, ipats = Some [IPatAnon All] *) + let new_l = ncons (nh - 1) l in + [IPatCase(Regular (new_l @ [[]]))] | Some (IPatCase(Regular []) :: _ as ipats) -> ipats + (* Erik: is the previous line correct/useful? *) | Some (IPatCase(Regular l) :: rest) -> IPatCase(Regular(l @ [[]])) :: rest | Some (IPatCase(Block _) :: _ as l) -> l | Some l -> [IPatCase(Regular [l;[]])] in @@ -457,7 +469,6 @@ let undertac ist ipats ((dir,_),_ as rule) hint = Proofview.tclUNIT () else let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in - let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in (* Usefulness of check_numgoals: tclDISPATCH would be enough, except for the error message w.r.t. the number of provided/expected tactics, as the last one is implied *) diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 6f7cc6d445..6dd01ca6fc 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -57,7 +57,13 @@ val sufftac : (bool * Tacinterp.Value.t option list)) -> Tacmach.tactic +(* pad_intro (by default false) indicates whether the intro-pattern + "=> i..." must be turned into "=> [i...|i...|i...|]" (n+1 branches, + assuming there are n provided tactics in the ssrhint argument + "do [...|...|...]"; it is useful when the intro-pattern is "=> *"). + Otherwise, "=> i..." is turned into "=> [i...|]". *) val undertac : + ?pad_intro:bool -> Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssripats option -> Ssrequality.ssrrwarg -> Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 2c46947658..4286ace519 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -2690,9 +2690,9 @@ TACTIC EXTEND under check_under_arg arg; Ssrfwd.undertac ist (Some ipats) arg h } - | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> *" *) + | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> [*|*]" *) check_under_arg arg; - Ssrfwd.undertac ist (Some [IPatAnon All]) arg h + Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h } END diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 1e3b0f678b..ba3aa9d621 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -104,6 +104,42 @@ under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1 | rewrite ad done. Qed. +Lemma test_big_2cond_0intro (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +under eq_big. +{ move=> n; rewrite (addnC n 1); over. } +{ move=> i Hi; rewrite (addnC i 2); over. } +done. +Qed. + +Lemma test_big_2cond_1intro (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +Fail under eq_big => i. +(* as it amounts to [under eq_big => [i]] *) +Abort. + +Lemma test_big_2cond_all (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +Fail under eq_big => *. +(* as it amounts to [under eq_big => [*]] *) +Abort. + +Lemma test_big_2cond_all_implied (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in one-liner mode *) +under eq_big do [move=> ? (* due to delta-head-cst *); rewrite addnC + |rewrite addnC]. +(* amounts to [under eq_big => [*|*] do [...|...]] *) +done. +Qed. + Lemma test_big_patt1 (F G : nat -> nat) (n : nat) : \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0. Proof. -- cgit v1.2.3 From e1e5d40a0f351cbf01f7e66d049f9a937d5f8563 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 3 Apr 2019 14:36:57 +0200 Subject: [doc] ssr_under: a few improvements --- .../proof-engine/ssreflect-proof-language.rst | 214 ++++++++++++--------- 1 file changed, 122 insertions(+), 92 deletions(-) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index c32788c9da..7545e1b8d7 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3636,10 +3636,10 @@ rewriting rule is stated using Leibniz equality (as opposed to setoid relations). It will be extended to other rewriting relations in the future. -.. _under_over_ssr: +.. _under_ssr: -A convenience under tactic -~~~~~~~~~~~~~~~~~~~~~~~~~~ +Rewriting under binders +~~~~~~~~~~~~~~~~~~~~~~~ Goals involving objects defined with higher-order functions often require "rewriting under binders". While setoid rewriting is a @@ -3661,92 +3661,127 @@ complete terms, as shown by the simple example below. .. coqtop:: in Axiom subnn : forall n : nat, n - n = 0. - Parameter G : (nat -> nat) -> nat -> nat. - Axiom eq_G : + Parameter map : (nat -> nat) -> list nat -> list nat. + Parameter sumlist : list nat -> nat. + Axiom eq_map : forall F1 F2 : nat -> nat, (forall n : nat, F1 n = F2 n) -> - forall n : nat, G F1 n = G F2 n. + forall l : list nat, map F1 l = map F2 l. .. coqtop:: all - Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. - In this context, one cannot directly use ``eq_G``: + In this context, one cannot directly use ``eq_map``: .. coqtop:: all fail - rewrite eq_G. + rewrite eq_map. as we need to explicitly provide the non-inferable argument ``F2``, which corresponds here to the term we want to obtain *after* the - rewriting step. We can thus do: + rewriting step. In order to perform the rewrie step one has to + provide the term by hand as follows: .. coqtop:: all abort - rewrite (@eq_G _ (fun _ : nat => 0)). + rewrite (@eq_map _ (fun _ : nat => 0)). by move=> m; rewrite subnn. - Otherwise, a more convenient approach consists in relying on the - :tacn:`under` tactic that alleviates this bookkeeping: + The :tacn:`under` tactic lets one perform the same operation in a more + convenient way: .. coqtop:: all abort - Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. - under eq_G => m do rewrite subnn. + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + under eq_map => m do rewrite subnn. + + +The under tactic +```````````````` + +The convenience :tacn:`under` tactic supports the following syntax: -.. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] ) } +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] ) } :name: under - Rewrite under :token:`term`. We distinguish two modes, - :ref:`interactive mode ` without a ``do`` clause, and - :ref:`one-liner mode ` with a ``do`` clause, - which are explained in more detail below. + Operate under the context proved to be extensional by + lemma :token:`term`. - .. exn:: Incorrect number of tactics (expected N tactics, was given N'). + .. exn:: Incorrect number of tactics (expected N tactics, was given M). This error can occur when using the version with a ``do`` clause. + The multiplier part of :token:`r_prefix` is not supported. + +We distinguish two modes, +:ref:`interactive mode ` without a ``do`` clause, and +:ref:`one-liner mode ` with a ``do`` clause, +which are explained in more detail below. + .. _under_interactive: Interactive mode ```````````````` + +Let us redo the running example in interactive mode. + +.. example:: + + .. coqtop:: all abort + + Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. + under eq_map => m. + rewrite subnn. + by over. + The execution of the Ltac expression: -:n:`under {@occ_switch}[@r_pattern]@term => [i|j].` + +:n:`under @term => [ @i_item__1 | … | @i_item__n ].` + involves the following steps: -1. It performs a full-blown :n:`rewrite {@occ_switch}[@r_pattern]@term`, - without failing like in the above example with ``eq_G``, but - creating evars. +1. It performs a :n:`rewrite @term` + without failing like in the above example with ``eq_map``, but + creating evars (see :tacn:`evar`). If :n:`term` is prefixed by + a pattern or an occurrence selector, then the modifiers is honoured. + +2. As a n-branches intro pattern is provided :tacn:`under` checks that + n+1 subgoals have been created. The last one is the main subgoal, + while the other ones correspond to premises of the rewrite rule (such as + ``forall n, F1 n = F2 n`` for ``eq_map``). + +3. Then :tacn:`under` checks that the first n subgoals + are (quantified) equalities or double implications between a + term and an evar (e.g. ``m - m = ?F2 m`` in the running example). -2. As a 2-branches intro pattern is provided, it checks that 3 subgoals - have been created (the last one being the initial, main subgoal that - now contains some evars). +4. If so :tacn:`under` executes the corresponding + intro pattern :n:`@ipat__i` in each goal. -3. In the first 2 subgoals, it introduces ``i``, resp. ``j``, and tests - whether these 2 subgoals are (quantified) equalities involving - an evar. For example: ``some_expr(i) = ?Goal i``. +5. Then :tacn:`under` protects these n goals against an + accidental instantiation of the evar. These protected goals are displayed + using the ``Under[ … ]`` notation (e.g. ``Under[ m - m ]`` + in the running example). -4. If this is the case, the subgoal is manipulated to get the - provably equivalent goal ``Under _ (some_expr i) (?Goal i)``, - pretty-printed as ``'Under[ some_expr i ]``. - This change avoids instantiating the evar by accident (e.g., if one - uses a proof script such as: :n:`rewrite lem1 // lem2`). +6. The expression inside the ``Under[ … ]`` notation can be + proved equivalent to the desired expression + by using a regular tacn:`rewrite` tactic. -5. Finally, a post-processing step is performed in the main (here, 3rd) - subgoal to try keeping (in the object after the rewrite) the same - bound variables as the identifers provided in the first - intro pattern branch (here, ``i``). +7. Interactive editing of the first n goals has to be signalled by + using the :tacn:`over` tactic or rewrite rule (see below). -Note: +8. Finally, a post-processing step is performed in the main goal + to keep the name(s) for the bound variables chosen by the user in + the intro pattern for the first branch. -+ For the steps 3. and 4. above, the :tacn:`under` tactic also - supports subgoals of the form ``some_expr(i) <-> ?Goal i``, which - are "protected" in the form ``Under_iff (some_expr i) (?Goal i)``, - itself pretty-printed as ``'Under_iff[ some_expr i ]``. +.. _over_ssr: + +The over tactic ++++++++++++++++ Two equivalent facilities (a terminator and a lemma) are provided to -close intermediate subgoal ``Under[ … ]`` and instantiate the -corresponding evar: +close intermediate subgoals generated by :tacn:`under` (i.e. goals +displayed as ``Under[ … ]``): .. tacn:: over :name: over @@ -3764,27 +3799,18 @@ corresponding evar: This is a variant of :tacn:`over` in order to close ``Under_iff[ … ]`` goals, relying on the ``over_iff`` lemma. -Let us focus again on the simple example involving an extensionality -lemma ``eq_G``, but this time in interactive mode: - -.. example:: - - .. coqtop:: all abort - - Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. - under eq_G => m. - rewrite subnn. - over. - .. _under_one_liner: One-liner mode `````````````` The Ltac expression: -:n:`under {@occ_switch}[@r_pattern]@term => [i|j] do [tac1|tac2]` -can be viewed as a shorter form for the following Ltac expression: -:n:`under {@occ_switch}[@r_pattern]@term => [i|j|]; [tac1; over | tac2; over | cbv beta iota].` + +:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].` + +can be seen as a shorter form for the following expression: + +:n:`under @term => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].` Notes: @@ -3792,19 +3818,19 @@ Notes: redexes that could be introduced after the substitution of the evars by the :tacn:`under` tactic. -+ Note that the provided tactics (e.g., ``tac1``) can just as well ++ Note that the provided tactics can as well involve other :tacn:`under` tactics. See below for a typical example involving the `bigop` theory from the Mathematical Components library. -+ If there is only one tactic, the brackets are optional, i.e.: - :n:`under @term => [i] do [tac1]` is equivalent to: - :n:`under @term => i do tac1.` and that shorter form should be ++ If there is only one tactic, the brackets can be omitted, e.g.: + :n:`under @term => i do @tac.` and that shorter form should be preferred. -+ If the ``do`` clause is provided but the intro pattern is omitted, - the Ltac expression: - :n:`under {@occ_switch}[@r_pattern]@term do [tac1|tac2]` defaults to: - :n:`under {@occ_switch}[@r_pattern]@term => [*|*] do [tac1|tac2].` ++ If the ``do`` clause is provided and the intro pattern is omitted, + then the defeault :token:`i_item` ``*`` is applied to each branch. + Eg the Ltac expression + :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to + :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ].` .. example:: @@ -3815,27 +3841,25 @@ Notes: Unset Strict Implicit. Unset Printing Implicit Defensive. + Coercion is_true : bool >-> Sortclass. + Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50, format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'"). - Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F" - (at level 36, F at level 36, op, idx at level 10, i, m, n at level 50, - format "'[' \big [ op / idx ]_ ( m <= i < n ) '/ ' F ']'"). - Variant bigbody (R I : Type) : Type := BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I. Parameter bigop : forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R. - Axiom eq_bigr : + Axiom eq_bigr_ : forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) (r : list I) (P : I -> bool) (F1 F2 : I -> R), - (forall x : I, P x = true -> F1 x = F2 x) -> + (forall x : I, is_true (P x) -> F1 x = F2 x) -> bigop idx r (fun i : I => BigBody i op (P i) (F1 i)) = bigop idx r (fun i : I => BigBody i op (P i) (F2 i)). - Axiom eq_big : + Axiom eq_big_ : forall (R : Type) (idx : R) (op : R -> R -> R) (I : Type) (r : list I) (P1 P2 : I -> bool) (F1 F2 : I -> R), (forall x : I, P1 x = P2 x) -> @@ -3846,34 +3870,40 @@ Notes: Reserved Notation "\sum_ ( m <= i < n | P ) F" (at level 41, F at level 41, i, m, n at level 50, format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). - Reserved Notation "\sum_ ( m <= i < n ) F" - (at level 41, F at level 41, i, m, n at level 50, - format "'[' \sum_ ( m <= i < n ) '/ ' F ']'"). Parameter index_iota : nat -> nat -> list nat. Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" := (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%bool F)). - Notation "\big [ op / idx ]_ ( m <= i < n ) F" := - (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F)). Notation "\sum_ ( m <= i < n | P ) F" := (\big[plus/O]_(m <= i < n | P%bool) F%nat). - Notation "\sum_ ( m <= i < n ) F" := - (\big[plus/O]_(m <= i < n) F%nat). + + Notation eq_bigr := (fun n m => eq_bigr_ 0 plus (index_iota n m)). + Notation eq_big := (fun n m => eq_big_ 0 plus (index_iota n m)). + + Parameter odd : nat -> bool. + Parameter prime : nat -> bool. .. coqtop:: in Parameter addnC : forall m n : nat, m + n = n + m. Parameter muln1 : forall n : nat, n * 1 = n. - Parameter odd : nat -> bool. .. coqtop:: all - Lemma test_big_nested (F G : nat -> nat) (m n : nat) : - \sum_(0 <= a < m) \sum_(0 <= j < n | odd (j * 1)) (a + j) = - \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). - under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1|rewrite addnC]. + Check eq_bigr. + Check eq_big. + + Lemma test_big_nested (m n : nat) : + \sum_(0 <= a < m | prime a) \sum_(0 <= j < n | odd (j * 1)) (a + j) = + \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i). + under eq_bigr => i prime_i do + under eq_big => [ j | j odd_j ] do + [ rewrite (muln1 j) | rewrite (addnC i j) ]. + + Remark how the final goal uses the name ``i`` (the name given in the + intro pattern) rather than ``a`` in the binder of the first summation. .. _locking_ssr: @@ -5612,13 +5642,13 @@ respectively. rewrite (see :ref:`rewriting_ssr`) -.. tacn:: under {? @occ_switch} {? [ @r_pattern ] } @term {? => @i_item} {? do ( @tactic | [ {*| @tactic } ] )} +.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] )} - under (see :ref:`under_over_ssr`) + under (see :ref:`under_ssr`) .. tacn:: over - over (see :ref:`under_over_ssr`) + over (see :ref:`over_ssr`) .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } -- cgit v1.2.3 From 4bc91ba5654574d156ebf2934a6fb36d31b40ff9 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Apr 2019 15:03:02 +0200 Subject: [ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations as suggested by @gares, and: * Rename some Under_* terms for better uniformity; * Update & Improve minor details in the documentation. --- .../proof-engine/ssreflect-proof-language.rst | 39 +++++----- plugins/ssr/ssreflect.v | 83 +++++++++++----------- plugins/ssr/ssrfwd.ml | 6 +- test-suite/output/ssr_under.out | 2 + test-suite/output/ssr_under.v | 15 ++++ test-suite/ssr/over.v | 8 +-- 6 files changed, 83 insertions(+), 70 deletions(-) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 7545e1b8d7..a40dfa486f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3680,7 +3680,7 @@ complete terms, as shown by the simple example below. as we need to explicitly provide the non-inferable argument ``F2``, which corresponds here to the term we want to obtain *after* the - rewriting step. In order to perform the rewrie step one has to + rewriting step. In order to perform the rewrite step one has to provide the term by hand as follows: .. coqtop:: all abort @@ -3742,30 +3742,30 @@ The execution of the Ltac expression: involves the following steps: 1. It performs a :n:`rewrite @term` - without failing like in the above example with ``eq_map``, but - creating evars (see :tacn:`evar`). If :n:`term` is prefixed by - a pattern or an occurrence selector, then the modifiers is honoured. + without failing like in the first example with ``rewrite eq_map.``, + but creating evars (see :tacn:`evar`). If :n:`term` is prefixed by + a pattern or an occurrence selector, then the modifiers are honoured. 2. As a n-branches intro pattern is provided :tacn:`under` checks that n+1 subgoals have been created. The last one is the main subgoal, while the other ones correspond to premises of the rewrite rule (such as ``forall n, F1 n = F2 n`` for ``eq_map``). -3. Then :tacn:`under` checks that the first n subgoals +3. If so :tacn:`under` executes the corresponding + intro pattern :n:`@ipat__i` in each goal. + +4. Then :tacn:`under` checks that the first n subgoals are (quantified) equalities or double implications between a term and an evar (e.g. ``m - m = ?F2 m`` in the running example). -4. If so :tacn:`under` executes the corresponding - intro pattern :n:`@ipat__i` in each goal. - -5. Then :tacn:`under` protects these n goals against an - accidental instantiation of the evar. These protected goals are displayed - using the ``Under[ … ]`` notation (e.g. ``Under[ m - m ]`` - in the running example). +5. If so :tacn:`under` protects these n goals against an + accidental instantiation of the evar. + These protected goals are displayed using the ``Under[ … ]`` + notation (e.g. ``Under[ m - m ]`` in the running example). 6. The expression inside the ``Under[ … ]`` notation can be proved equivalent to the desired expression - by using a regular tacn:`rewrite` tactic. + by using a regular :tacn:`rewrite` tactic. 7. Interactive editing of the first n goals has to be signalled by using the :tacn:`over` tactic or rewrite rule (see below). @@ -3787,17 +3787,12 @@ displayed as ``Under[ … ]``): :name: over This terminator tactic allows one to close goals of the form - ``'Under[ … ]`` or ``'Under_iff[ … ]``. + ``'Under[ … ]``. .. tacv:: by rewrite over This is a variant of :tacn:`over` in order to close ``Under[ … ]`` - goals, relying on the ``over`` lemma. - -.. tacv:: by rewrite over_iff - - This is a variant of :tacn:`over` in order to close ``Under_iff[ … ]`` - goals, relying on the ``over_iff`` lemma. + goals, relying on the ``over`` rewrite rule. .. _under_one_liner: @@ -3828,8 +3823,8 @@ Notes: + If the ``do`` clause is provided and the intro pattern is omitted, then the defeault :token:`i_item` ``*`` is applied to each branch. - Eg the Ltac expression - :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to + E.g., the Ltac expression: + :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to: :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ].` .. example:: diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 94e0b2a724..6c74ac1960 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -504,55 +504,55 @@ Proof. by move=> /(_ P); apply. Qed. (*****************************************************************************) (* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *) -Module Type UNDER. -Parameter Under : +Module Type UNDER_EQ. +Parameter Under_eq : forall (R : Type), R -> R -> Prop. -Parameter Under_from_eq : - forall (T : Type) (x y : T), @Under T x y -> x = y. +Parameter Under_eq_from_eq : + forall (T : Type) (x y : T), @Under_eq T x y -> x = y. -(** [Over, over, over_done]: for "by rewrite over" *) -Parameter Over : +(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *) +Parameter Over_eq : forall (R : Type), R -> R -> Prop. -Parameter over : - forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y. -Parameter over_done : - forall (T : Type) (x : T), @Over T x x. +Parameter over_eq : + forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. +Parameter over_eq_done : + forall (T : Type) (x : T), @Over_eq T x x. (* We need both hints below, otherwise the test-suite does not pass *) -Hint Extern 0 (@Over _ _ _) => solve [ apply over_done ] : core. +Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core. (* => for [test-suite/ssr/under.v:test_big_patt1] *) -Hint Resolve over_done : core. +Hint Resolve over_eq_done : core. (* => for [test-suite/ssr/over.v:test_over_1_1] *) -(** [under_done]: for Ltac-style over *) -Parameter under_done : - forall (T : Type) (x : T), @Under T x x. -Notation "''Under[' x ]" := (@Under _ x _) - (at level 8, format "''Under[' x ]"). -End UNDER. - -Module Export Under : UNDER. -Definition Under := @eq. -Lemma Under_from_eq (T : Type) (x y : T) : - @Under T x y -> x = y. +(** [under_eq_done]: for Ltac-style over *) +Parameter under_eq_done : + forall (T : Type) (x : T), @Under_eq T x x. +Notation "''Under[' x ]" := (@Under_eq _ x _) + (at level 8, format "''Under[' x ]", only printing). +End UNDER_EQ. + +Module Export Under_eq : UNDER_EQ. +Definition Under_eq := @eq. +Lemma Under_eq_from_eq (T : Type) (x y : T) : + @Under_eq T x y -> x = y. Proof. by []. Qed. -Definition Over := Under. -Lemma over : - forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y. +Definition Over_eq := Under_eq. +Lemma over_eq : + forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. Proof. by []. Qed. -Lemma over_done : - forall (T : Type) (x : T), @Over T x x. +Lemma over_eq_done : + forall (T : Type) (x : T), @Over_eq T x x. Proof. by []. Qed. -Lemma under_done : - forall (T : Type) (x : T), @Under T x x. +Lemma under_eq_done : + forall (T : Type) (x : T), @Under_eq T x x. Proof. by []. Qed. -End Under. +End Under_eq. -Register Under as plugins.ssreflect.Under. -Register Under_from_eq as plugins.ssreflect.Under_from_eq. +Register Under_eq as plugins.ssreflect.Under_eq. +Register Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq. Module Type UNDER_IFF. Parameter Under_iff : Prop -> Prop -> Prop. -Parameter Under_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y. +Parameter Under_iff_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y. (** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *) Parameter Over_iff : Prop -> Prop -> Prop. @@ -566,13 +566,13 @@ Hint Resolve over_iff_done : core. (** [under_iff_done]: for Ltac-style over *) Parameter under_iff_done : forall (x : Prop), @Under_iff x x. -Notation "''Under_iff[' x ]" := (@Under_iff x _) - (at level 8, format "''Under_iff[' x ]"). +Notation "''Under[' x ]" := (@Under_iff x _) + (at level 8, format "''Under[' x ]", only printing). End UNDER_IFF. Module Export Under_iff : UNDER_IFF. Definition Under_iff := iff. -Lemma Under_from_iff (x y : Prop) : +Lemma Under_iff_from_iff (x y : Prop) : @Under_iff x y -> x <-> y. Proof. by []. Qed. Definition Over_iff := Under_iff. @@ -588,11 +588,12 @@ Proof. by []. Qed. End Under_iff. Register Under_iff as plugins.ssreflect.Under_iff. -Register Under_from_iff as plugins.ssreflect.Under_from_iff. +Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff. + +Definition over := (over_eq, over_iff). Ltac over := - by [ apply: Under.under_done - | rewrite over + by [ apply: Under_eq.under_eq_done | apply: Under_iff.under_iff_done - | rewrite over_iff + | rewrite over ]. diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index d60e3857b1..313b46ddc3 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -347,7 +347,7 @@ let intro_lock ipats = let sigma, under_iff = Ssrcommon.mkSsrConst "Under_iff" env sigma in let sigma, under_from_iff = - Ssrcommon.mkSsrConst "Under_from_iff" env sigma in + Ssrcommon.mkSsrConst "Under_iff_from_iff" env sigma in let ty = EConstr.mkApp (under_iff,args) in let sigma, t = Evarutil.new_evar env sigma ty in sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|])) @@ -359,9 +359,9 @@ let intro_lock ipats = Array.length args = 3 && is_app_evar sigma args.(2) -> Tactics.New.refine ~typecheck:true (fun sigma -> let sigma, under = - Ssrcommon.mkSsrConst "Under" env sigma in + Ssrcommon.mkSsrConst "Under_eq" env sigma in let sigma, under_from_eq = - Ssrcommon.mkSsrConst "Under_from_eq" env sigma in + Ssrcommon.mkSsrConst "Under_eq_from_eq" env sigma in let ty = EConstr.mkApp (under,args) in let sigma, t = Evarutil.new_evar env sigma ty in sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|])) diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out index 8532b62a54..499d25391e 100644 --- a/test-suite/output/ssr_under.out +++ b/test-suite/output/ssr_under.out @@ -1,2 +1,4 @@ 'Under[ m - m ] (G (fun _ : nat => 0) n >= 0) +'Under[ r = R0 \/ E r ] +(Rbar_le Rbar0 (Lub_Rbar (fun r : R => r = R0 \/ E r))) diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v index b11dd1509c..7335c87e61 100644 --- a/test-suite/output/ssr_under.v +++ b/test-suite/output/ssr_under.v @@ -13,3 +13,18 @@ Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. under eq_G => m do show; rewrite subnn. show. Abort. + +Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar). +Parameter Rbar_le : Rbar -> Rbar -> Prop. +Parameter Lub_Rbar : (R -> Prop) -> Rbar. +Parameter Lub_Rbar_eqset : + forall E1 E2 : R -> Prop, + (forall x : R, E1 x <-> E2 x) -> + Lub_Rbar E1 = Lub_Rbar E2. + +Lemma test_Lub_Rbar (E : R -> Prop) : + Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)). +Proof. +under Lub_Rbar_eqset => r do show. +show. +Abort. diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v index cd6b196eeb..8232741b0d 100644 --- a/test-suite/ssr/over.v +++ b/test-suite/ssr/over.v @@ -12,7 +12,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i). unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. over. @@ -27,7 +27,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i). unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. by rewrite over. @@ -45,7 +45,7 @@ assert (H : forall i j, i + 2 * j - i = x2 i j). unfold R in *; clear R; unfold J in *; clear J; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. over. @@ -61,7 +61,7 @@ assert (H : forall i j : nat, i + 2 * j - i = x2 i j). unfold R in *; clear R; unfold J in *; clear J; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. rewrite over. -- cgit v1.2.3 From 36488400952da5e12c8af451b1a936a34b26039d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 3 Apr 2019 15:39:11 +0200 Subject: [ssr] under: optimization of the tactic for (under eq_bigl => *) so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|]. Also: replace "by over." in the doc example with "over." --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 15 +++++++++------ plugins/ssr/ssrfwd.ml | 15 +++++++++------ test-suite/ssr/under.v | 4 ++-- 3 files changed, 20 insertions(+), 14 deletions(-) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index a40dfa486f..4e40df6f94 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3733,7 +3733,7 @@ Let us redo the running example in interactive mode. Lemma example_map l : sumlist (map (fun m => m - m) l) = 0. under eq_map => m. rewrite subnn. - by over. + over. The execution of the Ltac expression: @@ -3751,8 +3751,9 @@ involves the following steps: while the other ones correspond to premises of the rewrite rule (such as ``forall n, F1 n = F2 n`` for ``eq_map``). -3. If so :tacn:`under` executes the corresponding - intro pattern :n:`@ipat__i` in each goal. +3. If so :tacn:`under` puts these n goals in head normal form (using + the defective form of the tactic :tacn:`move`), then executes + the corresponding intro pattern :n:`@ipat__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals are (quantified) equalities or double implications between a @@ -3805,7 +3806,7 @@ The Ltac expression: can be seen as a shorter form for the following expression: -:n:`under @term => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].` +:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].` Notes: @@ -3822,10 +3823,12 @@ Notes: preferred. + If the ``do`` clause is provided and the intro pattern is omitted, - then the defeault :token:`i_item` ``*`` is applied to each branch. + then the default :token:`i_item` ``*`` is applied to each branch. E.g., the Ltac expression: :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to: - :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ].` + :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]` + (and it can be noted here that the :tacn:`under` tactic performs a + ``move.`` before processing the intro patterns ``=> [ * | … | * ]``). .. example:: diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 313b46ddc3..01d71aa96a 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -331,7 +331,15 @@ let is_app_evar sigma t = | _ -> false end | _ -> false +let rec ncons n e = match n with + | 0 -> [] + | n when n > 0 -> e :: ncons (n - 1) e + | _ -> failwith "ncons" + let intro_lock ipats = + let hnf' = Proofview.numgoals >>= fun ng -> + Proofview.tclDISPATCH + (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ -> Proofview.tclORELSE (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())]) @@ -372,7 +380,7 @@ let intro_lock ipats = end) end in - Ssripats.tclIPATssr ipats <*> lock_eq () + hnf' <*> Ssripats.tclIPATssr ipats <*> lock_eq () let pretty_rename evar_map term varnames = let rec aux term vars = @@ -406,11 +414,6 @@ let check_numgoals ?(minus = 0) nh = else Proofview.tclUNIT () -let rec ncons n e = match n with - | 0 -> [] - | n when n > 0 -> e :: ncons (n - 1) e - | _ -> failwith "ncons" - let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = (* total number of implied hints *) diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index ba3aa9d621..84f6b9ad03 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -90,7 +90,7 @@ under eq_bigr => i Hi. under eq_big => [j|j Hj]. { rewrite muln1. over. } { rewrite addnC. over. } -(* MISSING BETA *) + simpl. (* or: cbv beta. *) over. by []. Qed. @@ -134,7 +134,7 @@ Lemma test_big_2cond_all_implied (F : nat -> nat) (m : nat) : \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. Proof. (* in one-liner mode *) -under eq_big do [move=> ? (* due to delta-head-cst *); rewrite addnC +under eq_big do [rewrite addnC |rewrite addnC]. (* amounts to [under eq_big => [*|*] do [...|...]] *) done. -- cgit v1.2.3 From 92e2bb2bebc99b6a72ea0babad9a1c374129a0c0 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 16 Apr 2019 03:18:03 +0200 Subject: [ssr] set under's tactic argument at LEVEL 3 So if the underlying tactic "contains a ;" one should actually write: under eq_bigl => i do [rewrite andb_idl; first by move/eqP->]. --- plugins/ssr/ssrparser.mlg | 20 ++++++++++++++++++-- test-suite/output/ssr_under.v | 2 +- test-suite/ssr/under.v | 2 +- 3 files changed, 20 insertions(+), 4 deletions(-) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 4286ace519..4d65fc81d1 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -86,6 +86,15 @@ GRAMMAR EXTEND Gram ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]]; END +(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *) +ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } +| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } +END +GRAMMAR EXTEND Gram + GLOBAL: ssrtac3arg; + ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]]; +END + { (* Lexically closed tactic for tacticals. *) @@ -1065,6 +1074,13 @@ ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintar | [ ssrtacarg(arg) ] -> { mk_hint arg } END +(* Copy of ssrhintarg with LEVEL "3", useful for: "under ... do ..." *) +ARGUMENT EXTEND ssrhint3arg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma } +| [ "[" "]" ] -> { nullhint } +| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs } +| [ ssrtac3arg(arg) ] -> { mk_hint arg } +END + ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma } | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs } END @@ -2686,11 +2702,11 @@ TACTIC EXTEND under check_under_arg arg; Ssrfwd.undertac ist (Some ipats) arg nohint } - | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhintarg(h) ] -> { + | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhint3arg(h) ] -> { check_under_arg arg; Ssrfwd.undertac ist (Some ipats) arg h } - | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> [*|*]" *) + | [ "under" ssrrwarg(arg) "do" ssrhint3arg(h) ] -> { (* implicit "=> [*|*]" *) check_under_arg arg; Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h } diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v index 7335c87e61..fb7503d902 100644 --- a/test-suite/output/ssr_under.v +++ b/test-suite/output/ssr_under.v @@ -10,7 +10,7 @@ Axiom eq_G : Ltac show := match goal with [|-?g] => idtac g end. Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. -under eq_G => m do show; rewrite subnn. +under eq_G => m do [show; rewrite subnn]. show. Abort. diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index 84f6b9ad03..f285ad138b 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -175,7 +175,7 @@ Qed. Lemma test_big_andb (F : nat -> nat) (m n : nat) : \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1. Proof. -under eq_bigl => i do rewrite andb_idl; first by move/eqP->. +under eq_bigl => i do [rewrite andb_idl; first by move/eqP->]. under eq_bigr => i do move/eqP=>{1}->. (* the 2nd occ should not be touched *) myadmit. Qed. -- cgit v1.2.3