diff options
58 files changed, 936 insertions, 788 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e4815920ce..9e96d3602b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -169,7 +169,15 @@ before_script: - not-a-real-job script: - cd _install_ci - - find lib/coq/ -name '*.vo' -print0 | xargs -0 bin/coqchk -silent -o -m -coqlib lib/coq/ + - find lib/coq/ -name '*.vo' -fprint0 vofiles + - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed + - tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail + - "[ ! -f coqchk.failed ]" # needs quoting for yml syntax reasons + artifacts: + name: "$CI_JOB_NAME.logs" + paths: + - coqchk.log + expire_in: 1 month .ci-template: stage: test diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh deleted file mode 100644 index f26e0904bc..0000000000 --- a/dev/ci/appveyor.sh +++ /dev/null @@ -1,17 +0,0 @@ -#!/bin/bash - -set -e -x - -APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c -NJOBS=2 - -wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz -tar -xf opam64.tar.xz -bash opam64/install.sh - -opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing -eval "$(opam env)" -opam install -j $NJOBS -y num ocamlfind ounit - -# Full regular Coq Build -cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index f97e781832..95fceb773a 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -98,7 +98,8 @@ # Coquelicot ######################################################################## : "${coquelicot_CI_REF:=master}" -: "${coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}" +: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" +: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}" ######################################################################## # CompCert diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 33627fd8ef..6cb8dad604 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")" install_ssreflect -FORCE_GIT=1 git_download coquelicot ( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/nix/coquelicot.nix b/dev/ci/nix/coquelicot.nix new file mode 100644 index 0000000000..d379bfa73d --- /dev/null +++ b/dev/ci/nix/coquelicot.nix @@ -0,0 +1,9 @@ +{ autoconf, automake, ssreflect }: + +{ + buildInputs = [ autoconf automake ]; + coqBuildInputs = [ ssreflect ]; + configure = "./autogen.sh && ./configure"; + make = "./remake"; + clean = "./remake clean"; +} diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index 17070e66ee..a9cc91170f 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -72,6 +72,7 @@ let projects = { CoLoR = callPackage ./CoLoR.nix {}; CompCert = callPackage ./CompCert.nix {}; coq_dpdgraph = callPackage ./coq_dpdgraph.nix {}; + coquelicot = callPackage ./coquelicot.nix {}; Corn = callPackage ./Corn.nix {}; cross_crypto = callPackage ./cross_crypto.nix {}; Elpi = callPackage ./Elpi.nix {}; diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix index e153043557..71028ec2dc 100644 --- a/dev/ci/nix/flocq.nix +++ b/dev/ci/nix/flocq.nix @@ -4,4 +4,5 @@ buildInputs = [ autoconf automake ]; configure = "./autogen.sh && ./configure"; make = "./remake"; + clean = "./remake clean"; } diff --git a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh new file mode 100644 index 0000000000..9f9cc19e83 --- /dev/null +++ b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10052" ] || [ "$CI_BRANCH" = "cleanup-logic-convert-hyp" ]; then + + relation_algebra_CI_REF=cleanup-logic-convert-hyp + relation_algebra_CI_GITURL=https://github.com/ppedrot/relation-algebra + +fi diff --git a/doc/changelog/03-notations/10061-print-custom-grammar.rst b/doc/changelog/03-notations/10061-print-custom-grammar.rst new file mode 100644 index 0000000000..8786c7ce6b --- /dev/null +++ b/doc/changelog/03-notations/10061-print-custom-grammar.rst @@ -0,0 +1,4 @@ +- Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` + (`#10061 <https://github.com/coq/coq/pull/10061>`_, + fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, + by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 48ad60c6dd..972a53ae36 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -47,7 +47,7 @@ with open("refman-preamble.rst") as s: # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. -#needs_sphinx = '1.0' +needs_sphinx = '1.7.8' # Add any Sphinx extension module names here, as strings. They can be # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 6cbd00f45d..efb5df720a 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -181,7 +181,14 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second section is devoted to file management: you may configure +The second and third sections are for controlling colors and style. + +The fourth section is for customizing the editor. It includes in +particular the ability to activate an Emacs mode named +micro-Proof-General (use the Help menu to know more about the +available bindings). + +The next section is devoted to file management: you may configure automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index b629d15b11..0ace9ef5b9 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -396,381 +396,3 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: none Qed. - -Using the tactic language -------------------------- - - -About the cardinality of the set of natural numbers -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The first example which shows how to use pattern matching over the -proof context is a proof of the fact that natural numbers have more -than two elements. This can be done as follows: - -.. coqtop:: in reset - - Lemma card_nat : - ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. - Proof. - -.. coqtop:: in - - red; intros (x, (y, Hy)). - -.. coqtop:: in - - elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; - - match goal with - | _ : ?a = ?b, _ : ?a = ?c |- _ => - cut (b = c); [ discriminate | transitivity a; auto ] - end. - -.. coqtop:: in - - Qed. - -We can notice that all the (very similar) cases coming from the three -eliminations (with three distinct natural numbers) are successfully -solved by a match goal structure and, in particular, with only one -pattern (use of non-linear matching). - - -Permutations of lists -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -A more complex example is the problem of permutations of -lists. The aim is to show that a list is a permutation of -another list. - -.. coqtop:: in reset - - Section Sort. - -.. coqtop:: in - - Variable A : Set. - -.. coqtop:: in - - Inductive perm : list A -> list A -> Prop := - | perm_refl : forall l, perm l l - | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) - | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) - | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. - -.. coqtop:: in - - End Sort. - -First, we define the permutation predicate as shown above. - -.. coqtop:: none - - Require Import List. - - -.. coqtop:: in - - Ltac perm_aux n := - match goal with - | |- (perm _ ?l ?l) => apply perm_refl - | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => - let newn := eval compute in (length l1) in - (apply perm_cons; perm_aux newn) - | |- (perm ?A (?a :: ?l1) ?l2) => - match eval compute in n with - | 1 => fail - | _ => - let l1' := constr:(l1 ++ a :: nil) in - (apply (perm_trans A (a :: l1) l1' l2); - [ apply perm_append | compute; perm_aux (pred n) ]) - end - end. - -Next we define an auxiliary tactic ``perm_aux`` which takes an argument -used to control the recursion depth. This tactic behaves as follows. If -the lists are identical (i.e. convertible), it concludes. Otherwise, if -the lists have identical heads, it proceeds to look at their tails. -Finally, if the lists have different heads, it rotates the first list by -putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the -number of performed rotations using the argument ``n``. We do this by -decrementing ``n`` each time we perform a rotation. It works because -for a list of length ``n`` we can make exactly ``n - 1`` rotations -to generate at most ``n`` distinct lists. Notice that we use the natural -numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know -that it is possible to use the usual natural numbers, but they are only -used as arguments for primitive tactics and they cannot be handled, so, -in particular, we cannot make computations with them. Thus the natural -choice is to use Coq data structures so that Coq makes the computations -(reductions) by ``eval compute in`` and we can get the terms back by match. - -.. coqtop:: in - - Ltac solve_perm := - match goal with - | |- (perm _ ?l1 ?l2) => - match eval compute in (length l1 = length l2) with - | (?n = ?n) => perm_aux n - end - end. - -The main tactic is ``solve_perm``. It computes the lengths of the two lists -and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they -aren't, the lists cannot be permutations of each other). Using this tactic we -can now prove lemmas as follows: - -.. coqtop:: in - - Lemma solve_perm_ex1 : - perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). - Proof. solve_perm. Qed. - -.. coqtop:: in - - Lemma solve_perm_ex2 : - perm nat - (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) - (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). - Proof. solve_perm. Qed. - -Deciding intuitionistic propositional logic -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Pattern matching on goals allows a powerful backtracking when returning tactic -values. An interesting application is the problem of deciding intuitionistic -propositional logic. Considering the contraction-free sequent calculi LJT* of -Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the -tactic language as shown below. - -.. coqtop:: in reset - - Ltac basic := - match goal with - | |- True => trivial - | _ : False |- _ => contradiction - | _ : ?A |- ?A => assumption - end. - -.. coqtop:: in - - Ltac simplify := - repeat (intros; - match goal with - | H : ~ _ |- _ => red in H - | H : _ /\ _ |- _ => - elim H; do 2 intro; clear H - | H : _ \/ _ |- _ => - elim H; intro; clear H - | H : ?A /\ ?B -> ?C |- _ => - cut (A -> B -> C); - [ intro | intros; apply H; split; assumption ] - | H: ?A \/ ?B -> ?C |- _ => - cut (B -> C); - [ cut (A -> C); - [ intros; clear H - | intro; apply H; left; assumption ] - | intro; apply H; right; assumption ] - | H0 : ?A -> ?B, H1 : ?A |- _ => - cut B; [ intro; clear H0 | apply H0; assumption ] - | |- _ /\ _ => split - | |- ~ _ => red - end). - -.. coqtop:: in - - Ltac my_tauto := - simplify; basic || - match goal with - | H : (?A -> ?B) -> ?C |- _ => - cut (B -> C); - [ intro; cut (A -> B); - [ intro; cut C; - [ intro; clear H | apply H; assumption ] - | clear H ] - | intro; apply H; intro; assumption ]; my_tauto - | H : ~ ?A -> ?B |- _ => - cut (False -> B); - [ intro; cut (A -> False); - [ intro; cut B; - [ intro; clear H | apply H; assumption ] - | clear H ] - | intro; apply H; red; intro; assumption ]; my_tauto - | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) - end. - -The tactic ``basic`` tries to reason using simple rules involving truth, falsity -and available assumptions. The tactic ``simplify`` applies all the reversible -rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main -tactic to be called) simplifies with ``simplify``, tries to conclude with -``basic`` and tries several paths using the backtracking rules (one of the -four Dyckhoff’s rules for the left implication to get rid of the contraction -and the right ``or``). - -Having defined ``my_tauto``, we can prove tautologies like these: - -.. coqtop:: in - - Lemma my_tauto_ex1 : - forall A B : Prop, A /\ B -> A \/ B. - Proof. my_tauto. Qed. - -.. coqtop:: in - - Lemma my_tauto_ex2 : - forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. - Proof. my_tauto. Qed. - - -Deciding type isomorphisms -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -A more tricky problem is to decide equalities between types modulo -isomorphisms. Here, we choose to use the isomorphisms of the simply -typed λ-calculus with Cartesian product and unit type (see, for -example, :cite:`RC95`). The axioms of this λ-calculus are given below. - -.. coqtop:: in reset - - Open Scope type_scope. - -.. coqtop:: in - - Section Iso_axioms. - -.. coqtop:: in - - Variables A B C : Set. - -.. coqtop:: in - - Axiom Com : A * B = B * A. - - Axiom Ass : A * (B * C) = A * B * C. - - Axiom Cur : (A * B -> C) = (A -> B -> C). - - Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). - - Axiom P_unit : A * unit = A. - - Axiom AR_unit : (A -> unit) = unit. - - Axiom AL_unit : (unit -> A) = A. - -.. coqtop:: in - - Lemma Cons : B = C -> A * B = A * C. - - Proof. - - intro Heq; rewrite Heq; reflexivity. - - Qed. - -.. coqtop:: in - - End Iso_axioms. - -.. coqtop:: in - - Ltac simplify_type ty := - match ty with - | ?A * ?B * ?C => - rewrite <- (Ass A B C); try simplify_type_eq - | ?A * ?B -> ?C => - rewrite (Cur A B C); try simplify_type_eq - | ?A -> ?B * ?C => - rewrite (Dis A B C); try simplify_type_eq - | ?A * unit => - rewrite (P_unit A); try simplify_type_eq - | unit * ?B => - rewrite (Com unit B); try simplify_type_eq - | ?A -> unit => - rewrite (AR_unit A); try simplify_type_eq - | unit -> ?B => - rewrite (AL_unit B); try simplify_type_eq - | ?A * ?B => - (simplify_type A; try simplify_type_eq) || - (simplify_type B; try simplify_type_eq) - | ?A -> ?B => - (simplify_type A; try simplify_type_eq) || - (simplify_type B; try simplify_type_eq) - end - with simplify_type_eq := - match goal with - | |- ?A = ?B => try simplify_type A; try simplify_type B - end. - -.. coqtop:: in - - Ltac len trm := - match trm with - | _ * ?B => let succ := len B in constr:(S succ) - | _ => constr:(1) - end. - -.. coqtop:: in - - Ltac assoc := repeat rewrite <- Ass. - -.. coqtop:: in - - Ltac solve_type_eq n := - match goal with - | |- ?A = ?A => reflexivity - | |- ?A * ?B = ?A * ?C => - apply Cons; let newn := len B in solve_type_eq newn - | |- ?A * ?B = ?C => - match eval compute in n with - | 1 => fail - | _ => - pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) - end - end. - -.. coqtop:: in - - Ltac compare_structure := - match goal with - | |- ?A = ?B => - let l1 := len A - with l2 := len B in - match eval compute in (l1 = l2) with - | ?n = ?n => solve_type_eq n - end - end. - -.. coqtop:: in - - Ltac solve_iso := simplify_type_eq; compare_structure. - -The tactic to judge equalities modulo this axiomatization is shown above. -The algorithm is quite simple. First types are simplified using axioms that -can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). -The normal forms are sequences of Cartesian products without Cartesian product -in the left component. These normal forms are then compared modulo permutation -of the components by the tactic ``compare_structure``. If they have the same -lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal. -The main tactic that puts all these components together is called ``solve_iso``. - -Here are examples of what can be solved by ``solve_iso``. - -.. coqtop:: in - - Lemma solve_iso_ex1 : - forall A B : Set, A * unit * B = B * (unit * A). - Proof. - intros; solve_iso. - Qed. - -.. coqtop:: in - - Lemma solve_iso_ex2 : - forall A B C : Set, - (A * unit -> B * (C * unit)) = - (A * unit -> (C -> unit) * C) * (unit -> A -> B). - Proof. - intros; solve_iso. - Qed. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d3562b52c5..a7eb7c2319 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -3,12 +3,25 @@ Ltac ==== -This chapter gives a compact documentation of |Ltac|, the tactic language -available in |Coq|. We start by giving the syntax, and next, we present the -informal semantics. If you want to know more regarding this language and -especially about its foundations, you can refer to :cite:`Del00`. Chapter -:ref:`detailedexamplesoftactics` is devoted to giving small but nontrivial -use examples of this language. +This chapter documents the tactic language |Ltac|. + +We start by giving the syntax, and next, we present the informal +semantics. To learn more about the language and +especially about its foundations, please refer to :cite:`Del00`. + +.. example:: Basic tactic macros + + Here are some examples of simple tactic macros that the + language lets you write. + + .. coqdoc:: + + Ltac reduce_and_try_to_solve := simpl; intros; auto. + + Ltac destruct_bool_and_rewrite b H1 H2 := + destruct b; [ rewrite H1; eauto | rewrite H2; eauto ]. + + See Section :ref:`ltac-examples` for more advanced examples. .. _ltac-syntax: @@ -1160,6 +1173,399 @@ Printing |Ltac| tactics This command displays a list of all user-defined tactics, with their arguments. + +.. _ltac-examples: + +Examples of using |Ltac| +------------------------- + +Proof that the natural numbers have at least two elements +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. example:: Proof that the natural numbers have at least two elements + + The first example shows how to use pattern matching over the proof + context to prove that natural numbers have at least two + elements. This can be done as follows: + + .. coqtop:: reset all + + Lemma card_nat : + ~ exists x y : nat, forall z:nat, x = z \/ y = z. + Proof. + intros (x & y & Hz). + destruct (Hz 0), (Hz 1), (Hz 2). + + At this point, the :tacn:`congruence` tactic would finish the job: + + .. coqtop:: all abort + + all: congruence. + + But for the purpose of the example, let's craft our own custom + tactic to solve this: + + .. coqtop:: none + + Lemma card_nat : + ~ exists x y : nat, forall z:nat, x = z \/ y = z. + Proof. + intros (x & y & Hz). + destruct (Hz 0), (Hz 1), (Hz 2). + + .. coqtop:: all abort + + all: match goal with + | _ : ?a = ?b, _ : ?a = ?c |- _ => assert (b = c) by now transitivity a + end. + all: discriminate. + + Notice that all the (very similar) cases coming from the three + eliminations (with three distinct natural numbers) are successfully + solved by a ``match goal`` structure and, in particular, with only one + pattern (use of non-linear matching). + + +Proving that a list is a permutation of a second list +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. example:: Proving that a list is a permutation of a second list + + Let's first define the permutation predicate: + + .. coqtop:: in reset + + Section Sort. + + Variable A : Set. + + Inductive perm : list A -> list A -> Prop := + | perm_refl : forall l, perm l l + | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) + | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) + | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. + + End Sort. + + .. coqtop:: none + + Require Import List. + + + Next we define an auxiliary tactic :g:`perm_aux` which takes an + argument used to control the recursion depth. This tactic works as + follows: If the lists are identical (i.e. convertible), it + completes the proof. Otherwise, if the lists have identical heads, + it looks at their tails. Finally, if the lists have different + heads, it rotates the first list by putting its head at the end. + + Every time we perform a rotation, we decrement :g:`n`. When :g:`n` + drops down to :g:`1`, we stop performing rotations and we fail. + The idea is to give the length of the list as the initial value of + :g:`n`. This way of counting the number of rotations will avoid + going back to a head that had been considered before. + + From Section :ref:`ltac-syntax` we know that Ltac has a primitive + notion of integers, but they are only used as arguments for + primitive tactics and we cannot make computations with them. Thus, + instead, we use Coq's natural number type :g:`nat`. + + .. coqtop:: in + + Ltac perm_aux n := + match goal with + | |- (perm _ ?l ?l) => apply perm_refl + | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in + (apply perm_cons; perm_aux newn) + | |- (perm ?A (?a :: ?l1) ?l2) => + match eval compute in n with + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (perm_trans A (a :: l1) l1' l2); + [ apply perm_append | compute; perm_aux (pred n) ]) + end + end. + + + The main tactic is :g:`solve_perm`. It computes the lengths of the + two lists and uses them as arguments to call :g:`perm_aux` if the + lengths are equal. (If they aren't, the lists cannot be + permutations of each other.) + + .. coqtop:: in + + Ltac solve_perm := + match goal with + | |- (perm _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => perm_aux n + end + end. + + And now, here is how we can use the tactic :g:`solve_perm`: + + .. coqtop:: out + + Goal perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + + .. coqtop:: all abort + + solve_perm. + + .. coqtop:: out + + Goal perm nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + + .. coqtop:: all abort + + solve_perm. + + +Deciding intuitionistic propositional logic +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern matching on goals allows powerful backtracking when returning tactic +values. An interesting application is the problem of deciding intuitionistic +propositional logic. Considering the contraction-free sequent calculi LJT* of +Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the +tactic language as shown below. + +.. coqtop:: in reset + + Ltac basic := + match goal with + | |- True => trivial + | _ : False |- _ => contradiction + | _ : ?A |- ?A => assumption + end. + +.. coqtop:: in + + Ltac simplify := + repeat (intros; + match goal with + | H : ~ _ |- _ => red in H + | H : _ /\ _ |- _ => + elim H; do 2 intro; clear H + | H : _ \/ _ |- _ => + elim H; intro; clear H + | H : ?A /\ ?B -> ?C |- _ => + cut (A -> B -> C); + [ intro | intros; apply H; split; assumption ] + | H: ?A \/ ?B -> ?C |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear H + | intro; apply H; left; assumption ] + | intro; apply H; right; assumption ] + | H0 : ?A -> ?B, H1 : ?A |- _ => + cut B; [ intro; clear H0 | apply H0; assumption ] + | |- _ /\ _ => split + | |- ~ _ => red + end). + +.. coqtop:: in + + Ltac my_tauto := + simplify; basic || + match goal with + | H : (?A -> ?B) -> ?C |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; intro; assumption ]; my_tauto + | H : ~ ?A -> ?B |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; red; intro; assumption ]; my_tauto + | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) + end. + +The tactic ``basic`` tries to reason using simple rules involving truth, falsity +and available assumptions. The tactic ``simplify`` applies all the reversible +rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main +tactic to be called) simplifies with ``simplify``, tries to conclude with +``basic`` and tries several paths using the backtracking rules (one of the +four Dyckhoff’s rules for the left implication to get rid of the contraction +and the right ``or``). + +Having defined ``my_tauto``, we can prove tautologies like these: + +.. coqtop:: in + + Lemma my_tauto_ex1 : + forall A B : Prop, A /\ B -> A \/ B. + Proof. my_tauto. Qed. + +.. coqtop:: in + + Lemma my_tauto_ex2 : + forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Proof. my_tauto. Qed. + + +Deciding type isomorphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A trickier problem is to decide equalities between types modulo +isomorphisms. Here, we choose to use the isomorphisms of the simply +typed λ-calculus with Cartesian product and unit type (see, for +example, :cite:`RC95`). The axioms of this λ-calculus are given below. + +.. coqtop:: in reset + + Open Scope type_scope. + +.. coqtop:: in + + Section Iso_axioms. + +.. coqtop:: in + + Variables A B C : Set. + +.. coqtop:: in + + Axiom Com : A * B = B * A. + + Axiom Ass : A * (B * C) = A * B * C. + + Axiom Cur : (A * B -> C) = (A -> B -> C). + + Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). + + Axiom P_unit : A * unit = A. + + Axiom AR_unit : (A -> unit) = unit. + + Axiom AL_unit : (unit -> A) = A. + +.. coqtop:: in + + Lemma Cons : B = C -> A * B = A * C. + + Proof. + + intro Heq; rewrite Heq; reflexivity. + + Qed. + +.. coqtop:: in + + End Iso_axioms. + +.. coqtop:: in + + Ltac simplify_type ty := + match ty with + | ?A * ?B * ?C => + rewrite <- (Ass A B C); try simplify_type_eq + | ?A * ?B -> ?C => + rewrite (Cur A B C); try simplify_type_eq + | ?A -> ?B * ?C => + rewrite (Dis A B C); try simplify_type_eq + | ?A * unit => + rewrite (P_unit A); try simplify_type_eq + | unit * ?B => + rewrite (Com unit B); try simplify_type_eq + | ?A -> unit => + rewrite (AR_unit A); try simplify_type_eq + | unit -> ?B => + rewrite (AL_unit B); try simplify_type_eq + | ?A * ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + | ?A -> ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + end + with simplify_type_eq := + match goal with + | |- ?A = ?B => try simplify_type A; try simplify_type B + end. + +.. coqtop:: in + + Ltac len trm := + match trm with + | _ * ?B => let succ := len B in constr:(S succ) + | _ => constr:(1) + end. + +.. coqtop:: in + + Ltac assoc := repeat rewrite <- Ass. + +.. coqtop:: in + + Ltac solve_type_eq n := + match goal with + | |- ?A = ?A => reflexivity + | |- ?A * ?B = ?A * ?C => + apply Cons; let newn := len B in solve_type_eq newn + | |- ?A * ?B = ?C => + match eval compute in n with + | 1 => fail + | _ => + pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) + end + end. + +.. coqtop:: in + + Ltac compare_structure := + match goal with + | |- ?A = ?B => + let l1 := len A + with l2 := len B in + match eval compute in (l1 = l2) with + | ?n = ?n => solve_type_eq n + end + end. + +.. coqtop:: in + + Ltac solve_iso := simplify_type_eq; compare_structure. + +The tactic to judge equalities modulo this axiomatization is shown above. +The algorithm is quite simple. First types are simplified using axioms that +can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). +The normal forms are sequences of Cartesian products without a Cartesian product +in the left component. These normal forms are then compared modulo permutation +of the components by the tactic ``compare_structure``. If they have the same +length, the tactic ``solve_type_eq`` attempts to prove that the types are equal. +The main tactic that puts all these components together is ``solve_iso``. + +Here are examples of what can be solved by ``solve_iso``. + +.. coqtop:: in + + Lemma solve_iso_ex1 : + forall A B : Set, A * unit * B = B * (unit * A). + Proof. + intros; solve_iso. + Qed. + +.. coqtop:: in + + Lemma solve_iso_ex2 : + forall A B C : Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). + Proof. + intros; solve_iso. + Qed. + + Debugging |Ltac| tactics ------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0f78a9b84a..c728b925ac 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3561,7 +3561,7 @@ Automation .. tacn:: autorewrite with {+ @ident} :name: autorewrite - This tactic [4]_ carries out rewritings according to the rewriting rule + This tactic carries out rewritings according to the rewriting rule bases :n:`{+ @ident}`. Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until @@ -4661,9 +4661,12 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: none reset Parameter P : nat -> Prop. + + .. coqtop:: all abort + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: cycle 2. @@ -4679,9 +4682,8 @@ Non-logical tactics .. example:: - .. coqtop:: reset all + .. coqtop:: all abort - Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: swap 1 3. @@ -4694,9 +4696,8 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: all abort - Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: revgoals. @@ -4717,7 +4718,7 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: all abort Goal exists n, n=0. refine (ex_intro _ _ _). @@ -4746,39 +4747,6 @@ Non-logical tactics The ``give_up`` tactic can be used while editing a proof, to choose to write the proof script in a non-sequential order. -Simple tactic macros -------------------------- - -A simple example has more value than a long explanation: - -.. example:: - - .. coqtop:: reset all - - Ltac Solve := simpl; intros; auto. - - Ltac ElimBoolRewrite b H1 H2 := - elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ]. - -The tactics macros are synchronous with the Coq section mechanism: a -tactic definition is deleted from the current environment when you -close the section (see also :ref:`section-mechanism`) where it was -defined. If you want that a tactic macro defined in a module is usable in the -modules that require it, you should put it outside of any section. - -:ref:`ltac` gives examples of more complex -user-defined tactics. - -.. [1] Actually, only the second subgoal will be generated since the - other one can be automatically checked. -.. [2] This corresponds to the cut rule of sequent calculus. -.. [3] Reminder: opaque constants will not be expanded by δ reductions. -.. [4] The behavior of this tactic has changed a lot compared to the - versions available in the previous distributions (V6). This may cause - significant changes in your theories to obtain the same result. As a - drawback of the re-engineering of the code, this tactic has also been - completely revised to get a very compact and readable version. - Delaying solving unification constraints ---------------------------------------- @@ -4917,3 +4885,8 @@ Performance-oriented tactic variants Goal False. native_cast_no_check I. Fail Qed. + +.. [1] Actually, only the second subgoal will be generated since the + other one can be automatically checked. +.. [2] This corresponds to the cut rule of sequent calculus. +.. [3] Reminder: opaque constants will not be expanded by δ reductions. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ac079ea7d5..edec13f681 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -840,10 +840,11 @@ gives a way to let any arbitrary expression which is not handled by the custom entry ``expr`` be parsed or printed by the main grammar of term up to the insertion of a pair of curly brackets. -.. cmd:: Print Grammar @ident. +.. cmd:: Print Custom Grammar @ident. + :name: Print Custom Grammar - This displays the state of the grammar for terms and grammar for - patterns associated to the custom entry :token:`ident`. + This displays the state of the grammar for terms associated to + the custom entry :token:`ident`. Summary ~~~~~~~ diff --git a/ide/coqide.ml b/ide/coqide.ml index aa9e150fd5..4f00be27a1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -561,7 +561,7 @@ let update_status sn = | None -> "" | Some n -> ", proving " ^ n in - display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name); + display ("Ready"^ (if microPG#get then ", [μPG]" else "") ^ path ^ name); Coq.return () in Coq.bind (Coq.status false) next @@ -1200,7 +1200,7 @@ let build_ui () = item "Help for μPG mode" ~label:"Help for μPG mode" ~callback:(fun _ -> on_current_term (fun sn -> sn.messages#default_route#clear; - sn.messages#default_route#add_string (NanoPG.get_documentation ()))); + sn.messages#default_route#add_string (MicroPG.get_documentation ()))); item "About Coq" ~label:"_About" ~stock:`ABOUT ~callback:MiscMenu.about ]; @@ -1234,7 +1234,7 @@ let build_ui () = let () = vbox#pack toolbar#coerce in (* Emacs/PG mode *) - NanoPG.init w notebook all_menus; + MicroPG.init w notebook all_menus; (* On tab switch, reset, update location *) let _ = notebook#connect#switch_page ~callback:(fun n -> @@ -1251,7 +1251,7 @@ let build_ui () = let () = refresh_notebook_pos () in let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in let () = lower_hbox#pack ~expand:true status#coerce in - let () = push_info ("Ready"^ if nanoPG#get then ", [μPG]" else "") in + let () = push_info ("Ready"^ if microPG#get then ", [μPG]" else "") in (* Location display *) let l = GMisc.label diff --git a/ide/ide.mllib b/ide/ide.mllib index ed6520f29f..f8e8ff48d6 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -30,5 +30,5 @@ CoqOps Wg_Command Session Coqide_ui -NanoPG +MicroPG Coqide diff --git a/ide/nanoPG.ml b/ide/microPG.ml index d85d87142c..25cab4638c 100644 --- a/ide/nanoPG.ml +++ b/ide/microPG.ml @@ -65,14 +65,27 @@ type 'c entry = { } let mC = [`CONTROL] -let mM = [`MOD1] +let mM = + if Coq_config.arch = "Darwin" then + (* We add both MOD2 and META because both are + returned when pressing Command on MacOS X *) + [`CONTROL;`MOD2;`META] + else + [`MOD1] -let mod_of t x = List.for_all (fun m -> List.mem m (GdkEvent.Key.state t)) x +let mod_of t x = + let y = GdkEvent.Key.state t in + List.for_all (fun m -> List.mem m y) x && + List.for_all (fun m -> List.mem m x) y let pr_keymod l = - if l = mC then "C-" - else if l = mM then "M-" - else "" + if l = mC then + "Ctrl-" + else + if l = mM then + if Coq_config.arch = "Darwin" then "Ctrl-Cmd-" else "Meta-" + else + "" let mkE ?(mods=mC) key keyname doc ?(alias=[]) contents = List.map (fun (mods, key, keyname) -> { mods; key; keyname; doc; contents }) @@ -147,6 +160,13 @@ let emacs = insert emacs "Emacs" [] [ mkE _e "e" "Move to end of line" (Motion(fun s i -> (if not i#ends_line then i#forward_to_line_end else i), { s with move = None })); + mkE ~mods:mM _Right "->" "Move to end of buffer" (Motion(fun s i -> + i#forward_to_end, + { s with move = None })); + mkE ~mods:mM _Left "<-" "Move to start of buffer" (Motion(fun s i -> + let buffer = new GText.buffer i#buffer in + buffer#start_iter, + { s with move = None })); mkE _a "a" "Move to beginning of line" (Motion(fun s i -> (i#set_line_offset 0), { s with move = None })); mkE ~mods:mM _e "e" "Move to end of sentence" (Motion(fun s i -> @@ -286,9 +306,9 @@ let find gui (Step(here,konts)) t = else if k = _c && mod_of t mC && sel_nonempty () then ignore(run t gui (Action("Edit","Copy")) empty); - let cmp { key; mods } = key = k && mod_of t mods in - try `Do (List.find cmp here) with Not_found -> - try `Cont (List.find cmp konts).contents with Not_found -> `NotFound + let cmp { key; mods } = key = k && mod_of t mods in + try `Do (List.find cmp here) with Not_found -> + try `Cont (List.find cmp konts).contents with Not_found -> `NotFound let init w nb ags = let gui = { notebook = nb; action_groups = ags } in @@ -305,7 +325,7 @@ let init w nb ags = then false else begin eprintf "got key %s\n%!" (pr_key t); - if nanoPG#get then begin + if microPG#get then begin match find gui !cur t with | `Do e -> eprintf "run (%s) %s on %s\n%!" e.keyname e.doc (pr_status !status); @@ -320,4 +340,6 @@ let init w nb ags = -let get_documentation () = print_keypaths pg +let get_documentation () = + "Chars, words, lines and sentences below pertain to standard unicode segmentation rules\n" ^ + print_keypaths pg diff --git a/ide/nanoPG.mli b/ide/microPG.mli index bc9b39d823..bc9b39d823 100644 --- a/ide/nanoPG.mli +++ b/ide/microPG.mli diff --git a/ide/preferences.ml b/ide/preferences.ml index 3893d023bd..4e2e3f31e6 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -561,7 +561,8 @@ let tab_length = let highlight_current_line = new preference ~name:["highlight_current_line"] ~init:false ~repr:Repr.(bool) -let nanoPG = +let microPG = + (* Legacy name in preference is "nanoPG" *) new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool) let user_queries = @@ -799,7 +800,7 @@ let configure ?(apply=(fun () -> ())) parent = let () = button "Show progress bar" show_progress_bar in let () = button "Insert spaces instead of tabs" spaces_instead_of_tabs in let () = button "Highlight current line" highlight_current_line in - let () = button "Emacs/PG keybindings (μPG mode)" nanoPG in + let () = button "Emacs/PG keybindings (μPG mode)" microPG in let callback () = () in custom ~label box callback true in diff --git a/ide/preferences.mli b/ide/preferences.mli index 785c191b46..b01c4598d8 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -102,7 +102,7 @@ val show_progress_bar : bool preference val spaces_instead_of_tabs : bool preference val tab_length : int preference val highlight_current_line : bool preference -val nanoPG : bool preference +val microPG : bool preference val user_queries : (string * string) list preference val diffs : string preference diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml index 7d04c8f5a1..e1dcfcc6ce 100644 --- a/lib/acyclicGraph.ml +++ b/lib/acyclicGraph.ml @@ -721,7 +721,10 @@ module Make (Point:Point) = struct let rmap, csts = PSet.fold (fun u (rmap,csts) -> let arcu = repr g u in if PSet.mem arcu.canon kept then - PMap.add arcu.canon arcu.canon rmap, Constraint.add (u,Eq,arcu.canon) csts + let csts = if Point.equal u arcu.canon then csts + else Constraint.add (u,Eq,arcu.canon) csts + in + PMap.add arcu.canon arcu.canon rmap, csts else match PMap.find arcu.canon rmap with | v -> rmap, Constraint.add (u,Eq,v) csts diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 372e918948..1fca132655 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -701,7 +701,7 @@ let mkDestructEq : let changefun patvars env sigma = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in - Proofview.V82.of_tactic (change_in_concl None changefun) g2); + Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 99a9c1ab9a..a68efa4713 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1574,8 +1574,8 @@ let newfail n s = let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in (* For compatibility *) - let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in - let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in + let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in + let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") @@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id) | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> + convert_hyp ~check:false ~reorder:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f3bc791b8d..ffc3506a1f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1849,12 +1849,12 @@ let destructure_hyps = match destructurate_type env sigma typ with | Kapp(Nat,_) -> (tclTHEN - (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) decl)) (loop lit)) | Kapp(Z,_) -> (tclTHEN - (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) decl)) (loop lit)) | _ -> loop lit diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 813c521ab0..ad2ee821b3 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1235,12 +1235,19 @@ Notation ring_correct := (ring_correct Rsth Reqe ARth CRmorph pow_th cdiv_th). (* simplify a field expression into a fraction *) -(* TODO: simplify when den is constant... *) Definition display_linear l num den := - NPphi_dev l num / NPphi_dev l den. + let lnum := NPphi_dev l num in + match den with + | Pc c => if ceqb c cI then lnum else lnum / NPphi_dev l den + | _ => lnum / NPphi_dev l den + end. Definition display_pow_linear l num den := - NPphi_pow l num / NPphi_pow l den. + let lnum := NPphi_pow l num in + match den with + | Pc c => if ceqb c cI then lnum else lnum / NPphi_pow l den + | _ => lnum / NPphi_pow l den + end. Theorem Field_rw_correct n lpe l : Ninterp_PElist l lpe -> @@ -1252,7 +1259,18 @@ Theorem Field_rw_correct n lpe l : Proof. intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. rewrite (Fnorm_FEeval_PEeval _ _ H). - unfold display_linear; apply rdiv_ext; + unfold display_linear. + destruct (Nnorm _ _ _) as [c | | ] eqn: HN; + try ( apply rdiv_ext; + eapply ring_rw_correct; eauto). + destruct (ceqb_spec c cI). + set (nnum := NPphi_dev _ _). + apply eq_trans with (nnum / NPphi_dev l (Pc c)). + apply rdiv_ext; + eapply ring_rw_correct; eauto. + rewrite Pphi_dev_ok; try eassumption. + now simpl; rewrite H0, phi_1, <- rdiv1. + apply rdiv_ext; eapply ring_rw_correct; eauto. Qed. @@ -1266,8 +1284,19 @@ Theorem Field_rw_pow_correct n lpe l : Proof. intros Hlpe lmp lmp_eq fe nfe eq_nfe H; subst nfe lmp. rewrite (Fnorm_FEeval_PEeval _ _ H). - unfold display_pow_linear; apply rdiv_ext; - eapply ring_rw_pow_correct;eauto. + unfold display_pow_linear. + destruct (Nnorm _ _ _) as [c | | ] eqn: HN; + try ( apply rdiv_ext; + eapply ring_rw_pow_correct; eauto). + destruct (ceqb_spec c cI). + set (nnum := NPphi_pow _ _). + apply eq_trans with (nnum / NPphi_pow l (Pc c)). + apply rdiv_ext; + eapply ring_rw_pow_correct; eauto. + rewrite Pphi_pow_ok; try eassumption. + now simpl; rewrite H0, phi_1, <- rdiv1. + apply rdiv_ext; + eapply ring_rw_pow_correct; eauto. Qed. Theorem Field_correct n l lpe fe1 fe2 : diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 3f69701bd3..b02b97f656 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -89,10 +89,10 @@ let protect_red map env sigma c0 = EConstr.of_constr (eval 0 c) let protect_tac map = - Tactics.reduct_option (protect_red map,DEFAULTcast) None + Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) None let protect_tac_in map id = - Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)) + Tactics.reduct_option ~check:false (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)) (****************************************************************************) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index a4caeb403c..56f17703ff 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -427,7 +427,7 @@ let mk_anon_id t gl_ids = Id.of_string_soft (Bytes.to_string (loop (n - 1))) let convert_concl_no_check t = Tactics.convert_concl ~check:false t DEFAULTcast -let convert_concl t = Tactics.convert_concl t DEFAULTcast +let convert_concl ~check t = Tactics.convert_concl ~check t DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with @@ -799,7 +799,7 @@ let discharge_hyp (id', (id, mode)) gl = | NamedDecl.LocalDef (_, v, t), _ -> let id' = {(NamedDecl.get_annot decl) with binder_name = Name id'} in Proofview.V82.of_tactic - (convert_concl (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl + (convert_concl ~check:true (EConstr.of_constr (mkLetIn (id', v, t, cl')))) gl (* wildcard names *) let clear_wilds wilds gl = @@ -1170,7 +1170,7 @@ let gentac gen gl = ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); let gl = pf_merge_uc ucst gl in if conv - then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (old_cleartac clr) gl + then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl else genclrtac cl [c] clr gl let genstac (gens, clr) = @@ -1215,7 +1215,7 @@ let unprotecttac gl = let prot, _ = EConstr.destConst (project gl) c in Tacticals.onClause (fun idopt -> let hyploc = Option.map (fun id -> id, InHyp) idopt in - Proofview.V82.of_tactic (Tactics.reduct_option + Proofview.V82.of_tactic (Tactics.reduct_option ~check:false (Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fBETA; @@ -1282,10 +1282,10 @@ let clr_of_wgen gen clrs = match gen with | clr, _ -> old_cleartac clr :: clrs -let reduct_in_concl t = Tactics.reduct_in_concl (t, DEFAULTcast) +let reduct_in_concl ~check t = Tactics.reduct_in_concl ~check (t, DEFAULTcast) let unfold cl = let module R = Reductionops in let module F = CClosure.RedFlags in - reduct_in_concl (R.clos_norm_flags (F.mkflags + reduct_in_concl ~check:false (R.clos_norm_flags (F.mkflags (List.map (fun c -> F.fCONST (fst (destConst (EConstr.Unsafe.to_constr c)))) cl @ [F.fBETA; F.fMATCH; F.fFIX; F.fCOFIX]))) diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 58ce84ecb3..575f016014 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -252,7 +252,7 @@ val ssrevaltac : Tacinterp.interp_sign -> Tacinterp.Value.t -> unit Proofview.tactic val convert_concl_no_check : EConstr.t -> unit Proofview.tactic -val convert_concl : EConstr.t -> unit Proofview.tactic +val convert_concl : check:bool -> EConstr.t -> unit Proofview.tactic val red_safe : Reductionops.reduction_function -> diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 6493e2d86b..93c0d5c236 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -118,7 +118,7 @@ let newssrcongrtac arg ist gl = match try Some (pf_unify_HO gl_c (pf_concl gl) c) with exn when CErrors.noncritical exn -> None with | Some gl_c -> - tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c))) + tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true (fs gl_c c))) (t_ok (proj gl_c)) gl | None -> t_fail () gl in let mk_evar gl ty = @@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl = try beta env0 (EConstr.of_constr (eval_pattern env0 sigma0 concl0 rdx occ unfold)) with Option.IsNone -> errorstrm Pp.(str"Failed to unfold " ++ pr_econstr_pat env0 sigma t) in let _ = conclude () in - Proofview.V82.of_tactic (convert_concl concl) gl + Proofview.V82.of_tactic (convert_concl ~check:true concl) gl ;; let foldtac occ rdx ft gl = @@ -303,7 +303,7 @@ let foldtac occ rdx ft gl = let concl0 = EConstr.Unsafe.to_constr concl0 in let concl = eval_pattern env0 sigma0 concl0 rdx occ fold in let _ = conclude () in - Proofview.V82.of_tactic (convert_concl (EConstr.of_constr concl)) gl + Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.of_constr concl)) gl ;; let converse_dir = function L2R -> R2L | R2L -> L2R @@ -406,7 +406,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr gl = let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in let sigma, _ = Typing.type_of env sigma cl' in let gl = pf_merge_uc_of sigma gl in - Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl + Proofview.V82.of_tactic (convert_concl ~check:true cl'), rewritetac ?under dir r', gl else let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in let r3, _, r3t = @@ -644,7 +644,7 @@ let unfoldtac occ ko t kt gl = let cl' = EConstr.Vars.subst1 (pf_unfoldn [OnlyOccurrences [1], get_evalref env (project gl) c] gl c) cl in let f = if ko = None then CClosure.betaiotazeta else CClosure.betaiota in Proofview.V82.of_tactic - (convert_concl (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl + (convert_concl ~check:true (pf_reduce (Reductionops.clos_norm_flags f) gl cl')) gl let unlocktac ist args gl = let utac (occ, gt) gl = diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 01d71aa96a..4d4400a0f8 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -56,7 +56,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in let cl' = EConstr.mkLetIn (make_annot (Name id) Sorts.Relevant, c, cty, cl) in - Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl + Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl')) (introid id) gl open Util @@ -161,7 +161,7 @@ let havetac ist let gl, ty = pfe_type_of gl t in let ctx, _ = EConstr.decompose_prod_n_assum (project gl) 1 ty in let assert_is_conv gl = - try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl + try Proofview.V82.of_tactic (convert_concl ~check:true (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) Sorts.Relevant concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c @@ -471,7 +471,7 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = if hint = nohint then Proofview.tclUNIT () else - let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in + let betaiota = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in (* Usefulness of check_numgoals: tclDISPATCH would be enough, except for the error message w.r.t. the number of provided/expected tactics, as the last one is implied *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 17e4114958..91ff432364 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -110,7 +110,7 @@ let endclausestac id_map clseq gl_id cl0 gl = | _ -> EConstr.map (project gl) unmark c in let utac hyp = Proofview.V82.of_tactic - (Tactics.convert_hyp ~check:false (NamedDecl.map_constr unmark hyp)) in + (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.map_constr unmark hyp)) in let utacs = List.map utac (pf_hyps gl) in let ugtac gl' = Proofview.V82.of_tactic diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 1deb935d5c..4e0866a0c5 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1299,7 +1299,7 @@ let ssrpatterntac _ist arg gl = let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in let concl = EConstr.mkLetIn (make_annot (Name (Id.of_string "selected")) Sorts.Relevant, t, tty, concl_x) in - Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl + Proofview.V82.of_tactic (convert_concl ~check:true concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) let () = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 120b4e6f00..85e6f51387 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -90,48 +90,43 @@ module ReductionBehaviour = struct open Names open Libobject - type t = { - b_nargs: int; - b_recargs: int list; - b_dont_expose_case: bool; - } + type t = NeverUnfold | UnfoldWhen of when_flags | UnfoldWhenNoMatch of when_flags + and when_flags = { recargs : int list ; nargs : int option } + + let more_args_when k { recargs; nargs } = + { nargs = Option.map ((+) k) nargs; + recargs = List.map ((+) k) recargs; + } + + let more_args k = function + | NeverUnfold -> NeverUnfold + | UnfoldWhen x -> UnfoldWhen (more_args_when k x) + | UnfoldWhenNoMatch x -> UnfoldWhenNoMatch (more_args_when k x) let table = Summary.ref (GlobRef.Map.empty : t GlobRef.Map.t) ~name:"reductionbehaviour" - type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ] - type req = - | ReqLocal - | ReqGlobal of GlobRef.t * (int list * int * flag list) - let load _ (_,(_,(r, b))) = table := GlobRef.Map.add r b !table let cache o = load 1 o - let classify = function - | ReqLocal, _ -> Dispose - | ReqGlobal _, _ as o -> Substitute o + let classify (local,_ as o) = if local then Dispose else Substitute o - let subst (subst, (_, (r,o as orig))) = - ReqLocal, - let r' = fst (subst_global subst r) in if r==r' then orig else (r',o) + let subst (subst, (local, (r,o) as orig)) = + let r' = subst_global_reference subst r in if r==r' then orig + else (local,(r',o)) let discharge = function - | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) -> + | _,(false, (gr, b)) -> let b = if Lib.is_in_section gr then let vars = Lib.variable_section_segment_of_reference gr in let extra = List.length vars in - let nargs' = - if b.b_nargs = max_int then max_int - else if b.b_nargs < 0 then b.b_nargs - else b.b_nargs + extra in - let recargs' = List.map ((+) extra) b.b_recargs in - { b with b_nargs = nargs'; b_recargs = recargs' } + more_args extra b else b in - Some (ReqGlobal (gr, req), (ConstRef c, b)) + Some (false, (gr, b)) | _ -> None let rebuild = function @@ -148,55 +143,45 @@ module ReductionBehaviour = struct rebuild_function = rebuild; } - let set local r (recargs, nargs, flags as req) = - let nargs = if List.mem `ReductionNeverUnfold flags then max_int else nargs in - let behaviour = { - b_nargs = nargs; b_recargs = recargs; - b_dont_expose_case = List.mem `ReductionDontExposeCase flags } in - let req = if local then ReqLocal else ReqGlobal (r, req) in - Lib.add_anonymous_leaf (inRedBehaviour (req, (r, behaviour))) - ;; + let set ~local r b = + Lib.add_anonymous_leaf (inRedBehaviour (local, (r, b))) - let get r = - try - let b = GlobRef.Map.find r !table in - let flags = - if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold] - else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in - Some (b.b_recargs, (if Int.equal b.b_nargs max_int then -1 else b.b_nargs), flags) - with Not_found -> None + let get r = GlobRef.Map.find_opt r !table let print ref = let open Pp in let pr_global = Nametab.pr_global_env Id.Set.empty in match get ref with | None -> mt () - | Some (recargs, nargs, flags) -> - let never = List.mem `ReductionNeverUnfold flags in - let nomatch = List.mem `ReductionDontExposeCase flags in - let pp_nomatch = spc() ++ if nomatch then - str "but avoid exposing match constructs" else str"" in - let pp_recargs = spc() ++ str "when the " ++ + | Some b -> + let pp_nomatch = spc () ++ str "but avoid exposing match constructs" in + let pp_recargs recargs = spc() ++ str "when the " ++ pr_enum (fun x -> pr_nth (x+1)) recargs ++ str (String.plural (List.length recargs) " argument") ++ str (String.plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++ str " to a constructor" in - let pp_nargs = - spc() ++ str "when applied to " ++ int nargs ++ - str (String.plural nargs " argument") in - hov 2 (str "The reduction tactics " ++ - match recargs, nargs, never with - | _,_, true -> str "never unfold " ++ pr_global ref - | [], 0, _ -> str "always unfold " ++ pr_global ref - | _::_, n, _ when n < 0 -> - str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch - | _::_, n, _ when n > List.fold_left max 0 recargs -> - str "unfold " ++ pr_global ref ++ pp_recargs ++ - str " and" ++ pp_nargs ++ pp_nomatch - | _::_, _, _ -> - str "unfold " ++ pr_global ref ++ pp_recargs ++ pp_nomatch - | [], n, _ when n > 0 -> - str "unfold " ++ pr_global ref ++ pp_nargs ++ pp_nomatch - | _ -> str "unfold " ++ pr_global ref ++ pp_nomatch ) + let pp_nargs nargs = + spc() ++ str "when applied to " ++ int nargs ++ + str (String.plural nargs " argument") in + let pp_when = function + | { recargs = []; nargs = Some 0 } -> + str "always unfold " ++ pr_global ref + | { recargs = []; nargs = Some n } -> + str "unfold " ++ pr_global ref ++ pp_nargs n + | { recargs = []; nargs = None } -> + str "unfold " ++ pr_global ref + | { recargs; nargs = Some n } when n > List.fold_left max 0 recargs -> + str "unfold " ++ pr_global ref ++ pp_recargs recargs ++ + str " and" ++ pp_nargs n + | { recargs; nargs = _ } -> + str "unfold " ++ pr_global ref ++ pp_recargs recargs + in + let pp_behavior = function + | NeverUnfold -> str "never unfold " ++ pr_global ref + | UnfoldWhen x -> pp_when x + | UnfoldWhenNoMatch x -> pp_when x ++ pp_nomatch + in + hov 2 (str "The reduction tactics " ++ pp_behavior b) + end (** Machinery about stack of unfolded constants *) @@ -928,6 +913,7 @@ let equal_stacks sigma (x, l) (y, l') = let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in + let open ReductionBehaviour in let rec whrec cst_l (x, stack) = let () = if !debug_RAKAM then let open Pp in @@ -974,37 +960,42 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = else (* Looks for ReductionBehaviour *) match ReductionBehaviour.get (Globnames.ConstRef c) with | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags - || (nargs > 0 && Stack.args_size stack < nargs)) - then fold () - else (* maybe unfolds *) - if List.mem `ReductionDontExposeCase flags then - let app_sk,sk = Stack.strip_app stack in - let (tm',sk'),cst_l' = - whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) - in - let rec is_case x = match EConstr.kind sigma x with - | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x - | App (hd, _) -> is_case hd - | Case _ -> true - | _ -> false in - if equal_stacks sigma (x, app_sk) (tm', sk') - || Stack.will_expose_iota sk' - || is_case tm' - then fold () - else whrec cst_l' (tm', sk' @ sk) - else match recargs with - |[] -> (* if nargs has been specified *) - (* CAUTION : the constant is NEVER refold - (even when it hides a (co)fix) *) - whrec cst_l (body, stack) - |curr::remains -> match Stack.strip_n_app curr stack with - | None -> fold () - | Some (bef,arg,s') -> - whrec Cst_stack.empty - (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') - end + | Some behavior -> + begin match behavior with + | NeverUnfold -> fold () + | (UnfoldWhen { nargs = Some n } | + UnfoldWhenNoMatch { nargs = Some n } ) + when Stack.args_size stack < n -> + fold () + | UnfoldWhenNoMatch { recargs } -> (* maybe unfolds *) + let app_sk,sk = Stack.strip_app stack in + let (tm',sk'),cst_l' = + whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) + in + let rec is_case x = match EConstr.kind sigma x with + | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x + | App (hd, _) -> is_case hd + | Case _ -> true + | _ -> false in + if equal_stacks sigma (x, app_sk) (tm', sk') + || Stack.will_expose_iota sk' + || is_case tm' + then fold () + else whrec cst_l' (tm', sk' @ sk) + | UnfoldWhen { recargs } -> (* maybe unfolds *) + begin match recargs with + |[] -> (* if nargs has been specified *) + (* CAUTION : the constant is NEVER refold + (even when it hides a (co)fix) *) + whrec cst_l (body, stack) + |curr::remains -> match Stack.strip_n_app curr stack with + | None -> fold () + | Some (bef,arg,s') -> + whrec Cst_stack.empty + (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') + end + end + end | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack -> let kargs = CPrimitives.kind p in let (kargs,o) = Stack.get_next_primitive_args kargs stack in @@ -1015,41 +1006,45 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = else fold () | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let npars = Projection.npars p in - if not tactic_mode then - let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in - whrec Cst_stack.empty stack' - else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with - | None -> + if not tactic_mode then + let stack' = (c, Stack.Proj (p, Cst_stack.empty (*cst_l*)) :: stack) in + whrec Cst_stack.empty stack' + else match ReductionBehaviour.get (Globnames.ConstRef (Projection.constant p)) with + | None -> let stack' = (c, Stack.Proj (p, cst_l) :: stack) in - let stack'', csts = whrec Cst_stack.empty stack' in - if equal_stacks sigma stack' stack'' then fold () - else stack'', csts - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags - || (nargs > 0 && Stack.args_size stack < (nargs - (npars + 1)))) - then fold () - else - let recargs = List.map_filter (fun x -> - let idx = x - npars in - if idx < 0 then None else Some idx) recargs - in - match recargs with - |[] -> (* if nargs has been specified *) - (* CAUTION : the constant is NEVER refold - (even when it hides a (co)fix) *) + let stack'', csts = whrec Cst_stack.empty stack' in + if equal_stacks sigma stack' stack'' then fold () + else stack'', csts + | Some behavior -> + begin match behavior with + | NeverUnfold -> fold () + | (UnfoldWhen { nargs = Some n } + | UnfoldWhenNoMatch { nargs = Some n }) + when Stack.args_size stack < n - (npars + 1) -> fold () + | UnfoldWhen { recargs } + | UnfoldWhenNoMatch { recargs }-> (* maybe unfolds *) + let recargs = List.map_filter (fun x -> + let idx = x - npars in + if idx < 0 then None else Some idx) recargs + in + match recargs with + |[] -> (* if nargs has been specified *) + (* CAUTION : the constant is NEVER refold + (even when it hides a (co)fix) *) let stack' = (c, Stack.Proj (p, cst_l) :: stack) in - whrec Cst_stack.empty(* cst_l *) stack' - | curr::remains -> - if curr == 0 then (* Try to reduce the record argument *) - whrec Cst_stack.empty - (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack) - else - match Stack.strip_n_app curr stack with - | None -> fold () - | Some (bef,arg,s') -> - whrec Cst_stack.empty - (arg,Stack.Cst(Stack.Cst_proj p,curr,remains, - Stack.append_app [|c|] bef,cst_l)::s')) + whrec Cst_stack.empty(* cst_l *) stack' + | curr::remains -> + if curr == 0 then (* Try to reduce the record argument *) + whrec Cst_stack.empty + (c, Stack.Cst(Stack.Cst_proj p,curr,remains,Stack.empty,cst_l)::stack) + else + match Stack.strip_n_app curr stack with + | None -> fold () + | Some (bef,arg,s') -> + whrec Cst_stack.empty + (arg,Stack.Cst(Stack.Cst_proj p,curr,remains, + Stack.append_app [|c|] bef,cst_l)::s') + end) | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA -> apply_subst (fun _ -> whrec) [b] sigma refold cst_l c stack diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b5d3ff7627..aa39921ea2 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -21,13 +21,12 @@ exception Elimconst (** Machinery to customize the behavior of the reduction *) module ReductionBehaviour : sig - type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ] -(** [set is_local ref (recargs, nargs, flags)] *) - val set : - bool -> GlobRef.t -> (int list * int * flag list) -> unit - val get : - GlobRef.t -> (int list * int * flag list) option + type t = NeverUnfold | UnfoldWhen of when_flags | UnfoldWhenNoMatch of when_flags + and when_flags = { recargs : int list ; nargs : int option } + + val set : local:bool -> GlobRef.t -> t -> unit + val get : GlobRef.t -> t option val print : GlobRef.t -> Pp.t end diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index bcc20a41b4..231219c9de 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -664,18 +664,38 @@ let whd_nothing_for_iota env sigma s = it fails if no redex is around *) let rec red_elim_const env sigma ref u largs = + let open ReductionBehaviour in let nargs = List.length largs in let largs, unfold_anyway, unfold_nonelim, nocase = match recargs ref with | None -> largs, false, false, false - | Some (_,n,f) when nargs < n || List.mem `ReductionNeverUnfold f -> raise Redelimination - | Some (x::l,_,_) when nargs <= List.fold_left max x l -> raise Redelimination - | Some (l,n,f) -> - let is_empty = match l with [] -> true | _ -> false in - reduce_params env sigma largs l, - n >= 0 && is_empty && nargs >= n, - n >= 0 && not is_empty && nargs >= n, - List.mem `ReductionDontExposeCase f + | Some NeverUnfold -> raise Redelimination + | Some (UnfoldWhen { nargs = Some n } | UnfoldWhenNoMatch { nargs = Some n }) + when nargs < n -> raise Redelimination + | Some (UnfoldWhen { recargs = x::l } | UnfoldWhenNoMatch { recargs = x::l }) + when nargs <= List.fold_left max x l -> raise Redelimination + | Some (UnfoldWhen { recargs; nargs = None }) -> + reduce_params env sigma largs recargs, + false, + false, + false + | Some (UnfoldWhenNoMatch { recargs; nargs = None }) -> + reduce_params env sigma largs recargs, + false, + false, + true + | Some (UnfoldWhen { recargs; nargs = Some n }) -> + let is_empty = List.is_empty recargs in + reduce_params env sigma largs recargs, + is_empty && nargs >= n, + not is_empty && nargs >= n, + false + | Some (UnfoldWhenNoMatch { recargs; nargs = Some n }) -> + let is_empty = List.is_empty recargs in + reduce_params env sigma largs recargs, + is_empty && nargs >= n, + not is_empty && nargs >= n, + true in try match reference_eval env sigma ref with | EliminationCases n when nargs >= n -> @@ -737,6 +757,7 @@ and reduce_params env sigma stack l = a reducible iota/fix/cofix redex (the "simpl" tactic) *) and whd_simpl_stack env sigma = + let open ReductionBehaviour in let rec redrec s = let (x, stack) = decompose_app_vect sigma s in let stack = Array.to_list stack in @@ -761,30 +782,30 @@ and whd_simpl_stack env sigma = with Redelimination -> s') | Proj (p, c) -> - (try - let unf = Projection.unfolded p in - if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then - let npars = Projection.npars p in - (match unf, ReductionBehaviour.get (ConstRef (Projection.constant p)) with - | false, Some (l, n, f) when List.mem `ReductionNeverUnfold f -> - (* simpl never *) s' - | false, Some (l, n, f) when not (List.is_empty l) -> - let l' = List.map_filter (fun i -> - let idx = (i - (npars + 1)) in - if idx < 0 then None else Some idx) l in - let stack = reduce_params env sigma stack l' in - (match reduce_projection env sigma p ~npars - (whd_construct_stack env sigma c) stack - with - | Reduced s' -> redrec (applist s') - | NotReducible -> s') - | _ -> - match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with - | Reduced s' -> redrec (applist s') - | NotReducible -> s') - else s' - with Redelimination -> s') - + (try + let unf = Projection.unfolded p in + if unf || is_evaluable env (EvalConstRef (Projection.constant p)) then + let npars = Projection.npars p in + (match unf, get (ConstRef (Projection.constant p)) with + | false, Some NeverUnfold -> s' + | false, Some (UnfoldWhen { recargs } | UnfoldWhenNoMatch { recargs }) + when not (List.is_empty recargs) -> + let l' = List.map_filter (fun i -> + let idx = (i - (npars + 1)) in + if idx < 0 then None else Some idx) recargs in + let stack = reduce_params env sigma stack l' in + (match reduce_projection env sigma p ~npars + (whd_construct_stack env sigma c) stack + with + | Reduced s' -> redrec (applist s') + | NotReducible -> s') + | _ -> + match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with + | Reduced s' -> redrec (applist s') + | NotReducible -> s') + else s' + with Redelimination -> s') + | _ -> match match_eval_ref env sigma x stack with | Some (ref, u) -> diff --git a/proofs/logic.ml b/proofs/logic.ml index a01ddf2388..b79e1e6024 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -78,14 +78,6 @@ let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoS let check = ref false let with_check = Flags.with_option check -(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and - returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp env sigma check sign id f = - try apply_to_hyp sign id f - with Hyp_not_found -> - if check then error_no_such_hypothesis env sigma id - else sign - let check_typability env sigma c = if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () @@ -161,12 +153,14 @@ let reorder_context env sigma sign ord = step ord ords sign mt_q [] let reorder_val_context env sigma sign ord = +match ord with +| [] | [_] -> + (* Single variable-free definitions need not be reordered *) + sign +| _ :: _ :: _ -> let open EConstr in val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) - - - let check_decl_position env sigma sign d = let open EConstr in let x = NamedDecl.get_id d in @@ -556,25 +550,25 @@ and treat_case sigma goal ci lbrty lf acc' = (lacc,sigma,fi::bacc)) (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags -let convert_hyp check sign sigma d = +let convert_hyp ~check ~reorder env sigma d = let id = NamedDecl.get_id d in let b = NamedDecl.get_value d in - let env = Global.env () in - let reorder = ref [] in - let sign' = - apply_to_hyp env sigma check sign id - (fun _ d' _ -> - let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in - let env = Global.env_of_context sign in - if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then - user_err ~hdr:"Logic.convert_hyp" - (str "Incorrect change of the type of " ++ Id.print id ++ str "."); - if check && not (Option.equal (is_conv env sigma) b c) then - user_err ~hdr:"Logic.convert_hyp" - (str "Incorrect change of the body of "++ Id.print id ++ str "."); - if check then reorder := check_decl_position env sigma sign d; - map_named_decl EConstr.Unsafe.to_constr d) in - reorder_val_context env sigma sign' !reorder + let sign = Environ.named_context_val env in + match lookup_named_ctxt id sign with + | exception Not_found -> + if check then error_no_such_hypothesis env sigma id + else sign + | d' -> + let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in + if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the type of " ++ Id.print id ++ str "."); + if check && not (Option.equal (is_conv env sigma) b c) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the body of "++ Id.print id ++ str "."); + let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in + if reorder then reorder_val_context env sigma sign' (check_decl_position env sigma sign d) + else sign' (************************************************************************) (************************************************************************) diff --git a/proofs/logic.mli b/proofs/logic.mli index f99076db23..406fe57985 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -62,7 +62,7 @@ type 'id move_location = val pr_move_location : ('a -> Pp.t) -> 'a move_location -> Pp.t -val convert_hyp : bool -> Environ.named_context_val -> evar_map -> +val convert_hyp : check:bool -> reorder:bool -> Environ.env -> evar_map -> EConstr.named_declaration -> Environ.named_context_val val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 70854e6e3c..0857c05968 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -514,7 +514,7 @@ let autounfold_one db cl = in if did then match cl with - | Some hyp -> change_in_hyp None (make_change_arg c') hyp + | Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp | None -> convert_concl ~check:false c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") end diff --git a/tactics/equality.ml b/tactics/equality.ml index 3d760f1c3d..f049f8c568 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1613,10 +1613,10 @@ let cutSubstInHyp l2r eqn id = tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENFIRST (tclTHENLIST [ - (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly)); + (change_in_hyp ~check:true None (make_change_arg typ) (id,InHypTypeOnly)); (replace_core (onHyp id) l2r eqn) ]) - (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))) + (change_in_hyp ~check:true None (make_change_arg expected) (id,InHypTypeOnly))) end let try_rewrite tac = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5e8869f9b0..806c955591 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -145,7 +145,7 @@ let introduction id = let error msg = CErrors.user_err Pp.(str msg) -let convert_concl ?(check=true) ty k = +let convert_concl ~check ty k = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let conclty = Proofview.Goal.concl gl in @@ -163,12 +163,12 @@ let convert_concl ?(check=true) ty k = end end -let convert_hyp ?(check=true) d = +let convert_hyp ~check ~reorder d = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.concl gl in - let sign = convert_hyp check (named_context_val env) sigma d in + let sign = convert_hyp ~check ~reorder env sigma d in let env = reset_with_named_context sign env in Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ty @@ -176,7 +176,7 @@ let convert_hyp ?(check=true) d = end let convert_concl_no_check = convert_concl ~check:false -let convert_hyp_no_check = convert_hyp ~check:false +let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> @@ -701,7 +701,7 @@ let bind_red_expr_occurrences occs nbcl redexp = (** Tactic reduction modulo evars (for universes essentially) *) -let e_change_in_concl ?(check = false) (redfun, sty) = +let e_change_in_concl ~check (redfun, sty) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in @@ -709,16 +709,16 @@ let e_change_in_concl ?(check = false) (redfun, sty) = (convert_concl ~check c' sty) end -let e_change_in_hyp ?(check = false) redfun (id,where) = +let e_change_in_hyp ~check ~reorder redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let hyp = Tacmach.New.pf_get_hyp id gl in let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (convert_hyp ~check c) + (convert_hyp ~check ~reorder c) end -let e_change_in_hyps ?(check=true) f args = +let e_change_in_hyps ~check ~reorder f args = Proofview.Goal.enter begin fun gl -> let fold (env, sigma) arg = let (redfun, id, where) = f arg in @@ -728,7 +728,7 @@ let e_change_in_hyps ?(check=true) f args = raise (RefinerError (env, sigma, NoSuchHyp id)) in let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in - let sign = Logic.convert_hyp check (named_context_val env) sigma d in + let sign = Logic.convert_hyp ~check ~reorder env sigma d in let env = reset_with_named_context sign env in (env, sigma) in @@ -745,26 +745,26 @@ let e_change_in_hyps ?(check=true) f args = let e_reduct_in_concl = e_change_in_concl -let reduct_in_concl ?(check = false) (redfun, sty) = +let reduct_in_concl ~check (redfun, sty) = let redfun env sigma c = (sigma, redfun env sigma c) in e_change_in_concl ~check (redfun, sty) -let e_reduct_in_hyp ?(check=false) redfun (id, where) = +let e_reduct_in_hyp ~check ~reorder redfun (id, where) = let redfun _ env sigma c = redfun env sigma c in - e_change_in_hyp ~check redfun (id, where) + e_change_in_hyp ~check ~reorder redfun (id, where) -let reduct_in_hyp ?(check = false) redfun (id, where) = +let reduct_in_hyp ~check ~reorder redfun (id, where) = let redfun _ env sigma c = (sigma, redfun env sigma c) in - e_change_in_hyp ~check redfun (id, where) + e_change_in_hyp ~check ~reorder redfun (id, where) let revert_cast (redfun,kind as r) = if kind == DEFAULTcast then (redfun,REVERTcast) else r -let e_reduct_option ?(check=false) redfun = function - | Some id -> e_reduct_in_hyp ~check (fst redfun) id +let e_reduct_option ~check redfun = function + | Some id -> e_reduct_in_hyp ~check ~reorder:check (fst redfun) id | None -> e_change_in_concl ~check (revert_cast redfun) -let reduct_option ?(check = false) (redfun, sty) where = +let reduct_option ~check (redfun, sty) where = let redfun env sigma c = (sigma, redfun env sigma c) in e_reduct_option ~check (redfun, sty) where @@ -802,7 +802,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = | Some sigma -> (sigma, t') (* Use cumulativity only if changing the conclusion not a subterm *) -let change_on_subterm check cv_pb deep t where env sigma c = +let change_on_subterm ~check cv_pb deep t where env sigma c = let mayneedglobalcheck = ref false in let (sigma, c) = match where with | None -> @@ -825,15 +825,13 @@ let change_on_subterm check cv_pb deep t where env sigma c = end; (sigma, c) -let change_in_concl ?(check=true) occl t = +let change_in_concl ~check occl t = (* No need to check in e_change_in_concl, the check is done in change_on_subterm *) - e_change_in_concl ~check:false ((change_on_subterm check Reduction.CUMUL false t occl),DEFAULTcast) + e_change_in_concl ~check:false ((change_on_subterm ~check Reduction.CUMUL false t occl),DEFAULTcast) -let change_in_hyp ?(check=true) occl t id = - (* FIXME: we set the [check] flag only to reorder hypotheses in case of - introduction of dependencies in new variables. We should separate this - check from the conversion function. *) - e_change_in_hyp ~check (fun x -> change_on_subterm check Reduction.CONV x t occl) id +let change_in_hyp ~check occl t id = + (* Same as above *) + e_change_in_hyp ~check:false ~reorder:check (fun x -> change_on_subterm ~check Reduction.CONV x t occl) id let concrete_clause_of enum_hyps cl = match cl.onhyps with | None -> @@ -842,7 +840,7 @@ let concrete_clause_of enum_hyps cl = match cl.onhyps with | Some l -> List.map (fun ((occs, id), w) -> (id, occs, w)) l -let change ?(check=true) chg c cls = +let change ~check chg c cls = Proofview.Goal.enter begin fun gl -> let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in begin match cls.concl_occs with @@ -852,33 +850,34 @@ let change ?(check=true) chg c cls = <*> let f (id, occs, where) = let occl = bind_change_occurrences occs chg in - let redfun deep env sigma t = change_on_subterm check Reduction.CONV deep c occl env sigma t in + let redfun deep env sigma t = change_on_subterm ~check Reduction.CONV deep c occl env sigma t in (redfun, id, where) in - e_change_in_hyps ~check f hyps + (* Don't check, we do it already in [change_on_subterm] *) + e_change_in_hyps ~check:false ~reorder:check f hyps end let change_concl t = change_in_concl ~check:true None (make_change_arg t) (* Pour usage interne (le niveau User est pris en compte par reduce) *) -let red_in_concl = reduct_in_concl (red_product,REVERTcast) -let red_in_hyp = reduct_in_hyp red_product -let red_option = reduct_option (red_product,REVERTcast) -let hnf_in_concl = reduct_in_concl (hnf_constr,REVERTcast) -let hnf_in_hyp = reduct_in_hyp hnf_constr -let hnf_option = reduct_option (hnf_constr,REVERTcast) -let simpl_in_concl = reduct_in_concl (simpl,REVERTcast) -let simpl_in_hyp = reduct_in_hyp simpl -let simpl_option = reduct_option (simpl,REVERTcast) -let normalise_in_concl = reduct_in_concl (compute,REVERTcast) -let normalise_in_hyp = reduct_in_hyp compute -let normalise_option = reduct_option (compute,REVERTcast) -let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast) -let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast) -let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname) -let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast) -let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast) +let red_in_concl = reduct_in_concl ~check:false (red_product,REVERTcast) +let red_in_hyp = reduct_in_hyp ~check:false ~reorder:false red_product +let red_option = reduct_option ~check:false (red_product,REVERTcast) +let hnf_in_concl = reduct_in_concl ~check:false (hnf_constr,REVERTcast) +let hnf_in_hyp = reduct_in_hyp ~check:false ~reorder:false hnf_constr +let hnf_option = reduct_option ~check:false (hnf_constr,REVERTcast) +let simpl_in_concl = reduct_in_concl ~check:false (simpl,REVERTcast) +let simpl_in_hyp = reduct_in_hyp ~check:false ~reorder:false simpl +let simpl_option = reduct_option ~check:false (simpl,REVERTcast) +let normalise_in_concl = reduct_in_concl ~check:false (compute,REVERTcast) +let normalise_in_hyp = reduct_in_hyp ~check:false ~reorder:false compute +let normalise_option = reduct_option ~check:false (compute,REVERTcast) +let normalise_vm_in_concl = reduct_in_concl ~check:false (Redexpr.cbv_vm,VMcast) +let unfold_in_concl loccname = reduct_in_concl ~check:false (unfoldn loccname,REVERTcast) +let unfold_in_hyp loccname = reduct_in_hyp ~check:false ~reorder:false (unfoldn loccname) +let unfold_option loccname = reduct_option ~check:false (unfoldn loccname,DEFAULTcast) +let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast) (* The main reduction function *) @@ -893,6 +892,7 @@ let reduce redexp cl = let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in let nbcl = (if cl.concl_occs = NoOccurrences then 0 else 1) + List.length hyps in let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in + let reorder = match redexp with Fold _ | Pattern _ -> true | _ -> false in begin match cl.concl_occs with | NoOccurrences -> Proofview.tclUNIT () | occs -> @@ -907,7 +907,7 @@ let reduce redexp cl = let redfun _ env sigma c = redfun env sigma c in (redfun, id, where) in - e_change_in_hyps ~check f hyps + e_change_in_hyps ~check ~reorder f hyps end end @@ -2654,7 +2654,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = [ Proofview.Unsafe.tclEVARS sigma; convert_concl ~check:false newcl DEFAULTcast; intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false; - Tacticals.New.tclMAP (convert_hyp ~check:false) depdecls; + Tacticals.New.tclMAP (convert_hyp ~check:false ~reorder:false) depdecls; eq_tac ] end @@ -3061,8 +3061,8 @@ let unfold_body x = Tacticals.New.afterHyp x begin fun aft -> let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in let rfun _ _ c = replace_vars [x, xval] c in - let reducth h = reduct_in_hyp rfun h in - let reductc = reduct_in_concl (rfun, DEFAULTcast) in + let reducth h = reduct_in_hyp ~check:false ~reorder:false rfun h in + let reductc = reduct_in_concl ~check:false (rfun, DEFAULTcast) in Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc] end end diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b3914816ac..9eb8196280 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -33,8 +33,8 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) val introduction : Id.t -> unit Proofview.tactic -val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic -val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic +val convert_concl : check:bool -> types -> cast_kind -> unit Proofview.tactic +val convert_hyp : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic [@@ocaml.deprecated "use [Tactics.convert_concl]"] val convert_hyp_no_check : named_declaration -> unit Proofview.tactic @@ -152,13 +152,13 @@ type e_tactic_reduction = Reductionops.e_reduction_function type change_arg = patvar_map -> env -> evar_map -> evar_map * constr val make_change_arg : constr -> change_arg -val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic -val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic -val reduct_in_concl : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic -val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic -val change_in_concl : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic +val reduct_in_hyp : check:bool -> reorder:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic +val reduct_option : check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic +val reduct_in_concl : check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic +val e_reduct_in_concl : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic +val change_in_concl : check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic val change_concl : constr -> unit Proofview.tactic -val change_in_hyp : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> +val change_in_hyp : check:bool -> (occurrences * constr_pattern) option -> change_arg -> hyp_location -> unit Proofview.tactic val red_in_concl : unit Proofview.tactic val red_in_hyp : hyp_location -> unit Proofview.tactic @@ -180,7 +180,7 @@ val unfold_in_hyp : val unfold_option : (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic val change : - ?check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic + check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 7074ad2d41..3c1e27ba9d 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -27,7 +27,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and - 2nd arguments evaluate to a constructor and when applied to 2 arguments + 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat @@ -35,7 +35,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and - 2nd arguments evaluate to a constructor + 2nd arguments evaluate to a constructor Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : @@ -54,7 +54,7 @@ fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] -The reduction tactics unfold fcomp when applied to 6 arguments +The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat @@ -75,7 +75,7 @@ f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and - 5th arguments evaluate to a constructor + 5th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat @@ -84,7 +84,7 @@ f is not universe polymorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 4th, 5th and - 6th arguments evaluate to a constructor + 6th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat @@ -93,7 +93,7 @@ f is not universe polymorphic Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 5th, 6th and - 7th arguments evaluate to a constructor + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.f = forall v : unit, f 0 0 5 v 3 = 2 @@ -104,7 +104,7 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic The reduction tactics unfold f when the 5th, 6th and - 7th arguments evaluate to a constructor + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.f forall w : r, w 3 true = tt @@ -115,3 +115,13 @@ w 3 true = tt : Prop The command has indeed failed with message: Extra arguments: _, _. +volatilematch : nat -> nat + +volatilematch is not universe polymorphic +Argument scope is [nat_scope] +The reduction tactics always unfold volatilematch + but avoid exposing match constructs +volatilematch is transparent +Expands to: Constant Arguments.volatilematch + = fun n : nat => volatilematch n + : nat -> nat diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 844f96aaa1..b909f1b64c 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -55,3 +55,12 @@ Arguments w x%F y%B : extra scopes. Check (w $ $ = tt). Fail Arguments w _%F _%B. +Definition volatilematch (n : nat) := + match n with + | O => O + | S p => p + end. + +Arguments volatilematch / n : simpl nomatch. +About volatilematch. +Eval simpl in fun n => volatilematch n. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 3f0717666c..65c902202d 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -62,7 +62,7 @@ Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] The reduction tactics unfold myplus when the 2nd and - 3rd arguments evaluate to a constructor + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus @@ -101,7 +101,7 @@ Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] The reduction tactics unfold myplus when the 2nd and - 3rd arguments evaluate to a constructor + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.myplus @myplus diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 9d972a68f7..c1b9a2b1c6 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,15 @@ [< 0 > + < 1 > * < 2 >] : nat +Entry constr:myconstr is +[ "6" RIGHTA + [ ] +| "5" RIGHTA + [ SELF; "+"; NEXT ] +| "4" RIGHTA + [ SELF; "*"; NEXT ] +| "3" RIGHTA + [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [< b > + < b > * < 2 >] : nat [<< # 0 >>] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 81c64418cb..d1063bfd04 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -9,6 +9,7 @@ Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5). Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Print Custom Grammar myconstr. Axiom a : nat. Notation b := a. diff --git a/test-suite/output/bug_9370.out b/test-suite/output/bug_9370.out new file mode 100644 index 0000000000..0ff151c8b4 --- /dev/null +++ b/test-suite/output/bug_9370.out @@ -0,0 +1,12 @@ +1 subgoal + + ============================ + 1 = 1 +1 subgoal + + ============================ + 1 = 1 +1 subgoal + + ============================ + 1 = 1 diff --git a/test-suite/output/bug_9370.v b/test-suite/output/bug_9370.v new file mode 100644 index 0000000000..a7f4b7c23e --- /dev/null +++ b/test-suite/output/bug_9370.v @@ -0,0 +1,12 @@ +Require Import Reals. +Open Scope R_scope. +Goal 1/1=1. +Proof. + field_simplify (1/1). +Show. + field_simplify. +Show. + field_simplify. +Show. + reflexivity. +Qed. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 2533a39cc4..d047f7560e 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -151,8 +151,8 @@ Module M16. Local Notation "##" := 0 (in custom foo2). (* Test Print Grammar *) - Print Grammar foo. - Print Grammar foo2. + Print Custom Grammar foo. + Print Custom Grammar foo2. End M16. (* Example showing the need for strong evaluation of diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index 03e6ff61ab..38bed570a3 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -324,8 +324,6 @@ unfold cos_approx; simpl; unfold cos_term. rewrite !INR_IZR_INZ. simpl. field_simplify. -unfold Rdiv. -rewrite Rmult_0_l. apply Rdiv_lt_0_compat ; now apply IZR_lt. Qed. @@ -1612,4 +1610,3 @@ Lemma PI_ineq : Proof. intros; rewrite <- Alt_PI_eq; apply Alt_PI_ineq. Qed. - diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml index 603e00c815..a8c1a67f6f 100644 --- a/user-contrib/Ltac2/tac2tactics.ml +++ b/user-contrib/Ltac2/tac2tactics.ml @@ -167,7 +167,7 @@ let change pat c cl = delayed_of_tactic (Tac2ffi.app_fun1 c (array constr) constr subst) env sigma in let cl = mk_clause cl in - Tactics.change pat c cl + Tactics.change ~check:true pat c cl end let rewrite ev rw cl by = diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 59d2a66259..94d4ed80d1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1003,6 +1003,9 @@ GRAMMAR EXTEND Gram | IDENT "Grammar"; ent = IDENT -> (* This should be in "syntax" section but is here for factorization*) { PrintGrammar ent } + | IDENT "Custom"; IDENT "Grammar"; ent = IDENT -> + (* Should also be in "syntax" section *) + { PrintCustomGrammar ent } | IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir } | IDENT "Modules" -> { user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") } diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 843296d24e..50914959dc 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -50,10 +50,10 @@ let pr_entry e = str (Buffer.contents entry_buf) let pr_registered_grammar name = - let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in + let gram = Pcoq.find_grammars_by_name name in match gram with - | None -> user_err Pp.(str "Unknown or unprintable grammar entry.") - | Some entries -> + | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.") + | entries -> let pr_one (Pcoq.AnyEntry e) = str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++ pr_entry e @@ -85,6 +85,8 @@ let pr_grammar = function pr_entry Pvernac.Vernac_.gallina_ext | name -> pr_registered_grammar name +let pr_custom_grammar name = pr_registered_grammar ("constr:"^name) + (**********************************************************************) (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 38dbdf7e41..6435df23c7 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -57,6 +57,7 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> (** Print the Camlp5 state of a grammar *) val pr_grammar : string -> Pp.t +val pr_custom_grammar : string -> Pp.t val check_infix_modifiers : syntax_modifier list -> unit diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 889dbafabd..f2332bab8b 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -476,6 +476,8 @@ open Pputils keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent + | PrintCustomGrammar ent -> + keyword "Print Custom Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> keyword "Print LoadPath" ++ pr_opt DirPath.print dir | PrintModules -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 388f6957cf..c7795602aa 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1231,16 +1231,13 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red let clear_implicits_flag = List.mem `ClearImplicits flags in let default_implicits_flag = List.mem `DefaultImplicits flags in let never_unfold_flag = List.mem `ReductionNeverUnfold flags in + let nomatch_flag = List.mem `ReductionDontExposeCase flags in let err_incompat x y = user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in if assert_flag && rename_flag then err_incompat "assert" "rename"; - if Option.has_some nargs_for_red && never_unfold_flag then - err_incompat "simpl never" "/"; - if never_unfold_flag && List.mem `ReductionDontExposeCase flags then - err_incompat "simpl never" "simpl nomatch"; if clear_scopes_flag && extra_scopes_flag then err_incompat "clear scopes" "extra scopes"; if clear_implicits_flag && default_implicits_flag then @@ -1385,19 +1382,24 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) in - let rec narrow = function - | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl - | [] -> [] | _ :: tl -> narrow tl - in - let red_flags = narrow flags in - let red_modifiers_specified = - not (List.is_empty rargs) || Option.has_some nargs_for_red - || not (List.is_empty red_flags) + let red_behavior = + let open Reductionops.ReductionBehaviour in + match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with + | true, false, [], None -> Some NeverUnfold + | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch" + | true, _, _::_, _ -> err_incompat "simpl never" "!" + | true, _, _, Some _ -> err_incompat "simpl never" "/" + | false, false, [], None -> None + | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red; + recargs = rargs; + }) + | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red; + recargs = rargs; + }) in - if not (List.is_empty rargs) && never_unfold_flag then - err_incompat "simpl never" "!"; + let red_modifiers_specified = Option.has_some red_behavior in (* Actions *) @@ -1424,8 +1426,8 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red match sr with | ConstRef _ as c -> Reductionops.ReductionBehaviour.set - section_local c - (rargs, Option.default ~-1 nargs_for_red, red_flags) + ~local:section_local c (Option.get red_behavior) + | _ -> user_err (strbrk "Modifiers of the behavior of the simpl tactic "++ strbrk "are relevant for constants only.") @@ -1883,6 +1885,7 @@ let vernac_print ~(pstate : Proof_global.t option) ~atts = | PrintSectionContext qid -> print_sec_context_typ env sigma qid | PrintInspect n -> inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent + | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () | PrintModule qid -> print_module qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 34a9b9394a..6a51fdfe59 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -29,6 +29,7 @@ type printable = | PrintSectionContext of qualid | PrintInspect of int | PrintGrammar of string + | PrintCustomGrammar of string | PrintLoadPath of DirPath.t option | PrintModules | PrintModule of qualid |