diff options
39 files changed, 692 insertions, 497 deletions
diff --git a/Makefile.doc b/Makefile.doc index a5ff8e0123..e9bc03565d 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -101,7 +101,7 @@ full-stdlib: \ doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf sphinx-clean: - rm -rf $(SPHINXBUILDDIR) + rm -rf $(SPHINXBUILDDIR) doc/sphinx/index.rst doc/sphinx/zebibliography.rst .PHONY: plugin-tutorial plugin-tutorial: states tools diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 7724d7433c..63ddbd0a3a 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -10,19 +10,16 @@ the user and the assistant. The building blocks for this dialog are tactics which the user will use to represent steps in the proof of a theorem. -Incomplete proofs have one or more open (unproven) sub-goals. Each -goal has its own context (a set of assumptions that can be used to -prove the goal). Tactics can transform goals and contexts. -Internally, the incomplete proof is represented as a partial proof -term, with holes for the unproven sub-goals. +The first section presents the proof mode (the core mechanism of the +dialog between the user and the proof assistant). Then, several +sections describe the available tactics. One section covers the +SSReflect proof language, which provides a consistent alternative set +of tactics to the standard basic tactics. The last section documents +the ``Scheme`` family of commands, which can be used to extend the +power of the :tacn:`induction` and :tacn:`inversion` tactics. -When a proof is complete, the user leaves the proof mode and defers -the verification of the resulting proof term to the :ref:`kernel -<core-language>`. - -This chapter is divided in several parts, describing the basic ideas -of the proof mode (during which tactics can be used), and several -flavors of tactics, including the SSReflect proof language. +Additional tactics are documented in the next chapter +:ref:`automatic-tactics`. .. toctree:: :maxdepth: 1 diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index a482e044d8..cc9e1bb31d 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -175,7 +175,21 @@ let rec remove_grammars n = camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries; remove_grammars (n - 1) -(* Parse a string, does NOT check if the entire string was read *) +let make_rule r = [None, None, r] + +(** An entry that checks we reached the end of the input. *) + +(* used by the Tactician plugin *) +let eoi_entry en = + let e = Entry.make ((Entry.name en) ^ "_eoi") in + let symbs = Rule.next (Rule.next Rule.stop (Symbol.nterm en)) (Symbol.token Tok.PEOI) in + let act = fun _ x loc -> x in + let ext = { pos = None; data = make_rule [Production.make symbs act] } in + safe_extend e ext; + e + +(* Parse a string, does NOT check if the entire string was read + (use eoi_entry) *) let parse_string f ?loc x = let strm = Stream.of_string x in @@ -289,6 +303,7 @@ module Constr = let constr = Entry.create "constr" let term = Entry.create "term" let operconstr = term + let constr_eoi = eoi_entry constr let lconstr = Entry.create "lconstr" let binder_constr = Entry.create "binder_constr" let ident = Entry.create "ident" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8bff5cfd94..06d05a4797 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -120,6 +120,7 @@ end (** Parse a string *) val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a +val eoi_entry : 'a Entry.t -> 'a Entry.t type gram_universe [@@deprecated "Deprecated in 8.13"] [@@@ocaml.warning "-3"] @@ -180,6 +181,7 @@ module Prim : module Constr : sig val constr : constr_expr Entry.t + val constr_eoi : constr_expr Entry.t val lconstr : constr_expr Entry.t val binder_constr : constr_expr Entry.t val term : constr_expr Entry.t diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 80c13a3698..196a68e67c 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -47,6 +47,8 @@ let binder_tactic = Entry.create "binder_tactic" let tactic = Entry.create "tactic" (* Main entry for quotations *) +let tactic_eoi = eoi_entry tactic + let () = let open Stdarg in let open Tacarg in diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 73bce84d18..c0bf6b9f76 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -40,3 +40,4 @@ val tactic_expr : raw_tactic_expr Entry.t [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"] val binder_tactic : raw_tactic_expr Entry.t val tactic : raw_tactic_expr Entry.t +val tactic_eoi : raw_tactic_expr Entry.t diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d0b724b755..4b0974ae03 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -127,9 +127,10 @@ let flex_kind_of_term flags env evd c sk = else Rigid | Evar ev -> if is_evar_allowed flags (fst ev) then Flexible ev else Rigid - | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid + | Lambda _ | Prod _ | Sort _ | Ind _ | Int _ | Float _ | Array _ -> Rigid + | Construct _ | CoFix _ (* Incorrect: should check only app in sk *) -> Rigid | Meta _ -> Rigid - | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) + | Fix _ -> Rigid (* happens when the fixpoint is partially applied (should check it?) *) | Cast _ | App _ | Case _ -> assert false let apprec_nohdbeta flags env evd c = @@ -328,12 +329,6 @@ let ise_and evd l = | UnifFailure _ as x -> x in ise_and evd l -let ise_exact ise x1 x2 = - match ise x1 x2 with - | None, out -> out - | _, (UnifFailure _ as out) -> out - | Some _, Success i -> UnifFailure (i,NotSameArgSize) - let ise_array2 evd f v1 v2 = let rec allrec i = function | -1 -> Success i @@ -355,37 +350,49 @@ let rec ise_inst2 evd f l1 l2 = match l1, l2 with (* Applicative node of stack are read from the outermost to the innermost but are unified the other way. *) -let rec ise_app_stack2 env f evd sk1 sk2 = - match sk1,sk2 with - | Stack.App node1 :: q1, Stack.App node2 :: q2 -> - let (t1,l1) = Stack.decomp_node_last node1 q1 in - let (t2,l2) = Stack.decomp_node_last node2 q2 in - begin match ise_app_stack2 env f evd l1 l2 with - |(_,UnifFailure _) as x -> x - |x,Success i' -> x,f env i' CONV t1 t2 +let rec ise_app_rev_stack2 env f evd revsk1 revsk2 = + match Stack.decomp_rev revsk1, Stack.decomp_rev revsk2 with + | Some (t1,revsk1), Some (t2,revsk2) -> + begin + match ise_app_rev_stack2 env f evd revsk1 revsk2 with + | (_, UnifFailure _) as x -> x + | x, Success i' -> x, f env i' CONV t1 t2 end - | _, _ -> (sk1,sk2), Success evd + | _, _ -> (revsk1,revsk2), Success evd (* This function tries to unify 2 stacks element by element. It works from the end to the beginning. If it unifies a non empty suffix of stacks but not the entire stacks, the first part of the answer is - Some(the remaining prefixes to tackle)) *) -let ise_stack2 no_app env evd f sk1 sk2 = - let rec ise_stack2 deep i sk1 sk2 = - let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i + Some(the remaining prefixes to tackle) + If [no_app] is set, situations like [match head u1 u2 with ... end] + will not try to match [u1] and [u2] (why?); but situations like + [match head u1 u2 with ... end v] will try to match [v] (??) *) +(* Input: E1[] =? E2[] where the E1, E2 are concatenations of + n-ary-app/case/fix/proj elimination rules + Output: + - either None if E1 = E2 is solved, + - or Some (E1'',E2'') such that there is a decomposition of + E1[] = E1'[E1''[]] and E2[] = E2'[E2''[]] s.t. E1' = E2' and + E1'' cannot be unified with E2'' + - UnifFailure if no such non-empty E1' = E2' exists *) +let rec ise_stack2 no_app env evd f sk1 sk2 = + let rec ise_rev_stack2 deep i revsk1 revsk2 = + let fail x = if deep then Some (List.rev revsk1, List.rev revsk2), Success i else None, x in - match sk1, sk2 with + match revsk1, revsk2 with | [], [] -> None, Success i | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 -> - (match f env i CONV t1 t2 with - | Success i' -> - (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with - | Success i'' -> ise_stack2 true i'' q1 q2 - | UnifFailure _ as x -> fail x) - | UnifFailure _ as x -> fail x) + begin + match ise_and i [ + (fun i -> f env i CONV t1 t2); + (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2)] + with + | Success i' -> ise_rev_stack2 true i' q1 q2 + | UnifFailure _ as x -> fail x + end | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) - then ise_stack2 true i q1 q2 + then ise_rev_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> @@ -393,51 +400,51 @@ let ise_stack2 no_app env evd f sk1 sk2 = match ise_and i [ (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); - (fun i -> ise_exact (ise_stack2 false i) a1 a2)] with - | Success i' -> ise_stack2 true i' q1 q2 + (fun i -> snd (ise_stack2 no_app env i f a1 a2))] with + | Success i' -> ise_rev_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else - begin match ise_app_stack2 env f i sk1 sk2 with + begin match ise_app_rev_stack2 env f i revsk1 revsk2 with |_,(UnifFailure _ as x) -> fail x - |(l1, l2), Success i' -> ise_stack2 true i' l1 l2 + |(l1, l2), Success i' -> ise_rev_stack2 true i' l1 l2 end |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead)) - in ise_stack2 false evd (List.rev sk1) (List.rev sk2) + in ise_rev_stack2 false evd (List.rev sk1) (List.rev sk2) (* Make sure that the matching suffix is the all stack *) -let exact_ise_stack2 env evd f sk1 sk2 = - let rec ise_stack2 i sk1 sk2 = - match sk1, sk2 with +let rec exact_ise_stack2 env evd f sk1 sk2 = + let rec ise_rev_stack2 i revsk1 revsk2 = + match revsk1, revsk2 with | [], [] -> Success i | Stack.Case (_,t1,_,c1)::q1, Stack.Case (_,t2,_,c2)::q2 -> ise_and i [ - (fun i -> ise_stack2 i q1 q2); + (fun i -> ise_rev_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2); (fun i -> f env i CONV t1 t2)] | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then ise_and i [ - (fun i -> ise_stack2 i q1 q2); + (fun i -> ise_rev_stack2 i q1 q2); (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); - (fun i -> ise_stack2 i a1 a2)] + (fun i -> exact_ise_stack2 env i f a1 a2)] else UnifFailure (i,NotSameHead) | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 -> if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) - then ise_stack2 i q1 q2 + then ise_rev_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) | Stack.App _ :: _, Stack.App _ :: _ -> - begin match ise_app_stack2 env f i sk1 sk2 with + begin match ise_app_rev_stack2 env f i revsk1 revsk2 with |_,(UnifFailure _ as x) -> x - |(l1, l2), Success i' -> ise_stack2 i' l1 l2 + |(l1, l2), Success i' -> ise_rev_stack2 i' l1 l2 end |_, _ -> UnifFailure (i,(* Maybe improve: *) NotSameHead) in if Reductionops.Stack.compare_shape sk1 sk2 then - ise_stack2 evd (List.rev sk1) (List.rev sk2) + ise_rev_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) (* Add equality constraints for covariant/invariant positions. For @@ -575,31 +582,35 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in - let miller_pfenning on_left fallback ev lF tM evd = + let miller_pfenning l2r fallback ev lF tM evd = match is_unification_pattern_evar env evd ev lF tM with | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = tM in let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (conv_fun evar_conv_x) flags env evd - (position_problem on_left pbty,ev,t2) + (position_problem l2r pbty,ev,t2) in - let consume_stack on_left (termF,skF) (termO,skO) evd = - let switch f a b = if on_left then f a b else f b a in + let consume_stack l2r (termF,skF) (termO,skO) evd = + let switch f a b = if l2r then f a b else f b a in let not_only_app = Stack.not_purely_applicative skO in match switch (ise_stack2 not_only_app env evd (evar_conv_x flags)) skF skO with - |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> + | Some (l,r), Success i' when l2r && (not_only_app || List.is_empty l) -> + (* E[?n]=E'[redex] reduces to either l[?n]=r[redex] with + case/fix/proj in E' (why?) or ?n=r[redex] *) switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> + | Some (r,l), Success i' when not l2r && (not_only_app || List.is_empty l) -> + (* E'[redex]=E[?n] reduces to either r[redex]=l[?n] with + case/fix/proj in E' (why?) or r[redex]=?n *) switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - |None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO - |_, (UnifFailure _ as x) -> x - |Some _, _ -> UnifFailure (evd,NotSameArgSize) in - let eta env evd onleft sk term sk' term' = - assert (match sk with [] -> true | _ -> false); + | None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO + | _, (UnifFailure _ as x) -> x + | Some _, _ -> UnifFailure (evd,NotSameArgSize) in + let eta_lambda env evd onleft term (term',sk') = + (* Reduces an equation [env |- <(fun na:c1 => c'1)|empty> = <term'|sk'>] to + [env, na:c1 |- c'1 = sk'[term'] (with some additional reduction) *) let (na,c1,c'1) = destLambda evd term in - let c = nf_evar evd c1 in - let env' = push_rel (RelDecl.LocalAssum (na,c)) env in + let env' = push_rel (RelDecl.LocalAssum (na,c1)) env in let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env' evd (c'1, Stack.empty) in let out2 = whd_nored_state env' evd @@ -617,32 +628,39 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] in - let consume on_left (_, skF as apprF) (_,skM as apprM) i = + let consume l2r (_, skF as apprF) (_,skM as apprM) i = if not (Stack.is_empty skF && Stack.is_empty skM) then - consume_stack on_left apprF apprM i + consume_stack l2r apprF apprM i else quick_fail i in - let miller on_left ev (termF,skF as apprF) (termM, skM as apprM) i = - let switch f a b = if on_left then f a b else f b a in + let miller l2r ev (termF,skF as apprF) (termM, skM as apprM) i = + let switch f a b = if l2r then f a b else f b a in let not_only_app = Stack.not_purely_applicative skM in match Stack.list_of_app_stack skF with | None -> quick_fail evd | Some lF -> let tM = Stack.zip evd apprM in - miller_pfenning on_left + miller_pfenning l2r (fun () -> if not_only_app then (* Postpone the use of an heuristic *) switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) ev lF tM i in - let flex_maybeflex on_left ev (termF,skF as apprF) (termM, skM as apprM) vM = - let switch f a b = if on_left then f a b else f b a in + let flex_maybeflex l2r ev (termF,skF as apprF) (termM, skM as apprM) vM = + (* Problem: E[?n[inst]] = E'[redex] + Strategy, as far as I understand: + 1. if E[]=[]u1..un and ?n[inst] u1..un = E'[redex] is a Miller pattern: solve it now + 2a. if E'=E'1[E'2] and E=E'1 unifiable, recursively solve ?n[inst] = E'2[redex] + 2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve E2[?n[inst]] = E'2[redex] + 3. reduce the redex into M and recursively solve E[?n[inst]] =? E'[M] *) + let switch f a b = if l2r then f a b else f b a in let delta i = switch (evar_eqappr_x flags env i pbty) apprF (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (vM,skM)) in - let default i = ise_try i [miller on_left ev apprF apprM; - consume on_left apprF apprM; + let default i = ise_try i [miller l2r ev apprF apprM; + consume l2r apprF apprM; delta] in match EConstr.kind evd termM with @@ -663,8 +681,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let delta' i = switch (evar_eqappr_x flags env i pbty) apprF apprM' in - fun i -> ise_try i [miller on_left ev apprF apprM'; - consume on_left apprF apprM'; delta'] + fun i -> ise_try i [miller l2r ev apprF apprM'; + consume l2r apprF apprM'; delta'] with Retyping.RetypeError _ -> (* Happens thanks to w_unify building ill-typed terms *) default @@ -672,21 +690,32 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty end | _ -> default evd in - let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = - let switch f a b = if on_left then f a b else f b a in + let flex_rigid l2r ev (termF, skF as apprF) (termR, skR as apprR) = + (* Problem: E[?n[inst]] = E'[M] with M blocking computation (in theory) + Strategy, as far as I understand: + 1. if E[]=[]u1..un and ?n[inst] u1..un = E'[M] is a Miller pattern: solve it now + 2a. if E'=E'1[E'2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve ?n[inst] = E'2[M] + 2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj, + recursively solve E2[?n[inst]] = E'2[M] + 3a. if M a lambda or a constructor: eta-expand and recursively solve + 3b. if M a constructor C ..ui..: eta-expand and recursively solve proji[E[?n[inst]]]=ui + 4. fail if E purely applicative and ?n occurs rigidly in E'[M] + 5. absorb arguments if purely applicative and postpone *) + let switch f a b = if l2r then f a b else f b a in let eta evd = match EConstr.kind evd termR with | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> - eta env evd false skR termR skF termF - | Construct u -> eta_constructor flags env evd skR u skF termF + eta_lambda env evd false termR apprF + | Construct u -> eta_constructor flags env evd u skR apprF | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> - ise_try evd [consume_stack on_left apprF apprR; eta] + ise_try evd [consume_stack l2r apprF apprR; eta] | Some lF -> let tR = Stack.zip evd apprR in - miller_pfenning on_left + miller_pfenning l2r (fun () -> ise_try evd [eta;(* Postpone the use of an heuristic *) @@ -716,6 +745,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem true pbty,destEvar i' ev1',term2) else + (* HH: Why not to drop sk1 and sk2 since they unified *) evar_eqappr_x flags env evd pbty (ev1', sk1) (term2, sk2) | Some (r,[]), Success i' -> @@ -736,7 +766,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if isEvar i' ev1' then solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r)) - else evar_eqappr_x flags env evd pbty + else + (* HH: Why not to drop sk1 and sk2 since they unified *) + evar_eqappr_x flags env evd pbty (ev1', sk1) (term2, sk2) | None, (UnifFailure _ as x) -> (* sk1 and sk2 have no common outer part *) @@ -764,7 +796,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else (* We could instead try Miller unification, then postpone to see if other equations help, as in: - [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *) + [Check fun a b c : unit => (eq_refl : _ a b = _ c a b)] *) UnifFailure (i,NotSameArgSize) | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") in @@ -776,7 +808,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with | Flexible (sp1,al1), Flexible (sp2,al2) -> - (* sk1[?ev1] =? sk2[?ev2] *) + (* Notations: + - "sk" is a stack (or, more abstractly, an evaluation context, written E) + - "ev" is an evar "?ev", more precisely an evar ?n with an instance inst + - "al" is an evar instance + Problem: E₁[?n₁[inst₁]] = E₂[?n₂[inst₂]] (i.e. sk1[?ev1] =? sk2[?ev2] + Strategy is first-order unification + 1a. if E₁=E₂ unifiable, solve ?n₁[inst₁] = ?n₂[inst₂] + 1b. if E₂=E₂'[E₂''] and E₁=E₂' unifiable, recursively solve ?n₁[inst₁] = E₂''[?n₂[inst₂]] + 1b'. if E₁=E₁'[E₁''] and E₁'=E₂ unifiable, recursively solve E₁''[?n₁[inst₁]] = ?n₂[inst₂] + recursively solve E2[?n[inst]] = E'2[redex] + 2. fails if neither E₁ nor E₂ is a prefix of the other *) let f1 i = first_order env i term1 term2 sk1 sk2 and f2 i = if Evar.equal sp1 sp2 then @@ -976,10 +1018,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (* Eta-expansion *) | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> - eta env evd true sk1 term1 sk2 term2 + eta_lambda env evd true term1 (term2,sk2) | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> - eta env evd false sk2 term2 sk1 term1 + eta_lambda env evd false term2 (term1,sk1) | Rigid, Rigid -> begin match EConstr.kind evd term1, EConstr.kind evd term2 with @@ -1033,10 +1075,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else UnifFailure (evd,NotSameHead) | Construct u, _ -> - eta_constructor flags env evd sk1 u sk2 term2 + eta_constructor flags env evd u sk1 (term2,sk2) | _, Construct u -> - eta_constructor flags env evd sk2 u sk1 term1 + eta_constructor flags env evd u sk2 (term1,sk1) | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then @@ -1131,7 +1173,9 @@ and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk (fst (decompose_app_vect i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 = +and eta_constructor flags env evd ((ind, i), u) sk1 (term2,sk2) = + (* reduces an equation <Construct(ind,i)|sk1> == <term2|sk2> to the + equations [arg_i = Proj_i (sk2[term2])] where [sk1] is [params args] *) let open Declarations in let mib = lookup_mind (fst ind) env in match get_projections env ind with diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 44414aa6a0..f9f6f74a66 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1585,7 +1585,16 @@ let rec invert_definition unify flags choose imitate_defs imitate envk (subst1 b c) | Evar (evk',args' as ev') -> if Evar.equal evk evk' then raise (OccurCheckIn (evd,rhs)); - (* Evar/Evar problem (but left evar is virtual) *) + (* At this point, we imitated a context say, C[ ], and virtually + instantiated ?evk@{x₁..xn} with C[?evk''@{x₁..xn,y₁..yk}] + for y₁..yk the spine of variables of C[ ], now facing the + equation env, y₁...yk |- ?evk'@{args'} =?= ?evk''@{args,y1:=y1..yk:=yk} *) + (* Assume evk' is defined in context x₁'..xk'. + As a first step, we try to find a restriction ?evk'''@{xᵢ₁'..xᵢⱼ} of + ?evk' and an instance args''' in the environment of ?evk such that + env, y₁..yk |- args'''[args] = args' and thus such that + env, y₁..yk |- ?evk'''@{args'''[args]} = ?evk''@{args,y1:=y1..yk:=yk} *) + (* Note that we don't need to declare ?evk'' yet: it may remain virtual *) let aliases = lift_aliases k aliases in (try let ev = (evk,List.map (lift k) argsv) in @@ -1597,14 +1606,14 @@ let rec invert_definition unify flags choose imitate_defs | CannotProject (evd,ev') -> if not !progress then raise (NotEnoughInformationEvarEvar t); - (* Make the virtual left evar real *) + (* We could not invert args' in terms of args, so we now make ?evk'' real *) let ty = get_type_of env' evd t in let (evd,evar'',ev'') = materialize_evar (evar_define unify flags ~choose) env' evd k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) let (evk',args' as ev') = normalize_evar evd ev' in let evd = - (* Try to project (a restriction of) the left evar ... *) + (* Try now to invert args in terms of args' *) try let evd,body = project_evar_on_evar false unify flags env' evd aliases 0 None ev'' ev' in let evd = Evd.define evk' body evd in diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 094dae4828..d347f46637 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -136,6 +136,24 @@ val solve_evar_evar : ?force:bool -> (** The two evars are expected to be in inferably convertible types; if not, an exception IllTypedInstance is raised *) +(* [solve_simple_eqn unifier flags env evd (direction,?ev[inst],t)] + makes progresses on problems of the form [?ev[inst] := t] (or + [?ev[inst] :<= t], or [?ev[inst] :>= t]). It uses imitation and a + limited form of projection. At the time of writing this comment, + only rels/vars (possibly indirectly via a chain of evars) and + constructors are used for projection. For instance + [?e[x,S 0] := x + S 0] will be solved by imitating [+] and + projecting [x] and [S 0] (so that [?e[a,b]:=a+b]) but in + [?e[0+0] := 0+0], the possible imitation will not be seen. + + [choose] tells to make an irreversible choice when two valid + projections are competing. It is to be used when no more reversible + progress can be done. It is [false] by default. + + [imitate_defs] tells to expand local definitions if they cannot be + projected. It is [true] by default. +*) + val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7a5d0897b5..52f60fbc5e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -194,6 +194,7 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + val decomp_rev : 'a t -> ('a * 'a t) option val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> @@ -214,13 +215,13 @@ end = struct open EConstr type 'a app_node = int * 'a array * int - (* first releavnt position, arguments, last relevant position *) + (* first relevant position, arguments, last relevant position *) (* - Invariant that this module must ensure : - (behare of direct access to app_node by the rest of Reductionops) + Invariant that this module must ensure: + (beware of direct access to app_node by the rest of Reductionops) - in app_node (i,_,j) i <= j - - There is no array realocation (outside of debug printing) + - There is no array reallocation (outside of debug printing) *) let pr_app_node pr (i,a,j) = @@ -267,12 +268,10 @@ struct let le = Array.length v in if Int.equal le 0 then s else App (0,v,pred le) :: s - let decomp_node (i,l,j) sk = - if i < j then (l.(i), App (succ i,l,j) :: sk) - else (l.(i), sk) - - let decomp = function - | App node::s -> Some (decomp_node node s) + let decomp_rev = function + | App (i,l,j) :: sk -> + if i < j then Some (l.(j), App (i,l,pred j) :: sk) + else Some (l.(j), sk) | _ -> None let decomp_node_last (i,l,j) sk = @@ -293,7 +292,7 @@ struct Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 | (Primitive(_,_,a1,_)::s1, Primitive(_,_,a2,_)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 - | ((Case _|Proj _|Fix _|Primitive _) :: _ | []) ,_ -> false in + | ((Case _ | Proj _ | Fix _ | Primitive _) :: _ | []) ,_ -> false in compare_rec 0 stk1 stk2 exception IncompatibleFold2 @@ -334,29 +333,35 @@ struct append_app a s let rec args_size = function - | App (i,_,j)::s -> j + 1 - i + args_size s - | (Case _|Fix _|Proj _|Primitive _)::_ | [] -> 0 + | App (i,_,j) :: s -> j + 1 - i + args_size s + | (Case _ | Fix _ | Proj _ | Primitive _) :: _ | [] -> 0 let strip_app s = let rec aux out = function | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s + let strip_n_app n s = let rec aux n out = function | App (i,a,j) as e :: s -> - let nb = j - i + 1 in + let nb = j - i + 1 in if n >= nb then - aux (n - nb) (e::out) s + aux (n - nb) (e :: out) s else - let p = i+n in + let p = i + n in Some (CList.rev (if Int.equal n 0 then out else App (i,a,p-1) :: out), a.(p), - if j > p then App(succ p,a,j)::s else s) + if j > p then App (succ p,a,j) :: s else s) | s -> None in aux n [] s + let decomp s = + match strip_n_app 0 s with + | Some (_,a,s) -> Some (a,s) + | None -> None + let not_purely_applicative args = List.exists (function (Fix _ | Case _ | Proj _ ) -> true | App _ | Primitive _ -> false) args @@ -369,12 +374,11 @@ struct (Array.fold_right (fun x y -> x::y) a' args', s') | s -> ([],s) in let (out,s') = aux s in - let init = match s' with [] -> true | _ -> false in - Option.init init out + match s' with [] -> Some out | _ -> None let assign s p c = match strip_n_app p s with - | Some (pre,_,sk) -> pre @ (App (0,[|c|],0)::sk) + | Some (pre,_,sk) -> pre @ (App (0,[|c|],0) :: sk) | None -> assert false let tail n0 s0 = @@ -382,12 +386,12 @@ struct if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> - let nb = j - i + 1 in + let nb = j - i + 1 in if n >= nb then aux (n - nb) s else let p = i+n in - if j >= p then App(p,a,j)::s else s + if j >= p then App (p,a,j) :: s else s | _ -> raise (Invalid_argument "Reductionops.Stack.tail") in aux n0 s0 @@ -1184,11 +1188,15 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 = let default_plain_instance_ident = Id.of_string "H" +type subst_fun = { sfun : metavariable -> EConstr.t } + (* Try to replace all metas. Does not replace metas in the metas' values * Differs from (strong whd_meta). *) -let plain_instance sigma s c = +let plain_instance sigma s c = match s with +| None -> c +| Some s -> let rec irec n u = match EConstr.kind sigma u with - | Meta p -> (try lift n (Metamap.find p s) with Not_found -> u) + | Meta p -> (try lift n (s.sfun p) with Not_found -> u) | App (f,l) when isCast sigma f -> let (f,_,t) = destCast sigma f in let l' = Array.Fun1.Smart.map irec n l in @@ -1197,7 +1205,7 @@ let plain_instance sigma s c = (* Don't flatten application nodes: this is used to extract a proof-term from a proof-tree and we want to keep the structure of the proof-tree *) - (try let g = Metamap.find p s in + (try let g = s.sfun p in match EConstr.kind sigma g with | App _ -> let l' = Array.Fun1.Smart.map lift 1 l' in @@ -1208,12 +1216,11 @@ let plain_instance sigma s c = with Not_found -> mkApp (f,l')) | _ -> mkApp (irec n f,l')) | Cast (m,_,_) when isMeta sigma m -> - (try lift n (Metamap.find (destMeta sigma m) s) with Not_found -> u) + (try lift n (s.sfun (destMeta sigma m)) with Not_found -> u) | _ -> map_with_binders sigma succ irec n u in - if Metamap.is_empty s then c - else irec 0 c + irec 0 c (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota] has (unfortunately) different subtle side effects: @@ -1415,23 +1422,41 @@ let is_arity env sigma c = (*************************************) (* Metas *) -let meta_value env evd mv = - let rec valrec mv = - match meta_opt_fvalue evd mv with - | Some (b,_) -> - let metas = Metamap.bind valrec b.freemetas in - instance env evd metas b.rebus - | None -> mkMeta mv +type meta_instance_subst = { + sigma : Evd.evar_map; + mutable cache : EConstr.t Metamap.t; +} + +let create_meta_instance_subst sigma = { + sigma; + cache = Metamap.empty; +} + +let eval_subst env subst = + let rec ans mv = + try Metamap.find mv subst.cache + with Not_found -> + match meta_opt_fvalue subst.sigma mv with + | None -> mkMeta mv + | Some (b, _) -> + let metas = + if Metaset.is_empty b.freemetas then None + else Some { sfun = ans } + in + let res = instance env subst.sigma metas b.rebus in + let () = subst.cache <- Metamap.add mv res subst.cache in + res in - valrec mv + { sfun = ans } -let meta_instance env sigma b = +let meta_instance env subst b = let fm = b.freemetas in if Metaset.is_empty fm then b.rebus else - let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in - instance env sigma c_sigma b.rebus + let sfun = eval_subst env subst in + instance env subst.sigma (Some sfun) b.rebus let nf_meta env sigma c = + let sigma = create_meta_instance_subst sigma in let cl = mk_freelisted c in meta_instance env sigma { cl with rebus = cl.rebus } diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 04dfc5ffe6..ae93eb48b4 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -69,10 +69,9 @@ module Stack : sig val empty : 'a t val is_empty : 'a t -> bool - val append_app : 'a array -> 'a t -> 'a t - val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) + [@@ocaml.deprecated "Use decomp_rev"] val compare_shape : 'a t -> 'a t -> bool @@ -84,23 +83,51 @@ module Stack : sig val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> constr t -> constr t -> 'a val map : ('a -> 'a) -> 'a t -> 'a t + + (** [append_app args sk] pushes array of arguments [args] on [sk] *) + val append_app : 'a array -> 'a t -> 'a t + + (** [append_app_list args sk] pushes list of arguments [args] on [sk] *) val append_app_list : 'a list -> 'a t -> 'a t - (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App *) + (** if [strip_app sk] = [(sk1,sk2)], then [sk = sk1 @ sk2] with + [sk1] purely applicative and [sk2] does not start with an argument *) val strip_app : 'a t -> 'a t * 'a t - (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) + (** @return (the nth first elements, the (n+1)th element, the remaining stack) + if there enough of those *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option + (** [decomp sk] extracts the first argument of [sk] is there is some *) + val decomp : 'a t -> ('a * 'a t) option + + (** [decomp sk] extracts the first argument of reversed stack [sk] is there is some *) + val decomp_rev : 'a t -> ('a * 'a t) option + + (** [not_purely_applicative sk] *) val not_purely_applicative : 'a t -> bool + + (** [list_of_app_stack sk] either returns [Some sk] turned into a list of + arguments if [sk] is purely applicative and [None] otherwise *) val list_of_app_stack : constr t -> constr list option + (** [assign sk n a] changes the [n]th argument of [sk] with [a], counting from 0 + @raise an anomaly if there is less that [n] arguments available *) val assign : 'a t -> int -> 'a -> 'a t + + (** [args_size sk] returns the number of arguments available at the + head of [sk] *) val args_size : 'a t -> int + + (** [tail n sk] drops the [n] first arguments of [sk] + @raise [Invalid_argument] if there are not enough arguments *) val tail : int -> 'a t -> 'a t + + (** [nth sk n] returns the [n]-th argument of [sk], counting from 0 + @raise [Not_found] if there is no [n]th argument *) val nth : 'a t -> int -> 'a + (** [zip sigma t sk] *) val zip : evar_map -> constr * constr t -> constr end @@ -258,7 +285,11 @@ val whd_betaiota_deltazeta_for_iota_state : TransparentState.t -> state_reduction_function (** {6 Meta-related reduction functions } *) -val meta_instance : env -> evar_map -> constr freelisted -> constr +type meta_instance_subst + +val create_meta_instance_subst : Evd.evar_map -> meta_instance_subst + +val meta_instance : env -> meta_instance_subst -> constr freelisted -> constr val nf_meta : env -> evar_map -> constr -> constr exception AnomalyInConversion of exn diff --git a/pretyping/typing.ml b/pretyping/typing.ml index aeb3873de7..e3e5244a8c 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -33,7 +33,7 @@ let meta_type env evd mv = let ty = try Evd.meta_ftype evd mv with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in - meta_instance env evd ty + meta_instance env (create_meta_instance_subst evd) ty let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 387f0f6f5f..00ac5a0624 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -37,15 +37,28 @@ type clausenv = { env : env; evd : evar_map; templval : constr freelisted; - templtyp : constr freelisted } + templtyp : constr freelisted; + cache : Reductionops.meta_instance_subst; +} + +let mk_clausenv env evd templval templtyp = { + env; evd; templval; templtyp; cache = create_meta_instance_subst evd; +} + +let update_clenv_evd clenv evd = + mk_clausenv clenv.env evd clenv.templval clenv.templtyp let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_term clenv c = meta_instance clenv.env clenv.evd c -let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv -let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval -let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp +let clenv_term clenv c = meta_instance clenv.env clenv.cache c +let clenv_meta_type clenv mv = + let ty = + try Evd.meta_ftype clenv.evd mv + with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in + meta_instance clenv.env clenv.cache ty +let clenv_value clenv = meta_instance clenv.env clenv.cache clenv.templval +let clenv_type clenv = meta_instance clenv.env clenv.cache clenv.templtyp let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t @@ -67,7 +80,8 @@ let clenv_push_prod cl = { templval = mk_freelisted def; templtyp = mk_freelisted concl; evd = e'; - env = cl.env } + env = cl.env; + cache = create_meta_instance_subst e' } | _ -> raise NotExtensibleClause in clrec typ @@ -109,7 +123,8 @@ let mk_clenv_from_env env sigma n (c,cty) = { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; evd = evd; - env = env } + env = env; + cache = create_meta_instance_subst evd } let mk_clenv_from_n gls n (c,cty) = let env = Proofview.Goal.env gls in @@ -158,7 +173,7 @@ let clenv_assign mv rhs clenv = clenv else let st = (Conv,TypeNotProcessed) in - {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} + update_clenv_evd clenv (meta_assign mv (rhs_fls.rebus,st) clenv.evd) with Not_found -> user_err Pp.(str "clenv_assign: undefined meta") @@ -202,19 +217,19 @@ let clenv_assign mv rhs clenv = In any case, we respect the order given in A. *) -let clenv_metas_in_type_of_meta env evd mv = - (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas +let clenv_metas_in_type_of_meta clenv mv = + (mk_freelisted (meta_instance clenv.env clenv.cache (meta_ftype clenv.evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right - (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.env clenv.evd mv)) + (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv mv)) mvs Metaset.empty let dependent_closure clenv mvs = let rec aux mvs acc = Metaset.fold (fun mv deps -> - let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.env clenv.evd mv in + let metas_of_meta_type = clenv_metas_in_type_of_meta clenv mv in aux metas_of_meta_type (Metaset.union deps metas_of_meta_type)) mvs acc in aux mvs mvs @@ -297,11 +312,10 @@ let meta_reducible_instance env evd b = else irec b.rebus let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv = - { clenv with - evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 } + update_clenv_evd clenv (w_unify ~flags clenv.env clenv.evd cv_pb t1 t2) let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = - { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } + update_clenv_evd clenv (w_unify_meta_types ~flags:flags clenv.env clenv.evd) let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd clenv.templtyp.rebus))) then @@ -414,11 +428,13 @@ let fchain_flags () = let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv = (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) + let evd = meta_merge ?with_univs nextclenv.evd clenv.evd in let clenv' = { templval = clenv.templval; templtyp = clenv.templtyp; - evd = meta_merge ?with_univs nextclenv.evd clenv.evd; - env = nextclenv.env } in + evd; + env = nextclenv.env; + cache = create_meta_instance_subst evd } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = clenv_unify ~flags CUMUL @@ -538,7 +554,7 @@ let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in - { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } + update_clenv_evd clenv' (meta_assign k (c,(Conv,status)) clenv'.evd) let clenv_match_args bl clenv = if List.is_empty bl then @@ -640,7 +656,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = Typeclasses.make_unresolvables (fun x -> true) evd' else clenv.evd in - let clenv = { clenv with evd = evd' } in + let clenv = update_clenv_evd clenv evd' in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS (Evd.clear_metas evd')) (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index a72c8c5e1f..6e472da452 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -22,14 +22,18 @@ open Tactypes (** {6 The Type of Constructions clausale environments.} *) -type clausenv = { +type clausenv = private { env : env; (** the typing context *) evd : evar_map; (** the mapping from metavar and evar numbers to their types and values *) templval : constr freelisted; (** the template which we are trying to fill out *) - templtyp : constr freelisted (** its type *)} + templtyp : constr freelisted; (** its type *) + cache : Reductionops.meta_instance_subst; (* Reductionops.create_meta_instance_subst evd) *) +} +val mk_clausenv : env -> evar_map -> constr freelisted -> types freelisted -> clausenv +val update_clenv_evd : clausenv -> evar_map -> clausenv (** subject of clenv (instantiated) *) val clenv_value : clausenv -> constr diff --git a/tactics/equality.ml b/tactics/equality.ml index fcdd23a9c1..633b9da053 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -154,7 +154,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenv.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} + let clenv = Clenv.update_clenv_evd eqclause evd' in + Clenv.clenv_pose_dependent_evars ~with_evars:true clenv in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = diff --git a/tactics/hints.ml b/tactics/hints.ml index 6fab111e6f..ace51c40d4 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -340,10 +340,8 @@ let instantiate_hint env sigma p = let mk_clenv (c, cty, ctx) = let sigma = merge_context_set_opt sigma ctx in let cl = mk_clenv_from_env env sigma None (c,cty) in - let cl = {cl with templval = - { cl.templval with rebus = strip_params env sigma cl.templval.rebus }; - env = empty_env} - in + let templval = { cl.templval with rebus = strip_params env sigma cl.templval.rebus } in + let cl = mk_clausenv empty_env cl.evd templval cl.templtyp in { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; } in let code = match p.code.obj with @@ -1649,14 +1647,17 @@ let connect_hint_clenv h gl = let emap c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in (* Only metas are mentioning the old universes. *) - { - templval = Evd.map_fl emap clenv.templval; - templtyp = Evd.map_fl emap clenv.templtyp; - evd = Evd.map_metas emap evd; - env = Proofview.Goal.env gl; - } + Clenv.mk_clausenv + (Proofview.Goal.env gl) + (Evd.map_metas emap evd) + (Evd.map_fl emap clenv.templval) + (Evd.map_fl emap clenv.templtyp) | None -> - { clenv with evd = evd ; env = Proofview.Goal.env gl } + Clenv.mk_clausenv + (Proofview.Goal.env gl) + evd + clenv.templval + clenv.templtyp let fresh_hint env sigma h = let { hint_term = c; hint_uctx = ctx } = h in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 130e0e97c2..39c5c9562f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1301,20 +1301,18 @@ let do_replace id = function let clenv_refine_in ?err with_evars targetid id sigma0 clenv tac = let clenv = Clenv.clenv_pose_dependent_evars ~with_evars clenv in - let clenv = - { clenv with evd = Typeclasses.resolve_typeclasses - ~fail:(not with_evars) clenv.env clenv.evd } - in + let evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd in + let clenv = Clenv.update_clenv_evd clenv evd in let new_hyp_typ = clenv_type clenv in if not with_evars then check_unresolved_evars_of_metas sigma0 clenv; - if not with_evars && occur_meta clenv.evd new_hyp_typ then + if not with_evars && occur_meta evd new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in let exact_tac = Logic.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf) in let naming = NamingMustBe (CAst.make targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) + (Proofview.Unsafe.tclEVARS (clear_metas evd)) (Tacticals.New.tclTHENLAST (assert_after_then_gen ?err with_clear naming new_hyp_typ tac) exact_tac) diff --git a/test-suite/success/change_case.v b/test-suite/success/change_case.v new file mode 100644 index 0000000000..490e4f4b6c --- /dev/null +++ b/test-suite/success/change_case.v @@ -0,0 +1,20 @@ +Inductive box (A : Type) := Box : A -> box A. + +Axiom PRED : unit -> Prop. +Axiom FUN : forall (u : unit), box (PRED u). + +Axiom U : unit. +Definition V := U. + +Goal match FUN U with Box _ _ => True end. +Proof. +repeat match goal with +| [ |- context G[ U ] ] => + let e := context G [ V ] in + change e +end. +set (Z := V). +clearbody Z. (* This fails if change misses the case parameters *) +destruct (FUN Z). +constructor. +Qed. diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index f002ee427c..dd10c758a5 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -46,7 +46,7 @@ Section Bool_eq_dec. Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}. Proof. - intros. + intros x y. exists (beq x y). constructor. Defined. diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index ef78121d63..5eb2a99739 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -18,7 +18,7 @@ Theorem ifdec_left : forall (A B:Prop) (C:Set) (H:{A} + {B}), ~ B -> forall x y:C, ifdec H x y = x. Proof. - intros; case H; auto. + intros A B C H **; case H; auto. intro; absurd B; trivial. Qed. @@ -26,7 +26,7 @@ Theorem ifdec_right : forall (A B:Prop) (C:Set) (H:{A} + {B}), ~ A -> forall x y:C, ifdec H x y = y. Proof. - intros; case H; auto. + intros A B C H **; case H; auto. intro; absurd A; trivial. Qed. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 7e9087c377..8366e8257e 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -29,13 +29,13 @@ case diff_true_false; trivial with bool. Qed. Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A. -intros. +intros A B H. inversion H. assumption. Qed. Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B. -intros. +intros A B H. inversion H. assumption. Qed. @@ -45,7 +45,7 @@ destruct 1; auto with bool. Qed. Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. -destruct b; intro H. +intros A B b; destruct b; intro H. - left; inversion H; auto with bool. - right; inversion H; auto with bool. Qed. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index aff5008410..418fc88489 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -19,26 +19,26 @@ Definition zerob (n:nat) : bool := | S _ => false end. -Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true. +Lemma zerob_true_intro (n : nat) : n = 0 -> zerob n = true. Proof. destruct n; [ trivial with bool | inversion 1 ]. Qed. #[global] Hint Resolve zerob_true_intro: bool. -Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0. +Lemma zerob_true_elim (n : nat) : zerob n = true -> n = 0. Proof. destruct n; [ trivial with bool | inversion 1 ]. Qed. -Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false. +Lemma zerob_false_intro (n : nat) : n <> 0 -> zerob n = false. Proof. destruct n; [ destruct 1; auto with bool | trivial with bool ]. Qed. #[global] Hint Resolve zerob_false_intro: bool. -Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. +Lemma zerob_false_elim (n : nat) : zerob n = false -> n <> 0. Proof. destruct n; [ inversion 1 | auto with bool ]. Qed. diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index f23cf158ac..82a76e8afd 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. now transitivity y. Qed. -Arguments equiv_symmetric {A R} sa x y. -Arguments equiv_transitive {A R} sa x y z. +Arguments equiv_symmetric {A R} sa x y : rename. +Arguments equiv_transitive {A R} sa x y z : rename. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 9ff18ebe2c..d6a0ae5411 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -567,9 +567,7 @@ Section Normalize. Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m. Proof. - red in H, H0. red in H. - apply (snd (H _ _)). - assumption. + apply (_ : Normalizes R0 R1). assumption. Qed. Lemma flip_atom R : Normalizes R (flip (flip R)). diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index c489d82d0b..561822ef0c 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -352,14 +352,12 @@ Section Binary. Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R. Proof with auto. reduce_goal. - apply H. firstorder. + firstorder. Qed. Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). Proof. - unfold flip; constructor; unfold flip. - - intros X. apply H. apply symmetry. apply X. - - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. + firstorder. Qed. End Binary. diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v index 7169aa673d..cd6765bab9 100644 --- a/theories/Classes/DecidableClass.v +++ b/theories/Classes/DecidableClass.v @@ -46,7 +46,7 @@ Qed. (** The generic function that should be used to program, together with some useful tactics. *) -Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). +Definition decide P {H : Decidable P} := @Decidable_witness _ H. Ltac _decide_ P H := let b := fresh "b" in diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index d96bd72561..4d9069b4d0 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. now transitivity y. Qed. -Arguments equiv_symmetric {A R} sa x y. -Arguments equiv_transitive {A R} sa x y z. +Arguments equiv_symmetric {A R} sa x y : rename. +Arguments equiv_transitive {A R} sa x y z : rename. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index e9d434b488..ae1d978bfb 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -16,7 +16,7 @@ Lemma equal_f : forall {A B : Type} {f g : A -> B}, f = g -> forall x, f x = g x. Proof. - intros. + intros A B f g H x. rewrite H. auto. Qed. @@ -118,7 +118,7 @@ Definition f_equal__functional_extensionality_dep_good {A B f g} H a : f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H) = H a. Proof. - apply forall_eq_rect with (H := H); clear H g. + apply (fun P k => forall_eq_rect _ P k _ H); clear H g. change (eq_refl (f a)) with (f_equal (fun h => h a) (eq_refl f)). apply f_equal, functional_extensionality_dep_good_refl. Defined. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 7ee3a99d60..21eed3a696 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -39,8 +39,8 @@ Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. Register JMeq_hom as core.JMeq.hom. Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. -Proof. -intros; destruct H; trivial. +Proof. +intros A B x y H; destruct H; trivial. Qed. #[global] @@ -150,7 +150,7 @@ Lemma JMeq_eq_dep : forall U (P:U->Type) p q (x:P p) (y:P q), p = q -> JMeq x y -> eq_dep U P p x q y. Proof. -intros. +intros U P p q x y H H0. destruct H. apply JMeq_eq in H0 as ->. reflexivity. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index c469a49903..f324bbf52b 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -226,7 +226,7 @@ Proof. apply Z.lt_le_trans with (1:= H5); auto with zarith. apply Zpower_le_monotone; auto with zarith. rewrite Zplus_mod; auto with zarith. - rewrite -> Zmod_small with (a := t); auto with zarith. + rewrite -> (Zmod_small t); auto with zarith. apply Zmod_small; auto with zarith. split; auto with zarith. assert (0 <= 2 ^a * r); auto with zarith. @@ -489,15 +489,15 @@ Definition cast i j := Lemma cast_refl : forall i, cast i i = Some (fun P H => H). Proof. - unfold cast;intros. + unfold cast;intros i. generalize (eqb_correct i i). - rewrite eqb_refl;intros. + rewrite eqb_refl;intros e. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. Lemma cast_diff : forall i j, i =? j = false -> cast i j = None. Proof. - intros;unfold cast;intros; generalize (eqb_correct i j). + intros i j H;unfold cast;intros; generalize (eqb_correct i j). rewrite H;trivial. Qed. @@ -509,15 +509,15 @@ Definition eqo i j := Lemma eqo_refl : forall i, eqo i i = Some (eq_refl i). Proof. - unfold eqo;intros. + unfold eqo;intros i. generalize (eqb_correct i i). - rewrite eqb_refl;intros. + rewrite eqb_refl;intros e. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None. Proof. - unfold eqo;intros; generalize (eqb_correct i j). + unfold eqo;intros i j H; generalize (eqb_correct i j). rewrite H;trivial. Qed. @@ -651,7 +651,7 @@ Proof. apply Zgcdn_is_gcd. unfold Zgcd_bound. generalize (to_Z_bounded b). - destruct φ b. + destruct φ b as [|p|p]. unfold size; auto with zarith. intros (_,H). cut (Psize p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto]. @@ -727,7 +727,7 @@ Proof. replace ((φ m + φ n) mod wB)%Z with ((((φ m + φ n) - wB) + wB) mod wB)%Z. rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. rewrite !Zmod_small; auto with zarith. - apply f_equal2 with (f := Zmod); auto with zarith. + apply (f_equal2 Zmod); auto with zarith. case_eq (n <=? m + n)%int63; auto. rewrite leb_spec, H1; auto with zarith. assert (H1: (φ (m + n) = φ m + φ n)%Z). @@ -805,7 +805,7 @@ Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. Proof. apply to_Z_inj; rewrite -> !lsl_spec, !add_spec, Zmult_mod_idemp_l. rewrite -> !lsl_spec, <-Zplus_mod. - apply f_equal2 with (f := Zmod); auto with zarith. + apply (f_equal2 Zmod); auto with zarith. Qed. Lemma lsr_M_r x i (H: (digits <=? i = true)%int63) : x >> i = 0%int63. @@ -973,14 +973,14 @@ Proof. case H2; intros _ H3; case (Zle_or_lt φ i φ j); intros F2. 2: generalize (H3 F2); discriminate. clear H2 H3. - apply f_equal with (f := negb). - apply f_equal with (f := is_zero). + apply (f_equal negb). + apply (f_equal is_zero). apply to_Z_inj. rewrite -> !lsl_spec, !lsr_spec, !lsl_spec. pattern wB at 2 3; replace wB with (2^(1+ φ (digits - 1))); auto. rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith. rewrite !Zmult_mod_distr_r. - apply f_equal2 with (f := Zmult); auto. + apply (f_equal2 Zmult); auto. replace wB with (2^ d); auto with zarith. replace d with ((d - φ i) + φ i)%Z by ring. case (to_Z_bounded i); intros H1i H2i. @@ -1078,8 +1078,8 @@ Proof. 2: generalize (Hn 0%int63); do 2 case bit; auto; intros [ ]; auto. rewrite lsl_add_distr. rewrite (bit_split x) at 1; rewrite (bit_split y) at 1. - rewrite <-!add_assoc; apply f_equal2 with (f := add); auto. - rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add); auto. + rewrite <-!add_assoc; apply (f_equal2 add); auto. + rewrite add_comm, <-!add_assoc; apply (f_equal2 add); auto. rewrite add_comm; auto. intros Heq. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. @@ -1360,7 +1360,7 @@ Lemma sqrt2_step_def rec ih il j: else j else j. Proof. - unfold sqrt2_step; case diveucl_21; intros;simpl. + unfold sqrt2_step; case diveucl_21; intros i j';simpl. case (j +c i);trivial. Qed. @@ -1390,7 +1390,7 @@ Proof. assert (W1:= to_Z_bounded a1). assert (W2:= to_Z_bounded a2). assert (Wb:= to_Z_bounded b). - assert (φ b>0) by (auto with zarith). + assert (φ b>0) as H by (auto with zarith). generalize (Z_div_mod (φ a1*wB+φ a2) φ b H). revert W. destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl (φ a1*wB+φ a2) φ b). diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index d1be8812e9..69873d0321 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -43,7 +43,7 @@ Section Well_founded. forall (x:A) (r:Acc R x), F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. Proof. - destruct r using Acc_inv_dep; auto. + intros x r; destruct r using Acc_inv_dep; auto. Qed. Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s. @@ -95,12 +95,12 @@ Section Measure_well_founded. Proof with auto. unfold well_founded. cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). - + intros. + + intros H a. apply (H (m a))... + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). - intros. + intros ? H ? H0. apply Acc_intro. - intros. + intros y H1. unfold MR in H1. rewrite H0 in H1. apply (H (m y))... @@ -174,7 +174,7 @@ Section Fix_rects. revert a'. pattern x, (Fix_F_sub A R P f x a). apply Fix_F_sub_rect. - intros. + intros ? H **. rewrite F_unfold. apply equiv_lowers. intros. @@ -197,11 +197,11 @@ Section Fix_rects. : forall x, Q _ (Fix_sub A R Rwf P f x). Proof with auto. unfold Fix_sub. - intros. + intros x. apply Fix_F_sub_rect. - intros. - assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))... - set (inv x0 X0 a). clearbody q. + intros x0 H a. + assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))) as X0... + set (q := inv x0 X0 a). clearbody q. rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... @@ -242,9 +242,9 @@ Module WfExtensionality. Fix_sub A R Rwf P F_sub x = F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)). Proof. - intros ; apply Fix_eq ; auto. - intros. - assert(f = g). + intros A R Rwf P F_sub x; apply Fix_eq ; auto. + intros ? f g H. + assert(f = g) as H0. - extensionality y ; apply H. - rewrite H0 ; auto. Qed. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index b008c6c2aa..4e596a165c 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -637,13 +637,13 @@ Qed. Lemma Qmult_1_l : forall n, 1*n == n. Proof. - intro; red; simpl; destruct (Qnum n); auto. + intro n; red; simpl; destruct (Qnum n); auto. Qed. Theorem Qmult_1_r : forall n, n*1==n. Proof. - intro; red; simpl. - rewrite Z.mul_1_r with (n := Qnum n). + intro n; red; simpl. + rewrite (Z.mul_1_r (Qnum n)). rewrite Pos.mul_comm; simpl; trivial. Qed. @@ -709,7 +709,7 @@ Qed. Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1. Proof. intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl; - intros; simpl_mult; try ring. + intros H **; simpl_mult; try ring. elim H; auto. Qed. @@ -722,7 +722,7 @@ Qed. Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x. Proof. - intros; unfold Qdiv. + intros x y H; unfold Qdiv. rewrite <- (Qmult_assoc x y (Qinv y)). rewrite (Qmult_inv_r y H). apply Qmult_1_r. @@ -730,7 +730,7 @@ Qed. Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x. Proof. - intros; unfold Qdiv. + intros x y ?; unfold Qdiv. rewrite (Qmult_assoc y x (Qinv y)). rewrite (Qmult_comm y x). fold (Qdiv (Qmult x y) y). @@ -845,7 +845,7 @@ Qed. Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z. Proof. - intros. + intros x y z ? ?. apply Qle_lt_trans with y; auto. apply Qlt_le_weak; auto. Qed. @@ -877,19 +877,19 @@ Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}. Proof. - unfold Qlt, Qle, Qeq; intros. + unfold Qlt, Qle, Qeq; intros x y. exact (Z_dec' (Qnum x * QDen y) (Qnum y * QDen x)). Defined. Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}. Proof. - unfold Qlt, Qle; intros. + unfold Qlt, Qle; intros x y. exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)). Defined. Lemma Qarchimedean : forall q : Q, { p : positive | q < Z.pos p # 1 }. Proof. - intros. destruct q as [a b]. destruct a. + intros q. destruct q as [a b]. destruct a as [|p|p]. - exists xH. reflexivity. - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))). simpl. rewrite Pos.mul_1_r. @@ -1169,12 +1169,12 @@ Qed. Lemma Qinv_lt_contravar : forall a b : Q, 0 < a -> 0 < b -> (a < b <-> /b < /a). Proof. - intros. split. - - intro. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0. + intros a b H H0. split. + - intro H1. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0. rewrite <- (Qmult_inv_r a). rewrite Qmult_comm. apply Qmult_lt_l. apply Qinv_lt_0_compat. apply H. apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). - - intro. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). + - intro H1. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). apply Qlt_shift_div_l. apply Qinv_lt_0_compat. apply H0. rewrite <- (Qmult_inv_r a). apply Qmult_lt_l. apply H. apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). @@ -1190,7 +1190,7 @@ Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive. Proof. intros x x' Hx y y' Hy. rewrite <-Hy; clear y' Hy. unfold Qpower_positive. -induction y; simpl; +induction y as [y IHy|y IHy|]; simpl; try rewrite IHy; try rewrite Hx; reflexivity. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 533c675415..e94ae1e789 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -129,19 +129,19 @@ Qed. Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp. Proof. - intros; unfold Qplus'. + intros ? ? H ? ? H0; unfold Qplus'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp. Proof. - intros; unfold Qmult'. + intros ? ? H ? ? H0; unfold Qmult'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp. Proof. - intros; unfold Qminus'. + intros ? ? H ? ? H0; unfold Qminus'. rewrite H, H0; auto with qarith. Qed. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 9a1bbca99f..c11077607e 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -58,9 +58,9 @@ Open Scope Z_scope. Lemma Zgcdn_pos : forall n a b, 0 <= Zgcdn n a b. Proof. - induction n. + intros n; induction n. simpl; auto with zarith. - destruct a; simpl; intros; auto with zarith; auto. + intros a; destruct a; simpl; intros; auto with zarith; auto. Qed. Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b. @@ -75,9 +75,9 @@ Open Scope Z_scope. Lemma Zgcdn_linear_bound : forall n a b, Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b). Proof. - induction n. + intros n; induction n as [|n IHn]. intros; lia. - destruct a; intros; simpl; + intros a; destruct a as [|p|p]; intros b H; simpl; [ generalize (Zis_gcd_0_abs b); intuition | | ]; unfold Z.modulo; generalize (Z_div_mod b (Zpos p) (eq_refl Gt)); @@ -106,7 +106,7 @@ Open Scope Z_scope. Lemma fibonacci_pos : forall n, 0 <= fibonacci n. Proof. enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto. - induction N. intros; lia. + intros N; induction N as [|N IHN]. intros; lia. intros [ | [ | n ] ]. 1-2: simpl; lia. intros. change (0 <= fibonacci (S n) + fibonacci n). @@ -116,11 +116,11 @@ Open Scope Z_scope. Lemma fibonacci_incr : forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m. Proof. - induction 1. + induction 1 as [|m H IH]. auto with zarith. apply Z.le_trans with (fibonacci m); auto. clear. - destruct m. + destruct m as [|m]. simpl; auto with zarith. change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). generalize (fibonacci_pos m); lia. @@ -137,10 +137,10 @@ Open Scope Z_scope. fibonacci (S n) <= a /\ fibonacci (S (S n)) <= b. Proof. - induction n. + intros n; induction n as [|n IHn]. intros [|a|a]; intros; simpl; lia. intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ]. - remember (S n) as m. + remember (S n) as m eqn:Heqm. rewrite Heqm at 2. simpl Zgcdn. unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl). destruct (Z.div_eucl b (Zpos a)) as (q,r). @@ -171,19 +171,19 @@ Open Scope Z_scope. 0 < a < b -> a < fibonacci (S n) -> Zis_gcd a b (Zgcdn n a b). Proof. - destruct a. 1,3 : intros; lia. + intros n a; destruct a as [|p|p]. 1,3 : intros; lia. cut (forall k n b, k = (S (Pos.to_nat p) - n)%nat -> 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). destruct 2; eauto. - clear n; induction k. + clear n; intros k; induction k as [|k IHk]. intros. apply Zgcdn_linear_bound. lia. - intros. - generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. - assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). + intros n b H H0 H1. + generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros H2. + assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)) as H3. apply IHk; auto. lia. replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. @@ -197,13 +197,13 @@ Open Scope Z_scope. Lemma Zgcd_bound_fibonacci : forall a, 0 < a -> a < fibonacci (Zgcd_bound a). Proof. - destruct a; [lia| | intro H; discriminate]. + intros a; destruct a as [|p|p]; [lia| | intro H; discriminate]. intros _. - induction p; [ | | compute; auto ]; + induction p as [p IHp|p IHp|]; [ | | compute; auto ]; simpl Zgcd_bound in *; rewrite plus_comm; simpl plus; set (n:= (Pos.size_nat p+Pos.size_nat p)%nat) in *; simpl; - assert (n <> O) by (unfold n; destruct p; simpl; auto). + assert (n <> O) as H by (unfold n; destruct p; simpl; auto). destruct n as [ |m]; [elim H; auto| ]. generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia. @@ -229,11 +229,11 @@ Open Scope Z_scope. Lemma Zgcdn_is_gcd_pos n a b : (Zgcd_bound (Zpos a) <= n)%nat -> Zis_gcd (Zpos a) b (Zgcdn n (Zpos a) b). Proof. - intros. + intros H. generalize (Zgcd_bound_fibonacci (Zpos a)). simpl Zgcd_bound in *. - remember (Pos.size_nat a+Pos.size_nat a)%nat as m. - assert (1 < m)%nat. + remember (Pos.size_nat a+Pos.size_nat a)%nat as m eqn:Heqm. + assert (1 < m)%nat as H0. { rewrite Heqm; destruct a; simpl; rewrite 1?plus_comm; auto with arith. } destruct m as [ |m]; [inversion H0; auto| ]. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index b69af424b1..bc3f5706c9 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -83,10 +83,10 @@ Proof. intros. apply Z.lt_le_incl. now apply Z.pow_gt_lin_r. Qed. Lemma Zpower2_Psize n p : Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat. Proof. - revert p; induction n. - destruct p; now split. + revert p; induction n as [|n IHn]. + intros p; destruct p; now split. assert (Hn := Nat2Z.is_nonneg n). - destruct p; simpl Pos.size_nat. + intros p; destruct p as [p|p|]; simpl Pos.size_nat. - specialize IHn with p. rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. - specialize IHn with p. @@ -138,7 +138,7 @@ Definition Zpow_mod a m n := Theorem Zpow_mod_pos_correct a m n : n <> 0 -> Zpow_mod_pos a m n = (Z.pow_pos a m) mod n. Proof. - intros Hn. induction m. + intros Hn. induction m as [m IHm|m IHm|]. - rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.add_1_r, <- Pos.add_diag. rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r. rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial. @@ -193,7 +193,7 @@ Proof. assert (p<=1) by (apply Z.divide_pos_le; auto with zarith). lia. - intros n Hn Rec. - rewrite Z.pow_succ_r by trivial. intros. + rewrite Z.pow_succ_r by trivial. intros H. assert (2<=p) by (apply prime_ge_2; auto). assert (2<=q) by (apply prime_ge_2; auto). destruct prime_mult with (2 := H); auto. @@ -229,7 +229,7 @@ Proof. (* x = 1 *) exists 0; rewrite Z.pow_0_r; auto. (* x = 0 *) - exists n; destruct H; rewrite Z.mul_0_r in H; auto. + exists n; destruct H as [? H]; rewrite Z.mul_0_r in H; auto. Qed. (** * Z.square: a direct definition of [z^2] *) diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 6f464d89bb..6b01d798e4 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp : forall (n m:nat) (z:Z), Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m. Proof. - induction n. + intros n; induction n as [|n IHn]. - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l. - intros. simpl. now rewrite IHn, Z.mul_assoc. Qed. @@ -135,7 +135,7 @@ Section Powers_of_2. Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n). Proof. - induction n. + induction n as [|n IHn]. - trivial. - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg. Qed. @@ -164,7 +164,7 @@ Section Powers_of_2. Theorem shift_nat_correct n x : Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x. Proof. - induction n. + induction n as [|n IHn]. - trivial. - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn. Qed. @@ -295,7 +295,7 @@ Section power_div_with_rest. rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. repeat split; auto. rewrite !Z.mul_1_l, H, Z.add_assoc. - apply f_equal2 with (f := Z.add); auto. + apply (f_equal2 Z.add); auto. rewrite <- Z.sub_sub_distr, <- !Z.add_diag, Z.add_simpl_r. now rewrite Z.mul_1_l. - rewrite Pos2Z.neg_xO in H. @@ -303,7 +303,7 @@ Section power_div_with_rest. repeat split; auto. - repeat split; auto. rewrite H, (Z.mul_opp_l 1), Z.mul_1_l, Z.add_assoc. - apply f_equal2 with (f := Z.add); auto. + apply (f_equal2 Z.add); auto. rewrite Z.add_comm, <- Z.add_diag. rewrite Z.mul_add_distr_l. replace (-1 * d) with (-d). diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index 515372466a..e4129f8382 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -1371,13 +1371,13 @@ Section S. destruct pol;auto. generalize (is_cnf_tt_inv (xcnf (negb true) f1)). destruct (is_cnf_tt (xcnf (negb true) f1)). - + intros. + + intros H. rewrite H by auto. reflexivity. + generalize (is_cnf_ff_inv (xcnf (negb true) f1)). destruct (is_cnf_ff (xcnf (negb true) f1)). - * intros. + * intros H. rewrite H by auto. unfold or_cnf_opt. simpl. diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index 1616b5a2a4..a4b631fc13 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -38,7 +38,7 @@ Ltac inv H := inversion H ; try subst ; clear H. Lemma eq_le_iff : forall x, 0 = x <-> (0 <= x /\ x <= 0). Proof. intros. - split ; intros. + split ; intros H. - subst. compute. intuition congruence. - destruct H. @@ -48,7 +48,7 @@ Qed. Lemma lt_le_iff : forall x, 0 < x <-> 0 <= x - 1. Proof. - split ; intros. + split ; intros H. - apply Zlt_succ_le. ring_simplify. auto. @@ -70,12 +70,13 @@ Lemma le_neg : forall x, Proof. intro. rewrite lt_le_iff. - split ; intros. + split ; intros H. - apply Znot_le_gt in H. apply Zgt_le_succ in H. rewrite le_0_iff in H. ring_simplify in H; auto. - - assert (C := (Z.add_le_mono _ _ _ _ H H0)). + - intro H0. + assert (C := (Z.add_le_mono _ _ _ _ H H0)). ring_simplify in C. compute in C. apply C ; reflexivity. @@ -84,7 +85,7 @@ Qed. Lemma eq_cnf : forall x, (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0. Proof. - intros. + intros x. rewrite Z.eq_sym_iff. rewrite eq_le_iff. rewrite (le_0_iff x 0). @@ -108,7 +109,7 @@ Proof. auto using Z.le_antisymm. eauto using Z.le_trans. apply Z.le_neq. - destruct (Z.lt_trichotomy n m) ; intuition. + apply Z.lt_trichotomy. apply Z.add_le_mono_l; assumption. apply Z.mul_pos_pos ; auto. discriminate. @@ -160,18 +161,18 @@ Fixpoint Zeval_const (e: PExpr Z) : option Z := Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n. Proof. - destruct n. + intros r n; destruct n as [|p]. reflexivity. simpl. unfold Z.pow_pos. replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring. generalize 1. - induction p; simpl ; intros ; repeat rewrite IHp ; ring. + induction p as [p IHp|p IHp|]; simpl ; intros ; repeat rewrite IHp ; ring. Qed. Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e. Proof. - induction e ; simpl ; try congruence. + intros env e; induction e ; simpl ; try congruence. reflexivity. rewrite ZNpower. congruence. Qed. @@ -201,7 +202,7 @@ Lemma pop2_bop2 : forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2. Proof. unfold is_true. - destruct op ; simpl; intros. + intro op; destruct op ; simpl; intros q1 q2. - apply Z.eqb_eq. - rewrite <- Z.eqb_eq. rewrite negb_true_iff. @@ -220,7 +221,7 @@ Definition Zeval_op2 (k: Tauto.kind) : Op2 -> Z -> Z -> Tauto.rtyp k:= Lemma Zeval_op2_hold : forall k op q1 q2, Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2. Proof. - destruct k. + intro k; destruct k. simpl ; tauto. simpl. apply pop2_bop2. Qed. @@ -235,18 +236,18 @@ Definition Zeval_formula' := Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f. Proof. - destruct k ; simpl. + intros env k; destruct k ; simpl. - tauto. - - destruct f ; simpl. - rewrite <- Zeval_op2_hold with (k:=Tauto.isBool). + - intros f; destruct f ; simpl. + rewrite <- (Zeval_op2_hold Tauto.isBool). simpl. tauto. Qed. Lemma Zeval_formula_compat' : forall env f, Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f. Proof. - intros. + intros env f. unfold Zeval_formula. - destruct f. + destruct f as [Flhs Fop Frhs]. repeat rewrite Zeval_expr_compat. unfold Zeval_formula' ; simpl. unfold eval_expr. @@ -343,7 +344,7 @@ Lemma Zunsat_sound : forall f, Zunsat f = true -> forall env, eval_nformula env f -> False. Proof. unfold Zunsat. - intros. + intros f H env ?. destruct f. eapply check_inconsistent_sound with (1 := Zsor) (2 := ZSORaddon) in H; eauto. Qed. @@ -365,7 +366,7 @@ Lemma xnnormalise_correct : forall env f, eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f. Proof. - intros. + intros env f. rewrite Zeval_formula_compat'. unfold xnnormalise. destruct f as [lhs o rhs]. @@ -375,18 +376,18 @@ Proof. generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env lhs); generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros. + (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros z z0. - split ; intros. - + assert (z0 + (z - z0) = z0 + 0) by congruence. + + assert (z0 + (z - z0) = z0 + 0) as H0 by congruence. rewrite Z.add_0_r in H0. rewrite <- H0. ring. + subst. ring. - - split ; repeat intro. + - split ; intros H H0. subst. apply H. ring. apply H. - assert (z0 + (z - z0) = z0 + 0) by congruence. + assert (z0 + (z - z0) = z0 + 0) as H1 by congruence. rewrite Z.add_0_r in H1. rewrite <- H1. ring. @@ -396,11 +397,11 @@ Proof. - split ; intros. + apply Zle_0_minus_le; auto. + apply Zle_minus_le_0; auto. - - split ; intros. + - split ; intros H. + apply Zlt_0_minus_lt; auto. + apply Zlt_left_lt in H. apply H. - - split ; intros. + - split ; intros H. + apply Zlt_0_minus_lt ; auto. + apply Zlt_left_lt in H. apply H. @@ -430,7 +431,7 @@ Ltac iff_ring := Lemma xnormalise_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f. Proof. - intros. + intros env f. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; generalize (eval_pol env e) as x; intro. @@ -458,11 +459,11 @@ Lemma cnf_of_list_correct : make_conj (fun x : NFormula Z => eval_nformula env x -> False) f. Proof. unfold cnf_of_list. - intros. + intros T tg f env. set (F := (fun (x : NFormula Z) (acc : list (list (NFormula Z * T))) => if Zunsat x then acc else ((x, tg) :: nil) :: acc)). set (E := ((fun x : NFormula Z => eval_nformula env x -> False))). - induction f. + induction f as [|a f IHf]. - compute. tauto. - rewrite make_conj_cons. @@ -489,10 +490,10 @@ Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t. Proof. - intros. + intros T env t tg. rewrite <- xnnormalise_correct. unfold normalise. - generalize (xnnormalise t) as f;intro. + generalize (xnnormalise t) as f;intro f. destruct (Zunsat f) eqn:U. - assert (US := Zunsat_sound _ U env). rewrite eval_cnf_ff. @@ -519,10 +520,10 @@ Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := Lemma xnegate_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f. Proof. - intros. + intros env f. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; - generalize (eval_pol env e) as x; intro. + generalize (eval_pol env e) as x; intro x. - tauto. - rewrite eq_cnf. destruct (Z.eq_decidable x 0);tauto. @@ -533,10 +534,10 @@ Qed. Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t. Proof. - intros. + intros T env t tg. rewrite <- xnnormalise_correct. unfold negate. - generalize (xnnormalise t) as f;intro. + generalize (xnnormalise t) as f;intro f. destruct (Zunsat f) eqn:U. - assert (US := Zunsat_sound _ U env). rewrite eval_cnf_tt. @@ -569,10 +570,10 @@ Require Import Znumtheory. Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b. Proof. unfold ceiling. - intros. + intros a b H. apply Zdivide_mod in H. case_eq (Z.div_eucl a b). - intros. + intros z z0 H0. change z with (fst (z,z0)). rewrite <- H0. change (fst (Z.div_eucl a b)) with (Z.div a b). @@ -642,12 +643,12 @@ Definition isZ0 (x:Z) := Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0. Proof. - destruct x ; simpl ; intuition congruence. + intros x; destruct x ; simpl ; intuition congruence. Qed. Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0. Proof. - destruct x ; simpl ; intuition congruence. + intros x; destruct x ; simpl ; intuition congruence. Qed. Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1. @@ -682,8 +683,8 @@ Inductive Zdivide_pol (x:Z): PolC Z -> Prop := Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p -> forall env, eval_pol env p = a * eval_pol env (Zdiv_pol p a). Proof. - intros until 2. - induction H0. + intros a p H H0. + induction H0 as [? ?|? ? IHZdivide_pol j|? ? ? IHZdivide_pol1 ? IHZdivide_pol2 j]. (* Pc *) simpl. intros. @@ -702,7 +703,7 @@ Qed. Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0. Proof. - induction p. 1-2: easy. + intros p; induction p as [c|p p1 IHp1|p1 IHp1 ? p3 IHp3]. 1-2: easy. simpl. case_eq (Zgcd_pol p1). case_eq (Zgcd_pol p3). @@ -715,7 +716,7 @@ Qed. Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) -> Zdivide_pol y p. Proof. - intros. + intros p x y H H0. induction H. constructor. apply Z.divide_trans with (1:= H0) ; assumption. @@ -725,7 +726,7 @@ Qed. Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p. Proof. - induction p ; constructor ; auto. + intros p; induction p as [c| |]; constructor ; auto. exists c. ring. Qed. @@ -744,19 +745,19 @@ Lemma Zdivide_pol_sub : forall p a b, Zdivide_pol a (PsubC Z.sub p b) -> Zdivide_pol (Z.gcd a b) p. Proof. - induction p. + intros p; induction p as [c|? p IHp|p ? ? ? IHp2]. simpl. - intros. inversion H0. + intros a b H H0. inversion H0. constructor. apply Zgcd_minus ; auto. - intros. + intros ? ? H H0. constructor. simpl in H0. inversion H0 ; subst; clear H0. apply IHp ; auto. - simpl. intros. + simpl. intros a b H H0. inv H0. constructor. - apply Zdivide_pol_Zdivide with (1:= H3). + apply Zdivide_pol_Zdivide with (1:= (ltac:(assumption) : Zdivide_pol a p)). destruct (Zgcd_is_gcd a b) ; assumption. apply IHp2 ; assumption. Qed. @@ -765,15 +766,15 @@ Lemma Zdivide_pol_sub_0 : forall p a, Zdivide_pol a (PsubC Z.sub p 0) -> Zdivide_pol a p. Proof. - induction p. + intros p; induction p as [c|? p IHp|? IHp1 ? ? IHp2]. simpl. - intros. inversion H. + intros ? H. inversion H. constructor. rewrite Z.sub_0_r in *. assumption. - intros. + intros ? H. constructor. simpl in H. inversion H ; subst; clear H. apply IHp ; auto. - simpl. intros. + simpl. intros ? H. inv H. constructor. auto. apply IHp2 ; assumption. @@ -783,9 +784,9 @@ Qed. Lemma Zgcd_pol_div : forall p g c, Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c). Proof. - induction p ; simpl. + intros p; induction p as [c|? ? IHp|p1 IHp1 ? p3 IHp2]; simpl. (* Pc *) - intros. inv H. + intros ? ? H. inv H. constructor. exists 0. now ring. (* Pinj *) @@ -793,28 +794,28 @@ Proof. constructor. apply IHp ; auto. (* PX *) intros g c. - case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros. + case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros z z0 H z1 z2 H0 H1. inv H1. unfold ZgcdM at 1. destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; destruct HH1 as [HH1 HH1'] ; rewrite HH1'. constructor. - apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2). + apply (Zdivide_pol_Zdivide _ (ZgcdM z1 z2)). unfold ZgcdM. destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. - destruct HH2. + destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_sub ; auto. apply Z.lt_le_trans with 1. reflexivity. now apply Z.ge_le. - destruct HH2. rewrite H2. + destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_one. unfold ZgcdM in HH1. unfold ZgcdM. destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. - destruct HH2. rewrite H2 in *. + destruct HH2 as [H1 H2]. rewrite H2 in *. destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto. - destruct HH2. rewrite H2. + destruct HH2 as [H1 H2]. rewrite H2. destruct (Zgcd_is_gcd 1 z); auto. - apply Zdivide_pol_Zdivide with (x:= z). + apply (Zdivide_pol_Zdivide _ z). apply (IHp2 _ _ H); auto. destruct (Zgcd_is_gcd (ZgcdM z1 z2) z); auto. constructor. apply Zdivide_pol_one. @@ -873,7 +874,7 @@ Definition is_pol_Z0 (p : PolC Z) : bool := Lemma is_pol_Z0_eval_pol : forall p, is_pol_Z0 p = true -> forall env, eval_pol env p = 0. Proof. unfold is_pol_Z0. - destruct p ; try discriminate. + intros p; destruct p as [z| |]; try discriminate. destruct z ; try discriminate. reflexivity. Qed. @@ -915,8 +916,8 @@ Fixpoint max_var (jmp : positive) (p : Pol Z) : positive := Lemma pos_le_add : forall y x, (x <= y + x)%positive. Proof. - intros. - assert ((Z.pos x) <= Z.pos (x + y))%Z. + intros y x. + assert ((Z.pos x) <= Z.pos (x + y))%Z as H. rewrite <- (Z.add_0_r (Zpos x)). rewrite <- Pos2Z.add_pos_pos. apply Z.add_le_mono_l. @@ -929,10 +930,10 @@ Qed. Lemma max_var_le : forall p v, (v <= max_var v p)%positive. Proof. - induction p; simpl. + intros p; induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - intros. apply Pos.le_refl. - - intros. + - intros v. specialize (IHp (p+v)%positive). eapply Pos.le_trans ; eauto. assert (xH + v <= p + v)%positive. @@ -942,7 +943,7 @@ Proof. } eapply Pos.le_trans ; eauto. apply pos_le_add. - - intros. + - intros v. apply Pos.max_case_strong;intros ; auto. specialize (IHp2 (Pos.succ v)%positive). eapply Pos.le_trans ; eauto. @@ -951,10 +952,10 @@ Qed. Lemma max_var_correct : forall p j v, In v (vars j p) -> Pos.le v (max_var j p). Proof. - induction p; simpl. + intros p; induction p; simpl. - tauto. - auto. - - intros. + - intros j v H. rewrite in_app_iff in H. destruct H as [H |[ H | H]]. + subst. @@ -980,7 +981,7 @@ Section MaxVar. (v <= acc -> v <= fold_left F l acc)%positive. Proof. - induction l ; simpl ; [easy|]. + intros l; induction l as [|a l IHl] ; simpl ; [easy|]. intros. apply IHl. unfold F. @@ -993,7 +994,7 @@ Section MaxVar. (acc <= acc' -> fold_left F l acc <= fold_left F l acc')%positive. Proof. - induction l ; simpl ; [easy|]. + intros l; induction l as [|a l IHl]; simpl ; [easy|]. intros. apply IHl. unfold F. @@ -1006,13 +1007,13 @@ Section MaxVar. Lemma max_var_nformulae_correct_aux : forall l p o v, In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive. Proof. - intros. + intros l p o v H H0. generalize 1%positive as acc. revert p o v H H0. - induction l. + induction l as [|a l IHl]. - simpl. tauto. - simpl. - intros. + intros p o v H H0 ?. destruct H ; subst. + unfold F at 2. simpl. @@ -1128,14 +1129,14 @@ Require Import Wf_nat. Lemma in_bdepth : forall l a b y, In y l -> ltof ZArithProof bdepth y (EnumProof a b l). Proof. - induction l. + intros l; induction l as [|a l IHl]. (* nil *) simpl. tauto. (* cons *) simpl. - intros. - destruct H. + intros a0 b y H. + destruct H as [H|H]. subst. unfold ltof. simpl. @@ -1180,8 +1181,8 @@ Lemma eval_Psatz_sound : forall env w l f', make_conj (eval_nformula env) l -> eval_Psatz l w = Some f' -> eval_nformula env f'. Proof. - intros. - apply (eval_Psatz_Sound Zsor ZSORaddon) with (l:=l) (e:= w) ; auto. + intros env w l f' H H0. + apply (fun H => eval_Psatz_Sound Zsor ZSORaddon l _ H w) ; auto. apply make_conj_in ; auto. Qed. @@ -1193,7 +1194,7 @@ Proof. unfold nformula_of_cutting_plane. unfold eval_nformula. unfold RingMicromega.eval_nformula. unfold eval_op1. - intros. + intros env e e' c H H0. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). simpl. (**) @@ -1201,10 +1202,10 @@ Proof. revert H0. case_eq (Zgcd_pol e) ; intros g c0. generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0). - intros. + intros H0 H1 H2. inv H2. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *. - apply Zgcd_pol_correct_lt with (env:=env) in H1. 2: auto using Z.gt_lt. + apply (Zgcd_pol_correct_lt _ env) in H1. 2: auto using Z.gt_lt. apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r. apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0). apply Z.le_ge. @@ -1213,7 +1214,7 @@ Proof. rewrite <- H1. assumption. (* g <= 0 *) - intros. inv H2. auto with zarith. + intros H0 H1 H2. inv H2. auto with zarith. Qed. Lemma cutting_plane_sound : forall env f p, @@ -1222,34 +1223,34 @@ Lemma cutting_plane_sound : forall env f p, eval_nformula env (nformula_of_cutting_plane p). Proof. unfold genCuttingPlane. - destruct f as [e op]. + intros env f; destruct f as [e op]. destruct op. (* Equal *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (Zgcd_pol e) ; intros g c. case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|]. case_eq (makeCuttingPlane e). - intros. + intros ? ? H H0 H1 H2 H3. inv H3. unfold makeCuttingPlane in H. rewrite H1 in H. revert H. change (eval_pol env e = 0) in H2. case_eq (Z.gtb g 0). - intros. - rewrite <- Zgt_is_gt_bool in H. + intros H H3. + rewrite <- Zgt_is_gt_bool in H. rewrite Zgcd_pol_correct_lt with (1:= H1) in H2. 2: auto using Z.gt_lt. - unfold nformula_of_cutting_plane. + unfold nformula_of_cutting_plane. change (eval_pol env (padd e' (Pc z)) = 0). inv H3. rewrite eval_pol_add. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x. simpl. rewrite andb_false_iff in H0. - destruct H0. + destruct H0 as [H0|H0]. rewrite Zgt_is_gt_bool in H ; congruence. rewrite andb_false_iff in H0. - destruct H0. + destruct H0 as [H0|H0]. rewrite negb_false_iff in H0. apply Zeq_bool_eq in H0. subst. simpl. @@ -1259,13 +1260,13 @@ Proof. apply Zeq_bool_eq in H0. assert (HH := Zgcd_is_gcd g c). rewrite H0 in HH. - inv HH. + destruct HH as [H3 H4 ?]. apply Zdivide_opp_r in H4. rewrite Zdivide_ceiling ; auto. apply Z.sub_move_0_r. apply Z.div_unique_exact. now intros ->. now rewrite Z.add_move_0_r in H2. - intros. + intros H H3. unfold nformula_of_cutting_plane. inv H3. change (eval_pol env (padd e' (Pc 0)) = 0). @@ -1273,7 +1274,7 @@ Proof. simpl. now rewrite Z.add_0_r. (* NonEqual *) - intros. + intros ? H H0. inv H0. unfold eval_nformula in *. unfold RingMicromega.eval_nformula in *. @@ -1282,20 +1283,20 @@ Proof. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). simpl. now rewrite Z.add_0_r. (* Strict *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane (PsubC Z.sub e 1)). - intros. + intros ? ? H H0 H1. inv H1. - apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). + apply (makeCuttingPlane_ns_sound env) with (2:= H). simpl in *. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). now apply Z.lt_le_pred. (* NonStrict *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane e). - intros. + intros ? ? H H0 H1. inv H1. - apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). + apply (makeCuttingPlane_ns_sound env) with (2:= H). assumption. Qed. @@ -1304,12 +1305,15 @@ Lemma genCuttingPlaneNone : forall env f, eval_nformula env f -> False. Proof. unfold genCuttingPlane. - destruct f. + intros env f; destruct f as [p o]. destruct o. case_eq (Zgcd_pol p) ; intros g c. case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))). - intros. + intros H H0 H1 H2. flatten_bool. + match goal with [ H' : (g >? 0) = true |- ?G ] => rename H' into H3 end. + match goal with [ H' : negb (Zeq_bool c 0) = true |- ?G ] => rename H' into H end. + match goal with [ H' : negb (Zeq_bool (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end. rewrite negb_true_iff in H5. apply Zeq_bool_neq in H5. rewrite <- Zgt_is_gt_bool in H3. @@ -1359,7 +1363,7 @@ Lemma agree_env_subset : forall v1 v2 env env', agree_env v2 env env'. Proof. unfold agree_env. - intros. + intros v1 v2 env env' H ? ? ?. apply H. eapply Pos.le_trans ; eauto. Qed. @@ -1369,7 +1373,7 @@ Lemma agree_env_jump : forall fr j env env', agree_env (fr + j) env env' -> agree_env fr (Env.jump j env) (Env.jump j env'). Proof. - intros. + intros fr j env env' H. unfold agree_env ; intro. intros. unfold Env.jump. @@ -1382,7 +1386,7 @@ Lemma agree_env_tail : forall fr env env', agree_env (Pos.succ fr) env env' -> agree_env fr (Env.tail env) (Env.tail env'). Proof. - intros. + intros fr env env' H. unfold Env.tail. apply agree_env_jump. rewrite <- Pos.add_1_r in H. @@ -1393,7 +1397,7 @@ Qed. Lemma max_var_acc : forall p i j, (max_var (i + j) p = max_var i p + j)%positive. Proof. - induction p; simpl. + intros p; induction p as [|? ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - intros. rewrite ! IHp. @@ -1415,27 +1419,27 @@ Lemma agree_env_eval_nformula : (AGREE : agree_env (max_var xH (fst e)) env env'), eval_nformula env e <-> eval_nformula env' e. Proof. - destruct e. - simpl; intros. + intros env env' e; destruct e as [p o]. + simpl; intros AGREE. assert ((RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env p) = - (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)). + (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)) as H. { revert env env' AGREE. generalize xH. - induction p ; simpl. + induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - - intros. - apply IHp with (p := p1%positive). + - intros p1 **. + apply (IHp p1). apply agree_env_jump. eapply agree_env_subset; eauto. rewrite (Pos.add_comm p). rewrite max_var_acc. apply Pos.le_refl. - - intros. + - intros p ? ? AGREE. f_equal. f_equal. - { apply IHp1 with (p:= p). + { apply (IHp1 p). eapply agree_env_subset; eauto. apply Pos.le_max_l. } @@ -1446,7 +1450,7 @@ Proof. apply Pos.le_1_l. } { - apply IHp2 with (p := p). + apply (IHp2 p). apply agree_env_tail. eapply agree_env_subset; eauto. rewrite !Pplus_one_succ_r. @@ -1463,11 +1467,11 @@ Lemma agree_env_eval_nformulae : make_conj (eval_nformula env) l <-> make_conj (eval_nformula env') l. Proof. - induction l. + intros env env' l; induction l as [|a l IHl]. - simpl. tauto. - intros. rewrite ! make_conj_cons. - assert (eval_nformula env a <-> eval_nformula env' a). + assert (eval_nformula env a <-> eval_nformula env' a) as H. { apply agree_env_eval_nformula. eapply agree_env_subset ; eauto. @@ -1491,7 +1495,7 @@ Qed. Lemma eq_true_iff_eq : forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2. Proof. - destruct b1,b2 ; intuition congruence. + intros b1 b2; destruct b1,b2 ; intuition congruence. Qed. Ltac pos_tac := @@ -1520,7 +1524,7 @@ Qed. Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False. Proof. - induction w using (well_founded_ind (well_founded_ltof _ bdepth)). + intros w; induction w as [w H] using (well_founded_ind (well_founded_ltof _ bdepth)). destruct w as [ | w pf | w pf | p pf1 pf2 | w1 w2 pf | x pf]. - (* DoneProof *) simpl. discriminate. @@ -1529,12 +1533,12 @@ Proof. intros l. case_eq (eval_Psatz l w) ; [| discriminate]. intros f Hf. case_eq (Zunsat f). - intros. + intros H0 ? ?. apply (checker_nf_sound Zsor ZSORaddon l w). unfold check_normalised_formulas. unfold eval_Psatz in Hf. rewrite Hf. unfold Zunsat in H0. assumption. - intros. - assert (make_impl (eval_nformula env) (f::l) False). + intros H0 H1 env. + assert (make_impl (eval_nformula env) (f::l) False) as H2. apply H with (2:= H1). unfold ltof. simpl. @@ -1553,8 +1557,8 @@ Proof. case_eq (eval_Psatz l w) ; [ | discriminate]. intros f' Hlc. case_eq (genCuttingPlane f'). - intros. - assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False). + intros p H0 H1 env. + assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False) as H2. eapply (H pf) ; auto. unfold ltof. simpl. @@ -1565,13 +1569,13 @@ Proof. intro. apply H2. split ; auto. - apply eval_Psatz_sound with (env:=env) in Hlc. + apply (eval_Psatz_sound env) in Hlc. apply cutting_plane_sound with (1:= Hlc) (2:= H0). auto. (* genCuttingPlane = None *) - intros. + intros H0 H1 env. rewrite <- make_conj_impl. - intros. + intros H2. apply eval_Psatz_sound with (2:= Hlc) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - (* SplitProof *) @@ -1581,18 +1585,20 @@ Proof. case_eq (genCuttingPlane (popp p, NonStrict)) ; [| discriminate]. intros cp1 GCP1 cp2 GCP2 ZC1 env. flatten_bool. + match goal with [ H' : ZChecker _ pf1 = true |- _ ] => rename H' into H0 end. + match goal with [ H' : ZChecker _ pf2 = true |- _ ] => rename H' into H1 end. destruct (eval_nformula_split env p). - + apply H with (env:=env) in H0. + + apply (fun H' ck => H _ H' _ ck env) in H0. rewrite <- make_conj_impl in *. intro ; apply H0. rewrite make_conj_cons. split; auto. - apply cutting_plane_sound with (f:= (p,NonStrict)) ; auto. + apply (cutting_plane_sound _ (p,NonStrict)) ; auto. apply ltof_bdepth_split_l. - + apply H with (env:=env) in H1. + + apply (fun H' ck => H _ H' _ ck env) in H1. rewrite <- make_conj_impl in *. intro ; apply H1. rewrite make_conj_cons. split; auto. - apply cutting_plane_sound with (f:= (popp p,NonStrict)) ; auto. + apply (cutting_plane_sound _ (popp p,NonStrict)) ; auto. apply ltof_bdepth_split_r. - (* EnumProof *) intros l. @@ -1601,22 +1607,22 @@ Proof. case_eq (eval_Psatz l w2) ; [ | discriminate]. intros f1 Hf1 f2 Hf2. case_eq (genCuttingPlane f2). - destruct p as [ [p1 z1] op1]. + intros p; destruct p as [ [p1 z1] op1]. case_eq (genCuttingPlane f1). - destruct p as [ [p2 z2] op2]. + intros p; destruct p as [ [p2 z2] op2]. case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)). intros Hcond. flatten_bool. - rename H1 into HZ0. - rename H2 into Hop1. - rename H3 into Hop2. + match goal with [ H1 : is_pol_Z0 (padd p1 p2) = true |- _ ] => rename H1 into HZ0 end. + match goal with [ H2 : valid_cut_sign op1 = true |- _ ] => rename H2 into Hop1 end. + match goal with [ H3 : valid_cut_sign op2 = true |- _ ] => rename H3 into Hop2 end. intros HCutL HCutR Hfix env. (* get the bounds of the enum *) rewrite <- make_conj_impl. - intro. - assert (-z1 <= eval_pol env p1 <= z2). + intro H0. + assert (-z1 <= eval_pol env p1 <= z2) as H1. split. - apply eval_Psatz_sound with (env:=env) in Hf2 ; auto. + apply (eval_Psatz_sound env) in Hf2 ; auto. apply cutting_plane_sound with (1:= Hf2) in HCutR. unfold nformula_of_cutting_plane in HCutR. unfold eval_nformula in HCutR. @@ -1628,10 +1634,10 @@ Proof. rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity. now apply Z.le_sub_le_add_r in HCutR. (**) - apply is_pol_Z0_eval_pol with (env := env) in HZ0. + apply (fun H => is_pol_Z0_eval_pol _ H env) in HZ0. rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0. rewrite HZ0. - apply eval_Psatz_sound with (env:=env) in Hf1 ; auto. + apply (eval_Psatz_sound env) in Hf1 ; auto. apply cutting_plane_sound with (1:= Hf1) in HCutL. unfold nformula_of_cutting_plane in HCutL. unfold eval_nformula in HCutL. @@ -1647,7 +1653,7 @@ Proof. match goal with | |- context[?F pf (-z1) z2 = true] => set (FF := F) end. - intros. + intros Hfix. assert (HH :forall x, -z1 <= x <= z2 -> exists pr, (In pr pf /\ ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z). @@ -1655,16 +1661,18 @@ Proof. revert Hfix. generalize (-z1). clear z1. intro z1. revert z1 z2. - induction pf;simpl ;intros. + induction pf as [|a pf IHpf];simpl ;intros z1 z2 Hfix x **. revert Hfix. now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x. flatten_bool. + match goal with [ H' : _ <= x <= _ |- _ ] => rename H' into H0 end. + match goal with [ H' : FF pf (z1 + 1) z2 = true |- _ ] => rename H' into H2 end. destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ]. 2: exists a; auto. rewrite <- Z.le_succ_l in LT. assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition. elim IHpf with (2:=H2) (3:= LE). - intros. + intros x0 ?. exists x0 ; split;tauto. intros until 1. apply H ; auto. @@ -1676,7 +1684,7 @@ Proof. apply Z.add_le_mono_r. assumption. (*/asser *) destruct (HH _ H1) as [pr [Hin Hcheker]]. - assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False). + assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False) as H2. eapply (H pr) ;auto. apply in_bdepth ; auto. rewrite <- make_conj_impl in H2. @@ -1690,15 +1698,15 @@ Proof. unfold eval_pol. ring. discriminate. (* No cutting plane *) - intros. + intros H0 H1 H2 env. rewrite <- make_conj_impl. - intros. + intros H3. apply eval_Psatz_sound with (2:= Hf1) in H3. apply genCuttingPlaneNone with (2:= H3) ; auto. (* No Cutting plane (bis) *) - intros. + intros H0 H1 env. rewrite <- make_conj_impl. - intros. + intros H2. apply eval_Psatz_sound with (2:= Hf2) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - intros l. @@ -1708,15 +1716,15 @@ Proof. set (z1 := (Pos.succ fr)) in *. set (t1 := (Pos.succ z1)) in *. destruct (x <=? fr)%positive eqn:LE ; [|congruence]. - intros. + intros H0 env. set (env':= fun v => if Pos.eqb v z1 then if Z.leb (env x) 0 then 0 else env x else if Pos.eqb v t1 then if Z.leb (env x) 0 then -(env x) else 0 else env v). - apply H with (env:=env') in H0. + apply (fun H' ck => H _ H' _ ck env') in H0. + rewrite <- make_conj_impl in *. - intro. + intro H1. rewrite !make_conj_cons in H0. apply H0 ; repeat split. * @@ -1729,17 +1737,17 @@ Proof. destruct (env x <=? 0); ring. { unfold t1. pos_tac; normZ. - lia (Hyp H2). + lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). } { unfold t1, z1. pos_tac; normZ. - lia (Add (Hyp LE) (Hyp H3)). + lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.succ (Z.pos fr))) ltac:(assumption))). } { unfold z1. pos_tac; normZ. - lia (Add (Hyp LE) (Hyp H3)). + lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.pos fr)) ltac:(assumption))). } * apply eval_nformula_bound_var. @@ -1749,7 +1757,7 @@ Proof. compute. congruence. rewrite Z.leb_gt in EQ. normZ. - lia (Add (Hyp EQ) (Hyp H2)). + lia (Add (Hyp EQ) (Hyp (e := 0 - (env x + 1)) ltac:(assumption))). * apply eval_nformula_bound_var. unfold env'. @@ -1758,15 +1766,15 @@ Proof. destruct (env x <=? 0) eqn:EQ. rewrite Z.leb_le in EQ. normZ. - lia (Add (Hyp EQ) (Hyp H2)). + lia (Add (Hyp EQ) (Hyp (e := 0 - (- env x + 1)) ltac:(assumption))). compute; congruence. unfold t1. clear. pos_tac; normZ. - lia (Hyp H). + lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). * - rewrite agree_env_eval_nformulae with (env':= env') in H1;auto. - unfold agree_env; intros. + rewrite (agree_env_eval_nformulae _ env') in H1;auto. + unfold agree_env; intros x0 H2. unfold env'. replace (x0 =? z1)%positive with false. replace (x0 =? t1)%positive with false. @@ -1776,13 +1784,13 @@ Proof. unfold fr in *. apply Pos2Z.pos_le_pos in H2. pos_tac; normZ. - lia (Add (Hyp H2) (Hyp H4)). + lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.succ (Z.pos (max_var_nformulae l)))) ltac:(assumption))). } { unfold z1, fr in *. apply Pos2Z.pos_le_pos in H2. pos_tac; normZ. - lia (Add (Hyp H2) (Hyp H4)). + lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.pos (max_var_nformulae l))) ltac:(assumption))). } + unfold ltof. simpl. @@ -1796,27 +1804,27 @@ Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, Proof. intros f w. unfold ZTautoChecker. - apply tauto_checker_sound with (eval' := eval_nformula). + apply (tauto_checker_sound _ _ _ _ eval_nformula). - apply Zeval_nformula_dec. - - intros until env. + - intros t ? env. unfold eval_nformula. unfold RingMicromega.eval_nformula. destruct t. apply (check_inconsistent_sound Zsor ZSORaddon) ; auto. - - unfold Zdeduce. intros. revert H. + - unfold Zdeduce. intros ? ? ? H **. revert H. apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto. - - intros. + intros ? ? ? ? H. rewrite normalise_correct in H. rewrite Zeval_formula_compat; auto. - - intros. + intros ? ? ? ? H. rewrite negate_correct in H ; auto. rewrite Tauto.hold_eNOT. rewrite Zeval_formula_compat; auto. - intros t w0. unfold eval_tt. - intros. - rewrite make_impl_map with (eval := eval_nformula env). + intros H env. + rewrite (make_impl_map (eval_nformula env)). eapply ZChecker_sound; eauto. tauto. Qed. diff --git a/theories/setoid_ring/Field_theory.v b/theories/setoid_ring/Field_theory.v index c12f46bed6..4b3bba9843 100644 --- a/theories/setoid_ring/Field_theory.v +++ b/theories/setoid_ring/Field_theory.v @@ -397,7 +397,7 @@ Qed. Theorem cross_product_eq a b c d : ~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d. Proof. -intros. +intros H H0 H1. transitivity (a / b * (d / d)). - now rewrite rdiv_r_r, rmul_1_r. - now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r. @@ -418,23 +418,23 @@ Qed. Lemma pow_pos_0 p : pow_pos rmul 0 p == 0. Proof. -induction p;simpl;trivial; now rewrite !IHp. +induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !IHp. Qed. Lemma pow_pos_1 p : pow_pos rmul 1 p == 1. Proof. -induction p;simpl;trivial; ring [IHp]. +induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp]. Qed. Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p]. Proof. -induction p;simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp. +induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp. Qed. Lemma pow_pos_mul_l x y p : pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p. Proof. -induction p;simpl;trivial; ring [IHp]. +induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp]. Qed. Lemma pow_pos_add_r x p1 p2 : @@ -446,7 +446,7 @@ Qed. Lemma pow_pos_mul_r x p1 p2 : pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2. Proof. -induction p1;simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r; +induction p1 as [p1 IHp1|p1 IHp1|];simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r; simpl; trivial; ring [IHp1]. Qed. @@ -459,8 +459,8 @@ Qed. Lemma pow_pos_div a b p : ~ b == 0 -> pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p. Proof. - intros. - induction p; simpl; trivial. + intros H. + induction p as [p IHp|p IHp|]; simpl; trivial. - rewrite IHp. assert (nz := pow_pos_nz p H). rewrite !rdiv4; trivial. @@ -578,14 +578,15 @@ Qed. Theorem PExpr_eq_semi_ok e e' : PExpr_eq e e' = true -> (e === e')%poly. Proof. -revert e'; induction e; destruct e'; simpl; try discriminate. +revert e'; induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe ?]; + intro e'; destruct e'; simpl; try discriminate. - intros H l. now apply (morph_eq CRmorph). - case Pos.eqb_spec; intros; now subst. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H. now rewrite IHe. -- intros H. destruct (if_true _ _ H). +- intros H. destruct (if_true _ _ H) as [H0 H1]. apply N.eqb_eq in H0. now rewrite IHe, H0. Qed. @@ -667,7 +668,7 @@ Proof. - case Pos.eqb_spec; [intro; subst | intros _]. + simpl. now rewrite rpow_pow. + destruct e;simpl;trivial. - repeat case ceqb_spec; intros; rewrite ?rpow_pow, ?H; simpl. + repeat case ceqb_spec; intros H **; rewrite ?rpow_pow, ?H; simpl. * now rewrite phi_1, pow_pos_1. * now rewrite phi_0, pow_pos_0. * now rewrite pow_pos_cst. @@ -686,7 +687,8 @@ Infix "**" := NPEmul (at level 40, left associativity). Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly. Proof. intros l. -revert e2; induction e1;destruct e2; simpl;try reflexivity; +revert e2; induction e1 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1|? IHe1 n]; + intro e2; destruct e2; simpl;try reflexivity; repeat (case ceqb_spec; intro H; try rewrite H; clear H); simpl; try reflexivity; try ring [phi_0 phi_1]. apply (morph_mul CRmorph). @@ -801,7 +803,7 @@ Qed. Theorem PCond_app l l1 l2 : PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2. Proof. -induction l1. +induction l1 as [|a l1 IHl1]. - simpl. split; [split|destruct 1]; trivial. - simpl app. rewrite !PCond_cons, IHl1. symmetry; apply and_assoc. Qed. @@ -813,7 +815,7 @@ Definition absurd_PCond := cons 0%poly nil. Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. Proof. unfold absurd_PCond; simpl. -red; intros. +red; intros ? H. apply H. apply phi_0. Qed. @@ -901,7 +903,7 @@ Theorem isIn_ok e1 p1 e2 p2 : Proof. Opaque NPEpow. revert p1 p2. -induction e2; intros p1 p2; +induction e2 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe2_1 ? IHe2_2|? IHe|? IHe2 n]; intros p1 p2; try refine (default_isIn_ok e1 _ p1 p2); simpl isIn. - specialize (IHe2_1 p1 p2). destruct isIn as [([|p],e)|]. @@ -936,7 +938,7 @@ induction e2; intros p1 p2; destruct IHe2_2 as (IH,GT). split; trivial. set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d. npe_simpl. rewrite IH. npe_ring. -- destruct n; trivial. +- destruct n as [|p]; trivial. specialize (IHe2 p1 (p * p2)%positive). destruct isIn as [(n,e)|]; trivial. destruct IHe2 as (IH,GT). split; trivial. @@ -983,7 +985,7 @@ Lemma split_aux_ok1 e1 p e2 : /\ e2 === right res * common res)%poly. Proof. Opaque NPEpow NPEmul. - intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). + intros res. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl. - intros (H1,H2); split; npe_simpl. + now rewrite PE_1_l. @@ -1000,7 +1002,8 @@ Theorem split_aux_ok: forall e1 p e2, (e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2) /\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly. Proof. -induction e1;intros k e2; try refine (split_aux_ok1 _ k e2);simpl. +intro e1;induction e1 as [| |?|?|? IHe1_1 ? IHe1_2|? IHe1_1 ? IHe1_2|e1_1 IHe1_1 ? IHe1_2|? IHe1|? IHe1 n]; + intros k e2; try refine (split_aux_ok1 _ k e2);simpl. destruct (IHe1_1 k e2) as (H1,H2). destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4). clear IHe1_1 IHe1_2. @@ -1101,7 +1104,8 @@ Eval compute Theorem Pcond_Fnorm l e : PCond l (condition (Fnorm e)) -> ~ (denum (Fnorm e))@l == 0. Proof. -induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app; +induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe|? IHe1 ? IHe2|? IHe n]; + simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok. - simpl. rewrite phi_1; exact rI_neq_rO. - simpl. rewrite phi_1; exact rI_neq_rO. @@ -1141,7 +1145,8 @@ Theorem Fnorm_FEeval_PEeval l fe: PCond l (condition (Fnorm fe)) -> FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l. Proof. -induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; +induction fe as [| |?|?|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe IHfe|fe IHfe|fe1 IHfe1 fe2 IHfe2|fe IHfe n]; + simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; intros (Hc1,Hc2) || intros Hc; try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1); try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2); @@ -1260,7 +1265,7 @@ Proof. destruct (Nnorm _ _ _) as [c | | ] eqn: HN; try ( apply rdiv_ext; eapply ring_rw_correct; eauto). - destruct (ceqb_spec c cI). + destruct (ceqb_spec c cI) as [H0|]. set (nnum := NPphi_dev _ _). apply eq_trans with (nnum / NPphi_dev l (Pc c)). apply rdiv_ext; @@ -1285,7 +1290,7 @@ Proof. destruct (Nnorm _ _ _) as [c | | ] eqn: HN; try ( apply rdiv_ext; eapply ring_rw_pow_correct; eauto). - destruct (ceqb_spec c cI). + destruct (ceqb_spec c cI) as [H0|]. set (nnum := NPphi_pow _ _). apply eq_trans with (nnum / NPphi_pow l (Pc c)). apply rdiv_ext; @@ -1415,7 +1420,8 @@ Theorem Field_simplify_eq_pow_in_correct : NPphi_pow l np1 == NPphi_pow l np2. Proof. - intros. subst nfe1 nfe2 lmp np1 np2. + intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?. + subst nfe1 nfe2 lmp np1 np2. rewrite !(Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec). repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl. apply Field_simplify_aux_ok; trivial. @@ -1434,7 +1440,8 @@ forall n l lpe fe1 fe2, PCond l (condition nfe1 ++ condition nfe2) -> NPphi_dev l np1 == NPphi_dev l np2. Proof. - intros. subst nfe1 nfe2 lmp np1 np2. + intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?. + subst nfe1 nfe2 lmp np1 np2. rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec). repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). apply Field_simplify_aux_ok; trivial. @@ -1458,7 +1465,7 @@ Lemma fcons_ok : forall l l1, (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1. Proof. intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. -induction l1; simpl; intros. +induction l1 as [|a l1 IHl1]; simpl; intros. trivial. elim PCond_fcons_inv with (1 := H); intros. destruct l1; trivial. split; trivial. apply IHl1; trivial. @@ -1480,7 +1487,7 @@ Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := Theorem PFcons_fcons_inv: forall l a l1, PCond l (Fcons a l1) -> ~ a @ l == 0 /\ PCond l l1. Proof. -induction l1 as [|e l1]; simpl Fcons. +intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons. - simpl; now split. - case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2); repeat split; trivial. @@ -1501,7 +1508,7 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := Theorem PFcons0_fcons_inv: forall l a l1, PCond l (Fcons0 a l1) -> ~ a @ l == 0 /\ PCond l l1. Proof. -induction l1 as [|e l1]; simpl Fcons0. +intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons0. - simpl; now split. - generalize (ring_correct O l nil a e). lazy zeta; simpl Peq. case Peq; intros H; rewrite !PCond_cons; intros (H1,H2); @@ -1529,7 +1536,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). destruct (H0 _ H3) as (H4,H5). split; trivial. simpl. apply field_is_integral_domain; trivial. -- intros. destruct (H _ H0). split; trivial. +- intros ? H ? ? H0. destruct (H _ H0). split; trivial. apply PEpow_nz; trivial. Qed. @@ -1580,7 +1587,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). split; trivial. apply ropp_neq_0; trivial. rewrite (morph_opp CRmorph), phi_0, phi_1 in H0. trivial. -- intros. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial. +- intros ? H ? ? H0. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial. Qed. Definition Fcons2 e l := Fcons1 (PEsimp e) l. @@ -1674,7 +1681,7 @@ Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. Lemma add_inj_r p x y : gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y. Proof. -elim p using Pos.peano_ind; simpl; intros. +elim p using Pos.peano_ind; simpl; [intros H|intros ? H ?]. apply S_inj; trivial. apply H. apply S_inj. @@ -1710,8 +1717,8 @@ Lemma gen_phiN_inj x y : gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> x = y. Proof. -destruct x; destruct y; simpl; intros; trivial. - elim gen_phiPOS_not_0 with p. +destruct x as [|p]; destruct y as [|p']; simpl; intros H; trivial. + elim gen_phiPOS_not_0 with p'. symmetry . rewrite (same_gen Rsth Reqe ARth); trivial. elim gen_phiPOS_not_0 with p. @@ -1770,14 +1777,14 @@ Lemma gen_phiZ_inj x y : gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> x = y. Proof. -destruct x; destruct y; simpl; intros. +destruct x as [|p|p]; destruct y as [|p'|p']; simpl; intros H. trivial. - elim gen_phiPOS_not_0 with p. + elim gen_phiPOS_not_0 with p'. rewrite (same_gen Rsth Reqe ARth). symmetry ; trivial. - elim gen_phiPOS_not_0 with p. + elim gen_phiPOS_not_0 with p'. rewrite (same_gen Rsth Reqe ARth). - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')). rewrite <- H. apply (ARopp_zero Rsth Reqe ARth). elim gen_phiPOS_not_0 with p. @@ -1790,12 +1797,12 @@ destruct x; destruct y; simpl; intros. rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). rewrite H. apply (ARopp_zero Rsth Reqe ARth). - elim gen_phiPOS_discr_sgn with p0 p. + elim gen_phiPOS_discr_sgn with p' p. symmetry ; trivial. - replace p0 with p; trivial. + replace p' with p; trivial. apply gen_phiPOS_inject. rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')). rewrite H; trivial. reflexivity. Qed. |