diff options
87 files changed, 1633 insertions, 390 deletions
diff --git a/.gitignore b/.gitignore index 35cdf9b4e..64c49b008 100644 --- a/.gitignore +++ b/.gitignore @@ -43,6 +43,7 @@ TAGS .DS_Store .pc bin/ +_build_ci _build myocamlbuild_config.ml config/Makefile diff --git a/.travis.yml b/.travis.yml index de16f2d0b..7138d5c61 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,4 +1,7 @@ dist: trusty +# Travis builds are slower using sudo: false (the container-based +# infrastructure) as of March 2017; see +# https://github.com/coq/coq/pull/467 for some discussion. sudo: required # Until Ocaml becomes a language, we set a known one. language: c @@ -27,9 +30,9 @@ env: - TEST_TARGET="ci-color" - TEST_TARGET="ci-compcert" - TEST_TARGET="ci-coquelicot" - - TEST_TARGET="ci-cpdt" - TEST_TARGET="ci-geocoq" - TEST_TARGET="ci-fiat-crypto" + - TEST_TARGET="ci-fiat-parsers" - TEST_TARGET="ci-flocq" - TEST_TARGET="ci-hott" - TEST_TARGET="ci-iris-coq" @@ -38,13 +41,14 @@ env: - TEST_TARGET="ci-sf" - TEST_TARGET="ci-unimath" # Not ready yet for 8.7 + # - TEST_TARGET="ci-cpdt" # - TEST_TARGET="ci-metacoq" # - TEST_TARGET="ci-tlc" matrix: allow_failures: - - env: TEST_TARGET="ci-cpdt" + - env: TEST_TARGET="ci-geocoq" # Full Coq test-suite with two compilers # [TODO: use yaml refs and avoid duplication for packages list] @@ -7,6 +7,15 @@ Tactics functional extensionality in H supposed to be a quantified equality until giving a bare equality. +Libraries + +- New file PropExtensionality.v to explicitly work in the axiomatic + context of propositional extensionality. +- New file SetoidChoice.v axiomatically providing choice over setoids, + and, consequently, choice of representatives in equivalence classes. + Various proof-theoretic characterizations of choice over setoids in + file ChoiceFacts.v. + Changes from V8.6beta1 to V8.6 ============================== @@ -1,5 +1,15 @@ +# TODO: Move to META.in once coq_makefile2 is merged. +# We need to reuse: +# - The variable substitution mechanism. +# - Sourcing of "coq_install_path" and "coq_version" variables. +# +# With this rules, we would have: +# version = ${coq_version} +# and +# linkopts(byte) = "-dllpath ${coq_install_path}/kernel/byterun/ -dllib -lcoqrun" + description = "The Coq Proof Assistant Plugin API" -version = "8.6" +version = "8.7" directory = "" requires = "camlp5" @@ -7,7 +17,7 @@ requires = "camlp5" package "config" ( description = "Coq Configuration Variables" - version = "8.6" + version = "8.7" directory = "config" @@ -16,7 +26,7 @@ package "config" ( package "lib" ( description = "Base Coq Library" - version = "8.6" + version = "8.7" directory = "lib" @@ -33,22 +43,16 @@ package "lib" ( package "vm" ( description = "Coq VM" + version = "8.7" - version = "8.6" - -# EJGA FIXME: Unfortunately dllpath is dependent on the type of Coq -# install. In a local one we'll want kernel/byterun, in a non-local -# one we want to set it to coqlib. We should thus generate this file -# at configure time, but let's hear for some more feedback from -# experts. + directory = "kernel/byterun" -# Enable for local native & byte builds -# directory = "kernel/byterun" +# We should generate this file at configure time for local byte builds +# to work properly. -# Enable for local byte builds and set up properly -# linkopts(byte) = "-dllpath /path/to/coq/kernel/byterun/ -dllib -lcoqrun" +# Enable this setting for local byte builds, disabling the one below. +# linkopts(byte) = "-dllpath path_to_coq/kernel/byterun/ -dllib -lcoqrun" -# Disable for local byte builds linkopts(byte) = "-dllib -lcoqrun" linkopts(native) = "-cclib -lcoqrun" @@ -56,8 +60,8 @@ package "vm" ( package "kernel" ( - description = "The Coq's Kernel" - version = "8.6" + description = "Coq's Kernel" + version = "8.7" directory = "kernel" @@ -71,7 +75,7 @@ package "kernel" ( package "library" ( description = "Coq Libraries (vo) support" - version = "8.6" + version = "8.7" requires = "coq.kernel" @@ -85,7 +89,7 @@ package "library" ( package "intf" ( description = "Coq Public Data Types" - version = "8.6" + version = "8.7" requires = "coq.library" @@ -95,8 +99,8 @@ package "intf" ( package "engine" ( - description = "Coq Libraries (vo) support" - version = "8.6" + description = "Coq Tactic Engine" + version = "8.7" requires = "coq.library" directory = "engine" @@ -109,7 +113,7 @@ package "engine" ( package "pretyping" ( description = "Coq Pretyper" - version = "8.6" + version = "8.7" requires = "coq.engine" directory = "pretyping" @@ -122,7 +126,7 @@ package "pretyping" ( package "interp" ( description = "Coq Term Interpretation" - version = "8.6" + version = "8.7" requires = "coq.pretyping" directory = "interp" @@ -135,7 +139,7 @@ package "interp" ( package "grammar" ( description = "Coq Base Grammar" - version = "8.6" + version = "8.7" requires = "coq.interp" directory = "grammar" @@ -147,7 +151,7 @@ package "grammar" ( package "proofs" ( description = "Coq Proof Engine" - version = "8.6" + version = "8.7" requires = "coq.interp" directory = "proofs" @@ -160,7 +164,7 @@ package "proofs" ( package "parsing" ( description = "Coq Parsing Engine" - version = "8.6" + version = "8.7" requires = "coq.proofs" directory = "parsing" @@ -172,8 +176,8 @@ package "parsing" ( package "printing" ( - description = "Coq Printing Libraries" - version = "8.6" + description = "Coq Printing Engine" + version = "8.7" requires = "coq.parsing" directory = "printing" @@ -185,8 +189,8 @@ package "printing" ( package "tactics" ( - description = "Coq Tactics" - version = "8.6" + description = "Coq Basic Tactics" + version = "8.7" requires = "coq.printing" directory = "tactics" @@ -196,12 +200,25 @@ package "tactics" ( ) +package "vernac" ( + + description = "Coq Vernacular Interpreter" + version = "8.7" + + requires = "coq.tactics" + directory = "vernac" + + archive(byte) = "vernac.cma" + archive(native) = "vernac.cmxa" + +) + package "stm" ( description = "Coq State Transactional Machine" - version = "8.6" + version = "8.7" - requires = "coq.tactics" + requires = "coq.vernac" directory = "stm" archive(byte) = "stm.cma" @@ -212,7 +229,7 @@ package "stm" ( package "toplevel" ( description = "Coq Toplevel" - version = "8.6" + version = "8.7" requires = "coq.stm" directory = "toplevel" @@ -225,7 +242,7 @@ package "toplevel" ( package "highparsing" ( description = "Coq Extra Parsing" - version = "8.6" + version = "8.7" requires = "coq.toplevel" directory = "parsing" @@ -238,12 +255,12 @@ package "highparsing" ( package "ltac" ( description = "Coq LTAC Plugin" - version = "8.6" + version = "8.7" requires = "coq.highparsing" - directory = "ltac" + directory = "plugins/ltac" - archive(byte) = "ltac.cma" - archive(native) = "ltac.cmxa" + archive(byte) = "ltac_plugin.cmo" + archive(native) = "ltac_plugin.cmx" ) diff --git a/Makefile.ci b/Makefile.ci index e4b5832f6..897318c4d 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,5 +1,5 @@ CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ - ci-color ci-math-classes ci-tlc ci-fiat-crypto \ + ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \ ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \ ci-unimath diff --git a/Makefile.common b/Makefile.common index df705034e..1e71bcf7d 100644 --- a/Makefile.common +++ b/Makefile.common @@ -122,12 +122,12 @@ DERIVECMO:=plugins/derive/derive_plugin.cmo LTACCMO:=plugins/ltac/ltac_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo -PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \ +PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \ $(QUOTECMO) $(RINGCMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ - $(DERIVECMO) $(SSRMATCHINGCMO) $(LTACCMO) + $(DERIVECMO) $(SSRMATCHINGCMO) ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) STATICPLUGINS:=$(PLUGINSCMO) diff --git a/Makefile.install b/Makefile.install index 4800ea0b9..bde035551 100644 --- a/Makefile.install +++ b/Makefile.install @@ -104,11 +104,12 @@ install-library: $(MKDIR) $(FULLCOQLIB) $(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS) $(MKDIR) $(FULLCOQLIB)/user-contrib + $(MKDIR) $(FULLCOQLIB)/kernel/byterun ifndef CUSTOM - $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB) + $(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)/kernel/byterun endif ifeq ($(BEST),opt) - $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB) + $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)/kernel/byterun $(INSTALLSH) $(FULLCOQLIB) $(PLUGINSOPT) endif # csdpcert is not meant to be directly called by the user; we install diff --git a/configure.ml b/configure.ml index 48e167c99..82ce931d6 100644 --- a/configure.ml +++ b/configure.ml @@ -261,7 +261,7 @@ module Prefs = struct let withdoc = ref false let geoproof = ref false let byteonly = ref false - let debug = ref false + let debug = ref true let profile = ref false let annotate = ref false let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) @@ -336,7 +336,9 @@ let args_options = Arg.align [ "-byteonly", Arg.Set Prefs.byteonly, " Compiles only bytecode version of Coq"; "-debug", Arg.Set Prefs.debug, - " Add debugging information in the Coq executables"; + " Deprecated"; + "-nodebug", Arg.Clear Prefs.debug, + " Do not add debugging information in the Coq executables"; "-profile", Arg.Set Prefs.profile, " Add profiling information in the Coq executables"; "-annotate", Arg.Set Prefs.annotate, @@ -924,7 +926,7 @@ let config_runtime () = | _ -> let ld="CAML_LD_LIBRARY_PATH" in build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld; - ["-dllib";"-lcoqrun";"-dllpath";libdir] + ["-dllib";"-lcoqrun";"-dllpath";libdir/"kernel/byterun"] let vmbyteflags = config_runtime () diff --git a/dev/base_include b/dev/base_include index 0abcefc38..242405ae2 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,7 +17,7 @@ #directory "grammar";; #directory "intf";; #directory "stm";; -#directory "ltac";; +#directory "vernac";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) @@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Pltac.tactic;; +let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh new file mode 100644 index 000000000..da5b42579 --- /dev/null +++ b/dev/ci/ci-basic-overlay.sh @@ -0,0 +1,103 @@ +#!/usr/bin/env bash + +# This is the basic overlay set for repositories in the CI. + +# Maybe we should just use Ruby to have real objects... + +######################################################################## +# MathComp +######################################################################## +: ${mathcomp_CI_BRANCH:=master} +: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git} + +######################################################################## +# UniMath +######################################################################## +: ${UniMath_CI_BRANCH:=master} +: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git} + +######################################################################## +# Unicoq + Metacoq +######################################################################## +: ${unicoq_CI_BRANCH:=master} +: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git} + +: ${metacoq_CI_BRANCH:=master} +: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git} + +######################################################################## +# Mathclasses + Corn +######################################################################## +: ${math_classes_CI_BRANCH:=v8.6} +: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} + +: ${Corn_CI_BRANCH:=v8.6} +: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} + +######################################################################## +# Iris +######################################################################## +: ${stdpp_CI_BRANCH:=master} +: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git} + +: ${Iris_CI_BRANCH:=master} +: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git} + +######################################################################## +# HoTT +######################################################################## +: ${HoTT_CI_BRANCH:=mz-8.7} +: ${HoTT_CI_GITURL:=https://github.com/ejgallego/HoTT.git} + +######################################################################## +# GeoCoq +######################################################################## +: ${GeoCoq_CI_BRANCH:=master} +: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git} + +######################################################################## +# Flocq +######################################################################## +: ${Flocq_CI_BRANCH:=master} +: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git} + +######################################################################## +# Coquelicot +######################################################################## +: ${Coquelicot_CI_BRANCH:=master} +: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} + +######################################################################## +# Coquelicot +######################################################################## +: ${CompCert_CI_BRANCH:=master} +: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} + +######################################################################## +# fiat_parsers +######################################################################## +: ${fiat_parsers_CI_BRANCH:=master} +: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} + +######################################################################## +# fiat_crypto +######################################################################## +: ${fiat_crypto_CI_BRANCH:=master} +: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git} + +######################################################################## +# CoLoR +######################################################################## +: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} + +######################################################################## +# SF +######################################################################## +: ${sf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz} + +######################################################################## +# TLC +######################################################################## +: ${tlc_CI_BRANCH:=master} +: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git} + diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 78ae7f02f..3f0716511 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color +Color_CI_DIR=${CI_BUILD_DIR}/color -( cd color && make -j ${NJOBS} ) +svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} + +( cd ${Color_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 412da626f..c94f15026 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash set -xe @@ -8,20 +8,30 @@ export PATH=`pwd`/bin:$PATH ls `pwd`/bin -# Maybe we should just use Ruby... -mathcomp_CI_BRANCH=master -mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git +# Where we clone and build external developments +CI_BUILD_DIR=`pwd`/_build_ci -# git_checkout branch +source ${ci_dir}/ci-user-overlay.sh +source ${ci_dir}/ci-basic-overlay.sh + +mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp + +# git_checkout branch url dest will create a git repository +# in <dest> (if it does not exist already) and checkout the +# remote branch <branch> from <url> git_checkout() { local _BRANCH=${1} local _URL=${2} local _DEST=${3} - echo "Checking out ${_DEST}" - git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST} - ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) + mkdir -p ${_DEST} + ( cd ${_DEST} && \ + if [ ! -d .git ] ; then git clone --depth 1 ${_URL} . ; fi && \ + echo "Checking out ${_DEST}" && \ + git fetch ${_URL} ${_BRANCH} && \ + git checkout FETCH_HEAD && \ + echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) } checkout_mathcomp() @@ -34,8 +44,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp math-comp - ( cd math-comp/mathcomp && \ + checkout_mathcomp ${mathcomp_CI_DIR} + ( cd ${mathcomp_CI_DIR}/mathcomp && \ sed -i.bak '/ssrtest/d' Make && \ sed -i.bak '/odd_order/d' Make && \ sed -i.bak '/all\/all.v/d' Make && \ diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index ec09389f8..c78ffdc2c 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -1,13 +1,12 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -CompCert_CI_BRANCH=master -CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git +CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir -git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} # Patch to avoid the upper version limit -( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) +( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 94bd5e468..40eff03b7 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,12 +1,12 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot + install_ssreflect -# Setup coquelicot -git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot +git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR} -( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh index 18d756180..0e791ebbf 100755 --- a/dev/ci/ci-cpdt.sh +++ b/dev/ci/ci-cpdt.sh @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index c669195dd..93d39aab0 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto +fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto -( cd fiat-crypto && make -j ${NJOBS} ) +git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} + +( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh new file mode 100755 index 000000000..c62aa1d85 --- /dev/null +++ b/dev/ci/ci-fiat-parsers.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat + +git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} + +( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 345924e40..ec19bd993 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq +Flocq_CI_DIR=${CI_BUILD_DIR}/flocq -( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR} + +( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index ce870e52b..4e5aa2687 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -1,16 +1,16 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: replace by generic template -GeoCoq_CI_BRANCH=master -GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git +GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq -git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} -( cd GeoCoq && \ +( cd ${GeoCoq_CI_DIR} && \ ./configure.sh && \ sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ + sed -i.bak '/Elements\/Book_1\.v/d' Make && \ + sed -i.bak '/Elements\/Book_3\.v/d' Make && \ coq_makefile -f Make -o Makefile && \ make -j ${NJOBS} ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 0c07564c0..1bf6e9a87 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT +HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT -( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) +git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} + +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index c21af976f..eb1d1be07 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -1,17 +1,22 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp + +Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq + install_ssreflect # Setup stdpp -git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp -( cd coq-stdpp && make -j ${NJOBS} && make install ) +git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} + +( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install ) # Setup Iris -git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq -( cd iris-coq && make -j ${NJOBS} ) +git_checkout ${Iris_CI_BRANCH} ${Iris_CI_GITURL} ${Iris_CI_DIR} + +( cd ${Iris_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 4450dc071..beb75773b 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,12 +1,20 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes -( cd math-classes && make -j ${NJOBS} && make install ) +math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes -git_checkout v8.6 https://github.com/c-corn/corn.git corn -( cd corn && make -j ${NJOBS} ) +Corn_CI_DIR=${CI_BUILD_DIR}/corn +# Setup Math-Classes + +git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} + +( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install ) + +# Setup Corn + +git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} + +( cd ${Corn_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 2eb150cb5..bb8188da4 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -1,13 +1,15 @@ -#!/bin/bash +#!/usr/bin/env bash # $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -checkout_mathcomp math-comp +mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp + +checkout_mathcomp ${mathcomp_CI_DIR} # odd_order takes too much time for travis. -( cd math-comp/mathcomp && \ +( cd ${mathcomp_CI_DIR}/mathcomp && \ sed -i.bak '/PFsection/d' Make && \ sed -i.bak '/stripped_odd_order_theorem/d' Make && \ make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 91a33695b..e31691179 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -1,16 +1,19 @@ -#!/bin/bash +#!/usr/bin/env bash -# $0 is not the safest way, but... ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# MetaCoq + UniCoq +unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq +metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq -git_checkout master https://github.com/unicoq/unicoq.git unicoq +# Setup UniCoq -( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) +git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR} -git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq +( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) -( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) +# Setup MetaCoq +git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR} + +( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 5e41211f1..7d23ccad9 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -1,9 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz +# XXX: Needs fixing to properly set the build directory. +wget ${sf_CI_TARURL} tar xvfz sf.tgz ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} ) diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh new file mode 100755 index 000000000..700105aed --- /dev/null +++ b/dev/ci/ci-template.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Template_CI_BRANCH=master +Template_CI_GITURL=https://github.com/Template/Template +Template_CI_DIR=${CI_BUILD_DIR}/Template + +git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR} + +( cd ${Template_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index b94632492..ce2639937 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -1,8 +1,10 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc +tlc_CI_DIR=${CI_BUILD_DIR}/tlc -( cd tlc && make -j ${NJOBS} ) +git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR} + +( cd ${tlc_CI_DIR} && make -j ${NJOBS} ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 15e619acb..175b82b5f 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,14 +1,13 @@ -#!/bin/bash +#!/usr/bin/env bash ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -UniMath_CI_BRANCH=master -UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git +UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath -git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} -( cd UniMath && \ +( cd ${UniMath_CI_DIR} && \ sed -i.bak '/Folds/d' Makefile && \ sed -i.bak '/HomologicalAlgebra/d' Makefile && \ make -j ${NJOBS} BUILD_COQ=no ) diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh new file mode 100644 index 000000000..028574743 --- /dev/null +++ b/dev/ci/ci-user-overlay.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash + +# Add user overlays here. You can use some logic to detect if you are +# in your travis branch and conditionally enable the overlay. + +# Some useful Travis variables: +# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables) +# +# - TRAVIS_BRANCH: For builds not triggered by a pull request this is +# the name of the branch currently being built; whereas for builds +# triggered by a pull request this is the name of the branch +# targeted by the pull request (in many cases this will be master). +# +# - TRAVIS_COMMIT: The commit that the current build is testing. +# +# - TRAVIS_PULL_REQUEST: The pull request number if the current job is +# a pull request, “false” if it’s not a pull request. +# +# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request, +# the name of the branch from which the PR originated. "" if the +# current job is a push build. + diff --git a/dev/core.dbg b/dev/core.dbg index 698db63d2..f04e5c07b 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -16,4 +16,4 @@ load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma load_printer highparsing.cma -load_printer ltac.cma +load_printer ltac_plugin.cmo diff --git a/dev/doc/api.txt b/dev/doc/api.txt new file mode 100644 index 000000000..5827257b5 --- /dev/null +++ b/dev/doc/api.txt @@ -0,0 +1,10 @@ +Recommendations in using the API: + +The type of terms: constr (see kernel/constr.ml and kernel/term.ml) + +- On type constr, the canonical equality on CIC (up to + alpha-conversion and cast removal) is Constr.equal +- The type constr is abstract, use mkRel, mkSort, etc. to build + elements in constr; use "kind_of_term" to analyze the head of a + constr; use destRel, destSort, etc. when the head constructor is + known diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 8d2d05590..12c3ec454 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -39,6 +39,8 @@ important things: instead - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes +- The TacFun tactic expression constructor now takes a `Name.t list` for the + variable list rather than an `Id.t option list`. The folder itself has been turned into a plugin. This does not change much, but because it is a packed plugin, it may wreak havoc for third-party plugins diff --git a/dev/doc/style.txt b/dev/doc/style.txt index 27695a09b..2ee3dadd7 100644 --- a/dev/doc/style.txt +++ b/dev/doc/style.txt @@ -1,75 +1,142 @@ - -<< L'uniformité du style est plus importante que le style lui-même. >> -(Kernigan & Pike, The Practice of Programming) - -Mode Emacs -========== - Tuareg, que l'on trouve ici : http://www.prism.uvsq.fr/~acohen/tuareg/ - - avec le réglage suivant : (setq tuareg-in-indent 2) - -Types récursifs et filtrages -============================ - Une barre de séparation y compris sur le premier constructeur - -type t = - | A - | B of machin - -match expr with - | A -> ... - | B x -> ... - -Remarque : à partir de la 8.2 environ, la tendance est à utiliser le -format suivant qui permet de limiter l'escalade d'indentation tout en -produisant un aspect visuel intéressant de bloc : - -type t = -| A -| B of machin - -match expr with -| A -> ... -| B x -> ... - -let f expr = match expr with -| A -> ... -| B x -> ... - -let f expr = function -| A -> ... -| B x -> ... - -Le deuxième cas est obtenu sous tuareg avec les réglages - - (setq tuareg-with-indent 0) - (setq tuareg-function-indent 0) - (setq tuareg-let-always-indent nil) /// notons que cette dernière est bien - /// pour les let mais pas pour les let-in - -Conditionnelles -=============== - if condition then - premier-cas - else - deuxieme-cas - - Si effets de bord dans les branches, utilisez begin ... end et non des - parenthèses i.e. - - if condition then begin - instr1; - instr2 - end else begin - instr3; - instr4 - end - - Si la première branche lève une exception, évitez le else i.e. - - if condition then if condition then error "machin"; - error "machin" -----> suite +<< Style uniformity is more important than style itself >> + (Kernigan & Pike, The Practice of Programming) + +OCaml Style: +- Spacing and indentation + - indent your code (using tuareg default) + - no strong constraints in formatting "let in"; possible styles are: + "let x = ... in" + "let x = + ... in" + "let + x = ... + in" + - but: no extra indentation before a "in" coming on next line, + otherwise, it first shifts further and further on the right, + reducing the amount of space available; second, it is not robust to + insertion of a new "let" + - it is established usage to have space around "|" as in + "match c with + | [] | [a] -> ... + | a::b::l -> ..." + - in a one-line "match", it is preferred to have no "|" in front of + the first case (this saves spaces for the match to hold in the line) + - from about 8.2, the tendency is to use the following format which + limit excessive indentation while providing an interesting "block" aspect + type t = + | A + | B of machin + + let f expr = match expr with + | A -> ... + | B x -> ... + + let f expr = function + | A -> ... + | B x -> ... + - add spaces around = and == (make the code "breaths") + - the common usage is to write "let x,y = ... in ..." rather than + "let (x,y) = ... in ..." + - parenthesizing with either "(" and ")" or with "begin" and "end" is + common practice + - preferred layout for conditionals: + if condition then + premier-cas else - suite - - + deuxieme-cas + - in case of effects in branches, use "begin ... end" rather than + parentheses + if condition then begin + instr1; + instr2 + end else begin + instr3; + instr4 + end + - if the first branch raises an exception, avoid the "else", i.e.: + if condition then if condition then error "foo"; + error "foo" -----> bar + else + bar + - it is the usage not to use ;; to end OCaml sentences (however, + inserting ";;" can be useful for debugging syntax errors crossing + the boundary of functions) + - relevant options in tuareg: + (setq tuareg-in-indent 2) + (setq tuareg-with-indent 0) + (setq tuareg-function-indent 0) + (setq tuareg-let-always-indent nil) + +- Coding methodology + - no "try ... with _ -> ..." which catches even Sys.Break (Ctrl-C), + Out_of_memory, Stack_overflow, etc. + at least, use "try with e when Errors.noncritical e -> ..." + (to be detailed, Pierre L. ?) + - do not abuse of fancy combinators: sometimes what a "let rec" loop + does is more readable and simpler to grasp than what a "fold" does + - do not break abstractions: if an internal property is hidden + behind an interface, do no rely on it in code which uses this + interface (e.g. do not use List.map thinking it is left-to-right, + use map_left) + - in particular, do not use "=" on abstract types: there is no + reason a priori that it is the intended equality on this type; use the + "equal" function normally provided with the abstract type + - avoid polymorphically typed "=" whose implementation is not + optimized in OCaml and which has moreover no reason to be the + intended implementation of the equality when it comes to be + instantiated on a particular type (e.g. use List.mem_f, + List.assoc_f, rather than List.mem, List.assoc, etc, unless it is + absolutely clear that "=" will implement the intended equality, and + with the right complexity) + - any new general-purpose enough combinator on list should be put in + cList.ml, on type option in cOpt.ml, etc. + - unless of a good reason not to so, follow the style of the + surrounding code in the same file as much as possible, + the general guidelines are otherwise "let spacing breaths" (we + have large screen nowadays), "make your code easy to read and + to understand" + - document what is tricky, but do not overdocument, sometimes the + choice of names and the structuration of the code is a better + documentation than a long discourse; use of unicode in comments is + welcome if it can make comments more readable (then + "toggle-enable-multibyte-characters" can help when using the + debugger in emacs) + - all of initial "open File", or of small-scope File.(...), or + per-ident File.foo are common practices + +- Choice of variable names + - be consistent when naming from one function to another + - be consistent with the naming adopted in the functions from the + same file, or with the naming used elsewhere by similar functions + - use variable names which express meaning + - keep "cst" for constants and avoid it for constructors which is + otherwise a source of confusion + - for constructors, use "cstr" in type constructor (resp. "cstru" in + constructor puniverse); avoid "constr" for "constructor" which + could be think as the name of an arbitrary Constr.t + - for inductive types, use "ind" in the type inductive (resp "indu" + in inductive puniverse) + - for env, use "env" + - for evar_map, use "sigma", with tolerance into "evm" and "evd" + - for named_context or rel_context, use "ctxt" or "ctx" (or "sign") + - for formal/actual indices of inductive types: "realdecls", "realargs" + - for formal/actual parameters of inductive types: "paramdecls", "paramargs" + - for terms, use e.g. c, b, a, ... + - if a term is known to be a function: f, ... + - if a term is known to be a type: t, u, typ, ... + - for a declaration, use d or "decl" + - for errors, exceptions, use e + +- Common OCaml pitfalls + - in "match ... with Case1 -> try ... with ... -> ... | Case2 -> ...", or in + "match ... with Case1 -> match ... with SubCase -> ... | Case2 -> ...", or in + parentheses are needed around the "try" and the inner "match" + - even if stream are lazy, the Pp.(++) combinator is strict and + forces the evaluation of its arguments (use a "lazy" or a "fun () ->") + to make it lazy explicitly + - in "if ... then ... else ... ++ ...", the default parenthesizing + is somehow counter-intuitive; use "(if ... then ... else ...) ++ ..." + - in "let myspecialfun = mygenericfun args", be sure that it does no + do side-effect; prefer otherwise "let mygenericfun arg = + mygenericfun args arg" to ensure that the function is evaluated at + runtime diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4fcad8820..dc354b130 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -234,7 +234,7 @@ let ppenvwithcst e = pp str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") -let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x)) +let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index c37367de5..16c822b6a 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -477,15 +477,15 @@ names. \item{\tt Show Intro.}\comindex{Show Intro}\\ If the current goal begins by at least one product, this command prints the name of the first product, as it would be generated by -an anonymous {\tt Intro}. The aim of this command is to ease the +an anonymous {\tt intro}. The aim of this command is to ease the writing of more robust scripts. For example, with an appropriate {\ProofGeneral} macro, it is possible to transform any anonymous {\tt - Intro} into a qualified one such as {\tt Intro y13}. + intro} into a qualified one such as {\tt intro y13}. In the case of a non-product goal, it prints nothing. \item{\tt Show Intros.}\comindex{Show Intros}\\ This command is similar to the previous one, it simulates the naming -process of an {\tt Intros}. +process of an {\tt intros}. \item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials} \\ It displays diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 21c39de96..61093709e 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -59,6 +59,12 @@ and pretty-printer of {\Coq} already know how to deal with the syntactic expression (see \ref{ReservedNotation}), explicit precedences and associativity rules have to be given. +\Rem The right-hand side of a notation is interpreted at the time the +notation is given. In particular, implicit arguments (see +Section~\ref{Implicit Arguments}), coercions (see +Section~\ref{Coercions}), etc. are resolved at the time of the +declaration of the notation. + \subsection[Precedences and associativity]{Precedences and associativity\index{Precedences} \index{Associativity}} @@ -297,7 +303,7 @@ the possible following elements delimited by single quotes: of each newline \end{itemize} -Thus, for the previous example, we get +%Thus, for the previous example, we get %\footnote{The ``@'' is here to shunt %the notation "'IF' A 'then' B 'else' C" which is defined in {\Coq} %initial state}: @@ -908,6 +914,28 @@ interpretation. See the next section. \SeeAlso The command to show the scopes bound to the arguments of a function is described in Section~\ref{About}. +\Rem In notations, the subterms matching the identifiers of the +notations are interpreted in the scope in which the identifiers +occurred at the time of the declaration of the notation. Here is an +example: + +\begin{coq_example} +Parameter g : bool -> bool. +Notation "@@" := true (only parsing) : bool_scope. +Notation "@@" := false (only parsing): mybool_scope. + +(* Defining a notation while the argument of g is bound to bool_scope *) +Bind Scope bool_scope with bool. +Notation "# x #" := (g x) (at level 40). +Check # @@ #. +(* Rebinding the argument of g to mybool_scope has no effect on the notation *) +Arguments g _%mybool_scope. +Check # @@ #. +(* But we can force the scope *) +Delimit Scope mybool_scope with mybool. +Check # @@%mybool #. +\end{coq_example} + \subsection[The {\tt type\_scope} interpretation scope]{The {\tt type\_scope} interpretation scope\index{type\_scope@\texttt{type\_scope}}} The scope {\tt type\_scope} has a special status. It is a primitive diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 9216c81fc..aeb0de48a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -46,6 +46,7 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/ClassicalDescription.v theories/Logic/ClassicalEpsilon.v theories/Logic/ClassicalUniqueChoice.v + theories/Logic/SetoidChoice.v theories/Logic/Berardi.v theories/Logic/Diaconescu.v theories/Logic/Hurkens.v @@ -55,7 +56,10 @@ through the <tt>Require Import</tt> command.</p> theories/Logic/Description.v theories/Logic/Epsilon.v theories/Logic/IndefiniteDescription.v + theories/Logic/PropExtensionality.v + theories/Logic/PropExtensionalityFacts.v theories/Logic/FunctionalExtensionality.v + theories/Logic/ExtensionalFunctionRepresentative.v theories/Logic/ExtensionalityFacts.v theories/Logic/WeakFan.v theories/Logic/WKL.v diff --git a/grammar/q_util.mli b/grammar/q_util.mli index a5e36e47b..37ec1d56a 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -41,6 +41,8 @@ val mlexpr_of_string : string -> MLast.expr val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr +val mlexpr_of_name : ('a -> MLast.expr) -> 'a option -> MLast.expr + val mlexpr_of_prod_entry_key : (string -> MLast.expr) -> user_symbol -> MLast.expr val type_of_user_symbol : user_symbol -> argument_type diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 919ca3ad7..0dd096ef7 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -58,6 +58,10 @@ let mlexpr_of_option f = function | None -> <:expr< None >> | Some e -> <:expr< Some $f e$ >> +let mlexpr_of_name f = function + | None -> <:expr< Anonymous >> + | Some e -> <:expr< Name $f e$ >> + let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> let rec mlexpr_of_prod_entry_key f = function diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index fe864ed40..8605dda3a 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -88,7 +88,7 @@ let declare_tactic loc s c cl = match cl with add any grammar nor printing rule and add it as a true Ltac definition. *) let patt = make_patt rem in let vars = List.map make_var rem in - let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in + let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c102d8e11..3ed8733df 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1591,7 +1591,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let idl_tmp = Array.map (fun ((loc,id),bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in + let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in (List.rev rbl, intern_type env' ty,env')) dl in let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 407cec084..fd57b70ca 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -60,6 +60,9 @@ let rec cases_pattern_fold_names f a = function | CPatPrim _ | CPatAtom _ -> a | CPatCast _ -> assert false +let ids_of_pattern = + cases_pattern_fold_names Id.Set.add Id.Set.empty + let ids_of_pattern_list = List.fold_left (Loc.located_fold_left @@ -173,7 +176,8 @@ let split_at_annot bl na = (List.rev ans, LocalRawAssum (r, k, t) :: rest) end | LocalRawDef _ as x :: rest -> aux (x :: acc) rest - | LocalPattern _ :: rest -> assert false + | LocalPattern (loc,_,_) :: rest -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix") | [] -> user_err ~loc (str "No parameter named " ++ Nameops.pr_id id ++ str".") @@ -196,8 +200,9 @@ let map_local_binders f g e bl = (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl) | LocalRawDef((loc,na),ty) -> (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) - | LocalPattern _ -> - assert false in + | LocalPattern (loc,pat,t) -> + let ids = ids_of_pattern pat in + (Id.Set.fold g ids e, LocalPattern (loc,pat,Option.map (f e) t)::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) diff --git a/intf/misctypes.mli b/intf/misctypes.mli index e4f595ac4..33dc2a335 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -28,7 +28,7 @@ and 'constr intro_pattern_action_expr = | IntroWildcard | IntroOrAndPattern of 'constr or_and_intro_pattern_expr | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list - | IntroApplyOn of 'constr * (Loc.t * 'constr intro_pattern_expr) + | IntroApplyOn of (Loc.t * 'constr) * (Loc.t * 'constr intro_pattern_expr) | IntroRewrite of bool and 'constr or_and_intro_pattern_expr = | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index a37cf306e..fcc2b86a9 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -16,6 +16,7 @@ open Pcoq.Constr open Pltac open Hints open Tacexpr +open Names DECLARE PLUGIN "g_auto" @@ -149,15 +150,6 @@ TACTIC EXTEND autounfold_one [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ] END -TACTIC EXTEND autounfoldify -| [ "autounfoldify" constr(x) ] -> [ - let db = match Term.kind_of_term x with - | Term.Const (c,_) -> Names.Label.to_string (Names.con_label c) - | _ -> assert false - in Eauto.autounfold ["core";db] Locusops.onConcl - ] -END - TACTIC EXTEND unify | ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] | ["unify" constr(x) constr(y) "with" preident(base) ] -> [ diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index a28132a4b..ca9537c82 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -13,6 +13,7 @@ open Class_tactics open Pltac open Stdarg open Tacarg +open Names DECLARE PLUGIN "g_class" diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index 905653281..679aa1127 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -15,6 +15,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Eqdecide +open Names DECLARE PLUGIN "g_eqdecide" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 54229bb2a..aab568746 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -17,6 +17,7 @@ open Misctypes open Genarg open Genredexpr open Tok (* necessary for camlp4 *) +open Names open Pcoq open Pcoq.Constr @@ -226,8 +227,8 @@ GEXTEND Gram | "multimatch" -> General ] ] ; input_fun: - [ [ "_" -> None - | l = ident -> Some l ] ] + [ [ "_" -> Anonymous + | l = ident -> Name l ] ] ; let_clause: [ [ id = identref; ":="; te = tactic_expr -> @@ -499,8 +500,8 @@ let pr_tacdef_body tacdef_body = | Tacexpr.TacFun (idl,b) -> idl,b | _ -> [], body in id ++ - prlist (function None -> str " _" - | Some id -> spc () ++ Nameops.pr_id id) idl + prlist (function Anonymous -> str " _" + | Name id -> spc () ++ Nameops.pr_id id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ Pptactic.pr_raw_tactic body diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 685c07c9a..fa01baab7 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -325,8 +325,9 @@ GEXTEND Gram l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> let loc0,pat = pat in let f c pat = - let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in - IntroAction (IntroApplyOn (c,(loc,pat))) in + let loc1 = Constrexpr_ops.constr_loc c in + let loc = Loc.merge loc0 loc1 in + IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in !@loc, List.fold_right f l pat ] ] ; simple_intropattern_closed: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index fccee6e40..6f4ef37b4 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -574,9 +574,7 @@ module Make str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - let pr_funvar = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id + let pr_funvar n = spc () ++ pr_name n let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 2e2b55be7..75edf150e 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -504,10 +504,7 @@ let print_ltacs () = | Tacexpr.TacFun (l, t) -> (l, t) | _ -> ([], body) in - let pr_ltac_fun_arg = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id - in + let pr_ltac_fun_arg n = spc () ++ pr_name n in hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9c25a1645..e23992a80 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -282,7 +282,7 @@ constraint 'a = < > and 'a gen_tactic_fun_ast = - Id.t option list * 'a gen_tactic_expr + Name.t list * 'a gen_tactic_expr constraint 'a = < term:'t; diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 763e0dc22..3f83f104e 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -248,8 +248,8 @@ and intern_intro_pattern_action lf ist = function | IntroInjection l -> IntroInjection (List.map (intern_intro_pattern lf ist) l) | IntroWildcard | IntroRewrite _ as x -> x - | IntroApplyOn (c,pat) -> - IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat) + | IntroApplyOn ((loc,c),pat) -> + IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat) and intern_or_and_intro_pattern lf ist = function | IntroAndPattern l -> @@ -646,7 +646,7 @@ and intern_tactic_or_tacarg ist = intern_tactic false ist and intern_pure_tactic ist = intern_tactic true ist and intern_tactic_fun ist (var,body) = - let lfun = List.fold_left opt_cons ist.ltacvars var in + let lfun = List.fold_left name_cons ist.ltacvars var in (var,intern_tactic_or_tacarg { ist with ltacvars = lfun } body) and intern_tacarg strict onlytac ist = function @@ -722,9 +722,7 @@ let split_ltac_fun = function | TacFun (l,t) -> (l,t) | t -> ([],t) -let pr_ltac_fun_arg = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id +let pr_ltac_fun_arg n = spc () ++ pr_name n let print_ltac id = try @@ -782,6 +780,7 @@ let intern_ltac ist tac = let () = Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); Genintern.register_intern0 wit_ref (lift intern_global_reference); + Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; Genintern.register_intern0 wit_var (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 32bcdfb6a..61a70d712 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -120,7 +120,7 @@ let combine_appl appl1 appl2 = (* Values for interpretation *) type tacvalue = | VFun of appl*ltac_trace * value Id.Map.t * - Id.t option list * glob_tactic_expr + Name.t list * glob_tactic_expr | VRec of value Id.Map.t ref * glob_tactic_expr let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = @@ -520,7 +520,7 @@ let rec intropattern_ids (loc,pat) = match pat with List.flatten (List.map intropattern_ids (List.flatten ll)) | IntroAction (IntroInjection l) -> List.flatten (List.map intropattern_ids l) - | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat + | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat | IntroNaming (IntroAnonymous | IntroFresh _) | IntroAction (IntroWildcard | IntroRewrite _) | IntroForthcoming _ -> [] @@ -913,14 +913,14 @@ and interp_intro_pattern_action ist env sigma = function | IntroInjection l -> let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l - | IntroApplyOn (c,ipat) -> + | IntroApplyOn ((loc,c),ipat) -> let c = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_open_constr ist env sigma c in Sigma.Unsafe.of_pair (c, sigma) } in let sigma,ipat = interp_intro_pattern ist env sigma ipat in - sigma, IntroApplyOn (c,ipat) + sigma, IntroApplyOn ((loc,c),ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x and interp_or_and_intro_pattern ist env sigma = function @@ -1087,8 +1087,8 @@ let head_with_value (lvar,lval) = | ([],[]) -> (lacc,[],[]) | (vr::tvr,ve::tve) -> (match vr with - | None -> head_with_value_rec lacc (tvr,tve) - | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) + | Anonymous -> head_with_value_rec lacc (tvr,tve) + | Name v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve)) | (vr,[]) -> (lacc,vr,[]) | ([],ve) -> (lacc,[],ve) in @@ -2023,9 +2023,6 @@ let () = let () = declare_uniform wit_string -let () = - declare_uniform wit_pre_ident - let lift f = (); fun ist x -> Ftactic.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in @@ -2053,9 +2050,13 @@ let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (interp_destruction_arg ist gl c) end } +let interp_pre_ident ist env sigma s = + s |> Id.of_string |> interp_ident ist env sigma |> Id.to_string + let () = register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); register_interp0 wit_ref (lift interp_reference); + register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); register_interp0 wit_var (lift interp_hyp); register_interp0 wit_intro_pattern (lifts interp_intro_pattern); @@ -2119,8 +2120,8 @@ let lift_constr_tac_to_ml_tac vars tac = let env = Proofview.Goal.env gl in let sigma = project gl in let map = function - | None -> None - | Some id -> + | Anonymous -> None + | Name id -> let c = Id.Map.find id ist.lfun in try Some (coerce_to_closed_constr env c) with CannotCoerceTo ty -> diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 6f64981ef..adbd1d32b 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -115,7 +115,7 @@ val error_ltac_variable : Loc.t -> Id.t -> (** Transforms a constr-expecting tactic into a tactic finding its arguments in the Ltac environment according to the given names. *) -val lift_constr_tac_to_ml_tac : Id.t option list -> +val lift_constr_tac_to_ml_tac : Name.t list -> (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic val default_ist : unit -> Geninterp.interp_sign diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 55de58361..fe3a9f3b2 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -51,8 +51,8 @@ let rec subst_intro_pattern subst = function | loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x and subst_intro_pattern_action subst = function - | IntroApplyOn (t,pat) -> - IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat) + | IntroApplyOn ((loc,t),pat) -> + IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat) | IntroOrAndPattern l -> IntroOrAndPattern (subst_intro_or_and_pattern subst l) | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l) @@ -291,6 +291,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) = let () = Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; + Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); Genintern.register_subst0 wit_var (fun _ v -> v); Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 756958c2f..fb05fd7d0 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -259,7 +259,7 @@ let with_flags flags _ ist = let register_tauto_tactic tac name0 args = let ids = List.map (fun id -> Id.of_string id) args in - let ids = List.map (fun id -> Some id) ids in + let ids = List.map (fun id -> Name id) ids in let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in let entry = { mltac_name = name; mltac_index = 0 } in let () = Tacenv.register_ml_tactic name [| tac |] in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index e4b58a56f..97f29df82 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -383,7 +383,6 @@ struct let coq_and = lazy (init_constant "and") let coq_or = lazy (init_constant "or") let coq_not = lazy (init_constant "not") - let coq_not_gl_ref = (Nametab.locate ( Libnames.qualid_of_string "Coq.Init.Logic.not")) let coq_iff = lazy (init_constant "iff") let coq_True = lazy (init_constant "True") diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 195dec362..635237d33 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -9,6 +9,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin +open Names DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 59f23a637..eb35d3f80 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -123,7 +123,7 @@ let closed_term_ast l = mltac_index = 0; } in let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in - TacFun([Some(Id.of_string"t")], + TacFun([Name(Id.of_string"t")], TacML(Loc.ghost,tacname, [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])) @@ -206,7 +206,7 @@ let exec_tactic env evd n f args = let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in - let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in + let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in (** Evaluate the whole result *) let gl = dummy_goal env evd in let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in @@ -723,8 +723,8 @@ let ltac_ring_structure e = let pow_tac = tacarg e.ring_pow_tac in let lemma1 = carg e.ring_lemma1 in let lemma2 = carg e.ring_lemma2 in - let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in - let posttac = tacarg (TacFun([None],e.ring_post_tac)) in + let pretac = tacarg (TacFun([Anonymous],e.ring_pre_tac)) in + let posttac = tacarg (TacFun([Anonymous],e.ring_post_tac)) in [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] @@ -995,8 +995,8 @@ let ltac_field_structure e = let field_simpl_eq_ok = carg e.field_simpl_eq_ok in let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in let cond_ok = carg e.field_cond in - let pretac = tacarg (TacFun([None],e.field_pre_tac)) in - let posttac = tacarg (TacFun([None],e.field_post_tac)) in + let pretac = tacarg (TacFun([Anonymous],e.field_pre_tac)) in + let posttac = tacarg (TacFun([Anonymous],e.field_post_tac)) in [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; field_simpl_eq_in_ok;cond_ok;pretac;posttac] diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index f4f6efa4a..03c4ae47d 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1412,7 +1412,7 @@ let () = let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = - TacFun ([Some (Id.of_string "pattern")], + TacFun ([Name (Id.of_string "pattern")], TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in let obj () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 7b2c5695f..360843711 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -28,7 +28,7 @@ and pr_intro_pattern_action prc = function | IntroInjection pl -> str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ str "]" - | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c + | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c | IntroRewrite true -> str "->" | IntroRewrite false -> str "<-" diff --git a/printing/printer.ml b/printing/printer.ml index bfc2e1bc9..00c2b636b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -296,6 +296,9 @@ let pr_named_context_of env sigma = let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) +let pr_var_list_decl env sigma decl = + hov 0 (pr_compacted_decl env sigma decl) + let pr_named_context env sigma ne_context = hv 0 (Context.Named.fold_outside (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d) @@ -329,39 +332,43 @@ let pr_ne_context_of header env sigma = List.is_empty (Environ.named_context env) then (mt ()) else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ()) -let pr_context_limit n env sigma = - let named_context = Environ.named_context env in - let lgsign = List.length named_context in - if n >= lgsign then - pr_context_unlimited env sigma - else - let k = lgsign-n in - let _,sign_env = - Context.Compacted.fold - (fun d (i,pps) -> - if i < k then - (i+1, (pps ++str ".")) - else - let pidt = pr_compacted_decl env sigma d in - (i+1, (pps ++ fnl () ++ - str (emacs_str "") ++ - pidt))) - (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ())) - in - let db_env = - fold_rel_context - (fun env d pps -> - let pnat = pr_rel_decl env sigma d in - (pps ++ fnl () ++ - str (emacs_str "") ++ - pnat)) - env ~init:(mt ()) - in - (sign_env ++ db_env) +let rec bld_sign_env env sigma ctxt pps = + match ctxt with + | [] -> pps + | d:: ctxt' -> + let pidt = pr_var_list_decl env sigma d in + let pps' = pps ++ brk (0,0) ++ pidt in + bld_sign_env env sigma ctxt' pps' + + +let pr_context_limit_compact ?n env sigma = + let ctxt = Termops.compact_named_context (named_context env) in + let lgth = List.length ctxt in + let n_capped = + match n with + | None -> lgth + | Some n when n > lgth -> lgth + | Some n -> n in + let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in + (* a dot line hinting the number of hiden hyps. *) + let hidden_dots = String.make (List.length ctxt_hidden) '.' in + let sign_env = v 0 (str hidden_dots ++ (mt ()) + ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in + let db_env = + fold_rel_context + (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d) + env ~init:(mt ()) in + (sign_env ++ db_env) + +(* compact printing an env (variables and de Bruijn). Separator: three + spaces between simple hyps, and newline otherwise *) +let pr_context_unlimited_compact env sigma = + pr_context_limit_compact env sigma -let pr_context_of env sigma = match Flags.print_hyps_limit () with - | None -> hv 0 (pr_context_unlimited env sigma) - | Some n -> hv 0 (pr_context_limit n env sigma) +let pr_context_of env sigma = + match Flags.print_hyps_limit () with + | None -> hv 0 (pr_context_limit_compact env sigma) + | Some n -> hv 0 (pr_context_limit_compact ~n env sigma) (* display goal parts (Proof mode) *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 80bea0c3b..b06ea43bd 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -143,12 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) with - | Proof_global.NoCurrentProof -> CErrors.error "No focused proof" - | CList.IndexOutOfRange -> - match gi with - | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in - CErrors.user_err msg - | _ -> assert false + Proof_global.NoCurrentProof -> CErrors.error "No focused proof" let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6205bd109..84d09d833 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1815,24 +1815,37 @@ let find_matching_clause unifier clause = with NotExtensibleClause -> failwith "Cannot apply" in find clause +exception UnableToApply + let progress_with_clause flags innerclause clause = let ordered_metas = List.rev (clenv_independent clause) in - if List.is_empty ordered_metas then error "Statement without assumptions."; + if List.is_empty ordered_metas then raise UnableToApply; let f mv = try Some (find_matching_clause (clenv_fchain ~with_univs:false mv ~flags clause) innerclause) with Failure _ -> None in try List.find_map f ordered_metas - with Not_found -> error "Unable to unify." + with Not_found -> raise UnableToApply + +let explain_unable_to_apply_lemma loc env sigma thm innerclause = + user_err ~loc (hov 0 + (Pp.str "Unable to apply lemma of type" ++ brk(1,1) ++ + Pp.quote (Printer.pr_lconstr_env env sigma thm) ++ spc() ++ + str "on hypothesis of type" ++ brk(1,1) ++ + Pp.quote (Printer.pr_lconstr_env innerclause.env innerclause.evd (clenv_type innerclause)) ++ + str ".")) -let apply_in_once_main flags innerclause env sigma (d,lbind) = +let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in let rec aux clause = try progress_with_clause flags innerclause clause with e when CErrors.noncritical e -> - let e = CErrors.push e in + let e' = CErrors.push e in try aux (clenv_push_prod clause) - with NotExtensibleClause -> iraise e + with NotExtensibleClause -> + match e with + | UnableToApply -> explain_unable_to_apply_lemma loc env sigma thm innerclause + | _ -> iraise e' in aux (make_clenv_binding env sigma (d,thm) lbind) @@ -1852,7 +1865,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try - let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in + let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in clenv_refine_in ~sidecond_first with_evars targetid id sigma clause (fun id -> Tacticals.New.tclTHENLIST [ @@ -2467,7 +2480,7 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id = intro_decomp_eq loc l' thin tac id | IntroRewrite l2r -> rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None []) - | IntroApplyOn (f,(loc,pat)) -> + | IntroApplyOn ((loc',f),(loc,pat)) -> let naming,tac_ipat = prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in let doclear = @@ -2479,7 +2492,7 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id = let Sigma (c, sigma, p) = f.delayed env sigma in Sigma ((c, NoBindings), sigma, p) } in - apply_in_delayed_once false true true with_evars naming id (None,(loc,f)) + apply_in_delayed_once false true true with_evars naming id (None,(loc',f)) (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []]) and prepare_intros_loc loc with_evars dft destopt = function diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v new file mode 100644 index 000000000..b2f00ffc6 --- /dev/null +++ b/test-suite/bugs/closed/2417.v @@ -0,0 +1,15 @@ +Parameter x y : nat. +Axiom H : x = y. +Hint Rewrite H : mybase. + +Ltac bar base := autorewrite with base. + +Tactic Notation "foo" ident(base) := autorewrite with base. + +Goal x = 0. + bar mybase. + now_show (y = 0). + Undo 2. + foo mybase. + now_show (y = 0). +Abort. diff --git a/test-suite/bugs/closed/5346.v b/test-suite/bugs/closed/5346.v new file mode 100644 index 000000000..0118c1870 --- /dev/null +++ b/test-suite/bugs/closed/5346.v @@ -0,0 +1,29 @@ +Inductive comp : Type -> Type := +| Ret {T} : forall (v:T), comp T +| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T. + +Notation "'do' x .. y <- p1 ; p2" := + (Bind p1 (fun x => .. (fun y => p2) ..)) + (at level 60, right associativity, + x binder, y binder). + +Definition Fst1 A B (p: comp (A*B)) : comp A := + do '(a, b) <- p; + Ret a. + +Definition Fst2 A B (p: comp (A*B)) : comp A := + match tt with + | _ => Bind p (fun '(a, b) => Ret a) + end. + +Definition Fst3 A B (p: comp (A*B)) : comp A := + match tt with + | _ => do a <- p; + Ret (fst a) + end. + +Definition Fst A B (p: comp (A * B)) : comp A := + match tt with + | _ => do '(a, b) <- p; + Ret a + end. diff --git a/test-suite/success/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v new file mode 100644 index 000000000..f12b4d1f4 --- /dev/null +++ b/test-suite/success/hintdb_in_ltac.v @@ -0,0 +1,14 @@ +Definition x := 0. + +Hint Unfold x : mybase. + +Ltac autounfoldify base := autounfold with base. + +Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base. + +Goal x = 0. + progress autounfoldify mybase. + Undo. + progress autounfoldify_bis mybase. + trivial. +Qed. diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v new file mode 100644 index 000000000..f5c25540e --- /dev/null +++ b/test-suite/success/hintdb_in_ltac_bis.v @@ -0,0 +1,15 @@ +Parameter Foo : Prop. +Axiom H : Foo. + +Hint Resolve H : mybase. + +Ltac foo base := eauto with base. + +Tactic Notation "bar" ident(base) := + typeclasses eauto with base. + +Goal Foo. + progress foo mybase. + Undo. + progress bar mybase. +Qed.
\ No newline at end of file diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 58d3a2b38..5a3d5631d 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -24,7 +24,7 @@ Section Between. Lemma bet_eq : forall k l, l = k -> between k l. Proof. - induction 1; auto with arith. + intros * ->; auto with arith. Qed. Hint Resolve bet_eq: arith. @@ -37,9 +37,7 @@ Section Between. Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l. Proof. - intros k l H; induction H as [|l H]. - intros; absurd (S k <= k); auto with arith. - destruct H; auto with arith. + induction 1 as [|* [|]]; auto with arith. Qed. Hint Resolve between_Sk_l: arith. @@ -74,32 +72,32 @@ Section Between. Lemma in_int_intro : forall p q r, p <= r -> r < q -> in_int p q r. Proof. - red; auto with arith. + split; assumption. Qed. Hint Resolve in_int_intro: arith. Lemma in_int_lt : forall p q r, in_int p q r -> p < q. Proof. - induction 1; intros. - apply le_lt_trans with r; auto with arith. + intros * []. + eapply le_lt_trans; eassumption. Qed. Lemma in_int_p_Sq : - forall p q r, in_int p (S q) r -> in_int p q r \/ r = q :>nat. + forall p q r, in_int p (S q) r -> in_int p q r \/ r = q. Proof. - induction 1; intros. - elim (le_lt_or_eq r q); auto with arith. + intros p q r []. + destruct (le_lt_or_eq r q); auto with arith. Qed. Lemma in_int_S : forall p q r, in_int p q r -> in_int p (S q) r. Proof. - induction 1; auto with arith. + intros * []; auto with arith. Qed. Hint Resolve in_int_S: arith. Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r. Proof. - induction 1; auto with arith. + intros * []; auto with arith. Qed. Hint Immediate in_int_Sp_q: arith. @@ -107,10 +105,9 @@ Section Between. forall k l, between k l -> forall r, in_int k l r -> P r. Proof. induction 1; intros. - absurd (k < k); auto with arith. - apply in_int_lt with r; auto with arith. - elim (in_int_p_Sq k l r); intros; auto with arith. - rewrite H2; trivial with arith. + - absurd (k < k). { auto with arith. } + eapply in_int_lt; eassumption. + - destruct (in_int_p_Sq k l r) as [| ->]; auto with arith. Qed. Lemma in_int_between : @@ -120,17 +117,17 @@ Section Between. Qed. Lemma exists_in_int : - forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. + forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. Proof. - induction 1. - case IHexists_between; intros p inp Qp; exists p; auto with arith. - exists l; auto with arith. + induction 1 as [* ? (p, ?, ?)|]. + - exists p; auto with arith. + - exists l; auto with arith. Qed. Lemma in_int_exists : forall k l r, in_int k l r -> Q r -> exists_between k l. Proof. - destruct 1; intros. - elim H0; auto with arith. + intros * (?, lt_r_l) ?. + induction lt_r_l; auto with arith. Qed. Lemma between_or_exists : @@ -139,9 +136,11 @@ Section Between. (forall n:nat, in_int k l n -> P n \/ Q n) -> between k l \/ exists_between k l. Proof. - induction 1; intros; auto with arith. - elim IHle; intro; auto with arith. - elim (H0 m); auto with arith. + induction 1 as [|m ? IHle]. + - auto with arith. + - intros P_or_Q. + destruct IHle; auto with arith. + destruct (P_or_Q m); auto with arith. Qed. Lemma between_not_exists : @@ -150,14 +149,14 @@ Section Between. (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l. Proof. induction 1; red; intros. - absurd (k < k); auto with arith. - absurd (Q l); auto with arith. - elim (exists_in_int k (S l)); auto with arith; intros l' inl' Ql'. - replace l with l'; auto with arith. - elim inl'; intros. - elim (le_lt_or_eq l' l); auto with arith; intros. - absurd (exists_between k l); auto with arith. - apply in_int_exists with l'; auto with arith. + - absurd (k < k); auto with arith. + - absurd (Q l). { auto with arith. } + destruct (exists_in_int k (S l)) as (l',[],?). + + auto with arith. + + replace l with l'. { trivial. } + destruct (le_lt_or_eq l' l); auto with arith. + absurd (exists_between k l). { auto with arith. } + eapply in_int_exists; eauto with arith. Qed. Inductive P_nth (init:nat) : nat -> nat -> Prop := @@ -168,15 +167,16 @@ Section Between. Lemma nth_le : forall (init:nat) l (n:nat), P_nth init l n -> init <= l. Proof. - induction 1; intros; auto with arith. - apply le_trans with (S k); auto with arith. + induction 1. + - auto with arith. + - eapply le_trans; eauto with arith. Qed. Definition eventually (n:nat) := exists2 k : nat, k <= n & Q k. Lemma event_O : eventually 0 -> Q 0. Proof. - induction 1; intros. + intros (x, ?, ?). replace 0 with x; auto with arith. Qed. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index ddaf08bf7..11d80dbc3 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -262,6 +262,11 @@ Inductive comparison : Set := | Lt : comparison | Gt : comparison. +Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'. +Proof. + destruct c, c'; intro H; reflexivity || destruct H; discriminate. +Qed. + Definition CompOpp (r:comparison) := match r with | Eq => Eq @@ -326,7 +331,6 @@ Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, CompSpec eq lt x y c -> CompSpecT eq lt x y c. Proof. intros. apply CompareSpec2Type; assumption. Defined. - (******************************************************************) (** * Misc Other Datatypes *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 504ef95d9..9b58c524e 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -125,6 +125,25 @@ Proof. [apply Hl | apply Hr]; assumption. Qed. +Theorem imp_iff_compat_l : forall A B C : Prop, + (B <-> C) -> ((A -> B) <-> (A -> C)). +Proof. + intros ? ? ? [Hl Hr]; split; intros H ?; [apply Hl | apply Hr]; apply H; assumption. +Qed. + +Theorem imp_iff_compat_r : forall A B C : Prop, + (B <-> C) -> ((B -> A) <-> (C -> A)). +Proof. + intros ? ? ? [Hl Hr]; split; intros H ?; [apply H, Hr | apply H, Hl]; assumption. +Qed. + +Theorem not_iff_compat : forall A B : Prop, + (A <-> B) -> (~ A <-> ~B). +Proof. + intros; apply imp_iff_compat_r; assumption. +Qed. + + (** Some equivalences *) Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False). diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 9fc00e80c..2cc2ecbc2 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -103,7 +103,7 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P of an [a] of type [A], a of a proof [h] that [a] satisfies [P], and a proof [h'] that [a] satisfies [Q]. Then [(proj1_sig (sig_of_sig2 y))] is the witness [a], - [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and + [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and [(proj3_sig y)] is the proof of [(Q a)]. *) Section Subset_projections2. @@ -190,6 +190,23 @@ Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X). +(** η Principles *) +Definition sigT_eta {A P} (p : { a : A & P a }) + : p = existT _ (projT1 p) (projT2 p). +Proof. destruct p; reflexivity. Defined. + +Definition sig_eta {A P} (p : { a : A | P a }) + : p = exist _ (proj1_sig p) (proj2_sig p). +Proof. destruct p; reflexivity. Defined. + +Definition sigT2_eta {A P Q} (p : { a : A & P a & Q a }) + : p = existT2 _ _ (projT1 (sigT_of_sigT2 p)) (projT2 (sigT_of_sigT2 p)) (projT3 p). +Proof. destruct p; reflexivity. Defined. + +Definition sig2_eta {A P Q} (p : { a : A | P a & Q a }) + : p = exist2 _ _ (proj1_sig (sig_of_sig2 p)) (proj2_sig (sig_of_sig2 p)) (proj3_sig p). +Proof. destruct p; reflexivity. Defined. + (** [sumbool] is a boolean type equipped with the justification of their value *) @@ -263,10 +280,10 @@ Section Dependent_choice_lemmas. (forall x:X, {y | R x y}) -> forall x0, {f : nat -> X | f O = x0 /\ forall n, R (f n) (f (S n))}. Proof. - intros H x0. + intros H x0. set (f:=fix f n := match n with O => x0 | S n' => proj1_sig (H (f n')) end). exists f. - split. reflexivity. + split. reflexivity. induction n; simpl; apply proj2_sig. Defined. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 1420a000b..07e8b6ef8 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -22,7 +22,16 @@ description principles - AC! = functional relation reification (known as axiom of unique choice in topos theory, sometimes called principle of definite description in - the context of constructive type theory) + the context of constructive type theory, sometimes + called axiom of no choice) + +- AC_fun_repr = functional choice of a representative in an equivalence class +- AC_fun_setoid_gen = functional form of the general form of the (so-called + extensional) axiom of choice over setoids +- AC_fun_setoid = functional form of the (so-called extensional) axiom of + choice from setoids +- AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of + choice from setoids on locally compatible relations - GAC_rel = guarded relational form of the (non extensional) axiom of choice - GAC_fun = guarded functional form of the (non extensional) axiom of choice @@ -45,6 +54,11 @@ description principles independence of premises) - Drinker = drinker's paradox (small form) (called Ex in Bell [[Bell]]) +- EM = excluded-middle + +- Ext_pred_repr = choice of a representative among extensional predicates +- Ext_pred = extensionality of predicates +- Ext_fun_prop_repr = choice of a representative among extensional functions to Prop We let also @@ -76,6 +90,10 @@ Table of contents 8. Choice -> Dependent choice -> Countable choice +9.1. AC_fun_ext = AC_fun + Ext_fun_repr + EM + +9.2. AC_fun_ext = AC_fun + Ext_prop_fun_repr + PI + References: [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, @@ -84,8 +102,13 @@ unpublished. [[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic Type Theories, Mathematical Logic Quarterly, volume 39, 1993. +[[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to +AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + [[Carlström05]] Jesper Carlström, Interpreting descriptions in intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. + +[[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997. *) Set Implicit Arguments. @@ -108,8 +131,6 @@ Variables A B :Type. Variable P:A->Prop. -Variable R:A->B->Prop. - (** ** Constructive choice and description *) (** AC_rel *) @@ -121,6 +142,10 @@ Definition RelationalChoice_on := (** AC_fun *) +(* Note: This is called Type-Theoretic Description Axiom (TTDA) in + [[Werner97]] (using a non-standard meaning of "description"). This + is called intensional axiom of choice (AC_int) in [[Carlström04]] *) + Definition FunctionalChoice_on := forall R:A->B->Prop, (forall x : A, exists y : B, R x y) -> @@ -148,6 +173,55 @@ Definition FunctionalRelReification_on := (forall x : A, exists! y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)). +(** AC_fun_repr *) + +(* Note: This is called Type-Theoretic Choice Axiom (TTCA) in + [[Werner97]] (by reference to the extensional set-theoretic + formulation of choice); Note also a typo in its intended + formulation in [[Werner97]]. *) + +Require Import RelationClasses Logic. + +Definition RepresentativeFunctionalChoice_on := + forall R:A->A->Prop, + (Equivalence R) -> + (exists f : A->A, forall x : A, (R x (f x)) /\ forall x', R x x' -> f x = f x'). + +(** AC_fun_setoid *) + +Definition SetoidFunctionalChoice_on := + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). + +(** AC_fun_setoid_gen *) + +(* Note: This is called extensional axiom of choice (AC_ext) in + [[Carlström04]]. *) + +Definition GeneralizedSetoidFunctionalChoice_on := + forall R : A -> A -> Prop, + forall S : B -> B -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + Equivalence S -> + (forall x x' y y', R x x' -> S y y' -> T x y -> T x' y') -> + (forall x, exists y, T x y) -> + exists f : A -> B, + forall x : A, T x (f x) /\ (forall x' : A, R x x' -> S (f x) (f x')). + +(** AC_fun_setoid_simple *) + +Definition SimpleSetoidFunctionalChoice_on A B := + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x, exists y, forall x', R x x' -> T x' y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). + (** ID_epsilon (constructive version of indefinite description; combined with proof-irrelevance, it may be connected to Carlström's type theory with a constructive indefinite description @@ -234,6 +308,14 @@ Notation FunctionalChoiceOnInhabitedSet := (forall A B : Type, inhabited B -> FunctionalChoice_on A B). Notation FunctionalRelReification := (forall A B : Type, FunctionalRelReification_on A B). +Notation RepresentativeFunctionalChoice := + (forall A : Type, RepresentativeFunctionalChoice_on A). +Notation SetoidFunctionalChoice := + (forall A B: Type, SetoidFunctionalChoice_on A B). +Notation GeneralizedSetoidFunctionalChoice := + (forall A B : Type, GeneralizedSetoidFunctionalChoice_on A B). +Notation SimpleSetoidFunctionalChoice := + (forall A B : Type, SimpleSetoidFunctionalChoice_on A B). Notation GuardedRelationalChoice := (forall A B : Type, GuardedRelationalChoice_on A B). @@ -271,6 +353,26 @@ Definition SmallDrinker'sParadox := forall (A:Type) (P:A -> Prop), inhabited A -> exists x, (exists x, P x) -> P x. +Definition ExcludedMiddle := + forall P:Prop, P \/ ~ P. + +(** Extensional schemes *) + +Local Notation ExtensionalPropositionRepresentative := + (forall (A:Type), + exists h : Prop -> Prop, + forall P : Prop, (P <-> h P) /\ forall Q, (P <-> Q) -> h P = h Q). + +Local Notation ExtensionalPredicateRepresentative := + (forall (A:Type), + exists h : (A->Prop) -> (A->Prop), + forall (P : A -> Prop), (forall x, P x <-> h P x) /\ forall Q, (forall x, P x <-> Q x) -> h P = h Q). + +Local Notation ExtensionalFunctionRepresentative := + (forall (A B:Type), + exists h : (A->B) -> (A->B), + forall (f : A -> B), (forall x, f x = h f x) /\ forall g, (forall x, f x = g x) -> h f = h g). + (**********************************************************************) (** * AC_rel + AC! = AC_fun @@ -284,7 +386,7 @@ Definition SmallDrinker'sParadox := relational formulation) without known inconsistency with classical logic, though functional relation reification conflicts with classical logic *) -Lemma description_rel_choice_imp_funct_choice : +Lemma functional_rel_reification_and_rel_choice_imp_fun_choice : forall A B : Type, FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B. Proof. @@ -298,7 +400,10 @@ Proof. apply HR'R; assumption. Qed. -Lemma funct_choice_imp_rel_choice : +Notation description_rel_choice_imp_funct_choice := + functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). + +Lemma fun_choice_imp_rel_choice : forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B. Proof. intros A B FunCh R H. @@ -311,7 +416,9 @@ Proof. trivial. Qed. -Lemma funct_choice_imp_description : +Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). + +Lemma fun_choice_imp_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B. Proof. intros A B FunCh R H. @@ -324,17 +431,21 @@ Proof. exists f; exact H0. Qed. -Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr : +Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). + +Corollary fun_choice_iff_rel_choice_and_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. Proof. intros A B. split. intro H; split; - [ exact (funct_choice_imp_rel_choice H) - | exact (funct_choice_imp_description H) ]. - intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H). + [ exact (fun_choice_imp_rel_choice H) + | exact (fun_choice_imp_functional_rel_reification H) ]. + intros [H H0]; exact (functional_rel_reification_and_rel_choice_imp_fun_choice H0 H). Qed. +Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := + fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). (**********************************************************************) (** * Connection between the guarded, non guarded and omniscient choices *) @@ -862,3 +973,334 @@ Proof. rewrite Heq in HR. assumption. Qed. + +(**********************************************************************) +(** * About the axiom of choice over setoids *) + +Require Import ClassicalFacts PropExtensionalityFacts. + +(**********************************************************************) +(** ** Consequences of the choice of a representative in an equivalence class *) + +Theorem repr_fun_choice_imp_ext_prop_repr : + RepresentativeFunctionalChoice -> ExtensionalPropositionRepresentative. +Proof. + intros ReprFunChoice A. + pose (R P Q := P <-> Q). + assert (Hequiv:Equivalence R) by (split; firstorder). + apply (ReprFunChoice _ R Hequiv). +Qed. + +Theorem repr_fun_choice_imp_ext_pred_repr : + RepresentativeFunctionalChoice -> ExtensionalPredicateRepresentative. +Proof. + intros ReprFunChoice A. + pose (R P Q := forall x : A, P x <-> Q x). + assert (Hequiv:Equivalence R) by (split; firstorder). + apply (ReprFunChoice _ R Hequiv). +Qed. + +Theorem repr_fun_choice_imp_ext_function_repr : + RepresentativeFunctionalChoice -> ExtensionalFunctionRepresentative. +Proof. + intros ReprFunChoice A B. + pose (R (f g : A -> B) := forall x : A, f x = g x). + assert (Hequiv:Equivalence R). + { split; try easy. firstorder using eq_trans. } + apply (ReprFunChoice _ R Hequiv). +Qed. + +(** *** This is a variant of Diaconescu and Goodman-Myhill theorems *) + +Theorem repr_fun_choice_imp_excluded_middle : + RepresentativeFunctionalChoice -> ExcludedMiddle. +Proof. + intros ReprFunChoice. + apply representative_boolean_partition_imp_excluded_middle, ReprFunChoice. +Qed. + +Theorem repr_fun_choice_imp_relational_choice : + RepresentativeFunctionalChoice -> RelationalChoice. +Proof. + intros ReprFunChoice A B T Hexists. + pose (D := (A*B)%type). + pose (R (z z':D) := + let x := fst z in + let x' := fst z' in + let y := snd z in + let y' := snd z' in + x = x' /\ (T x y -> y = y' \/ T x y') /\ (T x y' -> y = y' \/ T x y)). + assert (Hequiv : Equivalence R). + { split. + - split. easy. firstorder. + - intros (x,y) (x',y') (H1,(H2,H2')). split. easy. simpl fst in *. simpl snd in *. + subst x'. split; intro H. + + destruct (H2' H); firstorder. + + destruct (H2 H); firstorder. + - intros (x,y) (x',y') (x'',y'') (H1,(H2,H2')) (H3,(H4,H4')). + simpl fst in *. simpl snd in *. subst x'' x'. split. easy. split; intro H. + + simpl fst in *. simpl snd in *. destruct (H2 H) as [<-|H0]. + * destruct (H4 H); firstorder. + * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. + + simpl fst in *. simpl snd in *. destruct (H4' H) as [<-|H0]. + * destruct (H2' H); firstorder. + * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. } + destruct (ReprFunChoice D R Hequiv) as (g,Hg). + set (T' x y := T x y /\ exists y', T x y' /\ g (x,y') = (x,y)). + exists T'. split. + - intros x y (H,_); easy. + - intro x. destruct (Hexists x) as (y,Hy). + exists (snd (g (x,y))). + destruct (Hg (x,y)) as ((Heq1,(H',H'')),Hgxyuniq); clear Hg. + destruct (H' Hy) as [Heq2|Hgy]; clear H'. + + split. split. + * rewrite <- Heq2. assumption. + * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1, Heq2. subst; easy. + * intros y' (Hy',(y'',(Hy'',Heq))). + rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy. + split; right; easy. + + split. split. + * assumption. + * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1. subst x'; easy. + * intros y' (Hy',(y'',(Hy'',Heq))). + rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy. + split; right; easy. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple *) + +Theorem gen_setoid_fun_choice_imp_setoid_fun_choice : + forall A B, GeneralizedSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B. +Proof. + intros A B GenSetoidFunChoice R T Hequiv Hcompat Hex. + apply GenSetoidFunChoice; try easy. + apply eq_equivalence. + intros * H <-. firstorder. +Qed. + +Theorem setoid_fun_choice_imp_gen_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> GeneralizedSetoidFunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice R S T HequivR HequivS Hcompat Hex. + destruct SetoidFunChoice with (R:=R) (T:=T) as (f,Hf); try easy. + { intros; apply (Hcompat x x' y y); try easy. } + exists f. intros x; specialize Hf with x as (Hf,Huniq). intuition. now erewrite Huniq. +Qed. + +Corollary setoid_fun_choice_iff_gen_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B <-> GeneralizedSetoidFunctionalChoice_on A B. +Proof. + split; auto using gen_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_gen_setoid_fun_choice. +Qed. + +Theorem setoid_fun_choice_imp_simple_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> SimpleSetoidFunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice R T Hequiv Hexists. + pose (T' x y := forall x', R x x' -> T x' y). + assert (Hcompat : forall (x x' : A) (y : B), R x x' -> T' x y -> T' x' y) by firstorder. + destruct (SetoidFunChoice R T' Hequiv Hcompat Hexists) as (f,Hf). + exists f. firstorder. +Qed. + +Theorem simple_setoid_fun_choice_imp_setoid_fun_choice : + forall A B, SimpleSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B. +Proof. + intros A B SimpleSetoidFunChoice R T Hequiv Hcompat Hexists. + destruct (SimpleSetoidFunChoice R T Hequiv) as (f,Hf); firstorder. +Qed. + +Corollary setoid_fun_choice_iff_simple_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B <-> SimpleSetoidFunctionalChoice_on A B. +Proof. + split; auto using simple_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_simple_setoid_fun_choice. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC! + AC_fun_repr *) + +Theorem setoid_fun_choice_imp_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> FunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice T Hexists. + destruct SetoidFunChoice with (R:=@eq A) (T:=T) as (f,Hf). + - apply eq_equivalence. + - now intros * ->. + - assumption. + - exists f. firstorder. +Qed. + +Corollary setoid_fun_choice_imp_functional_rel_reification : + forall A B, SetoidFunctionalChoice_on A B -> FunctionalRelReification_on A B. +Proof. + intros A B SetoidFunChoice. + apply fun_choice_imp_functional_rel_reification. + now apply setoid_fun_choice_imp_fun_choice. +Qed. + +Theorem setoid_fun_choice_imp_repr_fun_choice : + SetoidFunctionalChoice -> RepresentativeFunctionalChoice . +Proof. + intros SetoidFunChoice A R Hequiv. + apply SetoidFunChoice; firstorder. +Qed. + +Theorem functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice : + FunctionalRelReification -> RepresentativeFunctionalChoice -> SetoidFunctionalChoice. +Proof. + intros FunRelReify ReprFunChoice A B R T Hequiv Hcompat Hexists. + assert (FunChoice : FunctionalChoice). + { intros A' B'. apply functional_rel_reification_and_rel_choice_imp_fun_choice. + - apply FunRelReify. + - now apply repr_fun_choice_imp_relational_choice. } + destruct (FunChoice _ _ T Hexists) as (f,Hf). + destruct (ReprFunChoice A R Hequiv) as (g,Hg). + exists (fun a => f (g a)). + intro x. destruct (Hg x) as (Hgx,HRuniq). + split. + - eapply Hcompat. symmetry. apply Hgx. apply Hf. + - intros y Hxy. f_equal. auto. +Qed. + +Theorem functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice : + FunctionalRelReification /\ RepresentativeFunctionalChoice <-> SetoidFunctionalChoice. +Proof. + split; intros. + - now apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + - split. + + now intros A B; apply setoid_fun_choice_imp_functional_rel_reification. + + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(** Note: What characterization to give of +RepresentativeFunctionalChoice? A formulation of it as a functional +relation would certainly be equivalent to the formulation of +SetoidFunctionalChoice as a functional relation, but in their +functional forms, SetoidFunctionalChoice seems strictly stronger *) + +(**********************************************************************) +(** * AC_fun_setoid = AC_fun + Ext_fun_repr + EM *) + +Import EqNotations. + +(** ** This is the main theorem in [[Carlström04]] *) + +(** Note: all ingredients have a computational meaning when taken in + separation. However, to compute with the functional choice, + existential quantification has to be thought as a strong + existential, which is incompatible with the computational content of + excluded-middle *) + +Theorem fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice : + FunctionalChoice -> ExtensionalFunctionRepresentative -> ExcludedMiddle -> RepresentativeFunctionalChoice. +Proof. + intros FunChoice SetoidFunRepr EM A R (Hrefl,Hsym,Htrans). + assert (H:forall P:Prop, exists b, b = true <-> P). + { intros P. destruct (EM P). + - exists true; firstorder. + - exists false; easy. } + destruct (FunChoice _ _ _ H) as (c,Hc). + pose (class_of a y := c (R a y)). + pose (isclass f := exists x:A, f x = true). + pose (class := {f:A -> bool | isclass f}). + pose (contains (c:class) (a:A) := proj1_sig c a = true). + destruct (FunChoice class A contains) as (f,Hf). + - intros f. destruct (proj2_sig f) as (x,Hx). + exists x. easy. + - destruct (SetoidFunRepr A bool) as (h,Hh). + assert (Hisclass:forall a, isclass (h (class_of a))). + { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). + rewrite <- Ha. apply Hc. apply Hrefl. } + pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). + exists (fun a => f (f' a)). + intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + + specialize Hf with (f' x). unfold contains in Hf. simpl in Hf. rewrite <- Hx in Hf. apply Hc. assumption. + + intros y Hxy. + f_equal. + assert (Heq1: h (class_of x) = h (class_of y)). + { apply Huniqx. intro z. unfold class_of. + destruct (c (R x z)) eqn:Hxz. + - symmetry. apply Hc. apply -> Hc in Hxz. firstorder. + - destruct (c (R y z)) eqn:Hyz. + + apply -> Hc in Hyz. rewrite <- Hxz. apply Hc. firstorder. + + easy. } + assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). + { apply proof_irrelevance_cci, EM. } + unfold f'. + rewrite <- Heq2. + rewrite <- Heq1. + reflexivity. +Qed. + +Theorem setoid_functional_choice_first_characterization : + FunctionalChoice /\ ExtensionalFunctionRepresentative /\ ExcludedMiddle <-> SetoidFunctionalChoice. +Proof. + split. + - intros (FunChoice & SetoidFunRepr & EM). + apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + + intros A B. apply fun_choice_imp_functional_rel_reification, FunChoice. + + now apply fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice. + - intro SetoidFunChoice. repeat split. + + now intros A B; apply setoid_fun_choice_imp_fun_choice. + + apply repr_fun_choice_imp_ext_function_repr. + now apply setoid_fun_choice_imp_repr_fun_choice. + + apply repr_fun_choice_imp_excluded_middle. + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC_fun + Ext_pred_repr + PI *) + +(** Note: all ingredients have a computational meaning when taken in + separation. However, to compute with the functional choice, + existential quantification has to be thought as a strong + existential, which is incompatible with proof-irrelevance which + requires existential quantification to be truncated *) + +Theorem fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice : + FunctionalChoice -> ExtensionalPredicateRepresentative -> ProofIrrelevance -> RepresentativeFunctionalChoice. +Proof. + intros FunChoice PredExtRepr PI A R (Hrefl,Hsym,Htrans). + pose (isclass P := exists x:A, P x). + pose (class := {P:A -> Prop | isclass P}). + pose (contains (c:class) (a:A) := proj1_sig c a). + pose (class_of a := R a). + destruct (FunChoice class A contains) as (f,Hf). + - intros c. apply proj2_sig. + - destruct (PredExtRepr A) as (h,Hh). + assert (Hisclass:forall a, isclass (h (class_of a))). + { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). + rewrite <- Ha; apply Hrefl. } + pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). + exists (fun a => f (f' a)). + intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + + specialize Hf with (f' x). simpl in Hf. rewrite <- Hx in Hf. assumption. + + intros y Hxy. + f_equal. + assert (Heq1: h (class_of x) = h (class_of y)). + { apply Huniqx. intro z. unfold class_of. firstorder. } + assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). + { apply PI. } + unfold f'. + rewrite <- Heq2. + rewrite <- Heq1. + reflexivity. +Qed. + +Theorem setoid_functional_choice_second_characterization : + FunctionalChoice /\ ExtensionalPredicateRepresentative /\ ProofIrrelevance <-> SetoidFunctionalChoice. +Proof. + split. + - intros (FunChoice & ExtPredRepr & PI). + apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + + intros A B. now apply fun_choice_imp_functional_rel_reification. + + now apply fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice. + - intro SetoidFunChoice. repeat split. + + now intros A B; apply setoid_fun_choice_imp_fun_choice. + + apply repr_fun_choice_imp_ext_pred_repr. + now apply setoid_fun_choice_imp_repr_fun_choice. + + red. apply proof_irrelevance_cci. + apply repr_fun_choice_imp_excluded_middle. + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index afd64efdf..021408a37 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -34,8 +34,11 @@ Table of contents: 3 3. Independence of general premises and drinker's paradox -4. Classical logic and principle of unrestricted minimization +4. Principles equivalent to classical logic +4.1 Classical logic = principle of unrestricted minimization + +4.2 Classical logic = choice of representatives in a partition of bool *) (************************************************************************) @@ -94,12 +97,14 @@ Qed. (** A weakest form of propositional extensionality: extensionality for provable propositions only *) +Require Import PropExtensionalityFacts. + Definition provable_prop_extensionality := forall A:Prop, A -> A = True. Lemma provable_prop_ext : prop_extensionality -> provable_prop_extensionality. Proof. - intros Ext A Ha; apply Ext; split; trivial. + exact PropExt_imp_ProvPropExt. Qed. (************************************************************************) @@ -516,7 +521,7 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in {[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]] [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. @@ -661,6 +666,8 @@ Proof. exists x0; exact Hnot. Qed. +(** * Axioms equivalent to classical logic *) + (** ** Principle of unrestricted minimization *) Require Import Coq.Arith.PeanoNat. @@ -736,3 +743,56 @@ Section Example_of_undecidable_predicate_with_the_minimization_property. Qed. End Example_of_undecidable_predicate_with_the_minimization_property. + +(** ** Choice of representatives in a partition of bool *) + +(** This is similar to Bell's "weak extensional selection principle" in [[Bell]] + + [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished. +*) + +Require Import RelationClasses. + +Local Notation representative_boolean_partition := + (forall R:bool->bool->Prop, + Equivalence R -> exists f, forall x, R x (f x) /\ forall y, R x y -> f x = f y). + +Theorem representative_boolean_partition_imp_excluded_middle : + representative_boolean_partition -> excluded_middle. +Proof. + intros ReprFunChoice P. + pose (R (b1 b2 : bool) := b1 = b2 \/ P). + assert (Equivalence R). + { split. + - now left. + - destruct 1. now left. now right. + - destruct 1, 1; try now right. left; now transitivity y. } + destruct (ReprFunChoice R H) as (f,Hf). clear H. + destruct (Bool.bool_dec (f true) (f false)) as [Heq|Hneq]. + + left. + destruct (Hf false) as ([Hfalse|HP],_); try easy. + destruct (Hf true) as ([Htrue|HP],_); try easy. + congruence. + + right. intro HP. + destruct (Hf true) as (_,H). apply Hneq, H. now right. +Qed. + +Theorem excluded_middle_imp_representative_boolean_partition : + excluded_middle -> representative_boolean_partition. +Proof. + intros EM R H. + destruct (EM (R true false)). + - exists (fun _ => true). + intros []; firstorder. + - exists (fun b => b). + intro b. split. + + reflexivity. + + destruct b, y; intros HR; easy || now symmetry in HR. +Qed. + +Theorem excluded_middle_iff_representative_boolean_partition : + excluded_middle <-> representative_boolean_partition. +Proof. + split; auto using excluded_middle_imp_representative_boolean_partition, + representative_boolean_partition_imp_excluded_middle. +Qed. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 23af5afc6..896be7c33 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -8,9 +8,9 @@ (************************************************************************) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle - in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show + in topoi [[Diaconescu75]]. Lacas and Werner adapted the proof to show that the axiom of choice in equivalence classes entails - Excluded-Middle in Type Theory [LacasWerner99]. + Excluded-Middle in Type Theory [[LacasWerner99]]. Three variants of Diaconescu's result in type theory are shown below. @@ -23,22 +23,22 @@ Benjamin Werner) C. A proof that extensional Hilbert epsilon's description operator - entails excluded-middle (taken from Bell [Bell93]) + entails excluded-middle (taken from Bell [[Bell93]]) - See also [Carlström] for a discussion of the connection between the + See also [[Carlström04]] for a discussion of the connection between the Extensional Axiom of Choice and Excluded-Middle - [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation, + [[Diaconescu75]] Radu Diaconescu, Axiom of Choice and Complementation, in Proceedings of AMS, vol 51, pp 176-178, 1975. - [LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply + [[LacasWerner99]] Samuel Lacas, Benjamin Werner, Which Choices imply the excluded middle?, preprint, 1999. - [Bell93] John L. Bell, Hilbert's epsilon operator and classical + [[Bell93]] John L. Bell, Hilbert's epsilon operator and classical logic, Journal of Philosophical Logic, 22: 1-18, 1993 - [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext, - Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent + to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) (**********************************************************************) @@ -263,7 +263,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (**********************************************************************) (** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) -(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) +(** Proof sketch from Bell [[Bell93]] (with thanks to P. Castéran) *) Local Notation inhabited A := A (only parsing). diff --git a/theories/Logic/ExtensionalFunctionRepresentative.v b/theories/Logic/ExtensionalFunctionRepresentative.v new file mode 100644 index 000000000..a9da68e16 --- /dev/null +++ b/theories/Logic/ExtensionalFunctionRepresentative.v @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module states a limited form axiom of functional + extensionality which selects a canonical representative in each + class of extensional functions *) + +(** Its main interest is that it is the needed ingredient to provide + axiom of choice on setoids (a.k.a. axiom of extensional choice) + when combined with classical logic and axiom of (intensonal) + choice *) + +(** It provides extensionality of functions while still supporting (a + priori) an intensional interpretation of equality *) + +Axiom extensional_function_representative : + forall A B, exists repr, forall (f : A -> B), + (forall x, f x = repr f x) /\ + (forall g, (forall x, f x = g x) -> repr f = repr g). diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 56e03e965..a10c180cc 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -360,13 +360,12 @@ Module NoRetractToModalProposition. Section Paradox. Variable M : Prop -> Prop. -Hypothesis unit : forall A:Prop, A -> M A. -Hypothesis join : forall A:Prop, M (M A) -> M A. Hypothesis incr : forall A B:Prop, (A->B) -> M A -> M B. Lemma strength: forall A (P:A->Prop), M(forall x:A,P x) -> forall x:A,M(P x). Proof. - eauto. + intros A P h x. + eapply incr in h; eauto. Qed. (** ** The universe of modal propositions *) @@ -470,7 +469,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem paradox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => ~~P). + exact bool. + exact p2b. @@ -480,8 +479,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End Paradox. @@ -516,7 +513,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)). Theorem mparadox : forall B:NProp, El B. Proof. intros B. - unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))). + unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))). + exact (fun P => P). + exact bool. + exact p2b. @@ -526,8 +523,6 @@ Proof. + cbn. auto. + cbn. auto. + cbn. auto. - + auto. - + auto. Qed. End MParadox. diff --git a/theories/Logic/PropExtensionality.v b/theories/Logic/PropExtensionality.v new file mode 100644 index 000000000..796c60273 --- /dev/null +++ b/theories/Logic/PropExtensionality.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module states propositional extensionality and draws + consequences of it *) + +Axiom propositional_extensionality : + forall (P Q : Prop), (P <-> Q) -> P = Q. + +Require Import ClassicalFacts. + +Theorem proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. +Proof. + apply ext_prop_dep_proof_irrel_cic. + exact propositional_extensionality. +Qed. + diff --git a/theories/Logic/PropExtensionalityFacts.v b/theories/Logic/PropExtensionalityFacts.v new file mode 100644 index 000000000..7e455dfa1 --- /dev/null +++ b/theories/Logic/PropExtensionalityFacts.v @@ -0,0 +1,109 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Some facts and definitions about propositional and predicate extensionality + +We investigate the relations between the following extensionality principles + +- Proposition extensionality +- Predicate extensionality +- Propositional functional extensionality +- Provable-proposition extensionality +- Refutable-proposition extensionality +- Extensional proposition representatives +- Extensional predicate representatives +- Extensional propositional function representatives + +Table of contents + +1. Definitions + +2.1 Predicate extensionality <-> Proposition extensionality + Propositional functional extensionality + +2.2 Propositional extensionality -> Provable propositional extensionality + +2.3 Propositional extensionality -> Refutable propositional extensionality + +*) + +Set Implicit Arguments. + +(**********************************************************************) +(** * Definitions *) + +(** Propositional extensionality *) + +Local Notation PropositionalExtensionality := + (forall A B : Prop, (A <-> B) -> A = B). + +(** Provable-proposition extensionality *) + +Local Notation ProvablePropositionExtensionality := + (forall A:Prop, A -> A = True). + +(** Refutable-proposition extensionality *) + +Local Notation RefutablePropositionExtensionality := + (forall A:Prop, ~A -> A = False). + +(** Predicate extensionality *) + +Local Notation PredicateExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q). + +(** Propositional functional extensionality *) + +Local Notation PropositionalFunctionalExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q). + +(**********************************************************************) +(** * Propositional and predicate extensionality *) + +(**********************************************************************) +(** ** Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality *) + +Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality. +Proof. + intros Ext A B Equiv. + change A with ((fun _ => A) I). + now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B). +Qed. + +Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality. +Proof. + intros Ext A P Q Eq. apply Ext. intros x. now rewrite (Eq x). +Qed. + +Lemma PropExt_and_PropFunExt_imp_PredExt : + PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality. +Proof. + intros Ext FunExt A P Q Equiv. + apply FunExt. intros x. now apply Ext. +Qed. + +Theorem PropExt_and_PropFunExt_iff_PredExt : + PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality. +Proof. + firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality and provable proposition extensionality *) + +Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; trivial. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality and refutable proposition extensionality *) + +Lemma PropExt_imp_RefutPropExt : PropositionalExtensionality -> RefutablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; easy. +Qed. diff --git a/theories/Logic/SetoidChoice.v b/theories/Logic/SetoidChoice.v new file mode 100644 index 000000000..84432dda1 --- /dev/null +++ b/theories/Logic/SetoidChoice.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module states the functional form of the axiom of choice over + setoids, commonly called extensional axiom of choice [[Carlström04]], + [[Martin-Löf05]]. This is obtained by a decomposition of the axiom + into the following components: + + - classical logic + - relational axiom of choice + - axiom of unique choice + - a limited form of functional extensionality + + Among other results, it entails: + - proof irrelevance + - choice of a representative in equivalence classes + + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to + AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + + [[Martin-Löf05] Per Martin-Löf, 100 years of Zermelo’s axiom of + choice: what was the problem with it?, lecture notes for KTH/SU + colloquium, 2005. + +*) + +Require Export ClassicalChoice. (* classical logic, relational choice, unique choice *) +Require Export ExtensionalFunctionRepresentative. + +Require Import ChoiceFacts. +Require Import ClassicalFacts. +Require Import RelationClasses. + +Theorem setoid_choice : + forall A B, + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). +Proof. + apply setoid_functional_choice_first_characterization. split; [|split]. + - exact choice. + - exact extensional_function_representative. + - exact classic. +Qed. + +Theorem representative_choice : + forall A (R:A->A->Prop), (Equivalence R) -> + exists f : A->A, forall x : A, R x (f x) /\ forall x', R x x' -> f x = f x'. +Proof. + apply setoid_fun_choice_imp_repr_fun_choice. + exact setoid_choice. +Qed. diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget index 323597395..ef2709b47 100644 --- a/theories/Logic/vo.itarget +++ b/theories/Logic/vo.itarget @@ -20,11 +20,14 @@ WeakFan.vo WKL.vo FunctionalExtensionality.vo ExtensionalityFacts.vo +ExtensionalFunctionRepresentative.vo Hurkens.vo IndefiniteDescription.vo JMeq.vo ProofIrrelevanceFacts.vo ProofIrrelevance.vo +PropExtensionality.vo RelationalChoice.vo SetIsType.vo -FinFun.vo
\ No newline at end of file +SetoidChoice.vo +FinFun.vo diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 7baf102aa..d6385ee31 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -813,6 +813,34 @@ Proof. rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'. Qed. +Lemma compare_cont_Lt_not_Lt p q : + compare_cont Lt p q <> Lt <-> p > q. +Proof. + rewrite compare_cont_Lt_Lt. + unfold gt, le, compare. + now destruct compare_cont; split; try apply comparison_eq_stable. +Qed. + +Lemma compare_cont_Lt_not_Gt p q : + compare_cont Lt p q <> Gt <-> p <= q. +Proof. + apply not_iff_compat, compare_cont_Lt_Gt. +Qed. + +Lemma compare_cont_Gt_not_Lt p q : + compare_cont Gt p q <> Lt <-> p >= q. +Proof. + apply not_iff_compat, compare_cont_Gt_Lt. +Qed. + +Lemma compare_cont_Gt_not_Gt p q : + compare_cont Gt p q <> Gt <-> p < q. +Proof. + rewrite compare_cont_Gt_Gt. + unfold ge, lt, compare. + now destruct compare_cont; split; try apply comparison_eq_stable. +Qed. + (** We can express recursive equations for [compare] *) Lemma compare_xO_xO p q : (p~0 ?= q~0) = (p ?= q). diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 5aa397f8a..1e3ab6687 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1367,7 +1367,7 @@ Lemma inj_testbit a n : 0<=n -> Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). Proof. apply Z.testbit_Zpos. Qed. -(** Some results concerning Z.neg *) +(** Some results concerning Z.neg and Z.pos *) Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q. Proof. now injection 1. Qed. @@ -1375,18 +1375,54 @@ Proof. now injection 1. Qed. Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q. Proof. split. apply inj_neg. intros; now f_equal. Qed. +Lemma inj_pos p q : Z.pos p = Z.pos q -> p = q. +Proof. now injection 1. Qed. + +Lemma inj_pos_iff p q : Z.pos p = Z.pos q <-> p = q. +Proof. split. apply inj_pos. intros; now f_equal. Qed. + Lemma neg_is_neg p : Z.neg p < 0. Proof. reflexivity. Qed. Lemma neg_is_nonpos p : Z.neg p <= 0. Proof. easy. Qed. +Lemma pos_is_pos p : 0 < Z.pos p. +Proof. reflexivity. Qed. + +Lemma pos_is_nonneg p : 0 <= Z.pos p. +Proof. easy. Qed. + +Lemma neg_le_pos p q : Zneg p <= Zpos q. +Proof. easy. Qed. + +Lemma neg_lt_pos p q : Zneg p < Zpos q. +Proof. easy. Qed. + +Lemma neg_le_neg p q : (q <= p)%positive -> Zneg p <= Zneg q. +Proof. intros; unfold Z.le; simpl. now rewrite <- Pos.compare_antisym. Qed. + +Lemma neg_lt_neg p q : (q < p)%positive -> Zneg p < Zneg q. +Proof. intros; unfold Z.lt; simpl. now rewrite <- Pos.compare_antisym. Qed. + +Lemma pos_le_pos p q : (p <= q)%positive -> Zpos p <= Zpos q. +Proof. easy. Qed. + +Lemma pos_lt_pos p q : (p < q)%positive -> Zpos p < Zpos q. +Proof. easy. Qed. + Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p. Proof. reflexivity. Qed. Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1. Proof. reflexivity. Qed. +Lemma pos_xO p : Z.pos p~0 = 2 * Z.pos p. +Proof. reflexivity. Qed. + +Lemma pos_xI p : Z.pos p~1 = 2 * Z.pos p + 1. +Proof. reflexivity. Qed. + Lemma opp_neg p : - Z.neg p = Z.pos p. Proof. reflexivity. Qed. @@ -1402,6 +1438,9 @@ Proof. reflexivity. Qed. Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p. Proof. reflexivity. Qed. +Lemma add_pos_pos p q : Z.pos p + Z.pos q = Z.pos (p+q). +Proof. reflexivity. Qed. + Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p). Proof. apply Z.divide_Zpos_Zneg_r. Qed. @@ -1412,6 +1451,10 @@ Lemma testbit_neg a n : 0<=n -> Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)). Proof. apply Z.testbit_Zneg. Qed. +Lemma testbit_pos a n : 0<=n -> + Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). +Proof. apply Z.testbit_Zpos. Qed. + End Pos2Z. Module Z2Pos. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 73dee0cf2..18915216a 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -339,7 +339,7 @@ Notation Zle_0_1 := Z.le_0_1 (compat "8.3"). Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. Proof. - easy. + exact Pos2Z.neg_le_pos. Qed. Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0. @@ -350,12 +350,12 @@ Qed. (* weaker but useful (in [Z.pow] for instance) *) Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p. Proof. - easy. + exact Pos2Z.pos_is_nonneg. Qed. Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0. Proof. - easy. + exact Pos2Z.neg_is_neg. Qed. Lemma Zle_0_nat : forall n:nat, 0 <= Z.of_nat n. diff --git a/tools/gallina-db.el b/tools/gallina-db.el index baabebb13..9664f69f8 100644 --- a/tools/gallina-db.el +++ b/tools/gallina-db.el @@ -163,7 +163,7 @@ for DB structure." (defun coq-sort-menu-entries (menu) (sort menu - '(lambda (x y) (string< + (lambda (x y) (string< (downcase (elt x 0)) (downcase (elt y 0)))))) diff --git a/vernac/record.ml b/vernac/record.ml index d5faafaf8..b494430c2 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -110,7 +110,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = List.iter (function LocalRawDef (b, _) -> error default_binder_kind b | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls - | LocalPattern _ -> assert false) ps + | LocalPattern (loc,_,_) -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in let t', template = match t with diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8b7d65457..3afe04b37 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -517,9 +517,6 @@ let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted | Proved (_,_) as e -> save_proof ?proof e - (* A stupid macro that should be replaced by ``Exact c. Save.'' all along - the theories [??] *) - let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) |