diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index fc67bf88e..7150ce72b 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -23,39 +23,20 @@ jobs: coq_version: - 'dev' ocaml_version: - - '4.09-flambda' - target: [ local, hott, dune ] + - '4.14.2-flambda' + target: [ dune ] # hott, disabled for now fail-fast: false steps: - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 with: fetch-depth: 1 - name: Docker-Coq-Action uses: coq-community/docker-coq-action@v1 with: - opam_file: 'coq-equations.opam' + opam_file: 'rocq-equations.opam' coq_version: ${{ matrix.coq_version }} ocaml_version: ${{ matrix.ocaml_version }} - before_script: | - startGroup "Workaround permission issue" - sudo chown -R coq:coq . # <-- - ocamlfind list - endGroup - script: | - startGroup "Build project" - opam exec -- ./configure.sh --enable-${{matrix.target}} - opam exec -- make -j 2 ci-${{matrix.target}} - endGroup - uninstall: | - startGroup "Clean project" - make clean - endGroup - - - name: Revert permissions - # to avoid a warning at cleanup time - if: ${{ always() }} - run: sudo chown -R 1001:116 . # <-- diff --git a/.gitignore b/.gitignore index 16c9ed20d..9066e1ecc 100644 --- a/.gitignore +++ b/.gitignore @@ -4,11 +4,11 @@ *.vo *.vok *.vos -/Makefile.coq -/Makefile.coq.conf +/Makefile.rocq +/Makefile.rocq.conf /Makefile.hott /Makefile.hott.conf -src/META.coq-equations +src/META.rocq-equations *.bak *.cm* *.o @@ -51,7 +51,6 @@ docs/_site .merlin _build *.install -/test-suite/*.agdai /custom-HoTT/ /examples/Makefile /examples/Makefile.conf diff --git a/Makefile b/Makefile index ac1e24e9c..61267dd7a 100644 --- a/Makefile +++ b/Makefile @@ -2,12 +2,12 @@ .PHONY: all default makefiles clean-makefiles -all: Makefile.coq - $(MAKE) -f Makefile.coq +all: Makefile.rocq + $(MAKE) -f Makefile.rocq test -f Makefile.hott && $(MAKE) -f Makefile.hott || true -install: Makefile.coq - $(MAKE) -f Makefile.coq install +install: Makefile.rocq + $(MAKE) -f Makefile.rocq install test -f Makefile.hott && $(MAKE) -f Makefile.hott install || true makefiles: test-suite/Makefile examples/Makefile @@ -16,10 +16,10 @@ clean-makefiles: rm -f test-suite/Makefile examples/Makefile test-suite/Makefile: test-suite/_CoqProject - cd test-suite && coq_makefile -f _CoqProject -o Makefile + cd test-suite && rocq makefile -f _CoqProject -o Makefile examples/Makefile: examples/_CoqProject - cd examples && coq_makefile -f _CoqProject -o Makefile + cd examples && rocq makefile -f _CoqProject -o Makefile pre-all:: makefiles @@ -43,7 +43,7 @@ examples: examples/Makefile all .PHONY: examples clean: clean-makefiles makefiles - $(MAKE) -f Makefile.coq clean + $(MAKE) -f Makefile.rocq clean test -f Makefile.hott && make -f Makefile.hott clean || true $(MAKE) clean-examples clean-test-suite @@ -52,20 +52,20 @@ siteexamples: examples/*.glob doc: html mkdir -p html/api && ocamldoc -html -d html/api \ - `ocamlfind query -r coq-core.lib coq-core.kernel coq-core.tactics coq-core.proofs \ - coq-core.toplevel coq-core.ltac coq-core.plugins.extraction -i-format` \ + `ocamlfind query -r rocq-runtime.lib rocq-runtime.kernel rocq-runtime.tactics rocq-runtime.proofs \ + rocq-runtime.toplevel rocq-runtime.ltac rocq-runtime.plugins.extraction -i-format` \ -I src src/*.ml toplevel: src/equations_plugin.cma bytefiles "$(OCAMLFIND)" ocamlc -linkpkg -linkall -g $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ - -package coq-core.toplevel,coq-core.plugins.extraction \ + -package rocq-runtime.toplevel,rocq-runtime.plugins.extraction \ $< $(COQLIB)/toplevel/coqtop_bin.ml -o coqtop_equations dune:- dune build ci-dune: - opam install -j 2 -y coq-hott.dev + # opam install -j 2 -y coq-hott.dev dune build ci-hott: @@ -75,10 +75,10 @@ ci-hott: $(MAKE) -f Makefile.hott uninstall ci-local: - $(MAKE) -f Makefile.coq all + $(MAKE) -f Makefile.rocq all $(MAKE) test-suite examples - $(MAKE) -f Makefile.coq install - $(MAKE) -f Makefile.coq uninstall + $(MAKE) -f Makefile.rocq install + $(MAKE) -f Makefile.rocq uninstall ci: ci-local diff --git a/Makefile.coq.local b/Makefile.coq.local deleted file mode 100644 index d0f997e6a..000000000 --- a/Makefile.coq.local +++ /dev/null @@ -1,2 +0,0 @@ -CAMLPKGS+=-package coq-core.plugins.extraction,coq-core.plugins.cc -ci: all test-suite examples diff --git a/Makefile.hott.local b/Makefile.hott.local index d0f997e6a..27b8a9d47 100644 --- a/Makefile.hott.local +++ b/Makefile.hott.local @@ -1,2 +1,2 @@ -CAMLPKGS+=-package coq-core.plugins.extraction,coq-core.plugins.cc +CAMLPKGS+=-package rocq-runtime.plugins.extraction,rocq-runtime.plugins.cc ci: all test-suite examples diff --git a/Makefile.rocq.local b/Makefile.rocq.local new file mode 100644 index 000000000..27b8a9d47 --- /dev/null +++ b/Makefile.rocq.local @@ -0,0 +1,2 @@ +CAMLPKGS+=-package rocq-runtime.plugins.extraction,rocq-runtime.plugins.cc +ci: all test-suite examples diff --git a/README.md b/README.md index 5380edbc5..3a703ae4e 100644 --- a/README.md +++ b/README.md @@ -105,11 +105,11 @@ if you didn't do it yet: and run: - opam install coq-equations + opam install rocq-equations To get the beta versions of Coq, activate the repository: - opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev + opam repo add rocq-runtime-dev https://coq.inria.fr/opam/core-dev To get the development version of Equations, activate the repository: @@ -144,7 +144,7 @@ in your own directory. E.g. on Ubuntu, you would prefix the command with ## HoTT Variant -The HoTT variant of Equations works with the coq-hott library for Coq 8.13 and up. When using `opam`, simply install first the `coq-hott` library and `coq-equations` will install its HoTT variant. From source, first +The HoTT variant of Equations works with the coq-hott library for Coq 8.13 and up. When using `opam`, simply install first the `coq-hott` library and `rocq-equations` will install its HoTT variant. From source, first install `coq-hott` and then use: ./configure.sh --enable-hott diff --git a/_CoqProject b/_CoqProject index b645fa1c3..0db130865 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,4 @@ -src/META.coq-equations.in +src/META.rocq-equations.in -I src -I test-suite -Q src Equations diff --git a/configure.sh b/configure.sh index aa3731c4f..5f37e59af 100755 --- a/configure.sh +++ b/configure.sh @@ -1,16 +1,16 @@ #!/usr/bin/env bash -rm -f Makefile.coq Makefile.hott +rm -f Makefile.rocq Makefile.hott if [ "$1" == "--enable-hott" ] then - if command -v coqtop >/dev/null 2>&1 - then coq_makefile -f _HoTTProject -o Makefile.hott - else echo "Error: coqtop not found in path" + if command -v rocq >/dev/null 2>&1 + then rocq makefile -f _HoTTProject -o Makefile.hott + else echo "Error: rocq not found in path" fi fi -if command -v coqtop >/dev/null 2>&1 -then coq_makefile -f _CoqProject -o Makefile.coq -else echo "Error: coqtop not found in path" +if command -v rocq >/dev/null 2>&1 +then rocq makefile -f _CoqProject -o Makefile.rocq +else echo "Error: rocq not found in path" fi diff --git a/coq-equations.opam b/coq-equations.opam deleted file mode 100644 index 97fcfbc60..000000000 --- a/coq-equations.opam +++ /dev/null @@ -1,39 +0,0 @@ -opam-version: "2.0" -version: "dev" -authors: [ "Matthieu Sozeau " "Cyprien Mangin " ] -dev-repo: "git+https://github.com/mattam82/Coq-Equations.git" -maintainer: "matthieu.sozeau@inria.fr" -homepage: "https://mattam82.github.io/Coq-Equations" -bug-reports: "https://github.com/mattam82/Coq-Equations/issues" -license: "LGPL-2.1-only" -synopsis: "A function definition package for Coq" -description: """ -Equations is a function definition plugin for Coq, that allows the -definition of functions by dependent pattern-matching and well-founded, -mutual or nested structural recursion and compiles them into core -terms. It automatically derives the clauses equations, the graph of the -function and its associated elimination principle. -""" -tags: [ - "keyword:dependent pattern-matching" - "keyword:functional elimination" - "category:Miscellaneous/Coq Extensions" - "logpath:Equations" -] -build: [ - ["./configure.sh"] - [make "-j%{jobs}%"] -] -install: [ - [make "install"] -] -run-test: [ - [make "test-suite"] -] -depends: [ - "coq" {= "dev"} - "ocamlfind" {build} -] -#depopts: [ -# "coq-hott" {= "8.13"} -#] diff --git a/doc/equations.tex b/doc/equations.tex index 851b5130a..f45efbb79 100644 --- a/doc/equations.tex +++ b/doc/equations.tex @@ -64,11 +64,11 @@ \section*{Installation} Equations is available through the \texttt{opam}\footnote{\url{http://opam.ocaml.org}} package manager as -package \texttt{coq-equations}. To install it on an already existing +package \texttt{rocq-equations}. To install it on an already existing \texttt{opam} installation with the \Coq repository, simply input the command: \begin{verbatim} -# opam install coq-equations +# opam install rocq-equations \end{verbatim} If you want to use it with the \href{https://github.com/HoTT/HoTT}{HoTT library for Coq}, simply install the diff --git a/doc/equations_intro.v b/doc/equations_intro.v index 509ef8b72..b01e11ea9 100644 --- a/doc/equations_intro.v +++ b/doc/equations_intro.v @@ -12,11 +12,11 @@ session by importing the [Equations] module. *) From Stdlib Require Import Arith Lia Program. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* begin hide *) Check @eq. -Require Import Bvector. +From Stdlib Require Import Bvector. (* Derive DependentElimination for nat bool option sum Datatypes.prod list *) (* end hide *) diff --git a/doc/manual.tex b/doc/manual.tex index 470e293da..0da7d0e0b 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -376,7 +376,7 @@ \section{Changes} \begin{itemize} \item \textbf{Incompatible change} Support for the Coq-HoTT library, out of the box. This required a slight reorganization of the directories. To use this, simply install the \texttt{opam} \texttt{coq-hott} package before - \texttt{coq-equations} and \[\texttt{From Equations.HoTT Require Import All}\] + \texttt{rocq-equations} and \[\texttt{From Equations.HoTT Require Import All}\] Now \[\texttt{Require Import Equations.Equations}\] no longer works, use \texttt{Require Import Equations.Prop.Equations} (absolute path, future-proof) or \texttt{From Equations Require Import Equations} (relative path) to use the diff --git a/dune-project b/dune-project index 252a8bd4e..22584373a 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,38 @@ -(lang dune 2.5) -(using coq 0.2) +(lang dune 3.13) +(using coq 0.8) +(name rocq-equations) +(source (github mattam82/Coq-Equations)) +(license LGPL-2.1-only) +(authors "Matthieu Sozeau " "Cyprien Mangin ") +(maintainers "Matthieu Sozeau ") +(homepage "https://mattam82.github.io/Coq-Equations") -(name coq-equations) +(package + (name rocq-equations) + (synopsis "A function definition package for Rocq") + (description "Equations is a function definition plugin for Rocq, that allows the \ + definition of functions by dependent pattern-matching and well-founded, \ + mutual or nested structural recursion and compiles them into core \ + terms. It automatically derives the clauses equations, the graph of the \ + function and its associated elimination principle.") + (tags ("keyword:dependent pattern-matching" + "keyword:functional elimination" + "category:Miscellaneous/Coq Extensions" + "logpath:Equations")) + (depends + (ocaml (>= 4.10.0)) + (rocq-prover (>= "9.0~")) + (ppx_optcomp :build) + (ocaml-lsp-server :with-dev-setup))) +(package + (name rocq-equations-examples) + (synopsis "Examples") + (description "Do not install") + (depends rocq-equations)) + +(package + (name rocq-equations-tests) + (synopsis "Technical package to run tests") + (description "Do not install") + (depends rocq-equations)) diff --git a/examples/AlmostFull.v b/examples/AlmostFull.v index 65534553c..e3a853184 100644 --- a/examples/AlmostFull.v +++ b/examples/AlmostFull.v @@ -1,16 +1,20 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. + Require Import Examples.Fin. -Require Import Relations Utf8. -Require Import Relations Wellfounded. -Require Import Setoid RelationClasses Morphisms. -Require Import Lia. -Require Import Bool. -Require Import List Arith String. +From Stdlib Require Import Relations Utf8. +From Stdlib Require Import Relations Wellfounded. +From Stdlib Require Import Setoid RelationClasses Morphisms. +From Stdlib Require Import Lia. +From Stdlib Require Import Bool. +From Stdlib Require Import List Arith String. From Stdlib Require Import FunctionalExtensionality. Set Equations Transparent. Set Keyed Unification. Set Asymmetric Patterns. +Local Set Firstorder Solver auto with arith core datatypes. + +Ltac intuition_solver ::= auto with *. Section Equality. Class Eq (A : Type) := @@ -448,7 +452,7 @@ Section OplusUnary. End OplusUnary. -Set Firstorder Solver auto. +Local Set Firstorder Solver auto. (* Lemma oplus_unary_sec_intersection {X} (p q : WFT X) *) (* (C : X -> X -> Prop) (A B : X -> Prop) : *) @@ -609,7 +613,7 @@ Ltac destruct_pairs := repeat | [ x : _ /\ _ |- _ ] => destruct x end. -Require Import ssreflect. +From Stdlib Require Import ssreflect. Section SCT. @@ -1352,7 +1356,7 @@ Print Assumptions size_change_wf. Print Assumptions size_change_termination. Definition R := product_rel Nat.le Nat.le. -Require Import Lia. +From Stdlib Require Import Lia. Derive Signature for clos_trans_1n. @@ -1390,7 +1394,7 @@ Definition gnlex : (nat * nat) -> nat. red. simpl. red. compute. simpl. intuition lia. red. simpl. compute. intuition lia. Defined. -Require Import ExtrOcamlBasic. +From Stdlib Require Import ExtrOcamlBasic. (* Extraction gnlex. Print Assumptions gnlex. *) diff --git a/examples/Basics.v b/examples/Basics.v index 1babe7ada..5c53fe0a3 100644 --- a/examples/Basics.v +++ b/examples/Basics.v @@ -22,9 +22,10 @@ If running this interactively you can ignore the printing and hide directives which are just used to instruct coqdoc. *) -Require Import Program Bvector List Relations. +#[warnings="-deprecated-library-file-since-8.20"] +From Stdlib Require Import Program Bvector List Relations. From Equations Require Import Equations Signature. -Require Import Utf8. +From Stdlib Require Import Utf8. Set Keyed Unification. @@ -65,7 +66,7 @@ app_with (cons a v) l with app_with v l => { (** Structurally recursive function on natural numbers, with inspection of a recursive call result. We use [auto with arith] to discharge the obligations. *) -Obligation Tactic := program_simpl ; try CoreTactics.solve_wf ; auto with arith. +Local Obligation Tactic := program_simpl ; try CoreTactics.solve_wf ; auto with arith. Equations equal (n m : nat) : { n = m } + { n <> m } := equal O O := in_left ; @@ -152,7 +153,7 @@ sublist p (cons x xs) with p x := { (** Well-founded definitions: *) -Require Import Arith Wf_nat. +From Stdlib Require Import Arith Wf_nat. (** One can declare new well-founded relations using instances of the [WellFounded] typeclass. *) #[local] Instance wf_nat : WellFounded lt := lt_wf. @@ -230,6 +231,7 @@ Equations app {A} (l l' : list A) : list A := app nil l := l; app (cons a v) l := cons a (app v l). +#[warnings="-notation-overridden"] Infix "++" := app (right associativity, at level 60) : list_scope. Equations rev_acc {A} (l : list A) (acc : list A) : list A := @@ -336,7 +338,8 @@ Qed. (* Eval compute in @zip''. *) -Require Import Bvector. +#[warnings="-deprecated-library-file-since-8.20"] +From Stdlib Require Import Bvector. (** This function can also be defined by structural recursion on [m]. *) diff --git a/examples/Equations_Tutorial_VeriMag.v b/examples/Equations_Tutorial_VeriMag.v new file mode 100644 index 000000000..f457c6cfb --- /dev/null +++ b/examples/Equations_Tutorial_VeriMag.v @@ -0,0 +1,796 @@ +(** printing now %\coqdoctac{now}% *) +(** printing elimination %\coqdoctac{elimination}% *) +(** printing Hint %\coqdockw{Hint}% *) +(** printing Rewrite %\coqdockw{Rewrite}% *) +(** printing Program %\name{Program}% *) +(** printing <= %\rightarrow% #⇐# *) +(** printing funelim %\coqdoctac{funelim}% *) +(** printing Derive %\coqdockw{Derive}% *) +(** printing Signature %\coqdocind{Signature}% *) +(** printing NoConfusion %\coqdocind{NoConfusion}% *) +(** printing simp %\coqdoctac{simp}% *) +(** printing <= %$\Leftarrow$% *) +(** printing <=? %$\le?$% *) +(* begin hide *) + +Set Warnings "-undo-batch-mode". +Set Warnings "-notation-overridden". +From Stdlib Require Import Utf8 Arith Compare_dec List Lia. +From Stdlib Require Import Relation_Operators Program. + +Close Scope program_scope. +Close Scope list_scope. +Arguments map {A B}. + +(* end hide *) + +(** [Equations] is a plugin for %\cite{Coq}% that comes with a few support modules defining + classes and tactics for running it. We will introduce its main + features through a handful of examples. We start our Coq primer + session by importing the [Equations] module. *) + +From Equations.Prop Require Import Equations. + +(* begin hide *) +Close Scope list_scope. +Set Equations Transparent. +Import EquationsNotations. +Local Open Scope equations_scope. +Extraction Inline Logic.transport. +(* end hide *) + +(** * Inductive types + + In its simplest form, [Equations] allows to define functions on inductive datatypes. + Take for example the booleans defined as an inductive type with two constructors + [true] and [false]: + [[ + Inductive bool : Set := true : bool | false : bool + ]] + + We can define the boolean negation as follows: *) + +Equations neg (b : bool) : bool := +neg true := false ; +neg false := true. + +(** [Equations] declarations are formed by a signature definition and a set of _clauses_ + that must form a _covering_ of this signature. The compiler is then expected to + automatically find a corresponding case-splitting tree (i.e. [match .. with]) + that implements the function. + In this case, it simply needs to split on the single variable [b] to + produce two new _programming problems_ [neg true] and [neg false] that are directly + handled by the user clauses. We will see in more complex examples that this search + for a splitting tree may be non-trivial. *) + +Print neg. + + +(** * Reasoning principles + + In the setting of a proof assistant like Coq, we need not only the ability + to define complex functions but also get good reasoning support for them. + Practically, this translates to the ability to simplify applications of functions + appearing in the goal and to give strong enough proof principles for (recursive) + definitions. + + ** Rewrite rules + + [Equations] provides this through an automatic generation of proofs related to + the function. Namely, each defining equation gives rise to a lemma stating the + equality between the left and right hand sides. These equations can be used as + rewrite rules for simplification during proofs, without having to rely on the + fragile simplifications implemented by raw reduction. *) + +Lemma negb_invol : + forall b, neg (neg b) = b. +Proof. + destruct b. rewrite neg_equation_1. + all:simp neg. all:easy. +Qed. + +(** The [simp foo] tactic is an alias to [autorewrite with foo], using the rewrite + rules associated to constant foo. *) + +(** ** Elimination principle + + We can also generate the inductive graph of any [Equations] definition, + giving the strongest elimination principle on the function. + + I.e., for [neg] the inductive graph is defined as: [[ +Inductive neg_graph : bool -> bool -> Set := +| neg_graph_equation_1 : neg_graph true false +| neg_graph_equation_2 : neg_graph false true ]] + + Along with a proof of [neg_graph_correct : ∀ b, neg_graph b (neg b)], we can + eliminate any call to [neg] specializing its argument and result in a single command. + + Suppose we want to show that [neg] is involutive for example, our goal will + look like: [[ + b : bool + ============================ + neg (neg b) = b ]] + + An application of the tactic [funelim (neg b)] will produce two goals corresponding to + the splitting done in [neg]: [neg false = true] and [neg true = false]. + These correspond exactly to the rewriting lemmas generated for [neg]. + + In the following sections we will show how these ideas generalize to more complex + types and definitions involving dependencies, overlapping clauses and recursion. *) + +Print neg_graph. +Check neg_graph_correct. + +Lemma neg_inv : forall b, neg (neg b) = b. +Proof. intros b. funelim (neg b). all:now reflexivity. Defined. + +Module BuildingUp. + +(** Equations naturally supports notations: the left-hand + sides of clauses only have to be elaborated to well-typed patterns for the given argument types. *) + +Declare Scope mylist_scope. +Notation "[]" := nil : mylist_scope. +Notation "[ x ]" := (cons x nil) : mylist_scope. +Notation "x :: l" := (cons x l) : mylist_scope. +Open Scope mylist_scope. + +(** ** Recursive inductive types + + Of course with inductive types comes recursion. Coq accepts a subset + of the structurally recursive definitions by default (it is + incomplete due to its syntactic nature). We will use this as a first + step towards a more robust treatment of recursion via well-founded + relations. A classical example is list concatenation: *) + + (** *** Recursive notations + + One can also define notations for recursive definitions, by + first _reserving_ them: +*) + +Reserved Notation "x +++ y" (at level 60, right associativity). + +(** Here we declare [x ++ y] as an infix operation with right associativity, + so [x ++ y ++ z] will mean [x ++ (y ++ z)]. *) + +Equations app {A} (l l' : list A) : list A := { + nil +++ l' := l' ; + (a :: l) +++ l' := a :: (l +++ l') } +where "x +++ y" := (app x y). + +(** We can directly bind and use this notation to write the left-hand side + and right-hand sides of the program. + + Remark: We enclose the clauses around curly braces, to scope the notation around the + whole program. Otherwise the notation [where] clause would only apply to the body + of the second branch. *) + +(** *** Functional elimination and recursion + + Recursive definitions like [app] can be unfolded easily so proving the + equations as rewrite rules is direct. The induction principle associated + to this definition is more interesting however. We can derive from it the + following _elimination_ principle for calls to [app]: [[ + app_elim : + forall P : forall (A : Type) (l l' : list A), list A -> Prop, + (forall (A : Type) (l' : list A), P A nil l' l') -> + (forall (A : Type) (a : A) (l l' : list A), + P A l l' (app l l') -> P A (a :: l) l' (a :: app l l')) -> + forall (A : Type) (l l' : list A), P A l l' (app l l') ]] + Using this eliminator, we can write proofs exactly following the + structure of the function definition, instead of redoing the splitting + and recursion. This idea is already present in the [Function] package + %\cite{Barthe:2006gp}% that derives induction principles from + function definitions. + + In the example below we can see that we get an instantiated induction + hypothesis corresponding to the recursive call to [app] in the [_ :: _] branch. +*) + +About app_elim. + +Lemma app_assoc {A} (x y z : list A) : + x +++ y +++ z = (x +++ y) +++ z. +Proof. + funelim (x +++ y); simpl; auto. + now rewrite H. +Qed. + +Lemma app_nil_r {A} (l : list A) : + l +++ [] = l. +Proof. funelim (l +++ []); auto. now rewrite H. Qed. + +(** ** Moving to the left + + The structure of real programs is richer than a simple case tree on + the original arguments in general. In the course of a computation, we + might want to scrutinize intermediate results (e.g. coming from + function calls) to produce an answer. This literally means adding a + new pattern to the left of our equations made available for further + refinement. This concept is know as with clauses in the Agda + %\cite{norell:thesis}% community and was first presented and + implemented in the Epigram language + %\cite{DBLP:journals/jfp/McBrideM04}%. + + The compilation of with clauses and its treatment for generating + equations and the induction principle are quite involved in the + presence of dependencies, but the basic idea is to add a new case + analysis to the program. To compute the type of the new subprogram, + we actually abstract the discriminee term from the expected type of + the clause, so that the type can get refined in the subprogram. In + the non-dependent case this does not change anything though. + + Each [with] node generates an auxiliary definition from the clauses + in the curly brackets, taking the additional object as argument. The + equation for the with node will simply be an indirection to the + auxiliary definition and simplification will continue as usual with + the auxiliary definition's rewrite rules. *) + +Equations filter {A} (l : list A) + (p : A -> bool) : + list A := +filter [] p := [] ; +filter (a :: l) p with (p a) => { + | true := a :: filter l p ; + | false := filter l p }. + +(** *** Elimination principle + + Introduction of these intermediate computations are also reflected + in the elimination principle: the motive for elimination of each + subprogram is augmented with an equality proof between the new + argument variable and the effective argument it is called with (here + [p a]). We have three subgoals corresponding to the leaves (right-hand sides) + of the program. *) + +Lemma filter_true {A} (l : list A) : + filter l (fun x => true) = l. +Proof. + funelim (filter l (fun _ => true)). + - (* [l = []] *) reflexivity. + - (* [l = (a :: l)] and [(fun x => true) a = true] *) + simpl. now rewrite H. + - (* [l = (a :: l)] and [(fun x => true) a = false] *) + discriminate. +Qed. + +(** ** Auxiliary local functions + + A common idiom of functional programming is the worker/wrapper + pattern. It usually involves a recursive function that computes the + result, wrapped in a toplevel function calling it with specific + parameters. The paradigmatic example is probably list reversal, + whose tail-recursive version can be written using a recursive local + where clause: *) + +Equations rev_acc {A} (l : list A) : list A := + rev_acc l := go l [] + where go : + list A -> list A -> list A := + go [] acc := acc; + go (hd :: tl) acc := go tl (hd :: acc). + +(** The [where] clause acts like [where] in Haskell or Agda, + or [let] in OCaml: + it defines an auxilliary function or value, which might use more pattern-matching + and be recursive itself. The auxilliary function's scope is the body of the program + which comes _before_ the [where], here [go l []]. *) + +(** A typical issue with such accumulating functions is + that one has to write lemmas in two versions to prove properties about them, once about the internal [go] function and then on its wrapper. Using the functional elimination principle associated to [rev_acc], we can show both properties simultaneously. + + First, lets define the usual list reversal function, + which is not tail recursive and might hence incur stack overflows on large lists: *) + +Equations rev {A} (l : list A) : list A := +rev [] := []; +rev (a :: l) := rev l +++ [a]. + +Lemma rev_acc_eq : forall {A} (l : list A), + rev_acc l = rev l. +Proof. + (** We apply functional elimination on the [rev_acc l] call. The eliminator expects two predicates: + one for the wrapper and another for the worker. + For the wrapper, we give the expected final goal but for the worker we have to invent a kind of loop invariant: here that the result of the whole [go acc l] call is equal to [rev l ++ acc]. *) + + apply (rev_acc_elim + (fun A l revaccl => revaccl = rev l) + (fun A _ l acc go_res => + go_res = rev l +++ acc)). + all:intros A l; simpl; trivial. + + (** Functional elimination provides us with the worker + property for the initial [go [] l] call, i.e. that it is equal to [rev l ++ []], which trivially gives us the result. *) + + + intros IH. now rewrite app_nil_r in IH. + + (* For the worker proof itself, the result follows from associativity of + list concatenation and the induction hypothesis. *) + intros a l1 l' IH. + rewrite <- app_assoc. simpl. assumption. +Qed. + +(** *** The Worker/Wrapper and Well-Founded Recursion + + Sometimes the natural expression of an algorithm in the worker/wrapper + pattern requires well-founded recursion: here we take an example + algorithm translated from Haskell whose termination is justified by a measure. + Note that the [worker] subprogram's termination measure and + implementation depends on the enclosing [k] argument which is captured + in the where clause. Termination is justified by a simple arithmetic argument. *) + + Local Obligation Tactic := idtac. + + Equations? isPrime (n : nat) : bool := + isPrime 0 := false; + isPrime 1 := false; + isPrime 2 := true; + isPrime k := worker 2 + where worker (n' : nat) : bool by wf (k - n') lt := + worker n' with ge_dec n' k := + { | left H := true; + | right H := + if Nat.eqb (Nat.modulo k n') 0 then false + else worker (S n') }. +Proof. lia. (* Linear arithmetic reasoning *) Qed. + +Import ListNotations. + +Eval vm_compute in map isPrime [13; 14; 28; 29]. + +End BuildingUp. + +(** * Dependent types + + Coq supports writing dependent functions, in other words, it gives the ability to + make the results _type_ depend on actual _values_, like the arguments of the function. + A simple example is given below of a function which decides the equality of two + natural numbers, returning a sum type carrying proofs of the equality or disequality + of the arguments. The sum type [{ A } + { B }] is a constructive variant of disjunction + that can be used in programs to give at the same time a boolean algorithmic information + (are we in branch [A] or [B]) and a _logical_ information (a proof witness of [A] or [B]). + Hence its constructors [left] and [right] take proofs as arguments. The [eq_refl] proof + term is the single proof of [x = x] (the [x] is generaly infered automatically). +*) + +Equations equal (n m : nat) : { n = m } + { n <> m } := +equal O O := left eq_refl ; +equal (S n) (S m) with equal n m := { + equal (S n) (S ?(n)) (left eq_refl) := left eq_refl ; + equal (S n) (S m) (right p) := right _ } ; +equal x y := right _. + +(** Of particular interest here is the inner program refining the recursive result. + As [equal n m] is of type [{ n = m } + { n <> m }] we have two cases to consider: + + - Either we are in the [left p] case, and we know that [p] is a proof of [n = m], + in which case we can do a nested match on [p]. The result of matching this equality + proof is to unify [n] and [m], hence the left hand side patterns become [S n] and + [S ?(n)] and the return type of this branch is refined to [{ n = n } + { n <> n }]. + We can easily provide a proof for the left case. + + - In the right case, we mark the proof unfilled with an underscore. This will + generate an obligation for the hole, that can be filled automatically by a + predefined tactic or interactively by the user in proof mode (this uses the + same obligation mechanism as the Program extension + %\cite{sozeau.Coq/FingerTrees/article}%). In this case the automatic tactic + is able to derive by itself that [n <> m -> S n <> S m]. + + Dependent types are also useful to turn partial functions into total functions by + restricting their domain. Typically, we can force the list passed to [head] + to be non-empty using the specification: +*) + +(** ** Inductive families + + The next step is to make constraints such as non-emptiness part of the + datatype itself. This ability is provided through inductive families in + Coq %\cite{paulin93tlca}%, which are a similar concept to the generalization + of algebraic datatypes to GADTs in functional languages like Haskell + %\cite{GADTcomplete}%. Families provide a way to associate to each constructor + a different type, making it possible to give specific information about a value + in its type. + + *** Indexed datatypes + + Functions on [vec]s provide more stricking examples of this + situation. The [vec] family is indexed by a natural number + representing the size of the vector: *) + +Module Vector. + +Inductive vec (A : Type) : nat -> Type := +| nil : vec A 0 +| cons n : A -> vec A n -> vec A (S n). + +Derive Signature for vec. + +(** + The empty vector [nil] has size [O] while the cons operation + increments the size by one. We declare notations similar to lists + on vectors, as the size information will generally be left _implicit_. *) + +Arguments nil {A}. +Arguments cons {A n}. + +Notation "x :: v" := (cons x v) : vector_scope. +Notation "[ ]" := nil : vector_scope. +Notation "[ x ]" := (cons x nil) : vector_scope. +Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) .. )) : vector_scope. + +End Vector. +Import Vector. +Local Open Scope vector_scope. + +(** Now let us define the usual map on vectors. *) +Equations map {A B} (f : A -> B) {n} (v : vec A n) : + vec B n := +map f (n:=?(0)) [] := [] ; +map f (a :: v) := f a :: map f v. + +Print map. + +(** Here the value of the index representing the size of the vector + is directly determined by the constructor, hence in the case tree + we have no need to eliminate [n]. This means in particular that + the function [map] does not do any computation with [n], and + the argument could be eliminated in the extracted code. + In other words, it provides only _logical_ information about + the shape of [v] but no computational information. + + The [map] function works on every member of the [vec] family, + but some functions may work only for some subfamilies, for example + [tail]: +*) + +Equations tail {A n} (v : vec A (S n)) : vec A n := +tail (a :: v') := v'. + +(** The type of [v] ensures that [tail] can only be applied to + non-empty vectors, moreover the patterns only need to consider + constructors that can produce objects in the subfamily [vec A (S n)], + excluding [nil]. The pattern-matching compiler uses unification + with the theory of constructors to discover which cases need to + be considered and which are impossible. In this case the failed + unification of [0] and [S n] shows that the [nil] case is impossible. + This powerful unification engine running under the hood permits to write + concise code where all uninteresting cases are handled automatically. *) + +Equations head {A n} (v : vec A (S n)) : A := +head (a :: v') := a. + +(** ** Derived notions, No-Confusion + + For this to work smoothlty, the package requires some derived definitions + on each (indexed) family, which can be generated automatically using + the generic [Derive] command. Here we ask to generate the homogeneous no-confusion principles for vectors: *) + +Derive NoConfusionHom for vec. + +Equations noconf {A n} (v v' : vec A n) : Prop := +noconf [] [] := True; +noconf (a :: v) (a' :: v') := (a = a' /\ v = v'). + +(* + proof that [v = v' <~> noconf v v'] *) + +(** The precise specification of these derived definitions can be found in the manual + section %(\S \ref{manual})%. Signature is used to "pack" a value in an inductive family + with its index, e.g. the "total space" of every index and value of the family. This + can be used to derive the heterogeneous no-confusion principle for the family, which + allows to discriminate between objects in potentially different instances/fibers of the family, + or deduce injectivity of each constructor. + + The [NoConfusionHom] variant derives + the homogeneous no-confusion principle between two objects in the _same_ instance + of the family, e.g. to simplify equations of the form [nil = nil :> vec A 0]. + This last principle can only be defined when pattern-matching on the inductive family + does not require the [K] axiom and will otherwise fail. + + ** Unification and indexed datatypes + + Back to our example, of course the equations and the induction principle are simplified in a + similar way. If we encounter a call to [tail] in a proof, we can + use the following elimination principle to simplify both the call and the + argument which will be automatically substituted by an object of the form + [cons _ _ _]:[[ +forall P : forall (A : Type) (n : nat), vec A (S n) -> vec A n -> Prop, +(forall (A : Type) (n : nat) (a : A) (v : vec A n), + P A n (a :: v) v) -> +forall (A : Type) (n : nat) (v : vec A (S n)), P A n v (tail v) ]] + + As a witness of the power of the unification, consider the following function + which computes the diagonal of a square matrix of size [n * n]. +*) + +Equations diag {A n} (v : vec (vec A n) n) : vec A n := +diag (n:=O) [] := [] ; +diag (n:=S _) ((a :: v) :: v') := + a :: diag (map tail v'). + +(** Here in the second equation, we know that the elements + of the vector are necessarily of size [S n] too, hence + we can do a nested refinement on the first one to find + the first element of the diagonal. + *) + +(** ** Recursion on indexed families + + Notice how in the [diag] example above we explicitely pattern-matched + on the index [n], even though the [nil] and [cons] pattern matching + would have been enough to determine these indices. This is because the + following definition also fails: *) + +Fail Equations diag' {A n} (v : vec (vec A n) n) : vec A n := +diag' [] := [] ; +diag' ((a :: v) :: v') := a :: diag' (map tail v'). + +(** Indeed, Coq cannot guess the decreasing argument of this fixpoint + using its limited syntactic guard criterion: [map tail v'] cannot + be seen to be a (large) subterm of [v'] using this criterion, even + if it is clearly "smaller". In general, it can also be the case that + the compilation algorithm introduces decorations to the proof term + that prevent the syntactic guard check from seeing that the + definition is structurally recursive. + + To aleviate this problem, [Equations] provides support for + _well-founded_ recursive definitions which do not rely on syntactic + checks. + + ** Wellfounded recursion + + For the diagonal, it is easier to give [n] as the decreasing argument + of the function, even if the pattern-matching itself is on vectors: *) + +Equations diag' {A n} (v : vec (vec A n) n) : + vec A n by wf n := +diag' [] := [] ; +diag' ((a :: v) :: v') := a :: diag' (map tail v'). + +(* Unfolding lemma *) +Check diag'_unfold_eq. +Check diag'_elim. + +(** One can check using [Extraction diag'] that the + computational behavior of [diag'] is indeed not + dependent on the index [n]. *) + +Extraction diag'. + +(** To go further and implement a safe lookup function on vectors, + we introduce an inductive definition of bounded natural numers [fin n]. + [fin n] represents the interval [ (0..n] ]. +*) + +Inductive fin : nat -> Set := + | f0 : forall n, fin (S n) + | fS : forall n, fin n -> fin (S n). + +Derive Signature NoConfusionHom for fin. + +Arguments f0 {n}. +Arguments fS {n}. + +(** For example, [fin 3] has the following inhabitants: *) + +Check f0 : fin 3. +Check fS f0 : fin 3. +Check fS (fS f0) : fin 3. + +(** But [fS (fS (fS f0))] is not an inhabitant of [fin 3]: *) + +Fail Check fS (fS (fS f0)) : fin 3. + +(** We can hence prove that [fin 0] is not inhabited: *) +Equations fin0 : fin 0 -> False := + fin0 !. + +(** Our safe lookup can now be concisely written: it takes + an index that must be within the bounds of the vector. *) + +Equations nth {A} {n} (v : vec A n) (f : fin n) : A := +nth (a :: v) f0 := a; +nth (_ :: v) (fS f) := nth v f. + +Equations fin_eq {n} (f g : fin n) : + { f = g } + { f <> g } := +fin_eq f0 f0 := left eq_refl; +fin_eq (n:=?(S n')) (fS f) (fS (n:=n') f') + with fin_eq f f' := + { fin_eq (fS f) (fS ?(f)) (left eq_refl) => left eq_refl; + fin_eq (fS f) (fS f') (right p) => right _ }; +fin_eq x y := right _. + +Extraction fin_eq. + +(** ** Dependent elimination tactics + + Alternatively to writing dependent pattern-matching programs, + we can also use dependent elimination whenever needed + in proof mode using the [depelim] and [dependent elimination] tactics + provided by Equations. *) + +Goal fin 0 -> False. +Proof. + intros f. + depelim f. +Qed. + +Lemma vec_eq_dec {A n} `{EqDec A} (v w : vec A n) : { v = w } + { v <> w }. +Proof. + induction v. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - dependent elimination w. + left; auto. + - dependent elimination w as [@cons n a' v']. + destruct (eq_dec a a') as [->|na]. + destruct (IHv v') as [->|nv]. + left; auto. + right; intros eq. + inversion eq. Undo. + noconf eq. contradiction. + right; intro eq. congruence. +Qed. + +Print Assumptions vec_eq_dec. + + +(*** Equality +The alma mater of inductive families is the propositional equality +[eq] defined as: [[ +Inductive eq (A : Type) (x : A) : A -> Prop := +eq_refl : eq A x x. ]] +*) + +Print eq. + +(** +Equality is a polymorphic relation on [A]. The [Prop] sort (or kind) categorizes +propositions, while the [Set] sort, equivalent to $\star$ in Haskell, categorizes +computational types. + +Equality is _parameterized_ by a value [x] of type [A] and +_indexed_ by another value of type [A]. Its single constructor states that +equality is reflexive, so the only way to build an object of [eq x y] is if +[x ~= y], that is if [x] is definitionaly equal to [y]. + +Now what is the elimination principle associated to this inductive family? +It is the good old Leibniz substitution principle: [[ +forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, x = y -> P y ]] + +Provided a proof that [x = y], we can create on object of type [P y] from an +existing object of type [P x]. This substitution principle is enough to show +that equality is symmetric and transitive. For example we can use +pattern-matching on equality proofs to show: +*) + +Equations eqt {A} (x y z : A) (p : x = y) (q : y = z) : + x = z := +eqt x ?(x) ?(x) eq_refl eq_refl := eq_refl. + +(** Let us explain the meaning of the non-linear patterns here that we +slipped through in the [equal] example. By pattern-matching on the +equalities, we have unified [x], [y] and [z], hence we determined the +_values_ of the patterns for the variables to be [x]. The [?(x)] +notation is essentially denoting that the pattern is not a candidate +for refinement, as it is determined by another pattern. This +particular patterns are called _inaccessible_. When they are variables +the inaccessibility annotation is optional. *) + +(** *** Pattern-matching and axiom K *) + +(** To use the K axiom or UIP with [Equations], one _must_ first set an option + allowing its use during dependenet pattern-matching compilation. *) + +Module KAxiom. + + (** By default we disallow the user of UIP, but it can be set. *) + + Set Equations With UIP. + + Module WithAx. + + (** The user must declare this axiom itself, as an instance of the [UIP] class. *) + Axiom uipa : forall A, UIP A. + Local Existing Instance uipa. + + (** In this case the following definition uses the [UIP] axiom just declared. *) + + Equations K {A} (x : A) (P : x = x -> Type) (p : P eq_refl) + (H : x = x) : P H := + K x P p eq_refl := p. + Print Assumptions K. + + End WithAx. + + (** Note that the definition loses its computational + content: it will get stuck on an axiom. We hence do not + recommend its use. + + Equations allows however to use constructive proofs of + UIP for types enjoying decidable equality. The following + example relies on an instance of the [EqDec] typeclass for natural numbers, from which + we can automatically derive a [UIP nat] instance. Note that + the computational behavior of this definition on open terms is not + to reduce to [p] but pattern-matches on the decidable equality + proof. However t/he defining equation still holds as a + _propositional_ equality, and the definition of K' is axiom-free. *) + + Equations K' (x : nat) (P : x = x -> Type) (p : P eq_refl) + (H : x = x) : P H := + K' x P p eq_refl := p. + + Print Assumptions K'. + (* Closed under the global context *) + +End KAxiom. + +Section ex. + Variable (X : Type) (g : X -> option X). + + Inductive dns : X -> Prop := + dns_I x : dnso (g x) -> dns x + with dnso : option X -> Prop := + | dnso_none: dnso None + | dnso_some x : dns x -> dnso (Some x). + + Equations pidns (x : X) (d : dns x) : dnso (g x) := + pidns x (dns_I x d) := d. + + Equations pidnso (x : X) (d : dnso (Some x)) : dns x := + pidnso x (dnso_some x d) := d. + + Fixpoint mutrec (x : X) (d : dns x) : nat := + mut' (g x) (pidns x d) + with mut' (x : option X) (d : dnso x) : nat := + match x return dnso x -> nat with + | None => fun d => 0 + | Some x' => fun d => S (mutrec x' (pidnso x' d)) + end d. + + (* + Equations mutrec (x : X) (d : dns x) : nat := + mutrec x d := mut' (g x) (pidns x d) + with mut' (x : option X) (d : dnso x) : nat := + mut' None d := 0; + mut' (Some x') d := S (mutrec x' (pidnso x' d)). + + Next Obligation. + depelim d. now cbn. + Defined. + Next Obligation. + depelim d. now cbn. + Defined. + About mutrec_elim. *) + + + +End ex. + +Extraction mutrec. \ No newline at end of file diff --git a/examples/Fin.v b/examples/Fin.v index 388c75267..ef613f492 100644 --- a/examples/Fin.v +++ b/examples/Fin.v @@ -8,8 +8,8 @@ (** An example development of the [fin] datatype using [equations]. *) -From Coq.Program Require Import Basics Combinators. -From Equations Require Import Equations. +From Stdlib.Program Require Import Basics Combinators. +From Equations.Prop Require Import Equations. Open Scope equations_scope. (** [fin n] is the type of naturals smaller than [n]. *) @@ -78,7 +78,8 @@ Scheme finle_ind_dep := Induction for finle Sort Prop. Arguments finle {n}. -Require Vectors.Vector. +#[warnings="-warn-library-file-stdlib-vector"] +From Stdlib Require Vectors.Vector. Arguments Vector.nil {A}. Arguments Vector.cons {A} _ {n}. Notation vnil := Vector.nil. diff --git a/examples/HoTT_light.v b/examples/HoTT_light.v index a72ace01f..089eb44e4 100644 --- a/examples/HoTT_light.v +++ b/examples/HoTT_light.v @@ -11,11 +11,10 @@ ** A lightweight version of the Homotopy Type Theory library prelude. *) Set Warnings "-notation-overridden". -Require Export Unicode.Utf8. -Require Import Stdlib.Program.Tactics Setoid. -Require Import Relations. +From Stdlib Require Export Unicode.Utf8. +From Stdlib Require Import Program.Tactics Setoid Relations. (** Switches to constants in Type *) -Require Import Equations.Type.All. +From Equations.Type Require Import All. (** This imports the polymorphic identity and sigma types in Type and their associated notations. *) Import Id_Notations. @@ -31,7 +30,7 @@ Set Implicit Arguments. (** Redefine a polymorphic identity function *) Definition id {A : Type} (a : A) : A := a. -Require Import CRelationClasses CMorphisms. +From Stdlib Require Import CRelationClasses CMorphisms. #[local] Instance id_reflexive A : Reflexive (@Id A). Proof. exact (@id_refl A). Defined. @@ -67,7 +66,9 @@ Notation "p # x" := (transport _ p x) (right associativity, at level 65, only pa Notation "1" := id_refl : equations_scope. (** Notation for the inverse *) -Reserved Notation "p ^" (at level 3, format "p '^'"). +#[warnings="-notation-incompatible-prefix"] +Reserved Notation "p ^" (at level 1, format "p '^'"). +#[warnings="-notation-incompatible-prefix"] Notation "p ^" := (id_sym p%equations) : equations_scope. Equations apd {A} {B : A -> Type} (f : forall x : A, B x) {x y : A} (p : x = y) : diff --git a/examples/MoreDep.v b/examples/MoreDep.v index a030e9e44..7ace00157 100644 --- a/examples/MoreDep.v +++ b/examples/MoreDep.v @@ -3,8 +3,8 @@ Porting a chapter of Adam Chlipala's Certified Programming with Dependent Types, #More Dependent Types#. *) -Require Import Bool Arith List Program. -From Equations Require Import Equations. +From Stdlib Require Import Bool Arith List Program. +From Equations.Prop Require Import Equations. Set Equations Transparent. Set Keyed Unification. @@ -101,7 +101,7 @@ pairOut _ => None. Set Printing Depth 1000000. -Require Import Wellfounded. +From Stdlib Require Import Wellfounded. Equations cfold {t} (e : exp t) : exp t := (* Works with well-foundedness too: cfold e by wf (signature_pack e) exp_subterm := *) @@ -147,7 +147,7 @@ Inductive rbtree : color -> nat -> Set := | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n). Derive Signature NoConfusion for rbtree. -Require Import Arith Lia. +From Stdlib Require Import Arith Lia. Section depth. Variable f : nat -> nat -> nat. diff --git a/examples/POPLMark1a.v b/examples/POPLMark1a.v index d9c3b9453..33e1b69e4 100644 --- a/examples/POPLMark1a.v +++ b/examples/POPLMark1a.v @@ -4,10 +4,10 @@ inductive definition of scope and well-scoped variables (and terms, types and environments). *) -Require Import Program. -From Equations Require Import Equations. +From Stdlib Require Import Program. +From Equations.Prop Require Import Equations. From Stdlib Require Import EquivDec. -Require Import Arith. +From Stdlib Require Import Arith. Definition scope := nat. Inductive var : scope -> Set := diff --git a/examples/RoseTree.v b/examples/RoseTree.v index 40576f419..1357bbd8d 100644 --- a/examples/RoseTree.v +++ b/examples/RoseTree.v @@ -6,11 +6,12 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Program. -From Equations Require Import Equations. -Require Import Utf8 Lia Arith. +From Stdlib Require Import Program. +From Equations.Prop Require Import Equations. -Require Import List. +From Stdlib Require Import Utf8 Lia Arith. + +From Stdlib Require Import List. Import ListNotations. Set Keyed Unification. diff --git a/examples/STLC.v b/examples/STLC.v index 6fe3216d7..ec5cb0a3a 100644 --- a/examples/STLC.v +++ b/examples/STLC.v @@ -14,11 +14,9 @@ well-founded order on typable terms and conclude with a normalizer building beta-short eta-long normal forms, typable in a bidirectional type system. *) -Require Program. -From Equations Require Import Equations. -Require Import Lia. -Require Import List Utf8. - +From Stdlib Require Program. +From Equations.Prop Require Import Equations. +From Stdlib Require Import Lia List Utf8. Import ListNotations. Set Keyed Unification. @@ -42,6 +40,7 @@ Delimit Scope term_scope with term. Bind Scope term_scope with term. Notation " @( f , x ) " := (App (f%term) (x%term)). +#[warnings="-notation-incompatible-prefix"] Notation " 'λ' t " := (Lambda (t%term)) (at level 10). Notation " << t , u >> " := (Pair (t%term) (u%term)). @@ -61,7 +60,7 @@ Coercion atom : atomic_type >-> type. Notation " x × y " := (product x y) (at level 90). Notation " x ---> y " := (arrow x y) (at level 30). -Require Import Arith. +From Stdlib Require Import Arith. Equations lift (k n : nat) (t : term) : term := lift k n (Var i) with Nat.compare i k := { @@ -103,7 +102,7 @@ Proof. funelim (lift k 0 t); term || rewrite ?H; crush. Qed. #[local] Hint Rewrite lift0 : lift. -Require Import Lia. +From Stdlib Require Import Lia. Lemma lift_k_lift_k k n m t : lift k n (lift k m t) = lift k (n + m) t. Proof. @@ -164,6 +163,7 @@ where "Γ |-- i : A " := (types Γ i A). Derive Signature for types. +#[warnings="-notation-incompatible-prefix"] Notation " [ t ] u " := (subst 0 u t) (at level 10). Notation " x @ y " := (app x y) (at level 30, right associativity). @@ -286,12 +286,12 @@ Inductive reduce : term -> term -> Prop := where " t --> u " := (reduce t u). Derive Signature for reduce. -Require Import Relations. +From Stdlib Require Import Relations. Definition reduces := clos_refl_trans term reduce. Notation " t -->* u " := (reduces t u) (at level 55). -Require Import Setoid. +From Stdlib Require Import Setoid. #[local] Instance: Transitive reduces. @@ -544,7 +544,7 @@ Proof. intros. now apply eta_expand in H0; term. Qed. (** Going to use the subterm order *) -Require Import Arith Wf_nat. +From Stdlib Require Import Arith Wf_nat. #[export] Instance wf_nat : Classes.WellFounded lt := lt_wf. #[local] Hint Constructors Subterm.lexprod : subterm_relation. @@ -720,7 +720,7 @@ Proof. (* Lt *) apply Nat.compare_lt_iff in Heq. depelim H0. replace (nth i (Γ' @ (_ :: Γ)) unit) with (nth i (Γ' @ Γ) unit). - constructor. rewrite app_length. auto with arith. + constructor. rewrite length_app. auto with arith. now do 2 rewrite <- nth_extend_right by auto. (* Gt *) @@ -783,7 +783,7 @@ Proof. intros Ht2; subst t. simpl in *. depelim H0. specialize (Hind _ _ H H0); eauto. now apply pair_elim_snd with A0. Qed. -Print Assumptions hereditary_subst_type. +(* Print Assumptions hereditary_subst_type. *) Import Program.Basics. #[export] Instance: subrelation eq (flip impl). Proof. reduce. subst; auto. Qed. @@ -855,18 +855,18 @@ Proof. split; intros Hsyn; depelim Hsyn; [depelim H1;constructor;auto|]; (rewrite nth_app_l by lia; rewrite <- nth_app_l with (l':=Γ) by lia; - constructor; rewrite app_length; auto with arith). + constructor; rewrite length_app; auto with arith). (* Gt *) - apply Nat.compare_gt_iff in Heq. split; intros Hsyn; depelim Hsyn. depelim H1. constructor. auto. replace (nth i (Γ' @ (A :: Γ)) unit) with (nth (pred i) (Γ' @ Γ) unit). - constructor. rewrite app_length in *. simpl in H1. lia. + constructor. rewrite length_app in *. simpl in H1. lia. now apply nth_pred. replace (nth _ (Γ' @ (_ :: _)) unit) with (nth (pred i) (Γ' @ Γ) unit). - constructor. rewrite app_length in *. simpl in H0. lia. + constructor. rewrite length_app in *. simpl in H0. lia. now apply nth_pred. (* App *) @@ -1002,7 +1002,7 @@ Proof. split; auto. intros H1. depelim H1. term. Qed. -Print Assumptions hereditary_subst_subst. +(* Print Assumptions hereditary_subst_subst. *) Lemma check_liftn {Γ Γ' t T} : Γ |-- t <= T -> Γ' @ Γ |-- lift 0 (length Γ') t <= T. Proof. intros. apply (check_lift Γ t T [] H Γ'). Qed. @@ -1053,4 +1053,4 @@ Proof. induction 1. (* eta-exp *) depelim H0. Qed. -Print Assumptions types_normalizes. +(* Print Assumptions types_normalizes. *) diff --git a/examples/_CoqProject b/examples/_CoqProject index bbc262c7a..bbb8f52a0 100644 --- a/examples/_CoqProject +++ b/examples/_CoqProject @@ -21,3 +21,4 @@ wfrec.v AlmostFull.v POPLMark1a.v bove_capretta.v +Equations_Tutorial_VeriMag.v diff --git a/examples/accumulator.v b/examples/accumulator.v index c83a81cc7..eddfc8361 100644 --- a/examples/accumulator.v +++ b/examples/accumulator.v @@ -15,7 +15,7 @@ to express and reason about using where clauses, well-founded recursion and function eliminators. *) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. From Stdlib Require Import List Syntax Arith Lia. Import ListNotations. @@ -70,7 +70,7 @@ Qed. *) -Obligation Tactic := idtac. +Local Obligation Tactic := idtac. Equations? isPrime (n : nat) : bool := isPrime 0 := false; diff --git a/examples/bove_capretta.v b/examples/bove_capretta.v index fb2abc6ba..534ba1507 100644 --- a/examples/bove_capretta.v +++ b/examples/bove_capretta.v @@ -5,8 +5,9 @@ but not direct pattern matching. We show a difficult example involving nested recursive calls. *) -From Equations Require Import Equations. -Require Import Arith Lia Relations Utf8. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Arith Lia Relations Utf8. Import Sigma_Notations. (** The graph of the [f91] function. *) diff --git a/examples/definterp.v b/examples/definterp.v index 640b85d2b..8725f46fc 100644 --- a/examples/definterp.v +++ b/examples/definterp.v @@ -22,12 +22,13 @@ store extension is resolved using type class resolution as well as the dependent-passing style version. *) -Require Import Program.Basics Program.Tactics. +From Stdlib Require Import Program.Basics Program.Tactics. +#[warnings="-warn-library-file-stdlib-vector"] Require Import Stdlib.Vectors.VectorDef. -Require Import List. +From Stdlib Require Import List. Import ListNotations. -Require Import Utf8. -From Equations Require Import Equations. +From Stdlib Require Import Utf8. +From Equations.Prop Require Import Equations. Set Warnings "-notation-overridden". (** The Σ notation of equations clashes with the Σ's used below, @@ -332,7 +333,7 @@ Definition neg : Expr [] (bool ⇒ bool) := Definition letref {t u} (v : Expr [] t) (b : Expr [ref t] u) : Expr [] u := app (abs b) (new v). -Obligation Tactic := idtac. +Local Obligation Tactic := idtac. Equations in_app_weaken {Σ Σ' Σ'' : StoreTy} {t} (p : t ∈ (Σ ++ Σ'')) : t ∈ (Σ ++ Σ' ++ Σ'') by struct Σ := in_app_weaken (Σ:=nil) p := pres_in (Σ', eq_refl) t p; diff --git a/examples/definterp_scope.v b/examples/disabled/definterp_scope.v similarity index 98% rename from examples/definterp_scope.v rename to examples/disabled/definterp_scope.v index c93759de0..0a4ce294e 100644 --- a/examples/definterp_scope.v +++ b/examples/disabled/definterp_scope.v @@ -1,7 +1,7 @@ -Require Import Program.Basics Program.Tactics. -Require Import Equations.Equations. -Require Import Stdlib.Vectors.VectorDef. -Require Import List. +From Stdlib Require Import Program.Basics Program.Tactics. +From Equations.Prop Require Import Equations. +From Stdlib Require Import Vectors.VectorDef. +From Stdlib Require Import List. Import ListNotations. Set Equations Transparent. @@ -171,7 +171,7 @@ Infix "⊚" := trans_incl (at level 10). Equations M : forall (Γ : Ctx) (P : StoreTy -> Type) (Σ : StoreTy), Type := M Γ P Σ := forall (E : Env Γ Σ) (μ : Store Σ), option &{ Σ' : _ & &{ _ : Store Σ' & &{ _ : P Σ' & Σ ⊑ Σ'}}}. -Require Import Utf8. +From Stdlib Require Import Utf8. Notation "( x , .. , y , z )" := (sigmaI _ x .. (sigmaI _ y z) ..) : core_scope. Equations bind {Σ Γ} {P Q : StoreTy -> Type} (f : M Γ P Σ) (g : ∀ {Σ'}, P Σ' -> M Γ Q Σ') : M Γ Q Σ := diff --git a/examples/definterp_simple.v b/examples/disabled/definterp_simple.v similarity index 94% rename from examples/definterp_simple.v rename to examples/disabled/definterp_simple.v index bbe00d1fa..53346d286 100644 --- a/examples/definterp_simple.v +++ b/examples/disabled/definterp_simple.v @@ -1,7 +1,8 @@ -Require Import Program.Basics Program.Tactics. -Require Import Equations.Equations. +From Stdlib Require Import Program.Basics Program.Tactics. +From Equations.Prop Require Import Equations. +Set Warnings "-warn-library-file-stdlib-vector". Require Import Stdlib.Vectors.VectorDef. -Require Import List. +From Stdlib Require Import List. Import ListNotations. Set Equations Transparent. @@ -19,6 +20,7 @@ Definition Ctx := list Ty. Reserved Notation " x ∈ s " (at level 70, s at level 10). +#[universes(template)] Inductive In {A} (x : A) : list A -> Type := | here {xs} : x ∈ (x :: xs) | there {y xs} : x ∈ xs -> x ∈ (y :: xs) @@ -69,7 +71,7 @@ Equations update : forall {A P xs} {x : A}, All P xs -> x ∈ xs -> P x -> All P Equations M : Ctx -> Type -> Type := M Γ A := Env Γ -> option A. -Require Import Utf8. +From Stdlib Require Import Utf8. Equations bind : ∀ {Γ A B}, M Γ A → (A → M Γ B) → M Γ B := bind m f γ := match m γ with diff --git a/examples/function_iter_style.v b/examples/disabled/function_iter_style.v similarity index 93% rename from examples/function_iter_style.v rename to examples/disabled/function_iter_style.v index 4d6e2e0b3..e01b9f454 100644 --- a/examples/function_iter_style.v +++ b/examples/disabled/function_iter_style.v @@ -1,6 +1,6 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. -Require Import List Program.Syntax Arith Lia. +From Stdlib Require Import List Program.Syntax Arith Lia. Equations div2 (n : nat) : nat := div2 0 := 0; diff --git a/examples/misc.v b/examples/disabled/misc.v similarity index 91% rename from examples/misc.v rename to examples/disabled/misc.v index 1777caebb..30ac78564 100644 --- a/examples/misc.v +++ b/examples/disabled/misc.v @@ -1,5 +1,7 @@ +From Equations.Prop Require Import Equations. +From Stdlib Require Import List. - +Import List_Notations. (** In general, one can require more elaborate loop invariants. This [fast_length] function computes the length of a list using @@ -29,7 +31,7 @@ Equations list_init {A} (n : nat) (a : A) : list A := list_init 0 _ := []; list_init (S n) x := x :: list_init n x. -Require Import NArith. +From Stdlib Require Import NArith. Equations pos_list_init {A} (n : positive) (a : A) : list A := pos_list_init xH x := [x]; diff --git a/examples/nm.v b/examples/disabled/nm.v similarity index 96% rename from examples/nm.v rename to examples/disabled/nm.v index 50a4b1dcc..c398a4e1d 100644 --- a/examples/nm.v +++ b/examples/disabled/nm.v @@ -1,7 +1,7 @@ (** Proving Termination of Normalization Functions for Conditional Expressions, L. Paulson *) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. -Require Import List Program.Syntax Arith Lia. +From Stdlib Require Import List Program.Syntax Arith Lia. Inductive exp := At | If : exp -> exp -> exp -> exp. diff --git a/examples/quicksort.v b/examples/disabled/quicksort.v similarity index 95% rename from examples/quicksort.v rename to examples/disabled/quicksort.v index 09f663961..5cb0f1eb4 100644 --- a/examples/quicksort.v +++ b/examples/disabled/quicksort.v @@ -1,6 +1,6 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. -Require Import Vector. +From Stdlib Require Import Vector. Notation vector := t. Derive NoConfusion NoConfusionHom for vector. @@ -44,13 +44,13 @@ Proof. firstorder. Qed. -(* Lemma All_In_All {A P n m} (v : vector A n) (v' : vector A m) : *) -(* All (fun x => In x v) v' -> All P v -> All P v'. *) -(* Proof. *) -(* induction 1. simpl. constructor. *) -(* intros. constructor; auto. *) -(* eapply In_All; eauto. *) -(* Qed. *) +Lemma All_In_All {A P n m} (v : vector A n) (v' : vector A m) : + All (fun x => In x v) v' -> All P v -> All P v'. +Proof. + induction 1. simpl. constructor. + intros. constructor; auto. + eapply In_All; eauto. +Qed. Inductive Sorted {A : Type} (R : A -> A -> Prop) : forall {n}, vector A n -> Prop := | Sorted_nil : Sorted R nil @@ -70,7 +70,7 @@ Proof. split; intros; depelim H0; cbn; simp In app in *; intuition eauto with *; simp In in *. apply H in H0. intuition. Qed. -Require Import Sumbool. +From Stdlib Require Import Sumbool. Notation dec x := (sumbool_of_bool x). diff --git a/examples/dune b/examples/dune new file mode 100644 index 000000000..45db7c6d9 --- /dev/null +++ b/examples/dune @@ -0,0 +1,10 @@ +(coq.theory + ; This determines the -R flag + (name Equations.Examples) + (package rocq-equations-examples) + (synopsis "Equations Plugin Examples") + (plugins rocq-runtime.plugins.extraction rocq-equations.plugin) + (modules :standard \ IdDec NoCycle) + (theories Stdlib Equations Equations.Prop Equations.Type)) + +(include_subdirs no) \ No newline at end of file diff --git a/examples/general_recursion.v b/examples/general_recursion.v index 463cddca6..34c285215 100644 --- a/examples/general_recursion.v +++ b/examples/general_recursion.v @@ -22,13 +22,15 @@ (** printing Signature %\coqdocclass{Signature}% *) (** printing Subterm %\coqdocclass{Subterm}% *) (** printing NoConfusion %\coqdocclass{NoConfusion}% *) -From Equations Require Import Equations. -Require Import ZArith Lia. -Require Import Program. -Require Import Psatz. -Require Import Nat. -Require Import Stdlib.Vectors.VectorDef. -Require Import Relations. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import ZArith Lia. +From Stdlib Require Import Program. +From Stdlib Require Import Psatz. +From Stdlib Require Import Nat. +#[warnings="-warn-library-file-stdlib-vector"] +From Stdlib Require Import Vectors.VectorDef. +From Stdlib Require Import Relations. Set Keyed Unification. Set Equations Transparent. @@ -49,6 +51,8 @@ Instance wf_total_init_compute : forall {A}, WellFounded (@total_relation A). exact (fun A => Acc_intro_generator 10 wf_total_init). Defined. +Set Warnings "-solve_obligation_error". + (** Now we define an obviously non-terminating function. *) Equations? nonterm (n : nat) : nat by wf n (@total_relation nat) := nonterm 0 := 0; @@ -123,6 +127,7 @@ Definition fact := | 0 => 1 | S n => S n * fact n end). +#[warnings="-abstract-large-number"] Check eq_refl : fact 8 = 40320. (** [Y] is only good in call-by-name or call-by-need, so we switch to Haskell *) diff --git a/examples/graph_complete.v b/examples/graph_complete.v index 2e0b22639..ab912a17c 100644 --- a/examples/graph_complete.v +++ b/examples/graph_complete.v @@ -1,8 +1,9 @@ Set Warnings "-notation-overridden". -Require Import Equations.Type.All. +From Equations.Type Require Import All. +#[warning="-notation-incompatible-prefix"] Require Import Examples.HoTT_light. Set Universe Polymorphism. -Require Import Relations. +From Stdlib Require Import Relations. Import Id_Notations. Import Sigma_Notations. diff --git a/examples/ho_finite_branching.v b/examples/ho_finite_branching.v index 0e8ba7fcc..fc810ebc1 100644 --- a/examples/ho_finite_branching.v +++ b/examples/ho_finite_branching.v @@ -1,6 +1,7 @@ (** * Higher-order recursion, an example with finite branching trees *) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. + Require Import Examples.Fin. Inductive ho : Set := diff --git a/examples/mutualwfrec.v b/examples/mutualwfrec.v index 141c26910..1f7e60a72 100644 --- a/examples/mutualwfrec.v +++ b/examples/mutualwfrec.v @@ -7,9 +7,9 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. From Stdlib Require Import List Syntax Arith Lia. -Require Import List Wellfounded. +From Stdlib Require Import List Wellfounded. Import ListNotations. (* end hide *) (** * Mutual well-founded recursion using dependent pattern-matching diff --git a/examples/nested_mut_rec.v b/examples/nested_mut_rec.v index 9ec43d771..d2b09d09a 100644 --- a/examples/nested_mut_rec.v +++ b/examples/nested_mut_rec.v @@ -4,8 +4,9 @@ Example of a term structure with two constructors taking lists of terms. *) -From Equations Require Import Equations. -Require Import Program Arith List Compare_dec. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Program Arith List Compare_dec. Import ListNotations. (** A nested recursive definition of terms with lists of terms *) diff --git a/examples/ordinals.v b/examples/ordinals.v index 177961172..d0ca2e363 100644 --- a/examples/ordinals.v +++ b/examples/ordinals.v @@ -1,8 +1,8 @@ -Require Import Arith. +From Stdlib Require Import Arith. From Stdlib Require Import Eqdep_dec. From Stdlib Require Import Peano_dec. -Require Import List. -Require Import Recdef. +From Stdlib Require Import List. +From Stdlib Require Import Recdef. (** Arithmétique @@ -150,7 +150,7 @@ Qed. Lemma padd_len_le_len : forall (w1 w2:(list nat)), (le (length w1) (length w2)) -> (length (padd w1 w2)) = (length w2). -intros. unfold padd. unfold dist. rewrite app_length. +intros. unfold padd. unfold dist. rewrite length_app. rewrite zs_len. rewrite Nat.sub_add by (exact H); reflexivity. Qed. @@ -551,7 +551,7 @@ Qed. (** Applications avec Program Fixpoint *) -Require Coq.Program.Wf. +From Stdlib Require Program.Wf. (* Tactique pour les preuves de bonne fondation. *) Ltac by_Acc_mwlt mwlt := diff --git a/examples/polynomials.v b/examples/polynomials.v index d4ba09a19..2b9f85561 100644 --- a/examples/polynomials.v +++ b/examples/polynomials.v @@ -17,11 +17,13 @@ 2016-2017. If running this interactively you can ignore the printing and hide directives which are just used to instruct coqdoc. *) (* begin hide *) -Require Import Program.Basics Program.Tactics. -From Equations Require Import Equations. -Require Import ZArith Lia. -Require Import Psatz. -Require Import Nat. +From Stdlib Require Import Program.Basics Program.Tactics. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import ZArith Lia. +From Stdlib Require Import Psatz. +From Stdlib Require Import Nat. +#[warnings="-warn-library-file-stdlib-vector"] Require Import Stdlib.Vectors.VectorDef. Set Keyed Unification. diff --git a/examples/string_matching.v b/examples/string_matching.v index 823828a4a..509826c95 100644 --- a/examples/string_matching.v +++ b/examples/string_matching.v @@ -1,12 +1,12 @@ (** Example by Nicky Vazou, unfinished *) -Require Import Arith. +From Stdlib Require Import Arith. From Stdlib Require Import DecidableClass. From Stdlib.Program Require Import Wf. -Require Import List Lia. -Require Import PeanoNat. -Require Import Program. -From Equations Require Import Equations. +From Stdlib Require Import List Lia. +From Stdlib Require Import PeanoNat. +From Stdlib Require Import Program. +From Equations.Prop Require Import Equations. Import ListNotations. @@ -236,7 +236,7 @@ Section pmconcat. | left H => mconcat x ; | right Hd => pmconcat i (map mconcat (chunk i x)) }. Proof. clear pmconcat. - rewrite map_length. + rewrite length_map. rewrite Bool.orb_false_iff in Hd. destruct Hd. apply leb_complete_conv in H2. apply leb_complete_conv in H3. apply length_chunk_lt; simpl; auto. diff --git a/examples/views.v b/examples/views.v index e7b35aabf..ad3e11c6d 100644 --- a/examples/views.v +++ b/examples/views.v @@ -8,7 +8,7 @@ (**********************************************************************) (* end hide *) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. From Stdlib Require Import List Syntax Arith Lia. (** * Views using dependent pattern-matching diff --git a/examples/wfrec.v b/examples/wfrec.v index b935728b2..b4d6233b8 100644 --- a/examples/wfrec.v +++ b/examples/wfrec.v @@ -7,9 +7,9 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. From Stdlib Require Import List Syntax Arith Lia. -Require Import List. +From Stdlib Require Import List. Import ListNotations. (* end hide *) (** * Well-founded recursion diff --git a/rocq-equations.opam b/rocq-equations.opam new file mode 100644 index 000000000..6a61f69b0 --- /dev/null +++ b/rocq-equations.opam @@ -0,0 +1,42 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "A function definition package for Rocq" +description: + "Equations is a function definition plugin for Rocq, that allows the definition of functions by dependent pattern-matching and well-founded, mutual or nested structural recursion and compiles them into core terms. It automatically derives the clauses equations, the graph of the function and its associated elimination principle." +maintainer: ["Matthieu Sozeau "] +authors: [ + "Matthieu Sozeau " + "Cyprien Mangin " +] +license: "LGPL-2.1-only" +tags: [ + "keyword:dependent pattern-matching" + "keyword:functional elimination" + "category:Miscellaneous/Coq Extensions" + "logpath:Equations" +] +homepage: "https://mattam82.github.io/Coq-Equations" +bug-reports: "https://github.com/mattam82/Coq-Equations/issues" +depends: [ + "dune" {>= "3.13"} + "ocaml" {>= "4.10.0"} + "rocq-prover" {>= "9.0~"} + "ppx_optcomp" {build} + "ocaml-lsp-server" {with-dev-setup} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/mattam82/Coq-Equations.git" diff --git a/src/META.coq-equations.in b/src/META.rocq-equations.in similarity index 72% rename from src/META.coq-equations.in rename to src/META.rocq-equations.in index be2aa4992..21d45f0bc 100644 --- a/src/META.coq-equations.in +++ b/src/META.rocq-equations.in @@ -1,7 +1,7 @@ package "plugin" ( directory = "." description = "Coq equations" - requires = "coq-core.plugins.ltac coq-core.plugins.extraction coq-core.plugins.cc" + requires = "rocq-runtime.plugins.ltac rocq-runtime.plugins.extraction rocq-runtime.plugins.cc" archive(byte) = "equations_plugin.cma" archive(native) = "equations_plugin.cmxa" plugin(byte) = "equations_plugin.cma" diff --git a/src/dune b/src/dune index 7373d3390..61fae895a 100644 --- a/src/dune +++ b/src/dune @@ -1,7 +1,9 @@ (library (name equations_plugin) - (public_name coq-equations.plugin) + (public_name rocq-equations.plugin) (flags :standard -w -9-27+40+60 -warn-error -3-9-32-33-50) - (libraries coq-core.plugins.cc coq-core.plugins.extraction)) + (libraries rocq-runtime.plugins.cc rocq-runtime.plugins.extraction) + (preprocess + (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~rocq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))) (coq.pp (modules g_equations)) diff --git a/src/equations.ml b/src/equations.ml index b83c396ff..2a7397365 100644 --- a/src/equations.ml +++ b/src/equations.ml @@ -83,11 +83,11 @@ let define_unfolding_eq ~pm env evd flags p unfp prog prog' ei hook = (mkApp (funfc, extended_rel_vect 0 sign))) sign in let evd, stmt = Typing.solve_evars (Global.env ()) !evd stmt in - let subproofs = Principles_proofs.extract_subprograms env evd ei.equations_where_map p unfp in + let subproofs = Principles_proofs.extract_subprograms env evd ei.Principles_proofs.equations_where_map p unfp in let fold pm (name, subst, uctx, typ) = let typ = EConstr.Unsafe.to_constr typ in let typ = collapse_term_qualities uctx typ in - let tac = Principles_proofs.prove_unfolding_sublemma info ei.equations_where_map prog.program_cst funf_cst subst in + let tac = Principles_proofs.prove_unfolding_sublemma info ei.Principles_proofs.equations_where_map prog.program_cst funf_cst subst in let cinfo = Declare.CInfo.make ~name ~typ () in let info = Declare.Info.make ~poly:info.poly ~scope:info.scope diff --git a/src/equations_common.ml b/src/equations_common.ml index 82c72918d..1649e4139 100644 --- a/src/equations_common.ml +++ b/src/equations_common.ml @@ -45,7 +45,7 @@ let equations_category = CWarnings.create_category ~name:"equations" () let () = Goptions.declare_bool_option { Goptions.optdepr = Some depr_with_k; - Goptions.optstage = Interp; + Goptions.optstage = Summary.Stage.Interp; Goptions.optkey = ["Equations"; "WithK"]; Goptions.optread = (fun () -> false); Goptions.optwrite = (fun b -> @@ -58,7 +58,7 @@ let () = Goptions.declare_bool_option { let _ = Goptions.declare_bool_option { Goptions.optdepr = Some depr_with_k; - Goptions.optstage = Interp; + Goptions.optstage = Summary.Stage.Interp; Goptions.optkey = ["Equations"; "WithKDec"]; Goptions.optread = (fun () -> !simplify_withUIP); Goptions.optwrite = (fun b -> simplify_withUIP := b) @@ -66,7 +66,7 @@ let _ = Goptions.declare_bool_option { let _ = Goptions.declare_bool_option { Goptions.optdepr = None; - Goptions.optstage = Interp; + Goptions.optstage = Summary.Stage.Interp; Goptions.optkey = ["Equations"; "With"; "UIP"]; Goptions.optread = (fun () -> !simplify_withUIP); Goptions.optwrite = (fun b -> simplify_withUIP := b) @@ -74,7 +74,7 @@ let _ = Goptions.declare_bool_option { let _ = Goptions.declare_bool_option { Goptions.optdepr = None; - Goptions.optstage = Interp; + Goptions.optstage = Summary.Stage.Interp; Goptions.optkey = ["Equations"; "Transparent"]; Goptions.optread = (fun () -> !equations_transparent); Goptions.optwrite = (fun b -> equations_transparent := b) @@ -82,7 +82,7 @@ let _ = Goptions.declare_bool_option { let _ = Goptions.declare_bool_option { Goptions.optdepr = None; - Goptions.optstage = Interp; + Goptions.optstage = Summary.Stage.Interp; Goptions.optkey = ["Equations"; "With"; "Funext"]; Goptions.optread = (fun () -> !equations_with_funext); Goptions.optwrite = (fun b -> equations_with_funext := b) @@ -90,7 +90,7 @@ let _ = Goptions.declare_bool_option { let _ = Goptions.declare_bool_option { Goptions.optdepr = None; - Goptions.optstage = Interp; + Goptions.optstage = Summary.Stage.Interp; Goptions.optkey = ["Equations"; "Derive"; "Equations"]; Goptions.optread = (fun () -> !equations_derive_equations); Goptions.optwrite = (fun b -> equations_derive_equations := b) @@ -98,7 +98,7 @@ let _ = Goptions.declare_bool_option { let _ = Goptions.declare_bool_option { Goptions.optdepr = None; - Goptions.optstage = Interp; + Goptions.optstage = Summary.Stage.Interp; Goptions.optkey = ["Equations"; "Derive"; "Eliminator"]; Goptions.optread = (fun () -> !equations_derive_eliminator); Goptions.optwrite = (fun b -> equations_derive_eliminator := b) @@ -110,7 +110,7 @@ let debug = ref false let _ = Goptions.declare_bool_option { Goptions.optdepr = None; - Goptions.optstage = Interp; + Goptions.optstage = Summary.Stage.Interp; Goptions.optkey = ["Equations"; "Debug"]; Goptions.optread = (fun () -> !debug); Goptions.optwrite = (fun b -> debug := b) @@ -204,7 +204,7 @@ let e_new_global evdref gr = type lazy_ref = Names.GlobRef.t Lazy.t -let equations_lib_ref s = Coqlib.lib_ref ("equations." ^ s) +let equations_lib_ref s = Rocqlib.lib_ref ("equations." ^ s) let find_global s = lazy (equations_lib_ref s) @@ -222,6 +222,7 @@ let e_type_of env evd t = evd := evm; t let collapse_term_qualities uctx c = + let open Sorts.Quality in let nf_qvar q = match UState.nf_qvar uctx q with | QConstant _ as q -> q | QVar q -> (* hack *) QConstant QType @@ -639,7 +640,7 @@ let tacident_arg h = Reference (qualid_of_ident h) let find_depelim_module () = - let gr = Coqlib.lib_ref "equations.depelim.module" in + let gr = Rocqlib.lib_ref "equations.depelim.module" in match gr with | GlobRef.ConstRef c -> Names.Constant.modpath c | _ -> CErrors.anomaly (str"equations.depelim.module is not defined") @@ -1090,6 +1091,12 @@ let evd_comb1 f evd x = (* Universe related functions *) +[%%if rocq = "9.1"] +let set_leq_sort _env = Evd.set_leq_sort +[%%else] +let set_leq_sort env = Evd.set_leq_sort env +[%%endif] + let nonalgebraic_universe_level_of_universe env sigma u = match ESorts.kind sigma u with | Sorts.Set | Sorts.Prop | Sorts.SProp -> @@ -1104,7 +1111,7 @@ let nonalgebraic_universe_level_of_universe env sigma u = | None -> let sigma, l = Evd.new_univ_level_variable Evd.univ_flexible sigma in let ul = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make l in - let sigma = Evd.set_leq_sort sigma u ul in + let sigma = set_leq_sort env sigma u ul in sigma, l, ul let instance_of env sigma ?argu goalu = diff --git a/src/g_equations.mlg b/src/g_equations.mlg index f3cf86ed6..7c2a105a8 100644 --- a/src/g_equations.mlg +++ b/src/g_equations.mlg @@ -9,7 +9,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -DECLARE PLUGIN "coq-equations.plugin" +DECLARE PLUGIN "rocq-equations.plugin" { @@ -111,7 +111,7 @@ END open Syntax -open Pcoq.Prim +open Procq.Prim } @@ -157,8 +157,8 @@ let pr_binders2 _env _sigma _ _ _ l = mt () let wit_binders2 : binders_argtype = Genarg.create_arg "binders2" -let binders2 : local_binder_expr list Pcoq.Entry.t = - Pcoq.create_generic_entry2 "binders2" (Genarg.rawwit wit_binders2) +let binders2 : local_binder_expr list Procq.Entry.t = + Procq.create_generic_entry2 "binders2" (Genarg.rawwit wit_binders2) let binders2_val = Geninterp.register_val0 wit_binders2 None @@ -176,8 +176,8 @@ let pr_raw_deppat_equations _env _sigma _ _ _ l = mt () let pr_glob_deppat_equations _env _sigma _ _ _ l = mt () let pr_deppat_equations _env _sigma _ _ _ l = mt () -let deppat_equations : Syntax.pre_equation list Pcoq.Entry.t = - Pcoq.create_generic_entry2 "deppat_equations" (Genarg.rawwit wit_deppat_equations) +let deppat_equations : Syntax.pre_equation list Procq.Entry.t = + Procq.create_generic_entry2 "deppat_equations" (Genarg.rawwit wit_deppat_equations) let _ = Pptactic.declare_extra_genarg_pprule wit_deppat_equations pr_raw_deppat_equations pr_glob_deppat_equations pr_deppat_equations @@ -193,8 +193,8 @@ let pr_raw_deppat_elim _env _sigma _ _ _ l = mt () let pr_glob_deppat_elim _env _sigma _ _ _ l = mt () let pr_deppat_elim _env _sigma _ _ _ l = mt () -let deppat_elim : Constrexpr.constr_expr list Pcoq.Entry.t = - Pcoq.create_generic_entry2 "deppat_elim" (Genarg.rawwit wit_deppat_elim) +let deppat_elim : Constrexpr.constr_expr list Procq.Entry.t = + Procq.create_generic_entry2 "deppat_elim" (Genarg.rawwit wit_deppat_elim) let _ = Pptactic.declare_extra_genarg_pprule wit_deppat_elim pr_raw_deppat_elim pr_glob_deppat_elim pr_deppat_elim @@ -209,8 +209,8 @@ let pr_raw_equations _env _sigma _ _ _ l = mt () let pr_glob_equations _env _sigma _ _ _ l = mt () let pr_equations _env _sigma _ _ _ l = mt () -let equations : (pre_equations * Vernacexpr.notation_declaration list) Pcoq.Entry.t = - Pcoq.create_generic_entry2 "equations" (Genarg.rawwit wit_equations) +let equations : (pre_equations * Vernacexpr.notation_declaration list) Procq.Entry.t = + Procq.create_generic_entry2 "equations" (Genarg.rawwit wit_equations) let _ = Pptactic.declare_extra_genarg_pprule wit_equations pr_raw_equations pr_glob_equations pr_equations @@ -245,18 +245,18 @@ let declare_uniform t = let () = declare_uniform wit_my_preident -let my_preident : string Pcoq.Entry.t = - Pcoq.create_generic_entry2 "my_preident" (Genarg.rawwit wit_my_preident) +let my_preident : string Procq.Entry.t = + Procq.create_generic_entry2 "my_preident" (Genarg.rawwit wit_my_preident) open Util -open Pcoq +open Procq open Constr open Syntax -let () = Pcoq.set_keyword_state (CLexer.add_keyword (Pcoq.get_keyword_state()) "λ") +let () = Procq.set_keyword_state (CLexer.add_keyword (Procq.get_keyword_state()) "λ") let check_eqns_ident = - let open Pcoq.Lookahead in + let open Procq.Lookahead in to_entry "check_eqns_ident" begin lk_kws ["|"; ";"] end @@ -474,8 +474,8 @@ type elim_patterns_argtype = (raw_elim_patterns, glob_elim_patterns, elim_patter * * let pr_glob_g_elim_patterns _ _ _ = Simplify.pr_elim_patterns * * let pr_g_elim_patterns _ _ _ = Simplify.pr_elim_patterns *\) * - * let g_elim_patterns : raw_elim_patterns Pcoq.Entry.t = - * Pcoq.create_generic_entry2 "g_elim_patterns" + * let g_elim_patterns : raw_elim_patterns Procq.Entry.t = + * Procq.create_generic_entry2 "g_elim_patterns" * (Genarg.rawwit wit_g_elim_patterns) * * let _ = Pptactic.declare_extra_genarg_pprule wit_g_elim_patterns @@ -558,8 +558,8 @@ let pr_raw_g_simplification_rules _env _sigma _ _ _ = Simplify.pr_simplification let pr_glob_g_simplification_rules _env _sigma _ _ _ = Simplify.pr_simplification_rules let pr_g_simplification_rules _env _sigma _ _ _ = Simplify.pr_simplification_rules -let g_simplification_rules : Simplify.simplification_rules Pcoq.Entry.t = - Pcoq.create_generic_entry2 "g_simplification_rules" +let g_simplification_rules : Simplify.simplification_rules Procq.Entry.t = + Procq.create_generic_entry2 "g_simplification_rules" (Genarg.rawwit wit_g_simplification_rules) let _ = Pptactic.declare_extra_genarg_pprule wit_g_simplification_rules diff --git a/src/principles_proofs.ml b/src/principles_proofs.ml index 8bdf1c906..7dd2996b4 100644 --- a/src/principles_proofs.ml +++ b/src/principles_proofs.ml @@ -210,7 +210,7 @@ let mutual_fix li l = let check_guard gls env sigma = let gl = Proofview.drop_state (List.hd gls) in try - let EvarInfo evi = Evd.find sigma gl in + let Evd.EvarInfo evi = Evd.find sigma gl in match Evd.evar_body evi with | Evd.Evar_defined b -> Inductiveops.control_only_guard (Evd.evar_env env evi) sigma b; true | Evd.Evar_empty -> true diff --git a/src/simplify.ml b/src/simplify.ml index 683cbf098..f4471869d 100644 --- a/src/simplify.ml +++ b/src/simplify.ml @@ -418,7 +418,7 @@ let compose_term (env : Environ.env) (evd : Evd.evar_map ref) ((h1, c1) : open_term) ((h2, c2) : open_term) : open_term = match h1 with | Some ((ctx1, _, u1), (ev1, _)) -> - let EvarInfo ev1_info = Evd.find !evd ev1 in + let Evd.EvarInfo ev1_info = Evd.find !evd ev1 in let ev1_ctx = Evd.evar_context ev1_info in (* Keep only the context corresponding to [ctx1]. *) let named_ctx1 = CList.firstn (List.length ctx1) ev1_ctx in @@ -795,7 +795,7 @@ SimpFun.make ~name:"solution" begin fun (env : Environ.env) (evd : Evd.evar_map checked_appvect env evd tsolution [| tA'; term'; tB'; c; trel' |] in (* We make some room for the application of the equality... *) - let env = push_rel (LocalAssum (name, ty1')) env in + let env = push_rel (Context.Rel.Declaration.LocalAssum (name, ty1')) env in let c = Vars.lift 1 c in let c = checked_appvect env evd c [| EConstr.mkRel 1 |] in (* [targs'] are arguments in the context [eq_decl :: ctx']. *) diff --git a/src/splitting.ml b/src/splitting.ml index 560b7ec3b..d035f4a0f 100644 --- a/src/splitting.ml +++ b/src/splitting.ml @@ -1112,8 +1112,9 @@ let gather_fresh_context sigma u octx = let qarr, uarr = UVars.Instance.to_array u in let qualities = Array.fold_left (fun ctx' l -> + let open Sorts.Quality in match l with - | Sorts.Quality.QConstant _ -> assert false + | QConstant _ -> assert false | QVar l -> if not (Sorts.QVar.Set.mem l qvars) then Sorts.QVar.Set.add l ctx' else ctx') diff --git a/test-suite/Basics.v b/test-suite/Basics.v index 0e6a4a395..5cc482348 100644 --- a/test-suite/Basics.v +++ b/test-suite/Basics.v @@ -6,9 +6,10 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Program Bvector List Relations. -Require Import Equations.Prop.Equations. -Require Import Utf8. +From Stdlib Require Import Program List Relations. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Utf8. Set Keyed Unification. Equations neg (b : bool) : bool := @@ -104,7 +105,7 @@ Derive Signature for vector. Derive NoConfusion NoConfusionHom for vector. Derive Subterm for vector. -Require Import Arith Wf_nat. +From Stdlib Require Import Arith Wf_nat. #[local] Instance wf_nat : WellFounded lt := lt_wf. @@ -121,7 +122,8 @@ testn (S n) with testn n => { | 0 := S 0 ; | (S n') := S n' }. -Require Import Vectors.Vector. +#[warnings="-warn-library-file-stdlib-vector"] +From Stdlib Require Import Vectors.Vector. Arguments Vector.nil {A}. Arguments Vector.cons {A} _ {n}. @@ -435,8 +437,6 @@ Extraction split. *) (* Eval compute in @zip''. *) -Require Import Bvector. - Equations split_struct {X : Type} {m n} (xs : vector X (m + n)) : Split m n xs := split_struct (m:=0) xs := append nil xs ; split_struct (m:=(S m)) (cons x xs) with split_struct xs => { @@ -622,13 +622,14 @@ Definition transpose {A m n} : mat A m n -> mat A n m := (* (e : vector (vector A 0) n) v : vfold_right f (vmake n Vnil) v = *) (* Typeclasses eauto :=. *) -Require Import fin. +From Equations.TestSuite Require Import fin. Generalizable All Variables. Opaque vmap. Opaque vtail. Opaque nth. -Require Vectors.Vector. +#[warnings="-warn-library-file-stdlib-vector"] +From Stdlib Require Vectors.Vector. Arguments Vector.nil {A}. Arguments Vector.cons {A} _ {n}. Notation vnil := Vector.nil. diff --git a/test-suite/BasicsDec.v b/test-suite/BasicsDec.v index 7585aaa98..0718fca7b 100644 --- a/test-suite/BasicsDec.v +++ b/test-suite/BasicsDec.v @@ -1,4 +1,6 @@ -Require Import Equations.Prop.Equations Bvector. +From Equations.Prop Require Import Equations. +#[warnings="-deprecated-library-file-since-8.20"] +From Stdlib Require Import Bvector. Inductive bar1 (A : Type) : A -> Prop := . Inductive bar2 (A : Type) : (A -> A) -> Prop := . diff --git a/test-suite/Below.v b/test-suite/Below.v index 3f4675355..2c6314e18 100644 --- a/test-suite/Below.v +++ b/test-suite/Below.v @@ -9,11 +9,11 @@ (** Instances of [Below] for the standard datatypes. To be used by [equations] when it needs to do recursion on a type. *) -Require Import Bvector. -Require Import Vectors.Vector. -Require Import Equations.Init Equations.CoreTactics Equations.Prop.DepElim Equations.Prop.Tactics - Equations.Prop.Constants. -Require Import Equations.Prop.FunctionalInduction. +Set Warnings "-deprecated-library-file-since-8.20". +Set Warnings "-warn-library-file-stdlib-vector". +From Stdlib Require Import Bvector Vectors.Vector. +From Equations Require Import Init CoreTactics. +From Equations.Prop Require Import DepElim Tactics Constants FunctionalInduction. (** The [BelowPackage] class provides the definition of a [Below] predicate for some datatype, allowing to talk about course-of-value recursion on it. *) diff --git a/test-suite/DataStruct.v b/test-suite/DataStruct.v index d8aa99442..623f55add 100644 --- a/test-suite/DataStruct.v +++ b/test-suite/DataStruct.v @@ -1,7 +1,7 @@ (* http://adam.chlipala.net/cpdt/html/DataStruct.html *) -Require Import Arith List. -Require Import Program Equations.Prop.Equations. +From Stdlib Require Import Arith List Program. +From Equations.Prop Require Import Equations. Set Implicit Arguments. Set Keyed Unification. diff --git a/test-suite/BasicsHoTT.v b/test-suite/HoTT/BasicsHoTT.v similarity index 98% rename from test-suite/BasicsHoTT.v rename to test-suite/HoTT/BasicsHoTT.v index d922b6d4b..fbc592659 100644 --- a/test-suite/BasicsHoTT.v +++ b/test-suite/HoTT/BasicsHoTT.v @@ -6,10 +6,10 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) From Equations Require Import CoreTactics. -Require Import Equations.HoTT.All Equations.HoTT.WellFounded. +From Equations Require Import HoTT.All Equations.HoTT.WellFounded. Require Import Stdlib.Unicode.Utf8. Require HoTT.Basics.Overture. -Require Import HoTT.Types.Bool HoTT.Spaces.Nat HoTT.Spaces.List.Core. +From Stdlib Require Import HoTT.Types.Bool HoTT.Spaces.Nat HoTT.Spaces.List.Core. Local Open Scope nat_scope. @@ -124,7 +124,7 @@ testn (S n) with testn n => { Local Open Scope vect_scope. Reserved Notation "x ++v y" (at level 60). -Require Import HoTT.Classes.implementations.peano_naturals. +From Stdlib Require Import HoTT.Classes.implementations.peano_naturals. (* Require Import HoTT.Classes.interfaces.canonical_names. *) Equations vapp {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m)%nat := @@ -137,7 +137,7 @@ where "x ++v y" := (vapp x y). Set Universe Minimization ToSet. Derive NoConfusionHom for vector. Unset Universe Minimization ToSet. -Require Import Equations.HoTT.Tactics. +From Equations Require Import HoTT.Tactics. #[local] Instance vector_eqdec@{i +|+} {A : Type@{i}} {n} `(EqDec@{i} A) : EqDec (vector A n). Proof. diff --git a/test-suite/test-hott.v b/test-suite/HoTT/test_hott.v similarity index 100% rename from test-suite/test-hott.v rename to test-suite/HoTT/test_hott.v diff --git a/test-suite/LogicType.v b/test-suite/LogicType.v index 3c21da12b..bd0d93050 100644 --- a/test-suite/LogicType.v +++ b/test-suite/LogicType.v @@ -2,7 +2,7 @@ Set Warnings "-notation-overridden". Set Universe Polymorphism. (** Switch to an equality in Type *) -Require Import Equations.Type.All. +From Equations.Type Require Import All. Derive Signature for Id. @@ -35,9 +35,8 @@ Arguments vector A%_type_scope n%_nat_scope. Arguments nil {A}. Arguments cons {A%_type_scope} {n%_nat_scope} a v. Derive Signature for vector. -Require Import Equations.CoreTactics Equations.Type.Tactics. -Require Import Equations.Type.Tactics. -Require Import Equations.Type.FunctionalInduction. +From Equations Require Import CoreTactics. +From Equations.Type Require Import Tactics FunctionalInduction. Set Universe Minimization ToSet. Derive NoConfusionHom for vector. diff --git a/test-suite/Noconfinv.v b/test-suite/Noconfinv.v index d7b414718..fa2ed89b7 100644 --- a/test-suite/Noconfinv.v +++ b/test-suite/Noconfinv.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations noConfusion_nat_inv (x y : nat) (P : NoConfusion x y) : x = y := noConfusion_nat_inv 0 0 _ := eq_refl; diff --git a/test-suite/ack.v b/test-suite/ack.v index c7b02159f..beb35be14 100644 --- a/test-suite/ack.v +++ b/test-suite/ack.v @@ -1,6 +1,6 @@ (* https://lawrencecpaulson.github.io/2022/08/31/Ackermann-not-PR-I.html *) -Require Import Arith Lia. -From Equations Require Import Equations. +From Stdlib Require Import Arith Lia. +From Equations.Prop Require Import Equations. Equations ack (p : nat * nat) : nat by wf p (lexprod _ _ lt lt) := ack (0, n) := S n; diff --git a/test-suite/agda_1408.v b/test-suite/agda_1408.v index b26a01bd0..3ed03a9e3 100644 --- a/test-suite/agda_1408.v +++ b/test-suite/agda_1408.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Axiom I : Set. Axiom i1 i2 : I. @@ -17,5 +17,6 @@ Inductive P : forall {i}, D i -> Set := Derive Signature for P. Derive NoConfusionHom for P. +#[warning="-solve_obligation_error,functional-induction-derivation-failure"] Equations Foo (p : P d1) : Set := Foo p1 := nat. diff --git a/test-suite/agda_1775.v b/test-suite/agda_1775.v index 0c29ea42e..4e6dae7bb 100644 --- a/test-suite/agda_1775.v +++ b/test-suite/agda_1775.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import Utf8. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Utf8. (* Set Universe Polymorphism. *) (** Can we define NoConfusion in SProp (squashing equalities of arguments)? Would not allow to show equivalence to (x = y) for non-strict sets. *) diff --git a/test-suite/attributes.v b/test-suite/attributes.v index 41f5ca489..8e7c4c6e2 100644 --- a/test-suite/attributes.v +++ b/test-suite/attributes.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Ltac solvetac := match goal with |- ?T => exact 0 end. diff --git a/test-suite/cfold.v b/test-suite/cfold.v index f1fd2f2b6..6214b311d 100644 --- a/test-suite/cfold.v +++ b/test-suite/cfold.v @@ -2,9 +2,10 @@ Proof size is now constant instead of quadratic., but program is as straightforward as in Agda. *) -Require Import Arith. -From Equations Require Import Equations. -Require Import Stdlib.Bool.Bool. +From Stdlib Require Import Arith. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Bool.Bool. Set Keyed Unification. Set Implicit Arguments. diff --git a/test-suite/daaa.v b/test-suite/daaa.v index 62ef6bab4..58f1296d5 100644 --- a/test-suite/daaa.v +++ b/test-suite/daaa.v @@ -1,4 +1,4 @@ -Require Import Equations. +From Equations Require Import Equations. Inductive A : Set := a : A | d : A -> A -> A -> A. diff --git a/test-suite/depelim.v b/test-suite/depelim.v index a7a27cc64..e0383db45 100644 --- a/test-suite/depelim.v +++ b/test-suite/depelim.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Goal forall x : nat, let y := S x in let z := S y in x = x. Proof. diff --git a/test-suite/Noconflet.v b/test-suite/disabled/Noconflet.v similarity index 93% rename from test-suite/Noconflet.v rename to test-suite/disabled/Noconflet.v index aabadf3c7..64ac378fc 100644 --- a/test-suite/Noconflet.v +++ b/test-suite/disabled/Noconflet.v @@ -1,4 +1,4 @@ -Require Import Equations. +From Equations.Prop Require Import Equations. Derive NoConfusion for vector. diff --git a/test-suite/agda_1775_full.v b/test-suite/disabled/agda_1775_full.v similarity index 98% rename from test-suite/agda_1775_full.v rename to test-suite/disabled/agda_1775_full.v index 22fc01423..4eedce685 100644 --- a/test-suite/agda_1775_full.v +++ b/test-suite/disabled/agda_1775_full.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations DepElimDec HSets. +From Equations Require Import Equations. (* Set Universe Polymorphism. *) (** Can we define NoConfusion in SProp (squashing equalities of arguments)? Would not allow to show equivalence to (x = y) for non-strict sets. *) @@ -40,7 +40,7 @@ Definition equiv_adj {A B} {E: Equiv A B} (x : A) Notation " 'rew' H 'in' c " := (@eq_rect _ _ _ c _ H) (at level 20). -Require Import Utf8. +From Stdlib Require Import Utf8. Notation " X <~> Y " := (Equiv X Y) (at level 90, no associativity, Y at next level). diff --git a/test-suite/noconf_hom.v b/test-suite/disabled/noconf_hom.v similarity index 83% rename from test-suite/noconf_hom.v rename to test-suite/disabled/noconf_hom.v index 7afee5f18..b54440a4e 100644 --- a/test-suite/noconf_hom.v +++ b/test-suite/disabled/noconf_hom.v @@ -1,7 +1,7 @@ - -Require Import Program Bvector List Relations. -From Equations Require Import Equations Signature DepElimDec. -Require Import Utf8. +Set Warnings "-deprecated-library-file-since-8.20". +From Stdlib Require Import Program Bvector List Relations. +From Equations Require Import Equations Signature. +From Stdlib Require Import Utf8. Unset Equations WithK. Inductive Vec (A : Set) : nat -> Set := diff --git a/test-suite/scope_noK.v b/test-suite/disabled/scope_noK.v similarity index 99% rename from test-suite/scope_noK.v rename to test-suite/disabled/scope_noK.v index d6f891f9a..0ec673809 100644 --- a/test-suite/scope_noK.v +++ b/test-suite/disabled/scope_noK.v @@ -1,12 +1,11 @@ (** Example by Rafaël Bocquet: POPLmark part 1A with inductive definition of scope and well-scoped variables (and terms, types and environments). *) -Require Import Equations.Equations. -Require Import Equations.DepElimDec. +From Equations.Prop Require Import Equations. Require Import Stdlib.Logic.Eqdep_dec. Require Import Stdlib.Classes.EquivDec. -Require Import Program. -Require Import Arith. +From Stdlib Require Import Program. +From Stdlib Require Import Arith. Ltac simpl_exist := repeat ( diff --git a/test-suite/smolka_inj_K2.v b/test-suite/disabled/smolka_inj_K2.v similarity index 97% rename from test-suite/smolka_inj_K2.v rename to test-suite/disabled/smolka_inj_K2.v index 0108eefb3..84f9ea307 100644 --- a/test-suite/smolka_inj_K2.v +++ b/test-suite/disabled/smolka_inj_K2.v @@ -1,9 +1,10 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. + Set Equations Transparent. -Inductive K : nat -> nat -> Type := -| K1: K x +Inductive K (x : nat) : nat -> nat -> Type := +| K1: K x x | K2: forall y z w, w = y -> K x w -> K y z -> K x z. diff --git a/test-suite/square_elim.v b/test-suite/disabled/square_elim.v similarity index 99% rename from test-suite/square_elim.v rename to test-suite/disabled/square_elim.v index 3a6951073..b180d8594 100644 --- a/test-suite/square_elim.v +++ b/test-suite/disabled/square_elim.v @@ -1,4 +1,5 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. + (** Taken from Agda issue 3034: https://github.com/agda/agda/issues/3034 *) @@ -13,7 +14,7 @@ Set Universe Polymorphism. Import Sigma_Notations. Set Equations Transparent. -Obligation Tactic := idtac. +Local Obligation Tactic := idtac. Lemma singleton_eq {A} (x : A) (p q : { y : A & x = y }) : p = q. Proof. destruct p, q. destruct pr2. destruct pr3. reflexivity. diff --git a/test-suite/telescopes.v b/test-suite/disabled/telescopes.v similarity index 96% rename from test-suite/telescopes.v rename to test-suite/disabled/telescopes.v index 985efc273..049e8770b 100644 --- a/test-suite/telescopes.v +++ b/test-suite/disabled/telescopes.v @@ -1,9 +1,10 @@ -Require Import Equations Utf8. +From Equations Require Import Equations. +From Stdlib Require Import Utf8. Set Universe Polymorphism. Import Sigma_Notations. Open Scope equations_scope. Polymorphic -Definition pr1_seq {A} {P : A -> Type} {p q : sigma A P} (e : p = q) : p.1 = q.1. +Definition pr1_seq {A} {P : A -> Type} {p q : sigma P} (e : p = q) : p.1 = q.1. Proof. destruct e. apply eq_refl. Defined. Require Vector. @@ -30,13 +31,13 @@ Definition cong@{i j} {A : Type@{i}} {B : Type@{j}} (f : A -> B) {x y : A} (e : (* aka ap *) Lemma cong_iter {A B C} (f : A -> B) (g : B -> C) (x y : A) (e : x = y) : - Top.cong g (Top.cong f e) = Top.cong (fun x => g (f x)) e. -Proof. revert y e. refine (Top.J _ _). reflexivity. Qed. + cong g (cong f e) = cong (fun x => g (f x)) e. +Proof. revert y e. refine (J _ _). reflexivity. Qed. Lemma cong_subst2 {A B C} (f : C -> B) (x y : A) (e : x = y) (z w : A -> C) (p : z x = w x) : - Top.cong f (Top.subst2 (P:=fun x : A => z x = w x) p y e) = - Top.subst2 (P := fun x : A => f (z x) = f (w x)) (Top.cong f p) y e. -Proof. revert y e. refine (Top.J _ _). simpl. reflexivity. Defined. + cong f (subst2 (P:=fun x : A => z x = w x) p y e) = + subst2 (P := fun x : A => f (z x) = f (w x)) (cong f p) y e. +Proof. revert y e. refine (J _ _). simpl. reflexivity. Defined. Definition congd {A} {B : A -> Type} (f : forall x : A, B x) {x y : A} (p : x = y) : subst p (f x) = f y := @@ -106,8 +107,6 @@ Proof. apply axiom_triangle. Defined. -Require Import DepElimDec. - (* Unset Equations OCaml Splitting. *) (* BUG *) (* Equations tel_eq (Δ : Tel) (t s : Tuple Δ) : Type := *) @@ -231,10 +230,10 @@ Module Telescopes. Equations J {Δ : Tel} (r : Δ) (P : forall s : Δ, eq Δ r s -> Type) (p : P r (refl r)) (s : Δ) (e : eq _ r s) : P s e := - J (Δ:=inj A) a P p b e := Top.J P p b e; + J (Δ:=inj A) a P p b e := J P p b e; J (Δ:=ext A f) a P p b e := (* (sigmaI _ r rs) P p (sigmaI _ s ss) (sigmaI _ e es) := *) - Top.J (x:=a.1) + J (x:=a.1) (fun (s' : A) (e' : a.1 = s') => forall (ss' : f s') (es' : eq (f s') (rewP e' at f in a.2) ss'), P &(s' & ss') &(e' & es')) @@ -306,7 +305,7 @@ Module Telescopes. unshelve refine {| equiv_inv e := telei t in eq_refl |}. - red; intros. destruct x. reflexivity. - red; intros. destruct x. now destruct pr2. - - intros [x eq]. revert t eq. refine (Top.J@{i i} _ _). constructor. + - intros [x eq]. revert t eq. refine (J@{i i} _ _). constructor. Defined. Fixpoint eq_eq_equiv@{i} (Δ : Tel@{i}) : forall (u v : Δ) (e : u = v), u == v := @@ -386,11 +385,11 @@ Module Telescopes. set (bar := (equiv_inv@{i} (equiv@{i} _ foo))) in *. change (bar = foo) in H0. symmetry in H0. unfold foo in H0. subst foo. clearbody bar. revert bar H0. - refine (@Top.subst2@{i i} _ _ _ _). simpl. - simpl. red in H. specialize (H _ _ _ He.2). destruct He. simpl. apply Top.cong. apply H. + refine (@subst2@{i i} _ _ _ _). simpl. + simpl. red in H. specialize (H _ _ _ He.2). destruct He. simpl. apply cong. apply H. Defined. - Require Import EqDecInstances. +From Equations.Prop Require Import EqDecInstances. Typeclasses Transparent telescope. Transparent path_sigma_equiv path_sigma_uncurried. @@ -404,7 +403,7 @@ Module Telescopes. (equiv_inv (IsEquiv := path_sigma_equiv _ _ _) e).2). set (foo := eq_eq_equiv_inv _ _ _ _) in *. symmetry in H. clearbody foo. revert foo H. - refine (Top.subst2@{i i} _). + refine (subst2@{i i} _). refine (eisretr (path_sigma_uncurried u v) _). Defined. @@ -422,8 +421,8 @@ Module Telescopes. - apply retr. - revert v. induction Δ as [ | A t IH]. - + refine (Top.J@{i i} _ _). constructor. - + simpl in u; refine (Top.J@{i i} _ _). + + refine (J@{i i} _ _). constructor. + + simpl in u; refine (J@{i i} _ _). simpl sect. rewrite (IH u.1 u.2 u.2 eq_refl). simpl eq_eq_equiv. simpl retr. set (r:=retr@{i} _ _ _ _) in *. @@ -434,7 +433,7 @@ Module Telescopes. apply axiom_triangle. (* clearbody lhs. *) (* clearbody lhs. *) - (* revert lhs. now refine (Top.J _ _). *) + (* revert lhs. now refine (J _ _). *) Defined. (** Telescopic equality is equivalent to equality of the sigmas. *) @@ -523,9 +522,9 @@ Module Telescopes. (compose f^-1 g^-1) _ _ _ . Proof. exact - (fun c => Top.cong g (eisretr f (g^-1 c)) @ eisretr g c). + (fun c => cong g (eisretr f (g^-1 c)) @ eisretr g c). exact - (fun a => Top.cong (f^-1) (eissect g (f a)) @ eissect f a). + (fun a => cong (f^-1) (eissect g (f a)) @ eissect f a). intro. simpl. apply axiom_triangle. @@ -545,7 +544,7 @@ End Telescopes. Module Example_cons. -Notation " 'rewP' H 'at' B 'in' c " := (@Top.subst _ _ B _ H c) (at level 20, only parsing). +Notation " 'rewP' H 'at' B 'in' c " := (@subst _ _ B _ H c) (at level 20, only parsing). Import Telescopes. @@ -597,7 +596,7 @@ Defined. Proof. intros. apply eq_points_equiv. - apply (Top.cong equiv_inv) in H. + apply (cong equiv_inv) in H. transitivity (f ^-1 (f u)). symmetry. apply (eissect f u). transitivity (f ^-1 (f v)). apply H. apply (eissect f v). Defined. @@ -624,15 +623,15 @@ Defined. format "'[' 'telei' '/ ' x .. y 'in' z ']'", only parsing) : telescope. - Notation " a '={' P ; e } b " := (Top.subst (P:=P) e a = b) (at level 90). + Notation " a '={' P ; e } b " := (subst (P:=P) e a = b) (at level 90). Notation " a '==={' P ; e } b " := (subst P _ _ e a = b) (at level 90, only parsing) : telescope. Lemma equiv_cong_subst {A B} (P : B -> Type) (f : A -> B) (s t : A) (e : s = t) (u : P (f s)) - (v : P (f t)) : u =_{(fun x => P (f x)); e} v <~> (u =_{P; Top.cong f e} v). + (v : P (f t)) : u =_{(fun x => P (f x)); e} v <~> (u =_{P; cong f e} v). Proof. - unfold Top.subst. + unfold subst. destruct e. simpl. apply equiv_id. Defined. @@ -640,10 +639,10 @@ Defined. (P : forall x : A, B x -> Type) (f : forall x : A, B x) (s t : A) (e : s = t) (u : P s (f s)) (v : P t (f t)) : u =_{(fun x => P x (f x)); e} v <~> - (Top.J (fun y e => P y (rew e in (f s))) - u _ e =_{(fun x => P _ x); Top.congd f e} v). + (J (fun y e => P y (rew e in (f s))) + u _ e =_{(fun x => P _ x); congd f e} v). Proof. - unfold Top.subst. + unfold subst. destruct e. simpl. apply equiv_id. Defined. @@ -673,7 +672,7 @@ Defined. apply axiom_triangle. (* apply eisretr. *) - (* red; intros. simpl. destruct x. simpl. apply Top.cong. *) + (* red; intros. simpl. destruct x. simpl. apply cong. *) (* apply eissect. *) (* intros [x bx]. *) @@ -687,9 +686,9 @@ Defined. simpl. unshelve refine {| equiv a := &(a.1 & e a.1 a.2) |}. unshelve refine {| equiv_inv a := &(a.1 & inv_equiv (e a.1) a.2) |}. - red; intros. simpl. destruct x. simpl. apply Top.cong. + red; intros. simpl. destruct x. simpl. apply cong. apply eisretr. - red; intros. simpl. destruct x. simpl. apply Top.cong. + red; intros. simpl. destruct x. simpl. apply cong. apply eissect. intros [x bx]. @@ -723,7 +722,7 @@ Defined. induction Δ. + simpl in *. destruct r. unfold subst. simpl. - edestruct (eq_sym (Top.J_on_refl@{i i} _ _ s)). + edestruct (eq_sym (J_on_refl@{i i} _ _ s)). apply eq_sym_equiv. + unfold subst. revert b r s. refine (J@{i i i} _ _ _). @@ -763,7 +762,7 @@ Defined. refine (equiv_tele_r _). intros x. unfold square_tel. simpl in x. - revert v x s. refine (Top.J@{i i} _ _). intros s. + revert v x s. refine (J@{i i} _ _). intros s. simpl. unfold square_tel. unfold cong_tel. simpl. subst eqΔ. simpl in *. refine (equiv_sym _). apply subst_subst. @@ -771,7 +770,7 @@ Defined. - simpl. refine (equiv_tele_r _). intros. destruct v. simpl in *. subst eqΔ. simpl in *. revert pr1 x pr2 s. - refine (Top.J@{i i} _ _). + refine (J@{i i} _ _). simpl. intros. specialize (X u.1 u.2 pr2). specialize (X (fun ρ => a &(u.1 & ρ))). simpl in X. specialize (X (fun ρ => b &(u.1 & ρ))). @@ -827,7 +826,7 @@ Defined. simpl. unfold solution_left. unfold NoConfusion.noConfusion_nat_obligation_1. simpl. destruct x. destruct pr2. destruct pr2. simpl. - refine (Top.cong@{i i} _ _). + refine (cong@{i i} _ _). revert pr3. simplify_one_dep_elim. simplify_one_dep_elim. intros. reflexivity. @@ -835,7 +834,7 @@ Defined. intros. simpl. destruct x as (x&n'&v&e). unfold solution_left_dep, apply_noConfusion. simpl. - unfold Top.cong. + unfold cong. revert e. simpl. simplify_one_dep_elim. simplify_one_dep_elim. @@ -937,7 +936,7 @@ Inductive Iseq2 {A : Type} : forall x y: A, x = y -> y = x -> Type := Lemma invIseq2' {A} (x : A) (e : x = x) (iseq : Iseq2 x x e eq_refl) : &{ H : eq_refl = e & - (Top.subst (P:=fun e => Iseq2 x x e eq_refl) H (iseq2 x)) = iseq }. + (subst (P:=fun e => Iseq2 x x e eq_refl) H (iseq2 x)) = iseq }. generalize_eqs_sig iseq. destruct iseq. @@ -1087,8 +1086,8 @@ Lemma invIseq2' {A} (x : A) (e : x = x) (iseq : Iseq2 x x e eq_refl) : Lemma rew_sym@{i} (A : Type@{i}) {Δ : A -> Tel@{i}} (x y : A) (px : Δ x) (py : Δ y) (e : y = x) : - px =={Δ x} Top.subst (P:=Δ) e py -> - Top.subst (P:=Δ) (eq_sym e) px =={Δ y} py. + px =={Δ x} subst (P:=Δ) e py -> + subst (P:=Δ) (eq_sym e) px =={Δ y} py. Proof. destruct e. simpl. trivial. Defined. Equations sym {Δ : Tel} {s t : Δ} (e : s =={Δ} t) : t =={Δ} s := @@ -1299,7 +1298,7 @@ Lemma invIseq2' {A} (x : A) (e : x = x) (iseq : Iseq2 x x e eq_refl) : destruct p. reflexivity. destruct p. destruct p. - apply Top.cong. apply IHx. + apply cong. apply IHx. apply p. Defined. @@ -1524,8 +1523,8 @@ Lemma invIseq2' {A} (x : A) (e : x = x) (iseq : Iseq2 x x e eq_refl) : reflexivity. destruct x0. destruct x0. - change (Top.cong S x0 = Top.cong S x1). - apply Top.cong. + change (cong S x0 = cong S x1). + apply cong. simpl in x0, x1. diff --git a/test-suite/telescopes_nonempty.v b/test-suite/disabled/telescopes_nonempty.v similarity index 99% rename from test-suite/telescopes_nonempty.v rename to test-suite/disabled/telescopes_nonempty.v index 66fe90658..ef4a20857 100644 --- a/test-suite/telescopes_nonempty.v +++ b/test-suite/disabled/telescopes_nonempty.v @@ -1,11 +1,12 @@ -Require Import Equations. +From Equations.Prop Require Import Equations SigmaNotations. Set Universe Polymorphism. -Open Scope sigma_scope. +Import Sigma_Notations. +Open Scope equations_scope. Polymorphic -Definition pr1_seq {A} {P : A -> Type} {p q : sigma A P} (e : p = q) : p.1 = q.1. +Definition pr1_seq {A} {P : A -> Type} {p q : sigma P} (e : p = q) : p.1 = q.1. Proof. destruct e. apply eq_refl. Defined. -Require Vector. +From Stdlib Require Vector. Derive NoConfusion for Vector.t. Notation " 'rew' H 'in' c " := (@eq_rect _ _ _ c _ H) (at level 20). @@ -93,8 +94,6 @@ Proof. apply axiom. Defined. -Require Import DepElimDec. - (* Unset Equations OCaml Splitting. *) (* BUG *) (* Equations tel_eq (Δ : Tel) (t s : Tuple Δ) : Type := *) @@ -404,8 +403,6 @@ telescope ((fun a : A => extend_tele (f a) (fun fa : f a => Γ &(a & fa))) t)) simpl. red in H. specialize (H _ _ _ He.2). destruct He. simpl. apply Top.cong. apply H. Defined. - Require Import EqDecInstances. - Typeclasses Transparent telescope. Transparent path_sigma_equiv path_sigma_uncurried. Lemma retr : forall (Δ : Tel) (u v : Δ), Sect (eq_eq_equiv Δ u v) (eq_eq_equiv_inv Δ u v). diff --git a/test-suite/univpoly.v b/test-suite/disabled/univpoly.v similarity index 90% rename from test-suite/univpoly.v rename to test-suite/disabled/univpoly.v index 3513a93ab..a09927f43 100644 --- a/test-suite/univpoly.v +++ b/test-suite/disabled/univpoly.v @@ -1,10 +1,10 @@ -Require Import Equations.Equations. +From Equations.Prop Require Import Equations. Set Universe Polymorphism. Set Implicit Arguments. (* Move fix_proto to poly version *) Equations(noind) id (A : Type) (a : A) : A := -id A x := x. +id x := x. Set Printing Universes. (* Move fix_proto to poly version *) Equations foo (A : _) (a : A) : A := diff --git a/test-suite/divmod.v b/test-suite/divmod.v index 9a85b2aa6..f16b7570c 100644 --- a/test-suite/divmod.v +++ b/test-suite/divmod.v @@ -1,5 +1,5 @@ From Stdlib Require Import Arith Lia. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations? Div (x y : nat) : nat by wf x lt := { Div x 0 := 0 ; diff --git a/test-suite/dune b/test-suite/dune new file mode 100644 index 000000000..64f6856fd --- /dev/null +++ b/test-suite/dune @@ -0,0 +1,9 @@ +(coq.theory + ; This determines the -R flag + (name Equations.TestSuite) + (package rocq-equations-tests) + (synopsis "Equations Plugin Tests") + (plugins rocq-runtime.plugins.extraction rocq-equations.plugin) + (theories Stdlib Equations Equations.Prop Equations.Type)) + +(include_subdirs no) diff --git a/test-suite/eqdec_error.v b/test-suite/eqdec_error.v index 2f4692c69..020369fd4 100644 --- a/test-suite/eqdec_error.v +++ b/test-suite/eqdec_error.v @@ -1,6 +1,6 @@ From Stdlib Require Import BinNums. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Fail Derive EqDec for positive. Derive NoConfusion EqDec for positive. diff --git a/test-suite/f91.v b/test-suite/f91.v index ba4f0d5c6..a24658ae3 100644 --- a/test-suite/f91.v +++ b/test-suite/f91.v @@ -6,11 +6,8 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Program. -Require Import Equations Bvector List. -Require Import Relations. -Require Import Lia. -Require Import Arith Wf_nat. +From Stdlib Require Import Program List Relations Lia Arith Wf_nat. +From Equations.Prop Require Import Equations. Set Program Mode. Arguments minus : simpl never. diff --git a/test-suite/fin.v b/test-suite/fin.v index 14926e622..97b321806 100644 --- a/test-suite/fin.v +++ b/test-suite/fin.v @@ -1,4 +1,5 @@ -Require Import Program Equations.Prop.EqDecInstances Equations.Prop.Equations. +From Stdlib Require Import Program. +From Equations.Prop Require Import EqDecInstances Equations. Import Sigma_Notations. Local Open Scope equations_scope. Set Equations Transparent. diff --git a/test-suite/fle_trans.v b/test-suite/fle_trans.v index 537087f67..af827a6fa 100644 --- a/test-suite/fle_trans.v +++ b/test-suite/fle_trans.v @@ -2,7 +2,7 @@ (** printing elimination %\coqdoctac{elimination}% *) (** printing Derive %\coqdockw{Derive}% *) (* begin hide *) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Set Implicit Arguments. @@ -51,7 +51,7 @@ Print Assumptions fle_trans. %\texttt{Closed under the global context}% *) (* end hide *) -Require Import Program. +From Stdlib Require Import Program. (* begin hide *) Fixpoint fle_trans' {n : nat} {i j k : fin n} (p : fle i j) (q : fle j k) : fle i k. diff --git a/test-suite/funelim_ack.v b/test-suite/funelim_ack.v index 4a018cbca..2a9a24a48 100644 --- a/test-suite/funelim_ack.v +++ b/test-suite/funelim_ack.v @@ -1,7 +1,7 @@ From Equations Require Import CoreTactics. From Equations.Prop Require Import DepElim. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Set Equations Transparent. Equations ack (m n : nat) : nat by wf (m, n) (Equations.Prop.Subterm.lexprod _ _ lt lt) := ack 0 n := S n; diff --git a/test-suite/gcd.v b/test-suite/gcd.v index e6684afc0..4810e3001 100644 --- a/test-suite/gcd.v +++ b/test-suite/gcd.v @@ -1,6 +1,7 @@ -From Equations Require Import Equations. -Require Import Relations. -Require Import Arith Lia. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Relations. +From Stdlib Require Import Arith Lia. Set Keyed Unification. Ltac subst_lets := @@ -24,7 +25,7 @@ gcd x y with gt_eq_gt_dec x y := { Transparent gcd. Eval compute in gcd 18 84. -Require Import ExtrOcamlBasic. +From Stdlib Require Import ExtrOcamlBasic. Extraction Inline pr1 pr2. Extraction gcd. (* Extraction gcd_unfold. *) diff --git a/test-suite/innacs.v b/test-suite/innacs.v index 3624eae55..76a5a5551 100644 --- a/test-suite/innacs.v +++ b/test-suite/innacs.v @@ -1,6 +1,8 @@ -Require Import Equations. -Require Import Vector. -Require Import fin. +From Equations.Prop Require Import Equations. + +#[warnings="-warn-library-file-stdlib-vector"] +From Stdlib Require Import Vector. +From Equations.TestSuite Require Import fin. Notation vector := Vector.t. Arguments Vector.nil {A}. Arguments Vector.cons {A} _ {n}. diff --git a/test-suite/interval.v b/test-suite/interval.v index 5c6dd13cc..98bbf4dd2 100644 --- a/test-suite/interval.v +++ b/test-suite/interval.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List Arith Lia. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List Arith Lia. Import ListNotations. Set Keyed Unification. diff --git a/test-suite/issues/coq_pr_16995.v b/test-suite/issues/coq_pr_16995.v index 69e5f9b78..b8d300d32 100644 --- a/test-suite/issues/coq_pr_16995.v +++ b/test-suite/issues/coq_pr_16995.v @@ -27,7 +27,7 @@ Register Classes.NoConfusionPackage as equations.noconfusion.class. Register Classes.apply_noConfusion as equations.depelim.apply_noConfusion. Register DepElim.simplification_sigma1_dep as equations.depelim.simpl_sigma_dep. Register DepElim.opaque_ind_pack_inv as equations.depelim.opaque_ind_pack_eq_inv. -Import Equations.CoreTactics. +Import CoreTactics. Set Warnings "-notation-overridden". Import Equations.Type.Logic. diff --git a/test-suite/issues/issue100.v b/test-suite/issues/issue100.v index 9d8316d71..f1236bedc 100644 --- a/test-suite/issues/issue100.v +++ b/test-suite/issues/issue100.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: * https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L13 *) diff --git a/test-suite/issues/issue104.v b/test-suite/issues/issue104.v index d6fd9f2ab..35b1baa55 100644 --- a/test-suite/issues/issue104.v +++ b/test-suite/issues/issue104.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. (* This type is from VST: * https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L13 *) Fixpoint compact_sum (T: list Type): Type := diff --git a/test-suite/issues/issue105.v b/test-suite/issues/issue105.v index 8e08fe392..4f0147f9c 100644 --- a/test-suite/issues/issue105.v +++ b/test-suite/issues/issue105.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. (* This type is from VST: * https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L13 *) Fixpoint compact_sum (T: list Type): Type := diff --git a/test-suite/issues/issue106.v b/test-suite/issues/issue106.v index 5146990c1..d01dbcdf6 100644 --- a/test-suite/issues/issue106.v +++ b/test-suite/issues/issue106.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue107.v b/test-suite/issues/issue107.v index 878250cdd..d4f290b49 100644 --- a/test-suite/issues/issue107.v +++ b/test-suite/issues/issue107.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. (* The rest is a nonsensical, just to give a minimalistic reproducible example *) Inductive Foo := diff --git a/test-suite/issues/issue107_2.v b/test-suite/issues/issue107_2.v index 34dbf0989..67501907f 100644 --- a/test-suite/issues/issue107_2.v +++ b/test-suite/issues/issue107_2.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. (* The rest is a nonsensical, just to give a minimalistic reproducible example *) Inductive Foo := diff --git a/test-suite/issues/issue112.v b/test-suite/issues/issue112.v index fe461be2f..131b8b1c7 100644 --- a/test-suite/issues/issue112.v +++ b/test-suite/issues/issue112.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue113.v b/test-suite/issues/issue113.v index e65326345..b3885d880 100644 --- a/test-suite/issues/issue113.v +++ b/test-suite/issues/issue113.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Inductive foo := | List : list foo -> foo. diff --git a/test-suite/issues/issue114.v b/test-suite/issues/issue114.v index 847998abb..ce830a575 100644 --- a/test-suite/issues/issue114.v +++ b/test-suite/issues/issue114.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue116.v b/test-suite/issues/issue116.v index dc2189fbe..06f4044b3 100644 --- a/test-suite/issues/issue116.v +++ b/test-suite/issues/issue116.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Inductive foo := | Sum : list foo -> foo. diff --git a/test-suite/issues/issue117.v b/test-suite/issues/issue117.v index 2317530d9..bb5e39a2e 100644 --- a/test-suite/issues/issue117.v +++ b/test-suite/issues/issue117.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Inductive foo := | Sum : list foo -> foo. diff --git a/test-suite/issues/issue120.v b/test-suite/issues/issue120.v index f2b9fd499..679bc7558 100644 --- a/test-suite/issues/issue120.v +++ b/test-suite/issues/issue120.v @@ -1,5 +1,5 @@ Require Export Lia. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. From Stdlib Require Import Relation_Operators. From Stdlib Require Import Lexicographic_Product. diff --git a/test-suite/issues/issue124.v b/test-suite/issues/issue124.v index 2c87b1132..077d9aea9 100644 --- a/test-suite/issues/issue124.v +++ b/test-suite/issues/issue124.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. Import ListNotations. Equations foo (f: option (nat -> nat)) (l: list nat) : list nat := diff --git a/test-suite/issues/issue129.v b/test-suite/issues/issue129.v index d376a9c7f..50885698d 100644 --- a/test-suite/issues/issue129.v +++ b/test-suite/issues/issue129.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Fixpoint slow n : unit := match n with O => tt | S n => match slow n with tt => slow n end end. diff --git a/test-suite/issues/issue143.v b/test-suite/issues/issue143.v index 99bf1e93f..9c233cf60 100644 --- a/test-suite/issues/issue143.v +++ b/test-suite/issues/issue143.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import Lia. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Lia. Section Tests. diff --git a/test-suite/issues/issue176.v b/test-suite/issues/issue176.v index 92e80b31d..a19d8a75a 100644 --- a/test-suite/issues/issue176.v +++ b/test-suite/issues/issue176.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations foo (n : nat) : nat := foo x := let x := 0 in x. diff --git a/test-suite/issues/issue190.v b/test-suite/issues/issue190.v index 7337a4e7a..02b6b7c48 100644 --- a/test-suite/issues/issue190.v +++ b/test-suite/issues/issue190.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations foo (n : nat) : nat := { foo 0 diff --git a/test-suite/issues/issue191.v b/test-suite/issues/issue191.v index 05696b7ad..4d8bd756f 100644 --- a/test-suite/issues/issue191.v +++ b/test-suite/issues/issue191.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* Assuming UIP *) From Stdlib.Logic Require Import Eqdep. diff --git a/test-suite/issues/issue193.v b/test-suite/issues/issue193.v index 9a744c007..6f1628da0 100644 --- a/test-suite/issues/issue193.v +++ b/test-suite/issues/issue193.v @@ -1,5 +1,5 @@ -Require Import Program. -From Equations Require Import Equations. +From Stdlib Require Import Program. +From Equations.Prop Require Import Equations. #[local] Obligation Tactic := program_simpl. Equations h_type (P : Type) (H : P) : P := h_type P H => let H1 := H in _. diff --git a/test-suite/issues/issue200.v b/test-suite/issues/issue200.v index 484e78f3d..ef1c6c98d 100644 --- a/test-suite/issues/issue200.v +++ b/test-suite/issues/issue200.v @@ -1,4 +1,5 @@ -From Equations Require Import Equations. -Require Import Vector. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Vector. Derive DependentElimination for t. diff --git a/test-suite/issues/issue212.v b/test-suite/issues/issue212.v index be2e5fb3e..c43c09006 100644 --- a/test-suite/issues/issue212.v +++ b/test-suite/issues/issue212.v @@ -1,4 +1,4 @@ -Require Import List. +From Stdlib Require Import List. From Stdlib Require Import Lia ssreflect. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -6,7 +6,7 @@ Set Asymmetric Patterns. Import ListNotations. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Section list_size. Context {A : Type} (f : A -> nat). diff --git a/test-suite/issues/issue228.v b/test-suite/issues/issue228.v index 11ee9c731..3b15f1d39 100644 --- a/test-suite/issues/issue228.v +++ b/test-suite/issues/issue228.v @@ -1,9 +1,9 @@ -From Coq Require Import Utf8. -From Coq Require Import Equality. -From Coq Require Import Arith. -From Coq Require Vector. +From Stdlib Require Import Utf8. +From Stdlib Require Import Equality. +From Stdlib Require Import Arith. +From Stdlib Require Vector. Import Vector.VectorNotations. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Inductive MType : Type := | Base : Set → MType diff --git a/test-suite/issues/issue24.v b/test-suite/issues/issue24.v index 9d48bf10d..975f3114c 100644 --- a/test-suite/issues/issue24.v +++ b/test-suite/issues/issue24.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Equations Rtuple' (domain : list Type) : Type := Rtuple' nil := unit; diff --git a/test-suite/issues/issue240.v b/test-suite/issues/issue240.v index 85b97f87d..8b9fd2b33 100644 --- a/test-suite/issues/issue240.v +++ b/test-suite/issues/issue240.v @@ -1,5 +1,4 @@ -Require Import Equations.Equations. - +From Equations.Prop Require Import Equations. Inductive T1: Type := | C { T: Type }: T1 . diff --git a/test-suite/issues/issue246.v b/test-suite/issues/issue246.v index 7350bff15..40f68179f 100644 --- a/test-suite/issues/issue246.v +++ b/test-suite/issues/issue246.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Inductive t (u : unit) := | strange : t tt -> t u. diff --git a/test-suite/issues/issue249.v b/test-suite/issues/issue249.v index d13975661..3f895f518 100644 --- a/test-suite/issues/issue249.v +++ b/test-suite/issues/issue249.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* Removing this line makes Derive Subterm go through without troubles *) Set Universe Polymorphism. diff --git a/test-suite/issues/issue25.v b/test-suite/issues/issue25.v index 0fc9a106a..7624e8942 100644 --- a/test-suite/issues/issue25.v +++ b/test-suite/issues/issue25.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Equations Rtuple'' (domain : list Type) : Type := Rtuple'' nil => unit; diff --git a/test-suite/issues/issue252.v b/test-suite/issues/issue252.v index 08c6b5fb6..19c5dcea5 100644 --- a/test-suite/issues/issue252.v +++ b/test-suite/issues/issue252.v @@ -1,5 +1,4 @@ -Require Import Equations.Equations. - +From Equations.Prop Require Import Equations. Inductive vec (A:Type) : nat -> Type := | nil : vec A 0 | cons : forall n, A -> vec A n -> vec A (S n). diff --git a/test-suite/issues/issue258.v b/test-suite/issues/issue258.v index 627e7c843..fe9c48014 100644 --- a/test-suite/issues/issue258.v +++ b/test-suite/issues/issue258.v @@ -1,5 +1,5 @@ From Stdlib Require Import Psatz. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Inductive Pre := Pi : Pre -> Pre. diff --git a/test-suite/issues/issue272.v b/test-suite/issues/issue272.v index cb69c15ff..c5cc0a34d 100644 --- a/test-suite/issues/issue272.v +++ b/test-suite/issues/issue272.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* If it's the full definition from the start, works fine *) (* Equations even (n : nat) : bool := { *) diff --git a/test-suite/issues/issue273.v b/test-suite/issues/issue273.v index a0dd5384d..e99efcec0 100644 --- a/test-suite/issues/issue273.v +++ b/test-suite/issues/issue273.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. Import ListNotations. Inductive T := C : list T -> T. Show Obligation Tactic. diff --git a/test-suite/issues/issue286.v b/test-suite/issues/issue286.v index 4c8f4fa42..a09d5fc71 100644 --- a/test-suite/issues/issue286.v +++ b/test-suite/issues/issue286.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Axiom P : nat -> Type. diff --git a/test-suite/issues/issue297.v b/test-suite/issues/issue297.v index 20a1f58b8..d3d3c33ae 100644 --- a/test-suite/issues/issue297.v +++ b/test-suite/issues/issue297.v @@ -1,4 +1,5 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. + Goal forall P y, P y -> let n := y in n = 12 -> P n. intros P y py n. simplify ?. apply py. diff --git a/test-suite/issues/issue306.v b/test-suite/issues/issue306.v index 84a4163e2..d2192033d 100644 --- a/test-suite/issues/issue306.v +++ b/test-suite/issues/issue306.v @@ -1,5 +1,5 @@ -Require Import Equations.Prop.Subterm Equations.Prop.DepElim. -From Equations Require Import Equations. +From Equations.Prop Require Import Subterm Equations.Prop.DepElim. +From Equations.Prop Require Import Equations. Unset Equations With Funext. diff --git a/test-suite/issues/issue321.v b/test-suite/issues/issue321.v index ebe990018..f812d68ca 100644 --- a/test-suite/issues/issue321.v +++ b/test-suite/issues/issue321.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Set Warnings "-equations-open-proof-complete". Equations? x : nat := x := 0. diff --git a/test-suite/issues/issue328.v b/test-suite/issues/issue328.v index 9894137ea..7206e68e9 100644 --- a/test-suite/issues/issue328.v +++ b/test-suite/issues/issue328.v @@ -1,6 +1,6 @@ From Stdlib Require Import Lia. Set Implicit Arguments. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Parameter A : Type. diff --git a/test-suite/issues/issue329.v b/test-suite/issues/issue329.v index 7637636e8..993a1175e 100644 --- a/test-suite/issues/issue329.v +++ b/test-suite/issues/issue329.v @@ -1,5 +1,6 @@ -Require Import List ssreflect. -Require Import Equations.Prop.Equations. +From Stdlib Require Import List ssreflect. +From Equations.Prop Require Import Equations. + Import ListNotations. Equations ok_clause (e : nat -> option bool) (xs : list nat) : bool := diff --git a/test-suite/issues/issue338.v b/test-suite/issues/issue338.v index b8c2fd557..b57012d2a 100644 --- a/test-suite/issues/issue338.v +++ b/test-suite/issues/issue338.v @@ -1,6 +1,6 @@ (* success *) From Stdlib Require Import ssreflect. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Import EquationsNotations. Open Scope equations_scope. diff --git a/test-suite/issues/issue346.v b/test-suite/issues/issue346.v index 94f6c9dae..17de835b1 100644 --- a/test-suite/issues/issue346.v +++ b/test-suite/issues/issue346.v @@ -1,5 +1,5 @@ From Stdlib Require Import Program. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Definition tyty := Type -> Type. Inductive X : tyty := | K : X nat. diff --git a/test-suite/issues/issue349.v b/test-suite/issues/issue349.v index f21f6a43a..15b971241 100644 --- a/test-suite/issues/issue349.v +++ b/test-suite/issues/issue349.v @@ -3,7 +3,7 @@ Set Implicit Arguments. From Stdlib Require Import Lia Lists.List. Import ListNotations. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Open Scope bool_scope. @@ -212,7 +212,7 @@ Program Lemma finite_subtree_domain_length_lt : Proof. unfold finite_subtree_domain, finite_subtree_domain'. intros (((? & ? & ? & ? & ?) & ?) & ?) ? ?. - rewrite map_length. + rewrite length_map. apply filter_length_lt'. induction π. - intuition. diff --git a/test-suite/issues/issue353.v b/test-suite/issues/issue353.v index ced20b033..58153e28c 100644 --- a/test-suite/issues/issue353.v +++ b/test-suite/issues/issue353.v @@ -1,5 +1,5 @@ From Stdlib Require Import Arith. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Fixpoint Ack (n m : nat) : nat := match n with diff --git a/test-suite/issues/issue354.v b/test-suite/issues/issue354.v index 782c45122..8cff3eb39 100644 --- a/test-suite/issues/issue354.v +++ b/test-suite/issues/issue354.v @@ -1,5 +1,5 @@ (* From Stdlib Require Import Logic.StrictProp. *) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Inductive Ssig {A : Type} (P : A -> SProp) := | Sexists (a : A) (b : P a) : Ssig P. diff --git a/test-suite/issues/issue389.v b/test-suite/issues/issue389.v index 9a954a4a4..839c0b742 100644 --- a/test-suite/issues/issue389.v +++ b/test-suite/issues/issue389.v @@ -1,4 +1,4 @@ -Require Import Equations.HoTT.All. +From Equations Require Import HoTT.All. Set Universe Polymorphism. Inductive A : Type := | foo : A diff --git a/test-suite/issues/issue393.v b/test-suite/issues/issue393.v index 21c2a96b9..c4033dd71 100644 --- a/test-suite/issues/issue393.v +++ b/test-suite/issues/issue393.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. Inductive In {X} (x : X) : list X -> Type := | here {xs} : In x (x :: xs) @@ -10,7 +11,7 @@ Arguments here {X x xs}. Arguments there {X x y xs} _. Check (there here) : 26 ∈ (43 :: 26 :: 76 :: nil). -(* Does coq-equations mistake variable names sometimes? *) +(* Does rocq-equations mistake variable names sometimes? *) Set Equations Debug. diff --git a/test-suite/issues/issue399.v b/test-suite/issues/issue399.v index 83ca61fbc..019554a60 100644 --- a/test-suite/issues/issue399.v +++ b/test-suite/issues/issue399.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. From Stdlib Require Import Bool. Inductive depInd : Type -> Type := | A : depInd bool diff --git a/test-suite/issues/issue43.v b/test-suite/issues/issue43.v index 832e6d33a..832aaaa11 100644 --- a/test-suite/issues/issue43.v +++ b/test-suite/issues/issue43.v @@ -1,5 +1,5 @@ -Require Import Program Bvector List. -Require Import Relations. +From Stdlib Require Import Program Bvector List. +From Stdlib Require Import Relations. From Equations Require Import Equations DepElimDec. Equations silly {A} (l : list A) : list A := diff --git a/test-suite/issues/issue499.v b/test-suite/issues/issue499.v index b1800c429..0f8233222 100644 --- a/test-suite/issues/issue499.v +++ b/test-suite/issues/issue499.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations bla (n : nat) : nat -> nat by wf n lt := bla 0 := fun m => 0; diff --git a/test-suite/issues/issue500.v b/test-suite/issues/issue500.v index be7dddb66..9ed46f54b 100644 --- a/test-suite/issues/issue500.v +++ b/test-suite/issues/issue500.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Section box. Universe u. diff --git a/test-suite/issues/issue577.v b/test-suite/issues/issue577.v index 3493354bf..fbee34254 100644 --- a/test-suite/issues/issue577.v +++ b/test-suite/issues/issue577.v @@ -1,5 +1,5 @@ From Stdlib Require Import List String. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Module A. Section test. diff --git a/test-suite/issues/issue61.v b/test-suite/issues/issue61.v index 146ad2dd3..737e4734a 100644 --- a/test-suite/issues/issue61.v +++ b/test-suite/issues/issue61.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Fail Equations bug (x : nat) : nat := bug O := O; diff --git a/test-suite/issues/issue63.v b/test-suite/issues/issue63.v index fecb3ca50..4aca5d212 100644 --- a/test-suite/issues/issue63.v +++ b/test-suite/issues/issue63.v @@ -1,7 +1,8 @@ Require Import Stdlib.Vectors.Vector. Require Import Stdlib.PArith.PArith. -Require Import Lia. -Require Import Equations.Prop.Equations. +From Stdlib Require Import Lia. +From Equations.Prop Require Import Equations. + Set Equations With UIP. Generalizable All Variables. @@ -24,7 +25,7 @@ Arguments Ident {a tys dom}. Arguments Morph {a tys} f. Arguments Comp {a tys dom mid cod} f g. Import Sigma_Notations. -Require Import Wellfounded Relations. +From Stdlib Require Import Wellfounded Relations. Derive NoConfusion for positive. Derive EqDec for positive. diff --git a/test-suite/issues/issue7.v b/test-suite/issues/issue7.v index aa75c6829..5f5157d50 100644 --- a/test-suite/issues/issue7.v +++ b/test-suite/issues/issue7.v @@ -1,7 +1,8 @@ Set Warnings "-notation-overridden". -Require Import ssreflect. -Require Import Utf8 Program. -Require Import Equations.Prop.Equations. +From Stdlib Require Import ssreflect. +From Stdlib Require Import Utf8 Program. +From Equations.Prop Require Import Equations. + Inductive TupleT : nat -> Type := | nilT : TupleT 0 diff --git a/test-suite/issues/issue70.v b/test-suite/issues/issue70.v index a9d3ba56b..3326cc2d2 100644 --- a/test-suite/issues/issue70.v +++ b/test-suite/issues/issue70.v @@ -1,5 +1,5 @@ From Stdlib Require Import Fin. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Set Equations Transparent. Derive Signature NoConfusion NoConfusionHom for t. diff --git a/test-suite/issues/issue73.v b/test-suite/issues/issue73.v index 774c0335b..a3d07c041 100644 --- a/test-suite/issues/issue73.v +++ b/test-suite/issues/issue73.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations zip {A} {B} (l1 : list A) (l2 : list B) : list (A*B) := zip (cons h1 t1) (cons h2 t2) := (h1,h2) :: zip t1 t2; diff --git a/test-suite/issues/issue74.v b/test-suite/issues/issue74.v index 6e9d2c57e..fc7788346 100644 --- a/test-suite/issues/issue74.v +++ b/test-suite/issues/issue74.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Import ListNotations. Inductive foo: Set := diff --git a/test-suite/issues/issue75.v b/test-suite/issues/issue75.v index 97a3fdcb3..46bd36e08 100644 --- a/test-suite/issues/issue75.v +++ b/test-suite/issues/issue75.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Set Program Mode. diff --git a/test-suite/issues/issue77.v b/test-suite/issues/issue77.v index c2cd1d0d3..56bef82a8 100644 --- a/test-suite/issues/issue77.v +++ b/test-suite/issues/issue77.v @@ -1,4 +1,5 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. + Require Vector. Notation vector := Vector.t. Arguments Vector.nil {A}. diff --git a/test-suite/issues/issue79.v b/test-suite/issues/issue79.v index baf63b87b..0abf58785 100644 --- a/test-suite/issues/issue79.v +++ b/test-suite/issues/issue79.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue7_extr.v b/test-suite/issues/issue7_extr.v index bcd5a5e1c..011538c6a 100644 --- a/test-suite/issues/issue7_extr.v +++ b/test-suite/issues/issue7_extr.v @@ -1,6 +1,6 @@ -Require Import Equations.Equations Utf8. +From Equations Require Import Equations Utf8. Add Rec LoadPath ".." as Top. -Require Import issue7. +From Stdlib Require Import issue7. Extraction Inline apply_noConfusion. diff --git a/test-suite/issues/issue8.v b/test-suite/issues/issue8.v index 4e1d3b036..12d86bf6b 100644 --- a/test-suite/issues/issue8.v +++ b/test-suite/issues/issue8.v @@ -1,5 +1,6 @@ -Require Import Utf8 Program. -Require Import Equations.Prop.Equations. +From Stdlib Require Import Utf8 Program. +From Equations.Prop Require Import Equations. + Open Scope equations_scope. Set Warnings "-notation-overridden". Notation " '{' x : A & y } " := (@sigma A (fun x : A => y)%type) : type_scope. diff --git a/test-suite/issues/issue81.v b/test-suite/issues/issue81.v index dce41ea8e..de0eeaf31 100644 --- a/test-suite/issues/issue81.v +++ b/test-suite/issues/issue81.v @@ -1,6 +1,6 @@ -Require Import Stdlib.Lists.List. +From Stdlib Require Import Lists.List. Import ListNotations. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations app {A} (l l' : list A) : list A := app [] l' := l' ; (* <- here notations work *) diff --git a/test-suite/issues/issue82.v b/test-suite/issues/issue82.v index 1b51bea2a..0a3acc6ea 100644 --- a/test-suite/issues/issue82.v +++ b/test-suite/issues/issue82.v @@ -1,5 +1,5 @@ From Stdlib Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations app {A} : list A -> list A -> list A := app xs ys := fold_right cons ys xs. \ No newline at end of file diff --git a/test-suite/issues/issue83.v b/test-suite/issues/issue83.v index 663c41b1c..350d1c4c5 100644 --- a/test-suite/issues/issue83.v +++ b/test-suite/issues/issue83.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Section CookingKillsOpaquenessForReduction. Equations id {A} (x : A) : A := diff --git a/test-suite/issues/issue84.v b/test-suite/issues/issue84.v index 97b4155a4..591426161 100644 --- a/test-suite/issues/issue84.v +++ b/test-suite/issues/issue84.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue85.v b/test-suite/issues/issue85.v index 6e759b5f2..626bc8510 100644 --- a/test-suite/issues/issue85.v +++ b/test-suite/issues/issue85.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue91.v b/test-suite/issues/issue91.v index b062f7801..18e3ee9d5 100644 --- a/test-suite/issues/issue91.v +++ b/test-suite/issues/issue91.v @@ -1,5 +1,5 @@ From Stdlib Require Import Vector. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Arguments Vector.nil {A}. Arguments Vector.cons {A} _ {n}. diff --git a/test-suite/issues/issue93.v b/test-suite/issues/issue93.v index 6ee11d7bf..b4fa31193 100644 --- a/test-suite/issues/issue93.v +++ b/test-suite/issues/issue93.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue95_1.v b/test-suite/issues/issue95_1.v index 0e780c6f2..b6efba116 100644 --- a/test-suite/issues/issue95_1.v +++ b/test-suite/issues/issue95_1.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Inductive type: Set := | T_bool: type diff --git a/test-suite/issues/issue95_2.v b/test-suite/issues/issue95_2.v index 59841032e..efe962792 100644 --- a/test-suite/issues/issue95_2.v +++ b/test-suite/issues/issue95_2.v @@ -1,6 +1,7 @@ -Require Import TestSuite.issues.issue95_1. -Require Import Lia. -Require Import Equations.Prop.Equations. +From Stdlib Require Import TestSuite.issues.issue95_1. +From Stdlib Require Import Lia. +From Equations.Prop Require Import Equations. + Lemma l: forall T t, diff --git a/test-suite/issues/issue96.v b/test-suite/issues/issue96.v index 01fa89cad..8209c5abb 100644 --- a/test-suite/issues/issue96.v +++ b/test-suite/issues/issue96.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Inductive type: Set := | T_bool: type diff --git a/test-suite/issues/issue98.v b/test-suite/issues/issue98.v index a81c9f318..c8f749fc7 100644 --- a/test-suite/issues/issue98.v +++ b/test-suite/issues/issue98.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue99.v b/test-suite/issues/issue99.v index c0c4b86cb..f5b7b38da 100644 --- a/test-suite/issues/issue99.v +++ b/test-suite/issues/issue99.v @@ -1,5 +1,5 @@ From Stdlib.Lists Require Import List. -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *) Fixpoint compact_prod (T: list Type): Type := diff --git a/test-suite/issues/issue_mutual.v b/test-suite/issues/issue_mutual.v index d63af773f..6a3e0c31a 100644 --- a/test-suite/issues/issue_mutual.v +++ b/test-suite/issues/issue_mutual.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. From Stdlib Require Import Program Arith Compare_dec List. Import ListNotations. (* diff --git a/test-suite/le.v b/test-suite/le.v index 715e405fa..6b873dd71 100644 --- a/test-suite/le.v +++ b/test-suite/le.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Inductive le : nat -> nat -> Prop := | le_0 n : le 0 n diff --git a/test-suite/letred.v b/test-suite/letred.v index 92e80b31d..a19d8a75a 100644 --- a/test-suite/letred.v +++ b/test-suite/letred.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Equations foo (n : nat) : nat := foo x := let x := 0 in x. diff --git a/test-suite/local_where.v b/test-suite/local_where.v index af01fef11..f4519632e 100644 --- a/test-suite/local_where.v +++ b/test-suite/local_where.v @@ -1,5 +1,6 @@ -Require Import Program.Basics Program.Tactics. -Require Import Equations.Prop.Equations. +From Stdlib Require Import Program.Basics Program.Tactics. +From Equations.Prop Require Import Equations. + Equations foo (n : nat) : nat := foo n := n + k 0 diff --git a/test-suite/mfix.v b/test-suite/mfix.v index 8efaec93f..be8d60e91 100644 --- a/test-suite/mfix.v +++ b/test-suite/mfix.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Inductive term : Set := | Var (n : nat) diff --git a/test-suite/mutrec.v b/test-suite/mutrec.v index 66f88dd39..158bedd13 100644 --- a/test-suite/mutrec.v +++ b/test-suite/mutrec.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Module two. Inductive term : Set := diff --git a/test-suite/mutrec_enc.v b/test-suite/mutrec_enc.v index 9cca6b34e..b94356932 100644 --- a/test-suite/mutrec_enc.v +++ b/test-suite/mutrec_enc.v @@ -1,4 +1,4 @@ -Require Import Equations. +From Equations.Prop Require Import Equations. Inductive foo : Set := | c0 : nat -> foo @@ -42,14 +42,6 @@ fn (c1 b b') := fnb b + fnb b' where fnb (x : bar) : nat := fnb (d0 x) := x; fnb (d1 f) := fn f. -Next Obligation. - revert x. fix f 1. - destruct x. constructor. Transparent fn. unfold fn. - assert(forall x: bar, fn_ind_1 b b0 x (fn_obligation_1 fn b b0 x)). - fix g 1. destruct x. simpl. constructor. constructor. apply f. - constructor. apply H. apply H. - simpl. constructor. apply f. -Defined. Eval compute in fn. (* Combined Scheme foo_bar from foo_bar_mut, foo_bar_mut'. *) diff --git a/test-suite/nestedobls.v b/test-suite/nestedobls.v index 64c3290fb..38abd3a41 100644 --- a/test-suite/nestedobls.v +++ b/test-suite/nestedobls.v @@ -9,13 +9,14 @@ Set Asymmetric Patterns. Set Implicit Arguments. Unset Strict Implicit. -Require Import Arith. -Require Import Lia. -From Equations Require Import Equations. -Require Import Wellfounded Relation_Definitions. -Require Import Relation_Operators Lexicographic_Product Wf_nat. +From Stdlib Require Import Arith. +From Stdlib Require Import Lia. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Wellfounded Relation_Definitions. +From Stdlib Require Import Relation_Operators Lexicographic_Product Wf_nat. Unset Implicit Arguments. -Require Import Program. +From Stdlib Require Import Program. Equations? test (n : nat) (pre : n >= 0 ) : { n' : nat | n' <= n } by wf n lt := diff --git a/test-suite/nestedrec.v b/test-suite/nestedrec.v index 104769274..4d4d17745 100644 --- a/test-suite/nestedrec.v +++ b/test-suite/nestedrec.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Inductive term : Set := | Var (n : nat) diff --git a/test-suite/nestedrec2.v b/test-suite/nestedrec2.v index c758108b5..eb0e02cc7 100644 --- a/test-suite/nestedrec2.v +++ b/test-suite/nestedrec2.v @@ -1,6 +1,7 @@ -Require Import Equations.Prop.Equations. -Require Import Arith. -Require Import Compare_dec. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Arith. +From Stdlib Require Import Compare_dec. Inductive term : Set := | Var (n : nat) diff --git a/test-suite/nestedwfrec.v b/test-suite/nestedwfrec.v index 38880a85e..3e79f1f8b 100644 --- a/test-suite/nestedwfrec.v +++ b/test-suite/nestedwfrec.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import Lia. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Lia. Equations? f (n : nat) : nat by wf n lt := f 0 := 0; diff --git a/test-suite/nestedwhererec.v b/test-suite/nestedwhererec.v index 8e1c73bc9..4ccece09e 100644 --- a/test-suite/nestedwhererec.v +++ b/test-suite/nestedwhererec.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. (* Bug with eqns *) (* Nested with equation not properly generated *) diff --git a/test-suite/nestedwhererecwith.v b/test-suite/nestedwhererecwith.v index 0ea9a0b0e..8d59d749f 100644 --- a/test-suite/nestedwhererecwith.v +++ b/test-suite/nestedwhererecwith.v @@ -1,6 +1,6 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. -Require Import List. +From Stdlib Require Import List. Import ListNotations. Equations test {A} (n : nat) (gs : list A) : unit by wf n lt := diff --git a/test-suite/nestfixnorec.v b/test-suite/nestfixnorec.v index 46f10d2b2..311e0fa20 100644 --- a/test-suite/nestfixnorec.v +++ b/test-suite/nestfixnorec.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Set Keyed Unification. Require Import Stdlib.Lists.List. @@ -143,7 +143,7 @@ Section RoseTreeInd. list_tree_elim (cons a t) := fcons a t (tree_elim a) (list_tree_elim t) }. End RoseTreeInd. -Require Import Bool. +From Stdlib Require Import Bool. Module IdealNoSec. diff --git a/test-suite/noconf_noK.v b/test-suite/noconf_noK.v deleted file mode 100644 index 12fc3a148..000000000 --- a/test-suite/noconf_noK.v +++ /dev/null @@ -1,311 +0,0 @@ -From Equations Require Import Equations DepElimDec HSets. -(* Set Universe Polymorphism. *) -(** Can we define NoConfusion in SProp (squashing equalities of arguments)? - Would not allow to show equivalence to (x = y) for non-strict sets. *) - - -Unset Equations WithK. - -Inductive ℕ (E:Set) : Set := -| O : ℕ E -| S : ℕ E -> ℕ E -| raise : E -> ℕ E. - -Arguments O {_}. -Arguments S {_} _. - -Inductive Vec E (A : Set) : ℕ E -> Set := - nil : Vec E A O -| cons : forall {n} (x : A) (xs : Vec E A n), Vec E A (S n). -(* | cons' : forall {n} (x : A), Vec E A (S n) *) -(* | cons3 : forall n, Vec E A n. *) - -Derive Signature for Vec. -Arguments nil {_ _}. -Arguments cons {_ _ _} _ _. -(* Arguments cons' {_ _ _} _ . *) - - -Inductive vector_param E (A : Set) : forall (n : ℕ E), Vec E A n -> Set := - vnil_param : vector_param E A O nil -| vcons_param : forall (n : ℕ E) (a : A) (v : Vec E A n), - vector_param E A n v -> - vector_param E A (S n) (cons a v). -Derive Signature for vector_param. - -Derive NoConfusion for ℕ. -Derive NoConfusion for Vec. -Derive NoConfusion for vector_param. -Import Sigma_Notations. -Open Scope equations_scope. - -Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := - forall x : A, r (s x) = x. - -Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { - equiv_inv : B -> A ; - eisretr : Sect equiv_inv f; - eissect : Sect f equiv_inv; - eisadj : forall x : A, eisretr (f x) = f_equal f (eissect x) -}. -Arguments eisretr {A B}%_type_scope {f%_function_scope} {_} _. -Arguments eissect {A B}%_type_scope {f%_function_scope} {_} _. -Arguments eisadj {A B}%_type_scope {f%_function_scope} {_} _. -Arguments IsEquiv {A B}%_type_scope f%_function_scope. - - -Polymorphic Record Equiv (A B : Type) := { equiv :> A -> B ; is_equiv :> IsEquiv equiv }. -Arguments equiv {A B} e. - -Polymorphic Instance Equiv_IsEquiv {A B} (e : Equiv A B) : IsEquiv (equiv e). -Proof. apply is_equiv. Defined. - -Definition inv_equiv {A B} (E: Equiv A B) : B -> A := - equiv_inv (IsEquiv:=is_equiv _ _ E). - -Polymorphic Definition equiv_inv_equiv {A B} {E: Equiv A B} (x : A) : inv_equiv _ (equiv E x) = x := - eissect x. -Definition inv_equiv_equiv {A B} {E: Equiv A B} (x : B) : equiv E (inv_equiv _ x) = x := eisretr x. -Definition equiv_adj {A B} {E: Equiv A B} (x : A) - : inv_equiv_equiv (equiv E x) = f_equal (equiv E) (equiv_inv_equiv x) - := eisadj x. - -Notation " 'rew' H 'in' c " := (@eq_rect _ _ _ c _ H) (at level 20). - -Require Import Utf8. - -Notation " X <~> Y " := (Equiv X Y) (at level 90, no associativity, Y at next level). - -Lemma apply_equiv_dom {A B} (P : A -> Type) (e : Equiv A B) : - (forall x : B, P (inv_equiv e x)) -> forall x : A, P x. -Proof. - intros. specialize (X (equiv e x)). - rewrite equiv_inv_equiv in X. exact X. -Defined. - -(* Equations noConfVec {E A n} (v v' : Vec E A n) : Prop := *) -(* noConfVec nil nil := True; *) -(* noConfVec (cons _ x xs) (cons _ x' xs') := *) -(* {| pr1 := x; pr2 := xs |} = {| pr1 := x'; pr2 := xs' |}; *) -(* noConfVec (cons' x) (cons' x') := x = x'; *) -(* noConfVec cons3 cons3 := True; *) -(* noConfVec _ _ := False. *) -(* Transparent noConfVec. *) -(* Print Assumptions noConfVec_elim. *) - -(* Next Obligation. *) -(* Proof. *) -(* depelim v. *) -(* generalize_eqs_sig v'. destruct v'. *) -(* simplify ?. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). destruct v'; *) -(* simplify *. constructor. *) -(* generalize_eqs_sig v'. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). destruct v'; *) -(* simplify *; constructor. *) -(* generalize_eqs_sig v'. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). destruct v'; *) -(* simplify *; constructor. *) -(* Defined. *) - -(* Definition noConfVec_eq {E A n} (v v' : Vec E A n) : v = v' -> noConfVec v v'. *) -(* Proof. *) -(* intros ->. destruct v'; constructor. *) -(* Defined. *) - -(* Definition noConfVec_eq_inv {E A n} (v v' : Vec E A n) : noConfVec v v' -> v = v'. *) -(* Proof. *) -(* funelim (noConfVec v v'); try simplify *; constructor. *) -(* (* refine (@f_equal _ _ (fun x => cons x.1 x.2) _ _). *) *) -(* (* simplify ?. *) *) -(* (* simplify ?. *) *) -(* (* refine (@f_equal _ _ (fun x => cons' x) _ _). *) *) -(* Defined. *) - -(* Lemma noConfVec_eq_eq_inv {E A n} (v v' : Vec E A n) (e : v = v') : *) -(* noConfVec_eq_inv _ _ (noConfVec_eq _ _ e) = e. *) -(* Proof. *) -(* destruct e. destruct v; reflexivity. *) -(* Defined. *) - -(* Lemma noConfVec_refl {E A n} (v : Vec E A n) : noConfVec v v. *) -(* Proof. destruct v; reflexivity. Defined. *) - -(* Lemma noConfVec_eq_inv_eq_refl {E A n} (v : Vec E A n) : *) -(* noConfVec_eq _ _ (noConfVec_eq_inv v v (noConfVec_refl v)) = (noConfVec_refl v). *) -(* Proof. *) -(* destruct v; reflexivity. *) -(* Defined. *) - -(* Lemma noConfVec_eq_inv_eq {E A n} (v v' : Vec E A n) (e : noConfVec v v') : *) -(* noConfVec_eq _ _ (noConfVec_eq_inv _ _ e) = e. *) -(* Proof. *) -(* destruct v; revert e; depelim v'; simplify *; reflexivity. *) -(* Defined. *) - -Definition NoConfVec {E A n} (v v' : Vec E A n) : Prop := - match v in Vec _ _ n return Vec E A n -> Prop with - | nil => fun v' => - match v' in Vec _ _ O return Prop with - | nil => True - end - | @cons _ _ n' x xs => - fun v' => - match v' in Vec _ _ (S n'') return Vec E A n'' -> Prop with - | @cons _ _ n'' x' xs' => fun xs => {| pr1 := x; pr2 := xs |} = {| pr1 := x'; pr2 := xs' |} - end xs - end v'. - -(* Definition noConfVec_eq {E A n} (v v' : Vec E A n) : v = v' -> NoConfVec v v'. *) -(* Proof. *) -(* intros ->. destruct v'. constructor. simpl. constructor. simpl. constructor. *) -(* Defined. *) - -(* Definition idx0_elim {E A} (P : Vec E A O -> Type) (H : P nil) : forall v, P v := *) -(* fun v => match v in Vec _ _ O return P v with *) -(* | nil => H *) -(* end. *) - -(* Definition idxS_elim {E A} (P : forall n, Vec E A (S n) -> Type) *) -(* (H : forall n a (v' : Vec E A n), P n (cons a v')) *) -(* (H' : forall n a, P n (cons' a)) *) -(* n v : P n v := *) -(* match v in Vec _ _ (S n') with *) -(* | cons a v' => H _ a v' *) -(* | cons' a => H' _ a *) -(* end. *) - -(* (* refine (match v as v' in Vec _ _ n' return *) *) -(* (* match n' as n'' return Vec E A n'' -> Type with *) *) -(* (* | O => fun _ => True *) *) -(* (* | S n' => fun v => P _ v *) *) -(* (* | raise _ _ => fun _ => True *) *) -(* (* end v' *) *) -(* (* with *) *) -(* (* | nil => I *) *) -(* (* | cons a v' => H _ a v' *) *) -(* (* | cons' a => H' _ a *) *) -(* (* end). *) *) - -(* Definition isNil {E A n} (v : Vec E A n) := *) -(* match v with *) -(* | nil => True *) -(* | _ => False *) -(* end. *) - -(* Lemma eq_simplification_sigma1_dep@{i j} {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{j}} *) -(* (p q : A) (x : P p) (y : P q) : *) -(* (forall e : p = q, (@eq_rect A p P x q e) = y -> B) -> *) -(* (sigmaI P p x = sigmaI P q y -> B). *) -(* Proof. *) -(* intros. revert X. *) -(* change p with (pr1 &(p& x)). *) -(* change q with (pr1 &(q & y)). *) -(* change x with (pr2 &(p& x)) at 3. *) -(* change y with (pr2 &(q & y)) at 4. *) -(* destruct H. *) -(* intros X. eapply (X eq_refl). apply eq_refl. *) -(* Defined. *) - -(* (* Definition isNil_eq {E A } (v : Vec E A O) : isNil v -> v = nil. *) *) -(* (* Proof. destruct v. *) *) -(* (* match v with *) *) -(* (* | nil => True *) *) -(* (* | _ => False *) *) -(* (* end. *) *) -(* Set Printing Universes. *) -(* Definition noConfVec_eq_inv {E A n} (v v' : Vec E A n) : NoConfVec v v' -> v = v'. *) -(* Proof. *) -(* destruct v. *) -(* generalize_eqs_sig v'. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). destruct v'. *) -(* simplify ?. simplify ?. simplify ?. simpl. reflexivity. *) -(* simplify ?. *) -(* simplify ?. *) -(* simpl. simplify ?. simplify ?. *) -(* intros. *) -(* generalize_eqs_sig v'. destruct v'. *) -(* simplify ?. *) -(* simplify ?. *) -(* simpl in H. apply (f_equal (fun x => cons x.1 x.2)) in H. apply H. *) -(* simplify ?. simpl in H. *) -(* elim H. *) -(* generalize_eqs_sig v'. destruct v'. *) -(* simplify *. *) -(* simplify *. *) -(* simplify *. reflexivity. *) -(* (* revert v'. refine (idx0_elim _ _). intros. constructor. *) *) -(* (* revert n v' v. refine (idxS_elim _ _ _). *) *) -(* (* simpl. intros. change a with (&(a & v').1). change v' with (&(a & v').2) at 2. *) *) -(* (* destruct H. reflexivity. simpl. intros. elim H. *) *) -(* (* revert n v'. refine (idxS_elim _ _ _). simpl. intros. elim H. *) *) -(* (* simpl. intros n a H. destruct H; reflexivity. *) *) -(* Defined. *) - -(* Lemma noConfVec_eq_eq_inv {E A n} (v v' : Vec E A n) (e : v = v') : *) -(* noConfVec_eq_inv _ _ (noConfVec_eq _ _ e) = e. *) -(* Proof. *) -(* destruct e. destruct v; reflexivity. *) -(* Defined. *) - -(* Lemma noConfVec_refl {E A n} (v : Vec E A n) : NoConfVec v v. *) -(* Proof. destruct v; reflexivity. Defined. *) - -(* Lemma noConfVec_eq_inv_eq_refl {E A n} (v : Vec E A n) : *) -(* noConfVec_eq _ _ (noConfVec_eq_inv v v (noConfVec_refl v)) = (noConfVec_refl v). *) -(* Proof. *) -(* destruct v; reflexivity. *) -(* Defined. *) - -(* Lemma noConfVec_eq_inv_eq {E A n} (v v' : Vec E A n) (e : NoConfVec v v') : *) -(* noConfVec_eq _ _ (noConfVec_eq_inv _ _ e) = e. *) -(* Proof. *) -(* destruct v. revert e. *) -(* generalize_eqs_vars_sig v'. destruct v'. intros v'. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). simplify ?. *) -(* simplify ?. simplify ?. simplify ?. reflexivity. *) -(* intro. simplify *. *) -(* intro. simplify *. *) - -(* depelim v'. simpl in e. *) -(* revert e. simplify *. simpl. reflexivity. *) -(* simpl. intros. elim e. *) -(* depelim v'. simpl in e. *) -(* revert e. simplify *. *) -(* revert e. simplify *. reflexivity. *) -(* Defined. *) - -(* (* destruct v. revert v' e. refine (idx0_elim _ _). simpl. destruct e. reflexivity. *) *) -(* (* revert n v' v e. refine (idxS_elim _ _ _). intros. *) *) -(* (* simpl in e. *) *) -(* (* revert e. simplify *. simpl. reflexivity. *) *) -(* (* simpl. intros. elim e. *) *) -(* (* revert n v' e. refine (idxS_elim _ _ _). intros. elim e. *) *) -(* (* intros ??. simplify *. simpl. reflexivity. *) *) -(* (* Defined. *) *) - -Definition noConf_vec_equiv {E A n} (v v' : Vec E A n) : Equiv (v = v') (noConfVec v v'). -Proof. - refine {| equiv := noConfVec_eq v v' |}. - unshelve refine {| equiv_inv := noConfVec_eq_inv v v' |}. - red. intros. - apply noConfVec_eq_inv_eq. - red; intros. - apply noConfVec_eq_eq_inv. - simplify *. destruct v'; reflexivity. -Defined. - -Lemma noConfVec_hom_equiv : forall {E A : Set} n, NoConfusionPackage (Vec E A n). -Proof. - unshelve econstructor. - refine noConfVec. - apply noConfVec_eq. - apply noConfVec_eq_inv. - apply noConfVec_eq_eq_inv. -Defined. -Existing Instances noConfVec_hom_equiv. - -Equations param_vector_vcons E (A : Set) (a : A) (n : ℕ E) (v : Vec E A n) - (X : vector_param E A (S n) (cons a v)) : vector_param E A n v := - param_vector_vcons E A _ _ _ (vcons_param _ _ _ X) := X. -Transparent param_vector_vcons. diff --git a/test-suite/noconf_noK_fin.v b/test-suite/noconf_noK_fin.v deleted file mode 100644 index 1271a2062..000000000 --- a/test-suite/noconf_noK_fin.v +++ /dev/null @@ -1,304 +0,0 @@ -From Equations Require Import Equations DepElimDec HSets. -(* Set Universe Polymorphism. *) -(** Can we define NoConfusion in SProp (squashing equalities of arguments)? - Would not allow to show equivalence to (x = y) for non-strict sets. *) - - -Unset Equations WithK. -Inductive fin : nat -> Set := -| fin0 n : fin (S n) -| finS n : fin n -> fin (S n). -Derive Signature for fin. - -Arguments fin0 {_}. -Arguments finS {_} _. - -Inductive fin_param : forall n, fin n -> Set := -| finS_param : forall n (f : fin n), - fin_param n f -> - fin_param (S n) (finS f). -Derive Signature for fin_param. - -(* Derive NoConfusion for ℕ. *) -Derive NoConfusion for fin. -Derive NoConfusion for fin_param. -Import Sigma_Notations. -Open Scope equations_scope. - -Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := - forall x : A, r (s x) = x. - -Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { - equiv_inv : B -> A ; - eisretr : Sect equiv_inv f; - eissect : Sect f equiv_inv; - eisadj : forall x : A, eisretr (f x) = f_equal f (eissect x) -}. -Arguments eisretr {A B}%_type_scope {f%_function_scope} {_} _. -Arguments eissect {A B}%_type_scope {f%_function_scope} {_} _. -Arguments eisadj {A B}%_type_scope {f%_function_scope} {_} _. -Arguments IsEquiv {A B}%_type_scope f%_function_scope. - - -Polymorphic Record Equiv (A B : Type) := { equiv :> A -> B ; is_equiv :> IsEquiv equiv }. -Arguments equiv {A B} e. - -Polymorphic Instance Equiv_IsEquiv {A B} (e : Equiv A B) : IsEquiv (equiv e). -Proof. apply is_equiv. Defined. - -Definition inv_equiv {A B} (E: Equiv A B) : B -> A := - equiv_inv (IsEquiv:=is_equiv _ _ E). - -Polymorphic Definition equiv_inv_equiv {A B} {E: Equiv A B} (x : A) : inv_equiv _ (equiv E x) = x := - eissect x. -Definition inv_equiv_equiv {A B} {E: Equiv A B} (x : B) : equiv E (inv_equiv _ x) = x := eisretr x. -Definition equiv_adj {A B} {E: Equiv A B} (x : A) - : inv_equiv_equiv (equiv E x) = f_equal (equiv E) (equiv_inv_equiv x) - := eisadj x. - -Notation " 'rew' H 'in' c " := (@eq_rect _ _ _ c _ H) (at level 20). - -Require Import Utf8. - -Notation " X <~> Y " := (Equiv X Y) (at level 90, no associativity, Y at next level). - -Lemma apply_equiv_dom {A B} (P : A -> Type) (e : Equiv A B) : - (forall x : B, P (inv_equiv e x)) -> forall x : A, P x. -Proof. - intros. specialize (X (equiv e x)). - rewrite equiv_inv_equiv in X. exact X. -Defined. - -Equations noConf_fin {n} (v v' : fin n) : Prop := -noConf_fin fin0 fin0 := True; -noConf_fin (finS f) (finS f') := f = f'; -noConf_fin _ _ := False. -Transparent noConf_fin. -Print Assumptions noConf_fin_elim. - -(* Next Obligation. *) -(* Proof. *) -(* depelim v. *) -(* generalize_eqs_sig v'. destruct v'. *) -(* simplify ?. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). destruct v'; *) -(* simplify *. constructor. *) -(* generalize_eqs_sig v'. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). destruct v'; *) -(* simplify *; constructor. *) -(* generalize_eqs_sig v'. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). destruct v'; *) -(* simplify *; constructor. *) -(* Defined. *) - -Definition noConf_fin_eq {n} (v v' : fin n) : v = v' -> noConf_fin v v'. -Proof. - intros ->. destruct v'; constructor. -Defined. - -Definition noConf_fin_eq_inv {n} (v v' : fin n) : noConf_fin v v' -> v = v'. -Proof. - funelim (noConf_fin v v'); try simplify *; constructor. - (* refine (@f_equal _ _ (fun x => cons x.1 x.2) _ _). *) - (* simplify ?. *) - (* simplify ?. *) - (* refine (@f_equal _ _ (fun x => cons' x) _ _). *) -Defined. - -Lemma noConf_fin_eq_eq_inv {n} (v v' : fin n) (e : v = v') : - noConf_fin_eq_inv _ _ (noConf_fin_eq _ _ e) = e. -Proof. - destruct e. destruct v; reflexivity. -Defined. - -Lemma noConf_fin_refl {n} (v : fin n) : noConf_fin v v. -Proof. destruct v; reflexivity. Defined. - -Lemma noConf_fin_eq_inv_eq_refl {n} (v : fin n) : - noConf_fin_eq _ _ (noConf_fin_eq_inv v v (noConf_fin_refl v)) = (noConf_fin_refl v). -Proof. - destruct v; reflexivity. -Defined. - -Lemma noConf_fin_eq_inv_eq {n} (v v' : fin n) (e : noConf_fin v v') : - noConf_fin_eq _ _ (noConf_fin_eq_inv _ _ e) = e. -Proof. - destruct v; revert e; depelim v'; simplify *; reflexivity. -Defined. - -Lemma noConf_fin_hom_equiv : forall n, NoConfusionPackage (fin n). -Proof. - unshelve econstructor. - refine noConf_fin. - apply noConf_fin_eq. - apply noConf_fin_eq_inv. - apply noConf_fin_eq_eq_inv. -Defined. -Existing Instances noConf_fin_hom_equiv. - -Definition noConf_fin_equiv {n} (v v' : fin n) : Equiv (v = v') (noConf_fin v v'). -Proof. - refine {| equiv := noConf_fin_eq v v' |}. - unshelve refine {| equiv_inv := noConf_fin_eq_inv v v' |}. - red. intros. - apply noConf_fin_eq_inv_eq. - red; intros. - apply noConf_fin_eq_eq_inv. - simplify *. destruct v'; reflexivity. -Defined. - -(* Definition NoConfVec {E A n} (v v' : Vec E A n) : Prop := *) -(* match v in Vec _ _ n return Vec E A n -> Prop with *) -(* | nil => fun v' => *) -(* match v' in Vec _ _ O return Prop with *) -(* | nil => True *) -(* | _ => False *) -(* end *) -(* | @cons _ _ n' x xs => *) -(* fun v' => *) -(* match v' in Vec _ _ (S n'') return Vec E A n'' -> Prop with *) -(* | @cons _ _ n'' x' xs' => fun xs => {| pr1 := x; pr2 := xs |} = {| pr1 := x'; pr2 := xs' |} *) -(* | cons' _ => fun _ => False *) -(* end xs *) -(* | @cons' _ _ n' x => *) -(* fun v' => *) -(* match v' in Vec _ _ (S n'') return Prop with *) -(* | nil => False *) -(* | @cons' _ _ n'' x' => x = x' *) -(* | cons _ _ => False *) -(* end *) -(* end v'. *) - -(* Definition noConfVec_eq {E A n} (v v' : Vec E A n) : v = v' -> NoConfVec v v'. *) -(* Proof. *) -(* intros ->. destruct v'. constructor. simpl. constructor. simpl. constructor. *) -(* Defined. *) - -(* Definition idx0_elim {E A} (P : Vec E A O -> Type) (H : P nil) : forall v, P v := *) -(* fun v => match v in Vec _ _ O return P v with *) -(* | nil => H *) -(* end. *) - -(* Definition idxS_elim {E A} (P : forall n, Vec E A (S n) -> Type) *) -(* (H : forall n a (v' : Vec E A n), P n (cons a v')) *) -(* (H' : forall n a, P n (cons' a)) *) -(* n v : P n v := *) -(* match v in Vec _ _ (S n') with *) -(* | cons a v' => H _ a v' *) -(* | cons' a => H' _ a *) -(* end. *) - -(* (* refine (match v as v' in Vec _ _ n' return *) *) -(* (* match n' as n'' return Vec E A n'' -> Type with *) *) -(* (* | O => fun _ => True *) *) -(* (* | S n' => fun v => P _ v *) *) -(* (* | raise _ _ => fun _ => True *) *) -(* (* end v' *) *) -(* (* with *) *) -(* (* | nil => I *) *) -(* (* | cons a v' => H _ a v' *) *) -(* (* | cons' a => H' _ a *) *) -(* (* end). *) *) - -(* Definition isNil {E A n} (v : Vec E A n) := *) -(* match v with *) -(* | nil => True *) -(* | _ => False *) -(* end. *) - -(* Lemma eq_simplification_sigma1_dep@{i j} {A : Type@{i}} {P : A -> Type@{i}} {B : Type@{j}} *) -(* (p q : A) (x : P p) (y : P q) : *) -(* (forall e : p = q, (@eq_rect A p P x q e) = y -> B) -> *) -(* (sigmaI P p x = sigmaI P q y -> B). *) -(* Proof. *) -(* intros. revert X. *) -(* change p with (pr1 &(p& x)). *) -(* change q with (pr1 &(q & y)). *) -(* change x with (pr2 &(p& x)) at 3. *) -(* change y with (pr2 &(q & y)) at 4. *) -(* destruct H. *) -(* intros X. eapply (X eq_refl). apply eq_refl. *) -(* Defined. *) - -(* (* Definition isNil_eq {E A } (v : Vec E A O) : isNil v -> v = nil. *) *) -(* (* Proof. destruct v. *) *) -(* (* match v with *) *) -(* (* | nil => True *) *) -(* (* | _ => False *) *) -(* (* end. *) *) -(* Set Printing Universes. *) -(* Definition noConfVec_eq_inv {E A n} (v v' : Vec E A n) : NoConfVec v v' -> v = v'. *) -(* Proof. *) -(* destruct v. *) -(* generalize_eqs_sig v'. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). destruct v'. *) -(* simplify ?. simplify ?. simplify ?. simpl. reflexivity. *) -(* simplify ?. *) -(* simplify ?. *) -(* simpl. simplify ?. simplify ?. *) -(* intros. *) -(* generalize_eqs_sig v'. destruct v'. *) -(* simplify ?. *) -(* simplify ?. *) -(* simpl in H. apply (f_equal (fun x => cons x.1 x.2)) in H. apply H. *) -(* simplify ?. simpl in H. *) -(* elim H. *) -(* generalize_eqs_sig v'. destruct v'. *) -(* simplify *. *) -(* simplify *. *) -(* simplify *. reflexivity. *) -(* (* revert v'. refine (idx0_elim _ _). intros. constructor. *) *) -(* (* revert n v' v. refine (idxS_elim _ _ _). *) *) -(* (* simpl. intros. change a with (&(a & v').1). change v' with (&(a & v').2) at 2. *) *) -(* (* destruct H. reflexivity. simpl. intros. elim H. *) *) -(* (* revert n v'. refine (idxS_elim _ _ _). simpl. intros. elim H. *) *) -(* (* simpl. intros n a H. destruct H; reflexivity. *) *) -(* Defined. *) - -(* Lemma noConfVec_eq_eq_inv {E A n} (v v' : Vec E A n) (e : v = v') : *) -(* noConfVec_eq_inv _ _ (noConfVec_eq _ _ e) = e. *) -(* Proof. *) -(* destruct e. destruct v; reflexivity. *) -(* Defined. *) - -(* Lemma noConfVec_refl {E A n} (v : Vec E A n) : NoConfVec v v. *) -(* Proof. destruct v; reflexivity. Defined. *) - -(* Lemma noConfVec_eq_inv_eq_refl {E A n} (v : Vec E A n) : *) -(* noConfVec_eq _ _ (noConfVec_eq_inv v v (noConfVec_refl v)) = (noConfVec_refl v). *) -(* Proof. *) -(* destruct v; reflexivity. *) -(* Defined. *) - -(* Lemma noConfVec_eq_inv_eq {E A n} (v v' : Vec E A n) (e : NoConfVec v v') : *) -(* noConfVec_eq _ _ (noConfVec_eq_inv _ _ e) = e. *) -(* Proof. *) -(* destruct v. revert e. *) -(* generalize_eqs_vars_sig v'. destruct v'. intros v'. *) -(* refine (eq_simplification_sigma1_dep _ _ _ _ _). simplify ?. *) -(* simplify ?. simplify ?. simplify ?. reflexivity. *) -(* intro. simplify *. *) -(* intro. simplify *. *) - -(* depelim v'. simpl in e. *) -(* revert e. simplify *. simpl. reflexivity. *) -(* simpl. intros. elim e. *) -(* depelim v'. simpl in e. *) -(* revert e. simplify *. *) -(* revert e. simplify *. reflexivity. *) -(* Defined. *) - -(* (* destruct v. revert v' e. refine (idx0_elim _ _). simpl. destruct e. reflexivity. *) *) -(* (* revert n v' v e. refine (idxS_elim _ _ _). intros. *) *) -(* (* simpl in e. *) *) -(* (* revert e. simplify *. simpl. reflexivity. *) *) -(* (* simpl. intros. elim e. *) *) -(* (* revert n v' e. refine (idxS_elim _ _ _). intros. elim e. *) *) -(* (* intros ??. simplify *. simpl. reflexivity. *) *) -(* (* Defined. *) *) - -Equations param_fin_finS (n : nat) (f : fin n) - (X : fin_param (S n) (finS f)) : fin_param n f := - param_fin_finS _ _ (finS_param f) := f. -Transparent param_fin_finS. -Print Assumptions param_fin_finS. diff --git a/test-suite/noconf_simplify.v b/test-suite/noconf_simplify.v index dc343d844..052142b35 100644 --- a/test-suite/noconf_simplify.v +++ b/test-suite/noconf_simplify.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. Import ListNotations. Record decl := { na : nat; body : option nat }. diff --git a/test-suite/nocycle.v b/test-suite/nocycle.v index e9a0c7022..458d1b59e 100644 --- a/test-suite/nocycle.v +++ b/test-suite/nocycle.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import Below. +From Equations.Prop Require Import Equations. + +From Equations.TestSuite Require Import Below. Module NoCycle_nat. Definition noSubterm x y := @@ -292,7 +293,7 @@ Module NoCycle_mut. Qed. End NoCycle_mut. -Require Import Eqdep_dec. +From Stdlib Require Import Eqdep_dec. Theorem nat_dec (n m : nat) : {n = m} + {n <> m}. Proof. decide equality. Defined. diff --git a/test-suite/nocycle_def.v b/test-suite/nocycle_def.v index e42cc2904..5a099d988 100644 --- a/test-suite/nocycle_def.v +++ b/test-suite/nocycle_def.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import Equations.Prop.Subterm. +From Equations.Prop Require Import Equations. + +From Equations.Prop Require Import Subterm. Derive Subterm for nat. diff --git a/test-suite/nolam.v b/test-suite/nolam.v index 5a72662b7..4528c93df 100644 --- a/test-suite/nolam.v +++ b/test-suite/nolam.v @@ -6,9 +6,9 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Bvector List Relations. +From Stdlib Require Import List Relations. From Equations Require Import Equations Signature. -Require Import Utf8. +From Stdlib Require Import Utf8. Import ListNotations. Equations f : forall {A : Type}, list A -> nat := diff --git a/test-suite/notations.v b/test-suite/notations.v index c26da3397..063cea384 100644 --- a/test-suite/notations.v +++ b/test-suite/notations.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List. Import ListNotations. Reserved Notation "x +++ y" (at level 50). @@ -29,7 +30,7 @@ Equations rev {A} : list A -> list A := { acc ++++ [] := acc; acc ++++ (x :: l') := (x :: acc) ++++ l' }. -Require Import Arith NArith. +From Stdlib Require Import Arith NArith. Local Open Scope N_scope. (** Parsing works with scopes as well *) diff --git a/test-suite/pattern_lambdas.v b/test-suite/pattern_lambdas.v index 6913ff8d3..98f30d267 100644 --- a/test-suite/pattern_lambdas.v +++ b/test-suite/pattern_lambdas.v @@ -6,9 +6,9 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. -Variable test : forall n : nat, (nat -> bool) -> nat. +Parameter test : forall n : nat, (nat -> bool) -> nat. Equations f : nat -> nat := f 0 := 0; @@ -16,7 +16,7 @@ Equations f : nat -> nat := Equations f' (n : nat) : nat := f' n := test n (λ{ | 0 => true ; - | S n => false }). + | S _ => false }). Definition foo (x : nat) := f' match x with 0 => 0 | S x => 0 end. diff --git a/test-suite/rec.v b/test-suite/rec.v index d23e7343c..905293ce9 100644 --- a/test-suite/rec.v +++ b/test-suite/rec.v @@ -5,11 +5,12 @@ (* This file is distributed under the terms of the *) (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Program Utf8. -Require Import Equations.Prop.Equations. -Require Import Bvector List Relations. -Require Import Arith Wf_nat. -Require Import Lia. +From Stdlib Require Import Program Utf8. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import List Relations. +From Stdlib Require Import Arith Wf_nat. +From Stdlib Require Import Lia. Module RecRel. Unset Equations With Funext. @@ -82,7 +83,7 @@ Inductive xor (A B : Prop) : Prop := | xor_left : A -> not B -> xor A B | xor_right : B -> not A -> xor A B. -Require Import Bool. +From Stdlib Require Import Bool. Coercion Is_true : bool >-> Sortclass. Lemma xor_reflect (x y : bool) : reflect (xor x y) (xorb x y). @@ -108,8 +109,8 @@ Proof with simpl; intros. intros. auto using Permutation_cons_app. elim H1. Qed. -Require Import EquivDec. -Require Import Permutation. +From Stdlib Require Import EquivDec. +From Stdlib Require Import Permutation. Module RecMeasure. diff --git a/test-suite/rose.v b/test-suite/rose.v index c1f5c4cce..952c78c84 100644 --- a/test-suite/rose.v +++ b/test-suite/rose.v @@ -3,8 +3,9 @@ (** printing by %\coqdockw{by}% *) (** printing rec %\coqdockw{rec}% *) (* begin hide *) -From Equations Require Import Equations. -Require Import Lia Utf8 List. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Lia Utf8 List. Import ListNotations. Set Keyed Unification. @@ -31,7 +32,7 @@ Section list_size. Qed. End list_size. -Require Import List. +From Stdlib Require Import List. (* end hide *) (** To demonstrate nested well-founded recursive definitions, we take a well-known example from the literature: rose trees. We will define a diff --git a/test-suite/scope.v b/test-suite/scope.v index 189b09e01..2a207e6c2 100644 --- a/test-suite/scope.v +++ b/test-suite/scope.v @@ -1,13 +1,14 @@ (** Example by Rafaël Bocquet: POPLmark part 1A with inductive definition of scope and well-scoped variables (and terms, types and environments). *) -Require Import Program. -Require Import Equations.Prop.DepElim. -Require Import Equations.Prop.Equations. +From Stdlib Require Import Program. +From Equations.Prop Require Import DepElim. +From Equations.Prop Require Import Equations. + From Stdlib Require Import Eqdep_dec. From Stdlib Require Import EquivDec. -Require Import Arith. +From Stdlib Require Import Arith. Derive Signature for eq. Definition scope := nat. diff --git a/test-suite/tabareau_vec.v b/test-suite/tabareau_vec.v index fa1dacc43..b2248ab11 100644 --- a/test-suite/tabareau_vec.v +++ b/test-suite/tabareau_vec.v @@ -1,4 +1,4 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. Set Universe Polymorphism. Inductive ℕ (E:Set) : Set := diff --git a/test-suite/terms.v b/test-suite/terms.v index 2b8e32ec9..a36887fd3 100644 --- a/test-suite/terms.v +++ b/test-suite/terms.v @@ -1,17 +1,18 @@ -From Equations Require Import Equations Fin DepElimDec. +From Equations.Prop Require Import Equations. Inductive term := | Var : nat -> term | App : term -> list term -> term | Lam : term -> term. -Equations(nocomp) term_size (t : term) : nat := +#[derive(eliminator=no)] Equations term_size (t : term) : nat := term_size (Var n) := 0; term_size (App f l) := S (List.fold_left (fun acc x => max acc (term_size x)) l (term_size f)); term_size (Lam f) := S (term_size f). (** TODO: recognize recursive call under lambda abstraction *) -Equations(nocomp) subst (t : term) (k : nat) (u : term) : term := +#[derive(eliminator=no)] +Equations subst (t : term) (k : nat) (u : term) : term := subst t k (Var n) := if Nat.eqb k n then t else Var n; subst t k (App f l) := App (subst t k f) (List.map (fun x => subst t k x) l); subst t k (Lam f) := Lam (subst t (S k) f). diff --git a/test-suite/wfnocycle.v b/test-suite/wfnocycle.v index a2692e350..7b439f252 100644 --- a/test-suite/wfnocycle.v +++ b/test-suite/wfnocycle.v @@ -1,12 +1,13 @@ Set Warnings "-notation-overridden". -From Equations Require Import Equations. -Require Import Utf8 Arith Compare_dec List Lia. -Require Import Relation_Operators. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Utf8 Arith Compare_dec List Lia. +From Stdlib Require Import Relation_Operators. Arguments clos_trans [A]. Import Sigma_Notations. Set Equations Transparent. -Require Import fin. +From Equations.TestSuite Require Import fin. Equations lift_fin {n} (k : nat) (f : fin n) : fin (S n) := lift_fin 0 f := fs f; @@ -20,7 +21,7 @@ Local Open Scope equations_scope. Arguments map {A B}. (* end hide *) -Require Import Equations.Prop.Subterm. +From Equations.Prop Require Import Subterm. Derive Subterm for nat. diff --git a/test-suite/yves.v b/test-suite/yves.v index ced824426..2ec95a215 100644 --- a/test-suite/yves.v +++ b/test-suite/yves.v @@ -1,5 +1,5 @@ -Require Import Arith. -From Equations Require Import Equations. +From Stdlib Require Import Arith. +From Equations.Prop Require Import Equations. Inductive btree (T : Type) : Type := Leaf | Node (val : T) (t1 t2 : btree T). diff --git a/test-suite/zoe.v b/test-suite/zoe.v index c447ba64c..f096cc3bb 100644 --- a/test-suite/zoe.v +++ b/test-suite/zoe.v @@ -1,5 +1,6 @@ -From Equations Require Import Equations. -Require Import Arith List ListSet Lia Program. +From Equations.Prop Require Import Equations. + +From Stdlib Require Import Arith List ListSet Lia Program. Import ListNotations. Set Keyed Unification. diff --git a/theories/CoreTactics.v b/theories/CoreTactics.v index 69944dbe1..2f6f65e9a 100644 --- a/theories/CoreTactics.v +++ b/theories/CoreTactics.v @@ -9,7 +9,7 @@ (** Tactics supporting equations *) Require Export Equations.Init. -Require Import Equations.Signature. +From Equations Require Import Signature. Local Open Scope equations_scope. diff --git a/theories/HoTT/Classes.v b/theories/HoTT/Classes.v index fd5107d5f..40c82a16e 100644 --- a/theories/HoTT/Classes.v +++ b/theories/HoTT/Classes.v @@ -6,10 +6,10 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Equations.Init Equations.CoreTactics. +From Equations Require Import Init CoreTactics. Set Warnings "-notation-overridden". -Require Import HoTT.Basics.Trunc HoTT.HSet. -Require Import Equations.HoTT.Logic Equations.HoTT.Relation +From Stdlib Require Import HoTT.Basics.Trunc HoTT.HSet. +From Equations Require Import HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties Equations.HoTT.WellFounded. Set Universe Polymorphism. diff --git a/theories/HoTT/Constants.v b/theories/HoTT/Constants.v index 7ce28c33a..059223cc4 100644 --- a/theories/HoTT/Constants.v +++ b/theories/HoTT/Constants.v @@ -1,7 +1,7 @@ Set Warnings "-notation-overridden". From Equations Require Import Init. -Require Import Equations.HoTT.Logic Equations.HoTT.DepElim +From Equations Require Import HoTT.Logic Equations.HoTT.DepElim Equations.HoTT.EqDec Equations.HoTT.Classes. From HoTT Require Import Spaces.Nat. diff --git a/theories/HoTT/DepElim.v b/theories/HoTT/DepElim.v index 21411cfd0..b657fad0c 100644 --- a/theories/HoTT/DepElim.v +++ b/theories/HoTT/DepElim.v @@ -10,12 +10,12 @@ Set Warnings "-notation-overridden". -Require Import Stdlib.Program.Tactics. +From Stdlib Require Import Program.Tactics. Require Export Equations.Init. -Require Import Equations.Signature Equations.CoreTactics. -Require Import Equations.HoTT.Logic. -Require Import Equations.HoTT.Classes. -Require Import Equations.HoTT.EqDec. +From Equations Require Import Signature CoreTactics. +From Equations Require Import HoTT.Logic. +From Equations Require Import HoTT.Classes. +From Equations Require Import HoTT.EqDec. Set Universe Polymorphism. diff --git a/theories/HoTT/EqDec.v b/theories/HoTT/EqDec.v index 54865b812..745ce4555 100644 --- a/theories/HoTT/EqDec.v +++ b/theories/HoTT/EqDec.v @@ -8,9 +8,9 @@ Set Warnings "-notation-overridden". -Require Import Equations.Init. -Require Import Equations.HoTT.Logic. -Require Import Equations.HoTT.Classes. +From Equations Require Import Init. +From Equations Require Import HoTT.Logic. +From Equations Require Import HoTT.Classes. (** Decidable equality. @@ -232,7 +232,7 @@ Definition apd_eq {A} {x y : A} (p : x = y) {z} (q : z = x) : transport (@paths A z) p q = q @ p. Proof. now destruct p, q. Defined. -Require Import HoTT.Basics.Trunc. +From Stdlib Require Import HoTT.Basics.Trunc. Lemma hprop_hset {A} (h : IsHProp A) : IsHSet A. Proof. diff --git a/theories/HoTT/EqDecInstances.v b/theories/HoTT/EqDecInstances.v index 634ae61a4..83df3af7d 100644 --- a/theories/HoTT/EqDecInstances.v +++ b/theories/HoTT/EqDecInstances.v @@ -7,7 +7,7 @@ (**********************************************************************) Set Warnings "-notation-overridden". From Equations Require Import Init. -Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.DepElim +From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.DepElim Equations.HoTT.Constants Equations.HoTT.Tactics Equations.HoTT.EqDec Equations.HoTT.NoConfusion. From HoTT Require Import Spaces.List.Core. diff --git a/theories/HoTT/FunctionalInduction.v b/theories/HoTT/FunctionalInduction.v index fdc24cc47..353d36954 100644 --- a/theories/HoTT/FunctionalInduction.v +++ b/theories/HoTT/FunctionalInduction.v @@ -7,9 +7,9 @@ (**********************************************************************) Set Warnings "-notation-overridden". -Require Import Equations.CoreTactics. -Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.DepElim. -Require Import HoTT.Spaces.Nat. +From Equations Require Import CoreTactics. +From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.DepElim. +From Stdlib Require Import HoTT.Spaces.Nat. Local Open Scope nat_scope. Local Open Scope equations_scope. diff --git a/theories/HoTT/Loader.v b/theories/HoTT/Loader.v index 6a5813f9b..4f2f13053 100644 --- a/theories/HoTT/Loader.v +++ b/theories/HoTT/Loader.v @@ -12,13 +12,13 @@ Set Warnings "-notation-overridden". From Equations Require Export Init Signature. -Require Import Equations.CoreTactics. +From Equations Require Import CoreTactics. Require Export Equations.HoTT.Logic Equations.HoTT.Classes. -Require Import Equations.HoTT.WellFounded. -Require Import Equations.HoTT.DepElim Equations.HoTT.EqDec Equations.HoTT.Constants. +From Equations Require Import HoTT.WellFounded. +From Equations Require Import HoTT.DepElim Equations.HoTT.EqDec Equations.HoTT.Constants. Require Export Equations.HoTT.EqDecInstances. Require Export Equations.HoTT.NoConfusion. -Require Import Equations.HoTT.Subterm. +From Equations Require Import HoTT.Subterm. Require Export Equations.HoTT.Tactics. Require Export Equations.HoTT.FunctionalInduction. (* funelim tactic *) diff --git a/theories/HoTT/Logic.v b/theories/HoTT/Logic.v index d161be9dc..fecb33d55 100644 --- a/theories/HoTT/Logic.v +++ b/theories/HoTT/Logic.v @@ -23,7 +23,7 @@ Register ap as core.identity.congr. Definition path_inspect {A : Type} (x : A) : { y | paths x y } := (x ; idpath). -Require Import HoTT.Types.Bool. +From Stdlib Require Import HoTT.Types.Bool. (* For compatibility with Coq's [induction] *) Definition Bool_rect := Bool_ind. diff --git a/theories/HoTT/NoConfusion.v b/theories/HoTT/NoConfusion.v index 292041ac7..88f6263db 100644 --- a/theories/HoTT/NoConfusion.v +++ b/theories/HoTT/NoConfusion.v @@ -13,10 +13,10 @@ Set Warnings "-notation-overridden". From Equations Require Import Init Signature. -Require Import Equations.CoreTactics. -Require Import Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Constants. -Require Import Equations.HoTT.DepElim Equations.HoTT.Tactics. -Require Import HoTT.Spaces.List.Core. +From Equations Require Import CoreTactics. +From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Constants. +From Equations Require Import HoTT.DepElim Equations.HoTT.Tactics. +From Stdlib Require Import HoTT.Spaces.List.Core. (** Parameterized inductive types just need NoConfusion. *) diff --git a/theories/HoTT/Relation.v b/theories/HoTT/Relation.v index 5aa424cec..14df41353 100644 --- a/theories/HoTT/Relation.v +++ b/theories/HoTT/Relation.v @@ -11,7 +11,7 @@ From Equations Require Import Init. Set Warnings "-notation-overridden". -Require Import Equations.HoTT.Logic. +From Equations Require Import HoTT.Logic. Require Export HoTT.Basics.Iff. Local Open Scope equations_scope. diff --git a/theories/HoTT/Relation_Properties.v b/theories/HoTT/Relation_Properties.v index a8fa236dc..eceb0a62b 100644 --- a/theories/HoTT/Relation_Properties.v +++ b/theories/HoTT/Relation_Properties.v @@ -16,9 +16,9 @@ Set Warnings "-notation-overridden". -Require Import Equations.Init. -Require Import Equations.HoTT.Logic. -Require Import Equations.HoTT.Relation. +From Equations Require Import Init. +From Equations Require Import HoTT.Logic. +From Equations Require Import HoTT.Relation. Import Sigma_Notations. diff --git a/theories/HoTT/Subterm.v b/theories/HoTT/Subterm.v index 422497f6a..fe96ef782 100644 --- a/theories/HoTT/Subterm.v +++ b/theories/HoTT/Subterm.v @@ -9,8 +9,8 @@ Set Warnings "-notation-overridden". From Equations Require Import Init Signature. -Require Import Equations.CoreTactics. -Require Import Equations.HoTT.Logic +From Equations Require Import CoreTactics. +From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Relation Equations.HoTT.WellFounded diff --git a/theories/HoTT/Tactics.v b/theories/HoTT/Tactics.v index 4340ddbd6..d9733215b 100644 --- a/theories/HoTT/Tactics.v +++ b/theories/HoTT/Tactics.v @@ -7,20 +7,19 @@ (**********************************************************************) Set Warnings "-notation-overridden". -Require Import Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.DepElim - Equations.HoTT.Subterm Equations.HoTT.EqDec - Equations.HoTT.WellFounded Equations.HoTT.FunctionalInduction. +From Equations Require Import CoreTactics. +From Equations.HoTT Require Import Logic DepElim Subterm EqDec WellFounded FunctionalInduction. -Ltac Equations.Init.simpl_equations ::= Equations.HoTT.DepElim.simpl_equations. -Ltac Equations.Init.simplify_equalities ::= Equations.HoTT.DepElim.simplify_dep_elim. +Ltac Equations.Init.simpl_equations ::= DepElim.simpl_equations. +Ltac Equations.Init.simplify_equalities ::= DepElim.simplify_dep_elim. Ltac Equations.Init.depelim H ::= dependent elimination H; cbn in *. -Ltac Equations.Init.depind H ::= Equations.HoTT.DepElim.depind H. -Ltac Equations.Init.simp_IHs_tac ::= Equations.HoTT.FunctionalInduction.simplify_IHs_call. -Ltac Equations.Init.funelim_constr_as H H' tac ::= Equations.HoTT.FunctionalInduction.funelim_constr_as H H' tac. -Ltac Equations.Init.apply_funelim H ::= Equations.HoTT.FunctionalInduction.apply_funelim H. +Ltac Equations.Init.depind H ::= DepElim.depind H. +Ltac Equations.Init.simp_IHs_tac ::= FunctionalInduction.simplify_IHs_call. +Ltac Equations.Init.funelim_constr_as H H' tac ::= FunctionalInduction.funelim_constr_as H H' tac. +Ltac Equations.Init.apply_funelim H ::= FunctionalInduction.apply_funelim H. -Ltac Equations.Init.noconf H ::= Equations.HoTT.DepElim.noconf H. +Ltac Equations.Init.noconf H ::= DepElim.noconf H. Create HintDb solve_subterm discriminated. @@ -34,8 +33,8 @@ Ltac solve_subterm := intros; simplify_dep_elim; try typeclasses eauto with solve_subterm. Ltac Equations.Init.solve_subterm ::= solve_subterm. -Ltac Equations.Init.unfold_recursor ::= Equations.HoTT.Subterm.unfold_recursor. -Ltac Equations.Init.unfold_recursor_ext ::= Equations.HoTT.Subterm.unfold_recursor_ext. +Ltac Equations.Init.unfold_recursor ::= Subterm.unfold_recursor. +Ltac Equations.Init.unfold_recursor_ext ::= Subterm.unfold_recursor_ext. Ltac solve_noconf_inv_eq a b := destruct_sigma a; destruct_sigma b; diff --git a/theories/HoTT/Telescopes.v b/theories/HoTT/Telescopes.v index 09dbf3a86..4627d7482 100644 --- a/theories/HoTT/Telescopes.v +++ b/theories/HoTT/Telescopes.v @@ -1,11 +1,11 @@ Set Warnings "-notation-overridden". -Require Import Equations.HoTT.Loader. -Require Import Equations.HoTT.Logic. -Require Import Equations.HoTT.WellFounded. -Require Import Equations.HoTT.DepElim. -Require Import Equations.HoTT.Tactics. -Require Import Equations.HoTT.FunctionalInduction. -Require Import Equations.HoTT.Subterm. +From Equations Require Import HoTT.Loader. +From Equations Require Import HoTT.Logic. +From Equations Require Import HoTT.WellFounded. +From Equations Require Import HoTT.DepElim. +From Equations Require Import HoTT.Tactics. +From Equations Require Import HoTT.FunctionalInduction. +From Equations Require Import HoTT.Subterm. From HoTT Require Import Basics.Tactics. (** Telescopes: allows treating variable arity fixpoints *) diff --git a/theories/HoTT/WellFounded.v b/theories/HoTT/WellFounded.v index 515321945..fdc427056 100644 --- a/theories/HoTT/WellFounded.v +++ b/theories/HoTT/WellFounded.v @@ -1,8 +1,8 @@ Set Warnings "-notation-overridden". -Require Import Equations.Init Equations.CoreTactics. -Require Import Equations.HoTT.Logic +From Equations Require Import Init CoreTactics. +From Equations Require Import HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties. -Require Import HoTT.Basics.Tactics. +From Stdlib Require Import HoTT.Basics.Tactics. Set Universe Polymorphism. Import Sigma_Notations. diff --git a/theories/HoTT/WellFoundedInstances.v b/theories/HoTT/WellFoundedInstances.v index 00d934dd3..01d4f8ea3 100644 --- a/theories/HoTT/WellFoundedInstances.v +++ b/theories/HoTT/WellFoundedInstances.v @@ -1,5 +1,5 @@ Set Warnings "-notation-overridden". -Require Import Equations.HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded. +From Equations Require Import HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded. From HoTT Require Import Spaces.Nat. Section Lt. diff --git a/theories/HoTT/dune b/theories/HoTT/dune index a9baa595d..3911cf948 100644 --- a/theories/HoTT/dune +++ b/theories/HoTT/dune @@ -1,6 +1,6 @@ (coq.theory (name Equations.HoTT) - (package coq-equations) + (package rocq-equations) (modules :standard) - (theories Equations) + (theories Equations) (flags ("-noinit" "-indices-matter"))) \ No newline at end of file diff --git a/theories/Init.v b/theories/Init.v index 244beabbf..d5b1ce606 100644 --- a/theories/Init.v +++ b/theories/Init.v @@ -6,10 +6,11 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Stdlib.Unicode.Utf8_core Extraction. +From Corelib Require Import Extraction. +From Stdlib Require Import Unicode.Utf8_core. -Declare ML Module "coq-core.plugins.ltac". -Declare ML Module "coq-equations.plugin". +Declare ML Module "rocq-runtime.plugins.ltac". +Declare ML Module "rocq-equations.plugin". (** A notation scope for equations declarations. diff --git a/theories/Prop/Classes.v b/theories/Prop/Classes.v index 62c3ce6ce..3d9350170 100644 --- a/theories/Prop/Classes.v +++ b/theories/Prop/Classes.v @@ -6,9 +6,9 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Equations.Init Equations.CoreTactics. +From Equations Require Import Init CoreTactics. From Stdlib Require Import Extraction Relation_Definitions. -Require Import Equations.Prop.Logic. +From Equations.Prop Require Import Logic. (** A class for well foundedness proofs. Instances can be derived automatically using [Derive Subterm for ind]. *) diff --git a/theories/Prop/Constants.v b/theories/Prop/Constants.v index 57d1fc83d..ac4740d1c 100644 --- a/theories/Prop/Constants.v +++ b/theories/Prop/Constants.v @@ -1,5 +1,5 @@ From Equations Require Import Init. -Require Import Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim. +From Equations.Prop Require Import Classes EqDec DepElim. From Stdlib Require Import Relations. (** Naturals *) diff --git a/theories/Prop/DepElim.v b/theories/Prop/DepElim.v index 3256a3fc0..e350f5da9 100644 --- a/theories/Prop/DepElim.v +++ b/theories/Prop/DepElim.v @@ -8,13 +8,13 @@ (** Tactics related to (dependent) equality and proof irrelevance. *) -Require Import Stdlib.Program.Tactics. +From Stdlib Require Import Program.Tactics. Require Export Equations.Init. -Require Import Equations.CoreTactics. -Require Import Equations.Signature. -Require Import Equations.Prop.Logic. -Require Import Equations.Prop.Classes. -Require Import Equations.Prop.EqDec. +From Equations Require Import CoreTactics. +From Equations Require Import Signature. +From Equations.Prop Require Import Logic. +From Equations.Prop Require Import Classes. +From Equations.Prop Require Import EqDec. Import Sigma_Notations. Local Open Scope equations_scope. diff --git a/theories/Prop/EqDec.v b/theories/Prop/EqDec.v index 3bb92277e..d7a461a20 100644 --- a/theories/Prop/EqDec.v +++ b/theories/Prop/EqDec.v @@ -6,8 +6,8 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Equations.Init. -Require Import Equations.Prop.Classes. +From Equations Require Import Init. +From Equations.Prop Require Import Classes. (** Decidable equality. diff --git a/theories/Prop/EqDecInstances.v b/theories/Prop/EqDecInstances.v index a564c3294..23cdca769 100644 --- a/theories/Prop/EqDecInstances.v +++ b/theories/Prop/EqDecInstances.v @@ -1,6 +1,4 @@ -Require Import Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim - Equations.Prop.NoConfusion - Equations.Prop.Tactics. +From Equations.Prop Require Import Classes EqDec DepElim NoConfusion Tactics. (** Standard instances. *) diff --git a/theories/Prop/Equations.v b/theories/Prop/Equations.v index 1e9216b30..ba69a6eeb 100644 --- a/theories/Prop/Equations.v +++ b/theories/Prop/Equations.v @@ -9,11 +9,11 @@ (** The set of libraries required to run Equations with all features. *) Require Export Equations.Prop.Loader. -Require Import Equations.Prop.Telescopes. +From Equations.Prop Require Import Telescopes. #[export] Existing Instance wf_tele_measure. -Require Import Program.Tactics. +From Stdlib Require Import Program.Tactics. (* program_solve_wf launches auto on well-founded and propositional (i.e. in Prop) goals *) diff --git a/theories/Prop/FunctionalInduction.v b/theories/Prop/FunctionalInduction.v index 6b726b0d0..375954a04 100644 --- a/theories/Prop/FunctionalInduction.v +++ b/theories/Prop/FunctionalInduction.v @@ -6,9 +6,8 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Equations.CoreTactics. -Require Import Equations.Prop.Logic - Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim. +From Equations Require Import CoreTactics. +From Equations.Prop Require Import Logic Classes EqDec DepElim. (** The tactic [funind c Hc] applies functional induction on the application [c] which must be of the form [f args] where [f] has a [FunctionalInduction] diff --git a/theories/Prop/Loader.v b/theories/Prop/Loader.v index dde838ff6..d29d29c64 100644 --- a/theories/Prop/Loader.v +++ b/theories/Prop/Loader.v @@ -8,16 +8,16 @@ (** The set of libraries required to run Equations with all features. *) -Require Import Extraction. +From Stdlib Require Import Extraction. (** This exports tactics *) -Declare ML Module "coq-equations.plugin". +Declare ML Module "rocq-equations.plugin". From Equations Require Export Init Signature. -Require Import Equations.CoreTactics. +From Equations Require Import CoreTactics. Require Export Equations.Prop.SigmaNotations. Require Export Equations.Prop.Classes. -Require Import Equations.Prop.DepElim Equations.Prop.Constants. +From Equations.Prop Require Import DepElim Constants. Require Export Equations.Prop.EqDec. Require Export Equations.Prop.EqDecInstances. Require Export Equations.Prop.NoConfusion Equations.Prop.Subterm. diff --git a/theories/Prop/NoConfusion.v b/theories/Prop/NoConfusion.v index bd6feb0eb..2613091e3 100644 --- a/theories/Prop/NoConfusion.v +++ b/theories/Prop/NoConfusion.v @@ -11,12 +11,12 @@ on some equation. *) Set Warnings "-deprecated-since-8.20". -Require Import Stdlib.Program.Tactics Bvector List. +From Stdlib Require Import Program.Tactics Bvector List. Set Warnings "deprecated-since-8.20". From Equations Require Import Init Signature. -Require Import Equations.CoreTactics. -Require Import Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.Constants. -Require Import Equations.Prop.DepElim Equations.Prop.Tactics. +From Equations Require Import CoreTactics. +From Equations.Prop Require Import Classes EqDec Constants. +From Equations.Prop Require Import DepElim Tactics. (** Simple of parameterized inductive types just need NoConfusion. *) Derive NoConfusion for unit bool nat option sum Datatypes.prod list sigT sig. diff --git a/theories/Prop/NoConfusion_UIP.v b/theories/Prop/NoConfusion_UIP.v index fe6649358..79536be6b 100644 --- a/theories/Prop/NoConfusion_UIP.v +++ b/theories/Prop/NoConfusion_UIP.v @@ -1,4 +1,5 @@ -From Equations Require Import Equations. +From Equations.Prop Require Import Equations. + Import Sigma_Notations. (** This noConfusion instance corresponds to the rule for simplifying injectivity with UIP. *) diff --git a/theories/Prop/NoCycle.v b/theories/Prop/NoCycle.v index 0728e61c7..2f2d90ace 100644 --- a/theories/Prop/NoCycle.v +++ b/theories/Prop/NoCycle.v @@ -6,7 +6,8 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Equations.Prop.Equations. +From Equations.Prop Require Import Equations. + Ltac find_noCycle_proof H := let rec aux t ty := @@ -54,7 +55,7 @@ Proof with trivial. + firstorder. } Qed. -Require Import CRelationClasses. +From Stdlib Require Import CRelationClasses. #[export] Instance nlt_refl : Reflexive nlt. diff --git a/theories/Prop/OpaqueEquations.v b/theories/Prop/OpaqueEquations.v index 7ca906338..7e40373f2 100644 --- a/theories/Prop/OpaqueEquations.v +++ b/theories/Prop/OpaqueEquations.v @@ -10,7 +10,7 @@ that computation is not possible inside Coq, the tactics need this to solve obligations. *) -Require Import Equations.Prop.DepElim. +From Equations.Prop Require Import DepElim. Global Opaque simplification_sigma2_uip simplification_sigma2_dec_point diff --git a/theories/Prop/Subterm.v b/theories/Prop/Subterm.v index d9935b6e9..3424f248c 100644 --- a/theories/Prop/Subterm.v +++ b/theories/Prop/Subterm.v @@ -12,9 +12,8 @@ From Stdlib Require Import Relation_Operators Lexicographic_Product Wf_nat. From Stdlib Require Export Program.Wf FunctionalExtensionality. From Equations Require Import Init Signature. -Require Import Equations.CoreTactics. -Require Import Equations.Prop.Classes Equations.Prop.EqDec - Equations.Prop.DepElim Equations.Prop.Constants. +From Equations Require Import CoreTactics. +From Equations.Prop Require Import Classes EqDec DepElim Constants. Generalizable Variables A R S B. diff --git a/theories/Prop/Tactics.v b/theories/Prop/Tactics.v index fed1f13ff..efd7ba78d 100644 --- a/theories/Prop/Tactics.v +++ b/theories/Prop/Tactics.v @@ -5,17 +5,17 @@ (* This file is distributed under the terms of the *) (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Equations.CoreTactics Equations.Prop.Classes Equations.Prop.DepElim - Equations.Prop.Subterm Equations.Prop.FunctionalInduction. - -Ltac Equations.Init.simpl_equations ::= Equations.Prop.DepElim.simpl_equations. -Ltac Equations.Init.simplify_equalities ::= Equations.Prop.DepElim.simplify_dep_elim. -Ltac Equations.Init.depelim H ::= Equations.Prop.DepElim.depelim H. -Ltac Equations.Init.depind H ::= Equations.Prop.DepElim.depind H. -Ltac Equations.Init.noconf H ::= Equations.Prop.DepElim.noconf H. -Ltac Equations.Init.simp_IHs_tac ::= Equations.Prop.FunctionalInduction.simplify_IHs_call. -Ltac Equations.Init.funelim_constr_as x H simp_IHs ::= Equations.Prop.FunctionalInduction.funelim_constr_as x H simp_IHs. -Ltac Equations.Init.apply_funelim H ::= Equations.Prop.FunctionalInduction.apply_funelim H. +From Equations Require Import CoreTactics. +From Equations.Prop Require Import Classes DepElim Subterm FunctionalInduction. + +Ltac Equations.Init.simpl_equations ::= DepElim.simpl_equations. +Ltac Equations.Init.simplify_equalities ::= DepElim.simplify_dep_elim. +Ltac Equations.Init.depelim H ::= DepElim.depelim H. +Ltac Equations.Init.depind H ::= DepElim.depind H. +Ltac Equations.Init.noconf H ::= DepElim.noconf H. +Ltac Equations.Init.simp_IHs_tac ::= FunctionalInduction.simplify_IHs_call. +Ltac Equations.Init.funelim_constr_as x H simp_IHs ::= FunctionalInduction.funelim_constr_as x H simp_IHs. +Ltac Equations.Init.apply_funelim H ::= FunctionalInduction.apply_funelim H. (** Tactic to solve EqDec goals, destructing recursive calls for the recursive structure of the type and calling instances of eq_dec on other types. *) @@ -64,9 +64,9 @@ Ltac eqdec_proof := try red; intros; end; try solve[left; reflexivity | right; red; simplify_dep_elim]. Ltac Equations.Init.solve_eqdec ::= eqdec_proof. -Ltac Equations.Init.solve_subterm ::= Equations.Prop.Subterm.solve_subterm. -Ltac Equations.Init.unfold_recursor ::= Equations.Prop.Subterm.unfold_recursor. -Ltac Equations.Init.unfold_recursor_ext ::= Equations.Prop.Subterm.unfold_recursor_ext. +Ltac Equations.Init.solve_subterm ::= Subterm.solve_subterm. +Ltac Equations.Init.unfold_recursor ::= Subterm.unfold_recursor. +Ltac Equations.Init.unfold_recursor_ext ::= Subterm.unfold_recursor_ext. Ltac solve_noconf_prf := intros; on_last_hyp ltac:(fun id => destruct id) ; (* Subtitute a = b *) diff --git a/theories/Prop/Telescopes.v b/theories/Prop/Telescopes.v index 85249ab2d..c595dfa54 100644 --- a/theories/Prop/Telescopes.v +++ b/theories/Prop/Telescopes.v @@ -1,8 +1,8 @@ -Require Import Equations.Prop.Loader. +From Equations.Prop Require Import Loader. From Stdlib Require Import FunctionalExtensionality. -Require Import Equations.Prop.DepElim. -Require Import Equations.Prop.Tactics. -Require Import Equations.Prop.FunctionalInduction. +From Equations.Prop Require Import DepElim. +From Equations.Prop Require Import Tactics. +From Equations.Prop Require Import FunctionalInduction. (** Telescopes: allows treating variable arity fixpoints *) Set Universe Polymorphism. Import Sigma_Notations. diff --git a/theories/Prop/TransparentEquations.v b/theories/Prop/TransparentEquations.v index b41eedb55..d408f1de3 100644 --- a/theories/Prop/TransparentEquations.v +++ b/theories/Prop/TransparentEquations.v @@ -9,7 +9,7 @@ (** This module sets the set constants of Equations to transparent mode so that computation is possible inside Coq. *) -Require Import Equations.Prop.DepElim. +From Equations.Prop Require Import DepElim. Global Transparent simplification_sigma2_uip diff --git a/theories/Prop/dune b/theories/Prop/dune index 0e8645c1a..fa79324f9 100644 --- a/theories/Prop/dune +++ b/theories/Prop/dune @@ -1,7 +1,7 @@ (coq.theory ; This determines the -R flag (name Equations.Prop) - (package coq-equations) + (package rocq-equations) (synopsis "Equations Plugin") (theories Equations) (modules :standard)) diff --git a/theories/Type/All.v b/theories/Type/All.v index f76d841ff..f4cb3b245 100644 --- a/theories/Type/All.v +++ b/theories/Type/All.v @@ -15,7 +15,7 @@ Require Export Equations.Type.Loader. Require Export Equations.Type.Telescopes. Require Export Equations.Type.WellFoundedInstances. -Global Obligation Tactic := Equations.CoreTactics.equations_simpl. +Global Obligation Tactic := CoreTactics.equations_simpl. (** Tactic to solve well-founded proof obligations by default *) diff --git a/theories/Type/Classes.v b/theories/Type/Classes.v index 7e7f39829..2eedee000 100644 --- a/theories/Type/Classes.v +++ b/theories/Type/Classes.v @@ -7,10 +7,9 @@ (**********************************************************************) From Stdlib Require Import Extraction CRelationClasses. -Require Import Equations.Init Equations.CoreTactics. +From Equations Require Import Init CoreTactics. Set Warnings "-notation-overridden". -Require Import Equations.Type.Logic Equations.Type.Relation - Equations.Type.Relation_Properties Equations.Type.WellFounded. +From Equations.Type Require Import Logic Relation Relation_Properties WellFounded. Set Universe Polymorphism. diff --git a/theories/Type/Constants.v b/theories/Type/Constants.v index 94a49472a..049d5cb5c 100644 --- a/theories/Type/Constants.v +++ b/theories/Type/Constants.v @@ -1,8 +1,7 @@ Set Warnings "-notation-overridden". From Equations Require Import Init. -Require Import Equations.Type.Logic Equations.Type.DepElim - Equations.Type.EqDec Equations.Type.Classes. +From Equations.Type Require Import Logic DepElim EqDec Classes. From Stdlib Require Import CRelationClasses Relations. (** Naturals *) diff --git a/theories/Type/DepElim.v b/theories/Type/DepElim.v index 7422c7f18..6eaa6f670 100644 --- a/theories/Type/DepElim.v +++ b/theories/Type/DepElim.v @@ -10,12 +10,12 @@ Set Warnings "-notation-overridden". -Require Import Stdlib.Program.Tactics. +From Stdlib Require Import Program.Tactics. Require Export Equations.Init. -Require Import Equations.Signature Equations.CoreTactics. -Require Import Equations.Type.Logic. -Require Import Equations.Type.Classes. -Require Import Equations.Type.EqDec. +From Equations Require Import Signature CoreTactics. +From Equations.Type Require Import Logic. +From Equations.Type Require Import Classes. +From Equations.Type Require Import EqDec. Set Universe Polymorphism. diff --git a/theories/Type/EqDec.v b/theories/Type/EqDec.v index 60eac52a6..ed4a9b45d 100644 --- a/theories/Type/EqDec.v +++ b/theories/Type/EqDec.v @@ -8,9 +8,9 @@ Set Warnings "-notation-overridden". -Require Import Equations.Init. -Require Import Equations.Type.Logic. -Require Import Equations.Type.Classes. +From Equations Require Import Init. +From Equations.Type Require Import Logic. +From Equations.Type Require Import Classes. (** Decidable equality. diff --git a/theories/Type/EqDecInstances.v b/theories/Type/EqDecInstances.v index 1195b8828..cf79809bf 100644 --- a/theories/Type/EqDecInstances.v +++ b/theories/Type/EqDecInstances.v @@ -7,8 +7,7 @@ (**********************************************************************) Set Warnings "-notation-overridden". From Equations Require Import Init. -Require Import Equations.Type.Logic Equations.Type.Classes Equations.Type.DepElim - Equations.Type.Tactics Equations.Type.EqDec. +From Equations.Type Require Import Logic Classes DepElim Tactics EqDec. Local Open Scope equations_scope. Import Id_Notations Sigma_Notations. diff --git a/theories/Type/FunctionalExtensionality.v b/theories/Type/FunctionalExtensionality.v index 9ae80764f..d67c5f16a 100644 --- a/theories/Type/FunctionalExtensionality.v +++ b/theories/Type/FunctionalExtensionality.v @@ -1,7 +1,7 @@ Set Warnings "-notation-overridden". From Equations Require Import Init. From Stdlib Require Import CRelationClasses. -Require Import Equations.Type.Logic. +From Equations.Type Require Import Logic. (** The polymorphic equality type used by Equations when working with equality in Type. *) diff --git a/theories/Type/FunctionalInduction.v b/theories/Type/FunctionalInduction.v index 2da091521..3d290df43 100644 --- a/theories/Type/FunctionalInduction.v +++ b/theories/Type/FunctionalInduction.v @@ -7,8 +7,8 @@ (**********************************************************************) Set Warnings "-notation-overridden". -Require Import Equations.CoreTactics. -Require Import Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec Equations.Type.DepElim. +From Equations Require Import CoreTactics. +From Equations.Type Require Import Logic Classes EqDec DepElim. Set Universe Polymorphism. diff --git a/theories/Type/Loader.v b/theories/Type/Loader.v index b09937762..e19b44474 100644 --- a/theories/Type/Loader.v +++ b/theories/Type/Loader.v @@ -8,20 +8,20 @@ (** The set of libraries required to run Equations with all features. *) -Require Import Extraction. +From Stdlib Require Import Extraction. (** This exports tactics *) -Declare ML Module "coq-equations.plugin". +Declare ML Module "rocq-equations.plugin". Set Warnings "-notation-overridden". From Equations Require Export Init Signature. -Require Import Equations.CoreTactics. -Require Export Equations.Type.Logic Equations.Type.Classes. -Require Import Equations.Type.WellFounded. -Require Import Equations.Type.DepElim Equations.Type.EqDec Equations.Type.Constants. -Require Export Equations.Type.EqDecInstances. -Require Import Equations.Type.NoConfusion. -Require Import Equations.Type.Subterm. +From Equations Require Import CoreTactics. +From Equations.Type Require Export Logic Classes. +From Equations.Type Require Import WellFounded. +From Equations.Type Require Import DepElim EqDec Constants. +From Equations.Type Require Export EqDecInstances. +From Equations.Type Require Import NoConfusion. +From Equations.Type Require Import Subterm. Require Export Equations.Type.Tactics. Require Export Equations.Type.FunctionalInduction. (* funelim tactic *) diff --git a/theories/Type/NoConfusion.v b/theories/Type/NoConfusion.v index 7833ad8d9..803bf4d83 100644 --- a/theories/Type/NoConfusion.v +++ b/theories/Type/NoConfusion.v @@ -11,9 +11,9 @@ on some equation. *) From Equations Require Import Init Signature. -Require Import Equations.CoreTactics. -Require Import Equations.Type.Classes Equations.Type.EqDec Equations.Type.Constants. -Require Import Equations.Type.DepElim Equations.Type.Tactics. +From Equations Require Import CoreTactics. +From Equations.Type Require Import Classes EqDec Constants. +From Equations.Type Require Import DepElim Tactics. (** Parameterized inductive types just need NoConfusion. *) diff --git a/theories/Type/Relation.v b/theories/Type/Relation.v index 4fc40fc71..f96215e06 100644 --- a/theories/Type/Relation.v +++ b/theories/Type/Relation.v @@ -12,7 +12,7 @@ From Equations Require Import Init. From Stdlib Require Import Extraction CRelationClasses. Set Warnings "-notation-overridden". -Require Import Equations.Type.Logic. +From Equations.Type Require Import Logic. Local Open Scope equations_scope. Import Sigma_Notations. diff --git a/theories/Type/Relation_Properties.v b/theories/Type/Relation_Properties.v index c350c5669..4e6718297 100644 --- a/theories/Type/Relation_Properties.v +++ b/theories/Type/Relation_Properties.v @@ -16,10 +16,10 @@ Set Warnings "-notation-overridden". -Require Import CRelationClasses. -Require Import Equations.Init. -Require Import Equations.Type.Logic. -Require Import Equations.Type.Relation. +From Stdlib Require Import CRelationClasses. +From Equations Require Import Init. +From Equations.Type Require Import Logic. +From Equations.Type Require Import Relation. Import Sigma_Notations. Import Id_Notations. @@ -36,7 +36,7 @@ Section Properties. Variable R : relation A. Section Clos_Refl_Trans. - + Set Warnings "-notation-incompatible-prefix". Local Notation "R *" := (clos_refl_trans R) (at level 8, no associativity, format "R *"). diff --git a/theories/Type/Subterm.v b/theories/Type/Subterm.v index 64cbb4da0..6af575389 100644 --- a/theories/Type/Subterm.v +++ b/theories/Type/Subterm.v @@ -9,13 +9,9 @@ Set Warnings "-notation-overridden". From Equations Require Import Init Signature. -Require Import Equations.CoreTactics. -Require Import Equations.Type.Logic - Equations.Type.Classes Equations.Type.EqDec - Equations.Type.Relation - Equations.Type.FunctionalExtensionality - Equations.Type.WellFounded - Equations.Type.DepElim Equations.Type.Constants. +From Equations Require Import CoreTactics. +From Equations.Type Require Import Logic Classes EqDec + Relation FunctionalExtensionality WellFounded DepElim Constants. Set Universe Polymorphism. diff --git a/theories/Type/Tactics.v b/theories/Type/Tactics.v index 67ac9c7f1..c33e3731e 100644 --- a/theories/Type/Tactics.v +++ b/theories/Type/Tactics.v @@ -7,19 +7,19 @@ (**********************************************************************) Set Warnings "-notation-overridden". -Require Import Equations.CoreTactics Equations.Type.Logic Equations.Type.DepElim Equations.Type.EqDec - Equations.Type.Subterm Equations.Type.WellFounded Equations.Type.FunctionalInduction. +From Equations Require Import CoreTactics. +From Equations.Type Require Import Logic DepElim EqDec Subterm WellFounded FunctionalInduction. -Ltac Equations.Init.simpl_equations ::= Equations.Type.DepElim.simpl_equations. -Ltac Equations.Init.simplify_equalities ::= Equations.Type.DepElim.simplify_dep_elim. +Ltac Equations.Init.simpl_equations ::= DepElim.simpl_equations. +Ltac Equations.Init.simplify_equalities ::= DepElim.simplify_dep_elim. Ltac Equations.Init.depelim H ::= dependent elimination H; cbn in *. -Ltac Equations.Init.depind H ::= Equations.Type.DepElim.depind H. -Ltac Equations.Init.simp_IHs_tac ::= Equations.Type.FunctionalInduction.simplify_IHs_call. -Ltac Equations.Init.funelim_constr_as H H' tac ::= Equations.Type.FunctionalInduction.funelim_constr_as H H' tac. -Ltac Equations.Init.apply_funelim H ::= Equations.Type.FunctionalInduction.apply_funelim H. +Ltac Equations.Init.depind H ::= DepElim.depind H. +Ltac Equations.Init.simp_IHs_tac ::= FunctionalInduction.simplify_IHs_call. +Ltac Equations.Init.funelim_constr_as H H' tac ::= FunctionalInduction.funelim_constr_as H H' tac. +Ltac Equations.Init.apply_funelim H ::= FunctionalInduction.apply_funelim H. -Ltac Equations.Init.noconf H ::= Equations.Type.DepElim.noconf H. +Ltac Equations.Init.noconf H ::= DepElim.noconf H. Create HintDb solve_subterm discriminated. @@ -36,8 +36,8 @@ Ltac solve_subterm := intros; Ltac Equations.Init.solve_subterm ::= solve_subterm. Ltac Equations.Init.solve_eqdec ::= eqdec_proof. -Ltac Equations.Init.unfold_recursor ::= Equations.Type.Subterm.unfold_recursor. -Ltac Equations.Init.unfold_recursor_ext ::= Equations.Type.Subterm.unfold_recursor_ext. +Ltac Equations.Init.unfold_recursor ::= Subterm.unfold_recursor. +Ltac Equations.Init.unfold_recursor_ext ::= Subterm.unfold_recursor_ext. Ltac solve_noconf_prf := intros; on_last_hyp ltac:(fun id => destruct id) ; (* Subtitute a = b *) diff --git a/theories/Type/Telescopes.v b/theories/Type/Telescopes.v index 7f9b70167..d6108215c 100644 --- a/theories/Type/Telescopes.v +++ b/theories/Type/Telescopes.v @@ -1,12 +1,12 @@ Set Warnings "-notation-overridden". -Require Import Equations.Type.Loader. -Require Import Equations.Type.Logic. -Require Import Equations.Type.FunctionalExtensionality. -Require Import Equations.Type.WellFounded. -Require Import Equations.Type.DepElim. -Require Import Equations.Type.Subterm. -Require Import Equations.Type.Tactics. -Require Import Equations.Type.FunctionalInduction. +From Equations.Type Require Import Loader. +From Equations.Type Require Import Logic. +From Equations.Type Require Import FunctionalExtensionality. +From Equations.Type Require Import WellFounded. +From Equations.Type Require Import DepElim. +From Equations.Type Require Import Subterm. +From Equations.Type Require Import Tactics. +From Equations.Type Require Import FunctionalInduction. (** Telescopes: allows treating variable arity fixpoints *) Set Universe Polymorphism. diff --git a/theories/Type/WellFounded.v b/theories/Type/WellFounded.v index a7ce9a839..860efeb2c 100644 --- a/theories/Type/WellFounded.v +++ b/theories/Type/WellFounded.v @@ -1,8 +1,7 @@ Set Warnings "-notation-overridden". From Stdlib Require Import Extraction CRelationClasses. -Require Import Equations.Init Equations.CoreTactics. -Require Import Equations.Type.Logic Equations.Type.FunctionalExtensionality - Equations.Type.Relation Equations.Type.Relation_Properties. +From Equations Require Import Init CoreTactics. +From Equations.Type Require Import Logic FunctionalExtensionality Relation Relation_Properties. Set Universe Polymorphism. Import Id_Notations. diff --git a/theories/Type/WellFoundedInstances.v b/theories/Type/WellFoundedInstances.v index 8427a138d..6bb27a3cb 100644 --- a/theories/Type/WellFoundedInstances.v +++ b/theories/Type/WellFoundedInstances.v @@ -1,5 +1,5 @@ Set Warnings "-notation-overridden". -Require Import Equations.Type.Loader Equations.Type.Relation Equations.Type.WellFounded. +From Equations.Type Require Import Loader Relation WellFounded. Import Id_Notations. Section Lt. diff --git a/theories/Type/dune b/theories/Type/dune index ae6e4f2bc..49bd5450a 100644 --- a/theories/Type/dune +++ b/theories/Type/dune @@ -1,7 +1,7 @@ (coq.theory ; This determines the -R flag (name Equations.Type) - (package coq-equations) + (package rocq-equations) (synopsis "Equations Plugin") (theories Equations) (modules :standard)) diff --git a/theories/dune b/theories/dune index aa6a1a0bb..7ee20c7a0 100644 --- a/theories/dune +++ b/theories/dune @@ -1,9 +1,11 @@ (coq.theory ; This determines the -R flag (name Equations) - (package coq-equations) + (package rocq-equations) (synopsis "Equations Plugin") - (libraries coq-core.plugins.extraction coq-equations.plugin) - (modules :standard \ IdDec NoCycle)) + (plugins rocq-runtime.plugins.extraction rocq-equations.plugin) + (modules :standard \ IdDec NoCycle) + (theories Stdlib)) -(include_subdirs no) \ No newline at end of file +(include_subdirs no) +(dirs ("Prop" "Type")) \ No newline at end of file