diff --git a/Makefile b/Makefile index d0bb706..3fba40a 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,13 @@ -############################################################################### -## v # The Coq Proof Assistant ## -## /dev/null 2>/dev/null; echo $$?)) -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) else -ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else -STDTIME?=time +STDTIME?=command time endif endif else -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +STDTIME?=command time -f $(TIMEFMT) +endif + +ifneq (,$(COQBIN)) +# add an ending / +COQBIN:=$(COQBIN)/ endif # Coq binaries @@ -86,9 +91,10 @@ COQC ?= "$(COQBIN)coqc" COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" -GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" # Timing scripts COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" @@ -98,7 +104,7 @@ BEFORE ?= AFTER ?= # FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=camlp5.gramlib,unix,str +CAMLDONTLINK=str,unix,dynlink,threads,zarith # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c @@ -106,7 +112,7 @@ CAMLOPTC ?= "$(OCAMLFIND)" opt -c CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) CAMLDOC ?= "$(OCAMLFIND)" ocamldoc -CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack # DESTDIR is prepended to all installation paths DESTDIR ?= @@ -122,6 +128,14 @@ CAMLPKGS ?= TIMING?= # Option for changing sorting of timing output file TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= +# Option for including the memory column(s) +TIMING_INCLUDE_MEM?= +# Option for sorting by the memory column +TIMING_SORT_BY_MEM?= # Output file names for timed builds TIME_OF_BUILD_FILE ?= time-of-build.log TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log @@ -130,6 +144,23 @@ TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line +TGTS ?= + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +# Substitution of the path by appending $(DESTDIR) if needed. +# The variable $(COQMF_WINDRIVE) can be needed for Cygwin environments. +windrive_path = $(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(1)),$(1)) +destination_path = $(if $(DESTDIR),$(DESTDIR)/$(call windrive_path,$(1)),$(1)) + +# Installation paths of libraries and documentation. +COQLIBINSTALL ?= $(call destination_path,$(COQLIB)/user-contrib) +COQDOCINSTALL ?= $(call destination_path,$(DOCDIR)/user-contrib) +COQTOPINSTALL ?= $(call destination_path,$(COQLIB)/toploop) # FIXME: Unused variable? + ########## End of parameters ################################################## # What follows may be relevant to you only if you need to # extend this Makefile. If so, look for 'Extension point' here and @@ -148,7 +179,11 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line # Flags ####################################################################### # -# We define a bunch of variables combining the parameters +# We define a bunch of variables combining the parameters. +# To add additional flags to coq, coqchk or coqdoc, set the +# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. +# To overwrite the default choice and set your own flags entirely, set the +# {COQ,COQCHK,COQDOC}FLAGS variable. SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) @@ -168,33 +203,29 @@ DYNOBJ:=.cmxs DYNLIB:=.cmxs endif -COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) -COQCHKFLAGS?=-silent -o $(COQLIBS) -COQDOCFLAGS?=-interpolate -utf8 +# these variables are meant to be overridden if you want to add *extra* flags +COQEXTRAFLAGS?= +COQCHKEXTRAFLAGS?= +COQDOCEXTRAFLAGS?= + +# these flags do NOT contain the libraries, to make them easier to overwrite +COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS) +COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) +COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) + COQDOCLIBS?=$(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) -COQMAKEFILE_VERSION:=8.8.1 - -COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") +COQMAKEFILE_VERSION:=8.13.0 -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) # ocamldoc fails with unknown argument otherwise -CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) - -# FIXME This should be generated by Coq -GRAMMARS:=grammar.cma -CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo - -CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) -ifeq (,$(CAMLLIB)) -PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") -else -PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' -endif +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) ifneq (,$(TIMING)) TIMING_ARG=-time @@ -211,26 +242,15 @@ else TIMING_ARG= endif -# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) -ifdef DSTROOT -DESTDIR := $(DSTROOT) -endif - -concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) - -COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)user-contrib) -COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)user-contrib) -COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)toploop) - # Files ####################################################################### # # We here define a bunch of variables about the files being part of the # Coq project in order to ease the writing of build target and build rules -VDFILE := .coqdeps +VDFILE := .Makefile.d ALLSRCFILES := \ - $(ML4FILES) \ + $(MLGFILES) \ $(MLFILES) \ $(MLPACKFILES) \ $(MLLIBFILES) \ @@ -241,18 +261,23 @@ vo_to_obj = $(addsuffix .o,\ $(filter-out Warning: Error:,\ $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + VO = vo +VOS = vos VOFILES = $(VFILES:.v=.$(VO)) GLOBFILES = $(VFILES:.v=.glob) -GFILES = $(VFILES:.v=.g) HTMLFILES = $(VFILES:.v=.html) GHTMLFILES = $(VFILES:.v=.g.html) BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) TEXFILES = $(VFILES:.v=.tex) GTEXFILES = $(VFILES:.v=.g.tex) CMOFILES = \ - $(ML4FILES:.ml4=.cmo) \ + $(MLGFILES:.mlg=.cmo) \ $(MLFILES:.ml=.cmo) \ $(MLPACKFILES:.mlpack=.cmo) CMXFILES = $(CMOFILES:.cmo=.cmx) @@ -263,25 +288,25 @@ CMIFILES = \ $(CMOFILES:.cmo=.cmi) \ $(MLIFILES:.mli=.cmi) # the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just -# a .ml4 file +# a .mlg file CMXSFILES = \ $(MLPACKFILES:.mlpack=.cmxs) \ $(CMXAFILES:.cmxa=.cmxs) \ $(if $(MLPACKFILES)$(CMXAFILES),,\ - $(ML4FILES:.ml4=.cmxs) $(MLFILES:.ml=.cmxs)) + $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) # files that are packed into a plugin (no extension) PACKEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) # files that are archived into a .cma (mllib) LIBEDFILES = \ $(call strip_dotslash, \ $(foreach lib, \ - $(call strip_dotslash, \ - $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$($(lib)))) + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) OBJFILES = $(call vo_to_obj,$(VOFILES)) @@ -309,7 +334,7 @@ else DO_NATDYNLINK = endif -ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE)) +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) # Compilation targets ######################################################### @@ -325,6 +350,31 @@ all.timing.diff: $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all .PHONY: all.timing.diff +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + +ifeq (0,$(TIMING_INCLUDE_MEM)) +TIMING_INCLUDE_MEM_ARG := --no-include-mem +else +TIMING_INCLUDE_MEM_ARG := +endif + +ifeq (1,$(TIMING_SORT_BY_MEM)) +TIMING_SORT_BY_MEM_ARG := --sort-by-mem +else +TIMING_SORT_BY_MEM_ARG := +endif + make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: @@ -332,21 +382,21 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed print-pretty-timed:: - $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) print-pretty-timed-diff:: - $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) ifeq (,$(BEFORE)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else ifeq (,$(AFTER)) print-pretty-single-time-diff:: - @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing' + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' $(HIDE)false else print-pretty-single-time-diff:: - $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) endif endif pretty-timed: @@ -380,33 +430,44 @@ optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles # FIXME, see Ralf's bugreport -quick: $(VOFILES:.vo=.vio) +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") .PHONY: quick vio2vo: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +# quick2vo is undocumented quick2vo: - $(HIDE)make -j $(J) quick + $(HIDE)make -j $(J) vio $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ done); \ echo "VIO2VO: $$VIOFILES"; \ if [ -n "$$VIOFILES" ]; then \ - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ fi .PHONY: quick2vo checkproofs: - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) .PHONY: checkproofs +vos: $(VOFILES:%.vo=%.vos) +.PHONY: vos + +vok: $(VOFILES:%.vo=%.vok) +.PHONY: vok + validate: $(VOFILES) - $(TIMER) $(COQCHK) $(COQCHKFLAGS) $^ + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^ .PHONY: validate only: $(TGTS) @@ -431,19 +492,17 @@ all-mli.tex: $(MLIFILES:.mli=.cmi) $(HIDE)$(CAMLDOC) -latex \ -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) -gallina: $(GFILES) - all.ps: $(VFILES) $(SHOW)'COQDOC -ps $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` all.pdf: $(VFILES) $(SHOW)'COQDOC -pdf $(GAL)' $(HIDE)$(COQDOC) \ -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ - -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` + -o $@ `$(COQDEP) -sort $(VFILES)` # FIXME: not quite right, since the output name is different gallinahtml: GAL=-g @@ -468,6 +527,9 @@ beautify: $(BEAUTYFILES) # Extensions can't assume when they run. install: + $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code $(HIDE)for f in $(FILESTOINSTALL); do\ df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ if [ "$$?" != "0" -o -z "$$df" ]; then\ @@ -519,7 +581,7 @@ uninstall:: instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ rm -f "$$instf" &&\ echo RM "$$instf" &&\ - (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ + (rmdir "$(COQLIBINSTALL)/$$df/" 2>/dev/null || true); \ done .PHONY: uninstall @@ -548,12 +610,14 @@ clean:: $(HIDE)rm -f $(CMXSFILES) $(HIDE)rm -f $(CMOFILES:.cmo=.o) $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) $(HIDE)rm -f $(ALLDFILES) $(HIDE)rm -f $(NATIVEFILES) $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) - $(HIDE)rm -f $(GFILES) + $(HIDE)rm -f $(VOFILES:.vo=.vos) + $(HIDE)rm -f $(VOFILES:.vo=.vok) $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex $(HIDE)rm -f $(VFILES:.v=.glob) @@ -572,6 +636,7 @@ cleanall:: clean $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) + $(HIDE)rm -f .lia.cache .nia.cache .PHONY: cleanall archclean:: @@ -586,64 +651,62 @@ archclean:: $(MLIFILES:.mli=.cmi): %.cmi: %.mli $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< - -$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 - $(SHOW)'CAMLC -pp -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) -impl $< + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< -$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4 - $(SHOW)'CAMLOPT -pp -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(PP) $(FOR_PACK) -impl $< +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< -$(MLFILES:.ml=.cmo): %.cmo: %.ml +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml $(SHOW)'CAMLC -c $<' - $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< -$(MLFILES:.ml=.cmx): %.cmx: %.ml +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' - $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< + $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -linkall -shared -o $@ $< $(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -linkall -o $@ $< $(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx $(SHOW)'CAMLOPT -a -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack $(SHOW)'CAMLC -a -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' - $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack $(SHOW)'CAMLOPT -pack -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ # This rule is for _CoqProject with no .mllib nor .mlpack -$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ -shared -o $@ $< ifneq (,$(TIMING)) @@ -654,27 +717,31 @@ endif $(VOFILES): %.vo: %.v $(SHOW)COQC $< - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA) + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) # FIXME ?merge with .vo / .vio ? $(GLOBFILES): %.glob: %.v - $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -quick $< - $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $< + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vos): %.vos: %.v + $(SHOW)COQC -vos $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vok): %.vok: %.v + $(SHOW)COQC -vok $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing - $(SHOW)PYTHON TIMING-DIFF $< + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" $(BEAUTYFILES): %.v.beautified: %.v $(SHOW)'BEAUTIFY $<' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $< - -$(GFILES): %.g: %.v - $(SHOW)'GALLINA $<' - $(HIDE)$(GALLINA) $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< $(TEXFILES): %.tex: %.v $(SHOW)'COQDOC -latex $<' @@ -694,11 +761,11 @@ $(GHTMLFILES): %.g.html: %.v %.glob # Dependency files ############################################################ -ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) - -include $(ALLDFILES) -else - ifeq ($(MAKECMDGOALS),) +ifndef MAKECMDGOALS -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) endif endif @@ -706,34 +773,37 @@ endif redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) +GENMLFILES:=$(MLGFILES:.mlg=.ml) +$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) + $(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) -$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 - $(SHOW)'CAMLDEP -pp $<' - $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" $(redir_if_ok) +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml $(SHOW)'CAMLDEP $<' $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack - $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) # If this makefile is created using a _CoqProject we have coqdep get # options from it. This avoids argument length limits for pathological # projects. Note that extra options might be on the command line. VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) -$(VDFILE).d: $(VFILES) +$(VDFILE): _CoqProject $(VFILES) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) + $(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) # Misc ######################################################################## @@ -754,16 +824,13 @@ printenv:: @echo 'COQLIB = $(COQLIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP5O = $(CAMLP5O)' - @echo 'CAMLP5BIN = $(CAMLP5BIN)' - @echo 'CAMLP5LIB = $(CAMLP5LIB)' - @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' @echo 'OCAMLFIND = $(OCAMLFIND)' @echo 'PP = $(PP)' @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIB = $(COQLIBS)' @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' .PHONY: printenv @@ -797,3 +864,7 @@ debug: .PHONY: debug .DEFAULT_GOAL := all + +# Local Variables: +# mode: makefile-gmake +# End: diff --git a/README.md b/README.md index 889e09f..afa2ef1 100644 --- a/README.md +++ b/README.md @@ -3,10 +3,10 @@ Ohio University Verification Toolsuite # REQUIREMENTS -coq 8.9.0 -mathcomp algebra 1.7.0 -mathcomp fingroup 1.7.0 -mathcomp ssreflect 1.7.0 +coq 8.13.0 +mathcomp algebra 1.12.0 +mathcomp fingroup 1.12.0 +mathcomp ssreflect 1.12.0 # BUILD @@ -18,7 +18,7 @@ To build OUVerT, clone it and do: The latter command installs the OUVerT files in your local `.opam` directory. -To use OUVerT files in another development, simply import them with OUVerT.filename, as in: +To use OUVerT files in another development, simply import them with OUVerT.filename, as in: > Require Import OUVerT.dyadic. diff --git a/_CoqProject b/_CoqProject index 489868c..7d9bb2f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,4 +1,5 @@ -R . OUVerT +dist.v axioms.v compile.v dyadic.v @@ -6,7 +7,6 @@ learning.v numerics.v vector.v bigops.v -dist.v expfacts.v listlemmas.v orderedtypes.v diff --git a/axioms.v b/axioms.v index 7124a47..478c35a 100644 --- a/axioms.v +++ b/axioms.v @@ -11,23 +11,23 @@ Require Import QArith Reals Rpower Ranalysis Fourier Lra. Require Import dist. -(** The following lemmas (stated here as axioms) are well +(** The following lemmas (stated here as axioms) are well known but should nevertheless be proved. Until proved, any paper that uses/references results from OUVerT.axioms should state explicitly that the formal claims depend upon - the following assumptions: + the following assumptions: - NOTE: We should see whether the results from Affeldt et al's: - https://staff.aist.go.jp/reynald.affeldt/shannon/ + NOTE: We should see whether the results from Affeldt et al's: + https://staff.aist.go.jp/reynald.affeldt/shannon/ can be imported here to prove [pinsker] and related theorems in information theory. *) -Axiom pinsker_Bernoulli : - forall (p q:R) (p_ax:0= TV_Bernoulli p q. Axiom gibbs_Bernoulli : - forall (p q:R) (p_ax:0 R) : Proof. elim: cs=> /=; first by rewrite Ropp_0. by move=> a l IH; rewrite Ropp_plus_distr IH. -Qed. +Qed. Lemma big_sum_ext' T U (cs : seq T) (cs' : seq U) f f' : length cs = length cs' -> @@ -28,7 +28,7 @@ Lemma big_sum_ext' T U (cs : seq T) (cs' : seq U) f f' : (fun p => let: (c, c') := p in f c = f' c') - (zip cs cs')) -> + (zip cs cs')) -> big_sum cs f = big_sum cs' f'. Proof. move=> H H2; elim: cs cs' H H2; first by case. @@ -45,7 +45,7 @@ Lemma big_sum_scalar T (cs : seq T) r f : Proof. elim: cs=> /=; first by rewrite Rmult_0_r. by move=> a l IH; rewrite IH /=; rewrite Rmult_plus_distr_l. -Qed. +Qed. Lemma big_sum_plus T (cs : seq T) f g : (big_sum cs (fun c => f c + g c) = @@ -56,11 +56,11 @@ Proof. rewrite [((_ + big_sum l (fun c => f c) + _))%R]Rplus_assoc. rewrite [(big_sum l (fun c => f c) + (_ + _))%R]Rplus_comm. rewrite Rplus_assoc. - rewrite Rplus_assoc. + rewrite Rplus_assoc. f_equal. f_equal. by rewrite Rplus_comm. -Qed. +Qed. Lemma big_sum_cat T (cs1 cs2 : seq T) f : (big_sum (cs1++cs2) (fun c => f c) = @@ -76,7 +76,7 @@ Lemma big_sum_perm T (cs1 cs2 : seq T) (H : Permutation cs1 cs2) f : Proof. elim: H => //=. { move => x l l' H -> //. } - { by move => x y l; rewrite -Rplus_assoc [f y + f x]Rplus_comm Rplus_assoc. } + { by move => x y l; rewrite -Rplus_assoc [(f y + f x)%R]Rplus_comm Rplus_assoc. } move => l l' l'' H /= -> H2 -> //. Qed. @@ -88,8 +88,9 @@ Proof. { by constructor. } by apply: Permutation_cons_app. } by rewrite big_sum_cat. -Qed. +Qed. +#[local] Open Scope R_scope. Lemma big_sum_ge0 (T:eqType) (cs : seq T) f (H : forall x, x \in cs -> 0 <= f x) : 0 <= big_sum cs f. Proof. @@ -97,17 +98,17 @@ Proof. move => a l IH H2; rewrite -[0]Rplus_0_l; apply: Rplus_le_compat => //. by apply: H2 => /=; apply: mem_head. by apply: IH => // x H3; apply: H2; rewrite/=/in_mem/=; apply/orP; right. -Qed. +Qed. Lemma rat_to_R_sum T (cs : seq T) (f : T -> rat) : - rat_to_R (\sum_(c <- cs) (f c)) = + rat_to_R (\sum_(c <- cs) (f c)) = big_sum cs (fun c => (rat_to_R (f c)))%R. Proof. elim: cs=> //=; first by rewrite big_nil rat_to_R0. move=> a' l IH; rewrite big_cons. rewrite rat_to_R_plus IH. by f_equal; rewrite rat_to_R_plus rat_to_R_opp rat_to_R_mul. -Qed. +Qed. Lemma big_sum_constant T (cs : seq T) n : (big_sum cs (fun _ => n) = INR (size cs) * n)%R. @@ -128,7 +129,7 @@ Proof. elim: cs => //=. { by rewrite Rmult_0_r. } move => a l /=; rewrite Rmult_plus_distr_l => -> //. -Qed. +Qed. Lemma big_sum_mult_right T (cs : seq T) c f : big_sum cs f * c = big_sum cs (fun x => f x * c). @@ -136,7 +137,7 @@ Proof. elim: cs => //=. { by rewrite Rmult_0_l. } move => a l /=; rewrite Rmult_plus_distr_r => -> //. -Qed. +Qed. Fixpoint big_product (T : Type) (cs : seq T) (f : T -> R) : R := if cs is [:: c & cs'] then (f c * big_product cs' f)%R @@ -173,28 +174,28 @@ Proof. apply: Rmult_lt_0_compat. by apply: H; rewrite in_cons; apply/orP; left. by apply: IH=> c H3; apply: H; rewrite in_cons; apply/orP; right. -Qed. - +Qed. + Lemma ln_big_product_sum (T : eqType) (cs : seq T) (f : T -> R) : - (forall t : T, 0 < f t)%R -> + (forall t : T, 0 < f t)%R -> ln (big_product cs f) = big_sum cs (fun c => ln (f c)). Proof. elim: cs=> /=; first by rewrite ln_1. move=> a l IH H; rewrite ln_mult=> //; first by rewrite IH. by apply: big_product_gt0. -Qed. +Qed. Lemma big_product_exp_sum (T : eqType) (cs : seq T) (f : T -> R) : big_product cs (fun x => exp (f x)) = exp (big_sum cs f). Proof. elim: cs => //=; first by rewrite exp_0. by move => a l IH; rewrite IH exp_plus. -Qed. +Qed. Lemma big_product_le (T : eqType) (cs : seq T) (f : T -> R) g : (forall c, c \in cs -> 0 <= f c)%R -> (forall c, c \in cs -> 0 <= g c)%R -> - (forall c, c \in cs -> f c <= g c)%R -> + (forall c, c \in cs -> f c <= g c)%R -> (big_product cs f <= big_product cs g)%R. Proof. elim: cs=> //=. @@ -208,7 +209,7 @@ Proof. { by move=> c H; apply: H1; rewrite in_cons; apply/orP; right. } { by move=> c H; apply: H2; rewrite in_cons; apply/orP; right. } by move=> c H; apply: H3; rewrite in_cons; apply/orP; right. -Qed. +Qed. Lemma big_product_assoc (T: finType) (F G : T -> R) : big_product (enum T) (fun i : T => F i) * @@ -218,10 +219,10 @@ Proof. clear - F G; elim: (enum T) => //=. { by rewrite Rmult_1_r. } move => i l /= IH; symmetry; rewrite -IH; lra. -Qed. +Qed. Lemma big_sum_lt_aux (T : eqType) (cs : seq T) (f : T -> R) g : - (forall c, c \in cs -> f c < g c)%R -> + (forall c, c \in cs -> f c < g c)%R -> cs=[::] \/ (big_sum cs f < big_sum cs g)%R. Proof. elim: cs=> //=. @@ -236,7 +237,7 @@ Proof. Qed. Lemma big_sum_lt (T : eqType) (cs : seq T) (f : T -> R) g : - (forall c, c \in cs -> f c < g c)%R -> + (forall c, c \in cs -> f c < g c)%R -> cs<>[::] -> (big_sum cs f < big_sum cs g)%R. Proof. @@ -269,30 +270,30 @@ Proof. { by constructor. } by apply: Permutation_cons_app. } by rewrite big_product_cat. -Qed. +Qed. Lemma big_product0 (T : eqType) (cs : seq T) c : - c \in cs -> + c \in cs -> big_product cs (fun _ => 0) = 0. Proof. by elim: cs c => // a l IH c /= _; rewrite Rmult_0_l. Qed. Lemma rat_to_R_prod T (cs : seq T) (f : T -> rat) : - rat_to_R (\prod_(c <- cs) (f c)) = + rat_to_R (\prod_(c <- cs) (f c)) = big_product cs (fun c => (rat_to_R (f c)))%R. Proof. elim: cs=> //=; first by rewrite big_nil rat_to_R1. move=> a' l IH; rewrite big_cons. rewrite rat_to_R_mul IH. by f_equal; rewrite rat_to_R_plus rat_to_R_opp rat_to_R_mul. -Qed. +Qed. -Lemma big_sum_lift (T : Type) (ts : seq T) f g +Lemma big_sum_lift (T : Type) (ts : seq T) f g (g_zero : g 0 = 0) (g_plus : forall x y, g (x + y) = g x + g y) : big_sum ts (fun x => g (f x)) = g (big_sum ts (fun x => f x)). Proof. by elim: ts => //= a l ->. Qed. -Lemma big_product_lift (T : Type) (ts : seq T) f g +Lemma big_product_lift (T : Type) (ts : seq T) f g (g_zero : g 1 = 1) (g_mult : forall x y, g (x * y) = g x * g y) : big_product ts (fun x => g (f x)) = g (big_product ts (fun x => f x)). @@ -349,7 +350,7 @@ Section SSR_RBigops. rewrite BigOp.bigopE /index_enum enumT. by elim: (Finite.enum I) => //= a l; case Heq: (P a) => //= ->. Qed. - + Lemma big_product_prod : big_product (enum I) F = \big[Rtimes/1]_i F i. Proof. rewrite BigOp.bigopE /index_enum enumT. @@ -361,8 +362,8 @@ Section SSR_RBigops. rewrite BigOp.bigopE /index_enum enumT. by elim: (Finite.enum I) => //= a l; case Heq: (P a) => //= ->. Qed. -End SSR_RBigops. - +End SSR_RBigops. + (*ssreflect: bigA_distr_bigA*) Lemma big_product_distr_sum (I J : finType) (F : I -> J -> R) : big_product (enum I) (fun i => big_sum (enum J) (fun j => F i j)) = @@ -371,14 +372,14 @@ Lemma big_product_distr_sum (I J : finType) (F : I -> J -> R) : Proof. rewrite big_sum_sum big_product_prod. have ->: - \big[Rtimes/1]_i big_sum (enum J) [eta F i] + \big[Rtimes/1]_i big_sum (enum J) [eta F i] = \big[Rtimes/1]_i \big[Rplus/0]_j F i j. { by apply: eq_big => // i _; rewrite big_sum_sum. } by rewrite bigA_distr_bigA; apply: eq_big => // f _; rewrite big_product_prod. -Qed. +Qed. Lemma marginal_unfoldR N i (A : finType) (F : {ffun 'I_N -> A} -> R) : - let P t (p : {ffun 'I_N -> A}) := p i == t in + let P t (p : {ffun 'I_N -> A}) := p i == t in \big[Rplus/0]_(p : [finType of (A * {ffun 'I_N -> A})] | P p.1 p.2) (F p.2) = \big[Rplus/0]_(p : {ffun 'I_N -> A}) (F p). Proof. @@ -392,13 +393,13 @@ Proof. \big[Rplus/0]_i0 \big[Rplus/0]_(j : {ffun 'I_N -> A} | j i == i0) F j = \big[Rplus/0]_i0 \big[Rplus/0]_(j : {ffun 'I_N -> A} | predT j && (j i == i0)) F j. { by apply: eq_big. } - rewrite -partition_big //. -Qed. + rewrite -partition_big //. +Qed. Lemma prod_splitR N (i : 'I_N) (A : finType) (y : {ffun 'I_N -> A}) f : \big[Rtimes/1]_(j in [set i]) (f j) (y j) * \big[Rtimes/1]_(j in [set~ i]) (f j) (y j) = \big[Rtimes/1]_(j < N) (f j) (y j). -Proof. +Proof. have ->: \big[Rtimes/1]_(j < N) (f j) (y j) = \big[Rtimes/1]_(j in [predU (pred1 i) & [set~ i]]) (f j) (y j). @@ -417,7 +418,7 @@ Qed. Lemma sum_splitR N (i : 'I_N) (A : finType) (y : {ffun 'I_N -> A}) f : \big[Rplus/0]_(j in [set i]) (f j) (y j) + \big[Rplus/0]_(j in [set~ i]) (f j) (y j) = \big[Rplus/0]_(j < N) (f j) (y j). -Proof. +Proof. have ->: \big[Rplus/0]_(j < N) (f j) (y j) = \big[Rplus/0]_(j in [predU (pred1 i) & [set~ i]]) (f j) (y j). @@ -433,7 +434,7 @@ Proof. Qed. Lemma big_sum_le (T : eqType) (cs : seq T) (f : T -> R) g : - (forall c, c \in cs -> f c <= g c)%R -> + (forall c, c \in cs -> f c <= g c)%R -> (big_sum cs f <= big_sum cs g)%R. Proof. elim: cs=> //=. @@ -446,8 +447,8 @@ Qed. Lemma perm_eq_nil (T:eqType) (cs : seq T) : perm_eq [::] cs -> cs=[::]. Proof. move => H; apply: perm_eq_small => //. - by rewrite perm_eq_sym. -Qed. + by rewrite perm_sym. +Qed. Lemma In_mem (T:eqType) (a:T) (cs : seq T) : List.In a cs <-> a \in cs. Proof. @@ -456,7 +457,7 @@ Proof. by rewrite /in_mem/=; apply/orP; right; rewrite -(IH ax). } rewrite /in_mem/=; case/orP; first by move/eqP => <-; left. by move => H; right; rewrite IH. -Qed. +Qed. Lemma uniq_NoDup (T:eqType) (cs : seq T) : uniq cs -> List.NoDup cs. Proof. @@ -468,21 +469,21 @@ Qed. Lemma perm_eqi (T:eqType) (cs1 cs2 : seq T) : uniq cs1 -> - uniq cs2 -> + uniq cs2 -> cs1 =i cs2 -> Permutation cs1 cs2. Proof. move => U1 U2 H; apply: NoDup_Permutation. by apply: uniq_NoDup. - by apply: uniq_NoDup. + by apply: uniq_NoDup. move => x; split => H2. { by rewrite In_mem; rewrite -(H x); rewrite -In_mem. } by rewrite In_mem; rewrite (H x); rewrite -In_mem. Qed. - + Lemma perm_sub (T:eqType) (cs1 cs2 : seq T) : uniq cs1 -> - uniq cs2 -> - {subset cs1 <= cs2} -> + uniq cs2 -> + {subset cs1 <= cs2} -> Permutation cs1 [seq x <- cs2 | x \in cs1]. Proof. move => U1 U2 H. @@ -495,12 +496,12 @@ Proof. apply: perm_eqi; try apply: filter_uniq => //. by move => x; rewrite 2!mem_filter andbC. Qed. - + Lemma big_sum_le2 (T : eqType) (cs1 cs2 : seq T) (f : T -> R) : uniq cs1 -> - uniq cs2 -> - (forall c, c \in cs2 -> 0 <= f c)%R -> - (forall c, c \in cs1 -> c \in cs2)%R -> + uniq cs2 -> + (forall c, c \in cs2 -> 0 <= f c)%R -> + (forall c, c \in cs1 -> c \in cs2)%R -> (big_sum cs1 f <= big_sum cs2 f)%R. Proof. move => U1 U2 H1 H2. @@ -510,14 +511,14 @@ Proof. { by apply: perm_sub. } rewrite (big_sum_perm Hperm); apply: Rle_refl. } by apply: big_sum_ge0 => x; rewrite mem_filter; case/andP => _ H; apply: H1. -Qed. +Qed. Lemma big_sum_le3 (T : eqType) (cs1 cs2 : seq T) (f g : T -> R) : uniq cs1 -> - uniq cs2 -> - (forall c, c \in cs2 -> 0 <= g c)%R -> + uniq cs2 -> + (forall c, c \in cs2 -> 0 <= g c)%R -> (forall c, c \in cs1 -> c \in cs2)%R -> - (forall c, c \in cs1 -> f c <= g c)%R -> + (forall c, c \in cs1 -> f c <= g c)%R -> (big_sum cs1 f <= big_sum cs2 g)%R. Proof. move => U1 U2 H1 H2 H. @@ -525,11 +526,11 @@ Proof. rewrite -[big_sum cs1 _]Rplus_0_r; apply: Rplus_le_compat. { have Hperm: Permutation cs1 [seq x <- cs2 | [pred x in cs1] x]. { by apply: perm_sub. } - rewrite (big_sum_perm Hperm). - apply: big_sum_le => c /= Hin; apply: H. + rewrite (big_sum_perm Hperm). + apply: big_sum_le => c /= Hin; apply: H. rewrite mem_filter in Hin; case: (andP Hin) => Hx Hy //. } apply: big_sum_ge0 => x; rewrite mem_filter; case/andP => Hx Hy; apply: H1 => //. -Qed. +Qed. Lemma big_sum_pred (T:eqType) (cs:seq T) (f:T -> R) (p:pred T) : big_sum cs (fun t => if p t then f t else 0) = diff --git a/chernoff.v b/chernoff.v index ebf9155..0b1a7dc 100644 --- a/chernoff.v +++ b/chernoff.v @@ -11,12 +11,14 @@ Require Import QArith Reals Rpower Ranalysis Fourier Lra. Require Import bigops numerics expfacts dist axioms. +#[local] Open Scope R_scope. + Section relative_entropy_lemmas. Variables p eps : R. Variable p_range : 0 < p < 1. Variable eps_range : 0 < eps < 1 - p. - Lemma RE_Bernoulli_bounded_below : + Lemma RE_Bernoulli_bounded_below : RE_Bernoulli (p + eps) p >= 2 * eps^2. Proof. have p_eps_ax: 0 T -> R. Variable f_range : forall i x, 0 <= f i x <= 1. - Definition identically_distributed := forall i j : 'I_m, expValR d (f i) = expValR d (f j). + Definition identically_distributed := forall i j : 'I_m, expValR d (f i) = expValR d (f j). Variable f_identically_distributed : identically_distributed. - (* Mutual independence of the f's: - -The expected value of the product of a function of the f_i's is equal to + (* Mutual independence of the f's: + -The expected value of the product of a function of the f_i's is equal to the product of the expected value of the same function of the f_i's. -NOTE: this is a stronger assumption than pairwise independence. *) Definition mutual_independence := - forall g : R -> R, + forall g : R -> R, expValR (prodR d_prod) (fun p => big_product (enum 'I_m) (fun i => g (f i (p i)))) = big_product (enum 'I_m) (fun i => expValR d (fun x => g (f i x))). Definition mutual_independence' := @@ -81,7 +83,7 @@ Section chernoff_geq. Variable m_gt0 : (0 < m)%nat. Notation d_prod := (@d_prod T d m). - + Variable f : 'I_m -> T -> R. Variable f_range : forall i x, 0 <= f i x <= 1. Variable f_identically_distributed : @identically_distributed T d m f. @@ -90,18 +92,18 @@ Section chernoff_geq. rewrite /mutual_independence => g; rewrite /expValR /= big_product_distr_sum /=. rewrite /prodR /d_prod; apply: big_sum_ext => // p. by rewrite -big_product_assoc. - Qed. - + Qed. + Definition mR := INR m. Lemma mR_gt0 : (0 < mR)%R. Proof. by apply: lt_0_INR; apply/ltP. Qed. Lemma mR_neq0 : (mR <> 0)%R. Proof. by move: mR_gt0 => H H2; rewrite H2 in H; move: (Rlt_asym _ _ H). Qed. - + Definition i0 : 'I_m := Ordinal m_gt0. Definition p := expValR d (f i0). - Variable p_nontrivial : 0 < p < 1. (*required to construct lambda_min*) - + Variable p_nontrivial : 0 < p < 1. (*required to construct lambda_min*) + Lemma expVal_independence c : expValR (prodR d_prod) (fun p => big_product (enum 'I_m) (fun i => exp (c * f i (p i)))) = big_product (enum 'I_m) (fun i => expValR d (fun x => exp (c * f i x))). @@ -118,10 +120,10 @@ Section chernoff_geq. Variable eps : R. Variable eps_gt0 : 0 < eps. Variable eps_lt_1p : eps < 1 - p. - (*This above assumption, which is required to show that lambda_min > 0, - is strange in the sense that it limits the values epsilon we can choose + (*This above assumption, which is required to show that lambda_min > 0, + is strange in the sense that it limits the values epsilon we can choose to (0, 1-p).*) - + Definition q := p + eps. Lemma lt_p_q : p < q. @@ -135,14 +137,14 @@ Section chernoff_geq. Lemma lt_p_p2_eps : 0 < p - (p*(p + eps)). Proof. apply: Rlt_Rminus; rewrite Rmult_plus_distr_l. - apply: (@Rlt_le_trans _ (p*p + p*(1-p)) _). + apply: (@Rlt_le_trans _ (p * p + p*(1-p)) _). { apply: Rplus_lt_compat_l. apply Rmult_lt_compat_l => //. by case: p_nontrivial. } rewrite Rmult_plus_distr_l Rmult_1_r [p + _]Rplus_comm -Rplus_assoc. - rewrite -Ropp_mult_distr_r Rplus_opp_r Rplus_0_l; apply: Rle_refl. + rewrite -Ropp_mult_distr_r Rplus_opp_r Rplus_0_l; apply: Rle_refl. Qed. - + Lemma p_leq1 : p <= 1. Proof. rewrite /p/expValR -d_dist; apply: big_sum_le; last first. @@ -153,12 +155,12 @@ Section chernoff_geq. { by apply: Rle_refl. } by case: (f_range i0 c). Qed. - + Section LAMBDA. Variable lambda : R. Variable lambda_gt0 : 0 < lambda. - - Lemma expValR_linear_approx : + + Lemma expValR_linear_approx : exp (-lambda * mR * q) * big_product (enum 'I_m) (fun i => expValR d (fun x => exp (lambda * f i x))) <= @@ -207,21 +209,21 @@ Section chernoff_geq. rewrite /p/expValR/Rminus. move: f_identically_distributed; rewrite /identically_distributed. by move/(_ i i0); rewrite /expValR. - Qed. - - Lemma big_product_expValR_simpl_aux : + Qed. + + Lemma big_product_expValR_simpl_aux : big_product (enum 'I_m) (fun i => expValR d (fun x => 1 - f i x + f i x * exp lambda)) = big_product (enum 'I_m) (fun i => 1 - p + p * exp lambda). Proof. by apply: big_product_ext => // p; rewrite expValR_simpl. Qed. - + Lemma big_product_expValR_simpl : big_product (enum 'I_m) (fun i => expValR d (fun x => 1 - f i x + f i x * exp lambda)) = (1 - p + p * exp lambda) ^ m. - Proof. by rewrite big_product_expValR_simpl_aux big_product_constant size_enum_ord. Qed. + Proof. by rewrite big_product_expValR_simpl_aux big_product_constant size_enum_ord. Qed. Definition phi := ln (exp (-lambda*q) * (1 - p + p * exp lambda)). @@ -229,7 +231,7 @@ Section chernoff_geq. Proof. by move => p_neq1; move: p_leq1; case => H; try lra. Qed. - + Lemma one_minus_p_etc_gt0 : 0 < 1 - p + p * exp lambda. Proof. case: (Req_dec p 1). @@ -239,8 +241,8 @@ Section chernoff_geq. apply: Rmult_le_pos. { by apply: expValR_ge0 => x; case: (f_range i0 x). } left; apply: exp_pos. - Qed. - + Qed. + Lemma phi_simpl : exp (phi * mR) = exp (-lambda * mR * q) * (1 - p + p * exp lambda) ^ m. Proof. @@ -250,12 +252,12 @@ Section chernoff_geq. rewrite ln_exp Rmult_plus_distr_r exp_plus; f_equal. { by rewrite Rmult_assoc [q * mR]Rmult_comm Rmult_assoc. } rewrite exp_mult exp_ln => //. - apply: one_minus_p_etc_gt0. + apply: one_minus_p_etc_gt0. Qed. (** The probability that phat is greater than or equal to q: *) Definition phat_ge_q : R := conv (fun _ => d) f q. - + Lemma probOfR_phat_q : phat_ge_q <= exp (-lambda * mR * q) * @@ -292,8 +294,8 @@ Section chernoff_geq. rewrite big_sum_mult_left -big_product_exp_sum; apply: Rle_refl. Qed. - Lemma probOfR_phat_q_bound : - phat_ge_q <= + Lemma probOfR_phat_q_bound : + phat_ge_q <= exp (-lambda * mR * q) * big_product (enum 'I_m) (fun i => expValR d (fun x => 1 - f i x + f i x * exp lambda)). @@ -301,13 +303,13 @@ Section chernoff_geq. apply: Rle_trans; first by apply: probOfR_phat_q. apply: expValR_linear_approx. Qed. - + Lemma chernoff0 : phat_ge_q <= exp (phi * mR). Proof. apply: Rle_trans; first by apply: probOfR_phat_q_bound. rewrite big_product_expValR_simpl phi_simpl; f_equal; apply: Rle_refl. Qed. - End LAMBDA. + End LAMBDA. Lemma chernoff0_lambda_ge0 (lambda:R) (lambda_ge0 : 0 <= lambda) : phat_ge_q <= exp (phi lambda * mR). @@ -319,8 +321,8 @@ Section chernoff_geq. rewrite exp_0 /phat_ge_q /conv; apply: Rle_trans. { apply: probOfR_le_1; [by apply: prodR_dist|by apply: prodR_nonneg]. } by rewrite pow1 Rmult_1_r; apply: Rle_refl. - Qed. - + Qed. + Definition lambda_min := ln ((q * (1 - p)) / ((1 - q) * p)). Lemma lambda_min_gt0 : 0 < lambda_min. @@ -328,7 +330,7 @@ Section chernoff_geq. apply: exp_lt_inv; rewrite exp_0 /lambda_min. have Hlt: 1 < q * (1 - p) / ((1 - q) * p). { rewrite Rmult_minus_distr_l Rmult_1_r. - rewrite [(1-q)*p]Rmult_comm Rmult_minus_distr_l Rmult_1_r. + rewrite [(1-q) * p]Rmult_comm Rmult_minus_distr_l Rmult_1_r. rewrite Rmult_comm /q; move: lt_p_p2_eps; move: (p*(p+eps)) => r H. apply: (Rmult_lt_reg_r (p-r)) => //. rewrite Rmult_1_l Rmult_assoc Rinv_l; last first. @@ -337,8 +339,8 @@ Section chernoff_geq. rewrite exp_ln => //. apply: Rlt_trans; last by apply: Hlt. lra. - Qed. - + Qed. + Lemma phi_lambda_min : phi lambda_min = -(RE_Bernoulli (p + eps) p). Proof. @@ -347,7 +349,7 @@ Section chernoff_geq. { have H: 0 < 1 - p by lra. apply: Rlt_le_trans; first by apply: H. rewrite -{1}[1-p]Rplus_0_r; apply: Rplus_le_compat_l. - case: p_nontrivial => H1 H2; apply: Rmult_le_pos; [lra|]. + case: p_nontrivial => H1 H2; apply: Rmult_le_pos; [lra|]. by apply: Rlt_le; apply: exp_pos. } simpl; rewrite ln_mult; [|by apply: exp_pos|] => //. case: p_nontrivial => X1 X2. @@ -394,7 +396,7 @@ Section chernoff_geq. { rewrite -Rdiv_plus_distr. have ->: (1 - q) * (1 - p) + q * (1 - p) = 1 - p. { have ->: (1 - q) * (1 - p) = 1 - p - q + p * q by lra. - rewrite Rmult_minus_distr_l Rmult_1_r [q*p]Rmult_comm /Rminus. + rewrite Rmult_minus_distr_l Rmult_1_r [q * p]Rmult_comm /Rminus. rewrite [_ + p*q]Rplus_comm -Rplus_assoc Rplus_comm. rewrite [p * q + _ + q]Rplus_assoc -[-_ + _]Rplus_assoc Rplus_opp_l Rplus_0_l. rewrite Rplus_assoc Rplus_opp_l Rplus_0_r //. } @@ -418,7 +420,7 @@ Section chernoff_geq. apply: Rinv_0_lt_compat; lra. } have X3: p * (1 - q) / (q * (1 - p)) = (p / q) * ((1 - q) / (1 - p)). { rewrite /Rdiv [p * (1 - q) * _]Rmult_assoc [(1 - q) * _]Rmult_comm -Rmult_assoc. - rewrite Rinv_mult_distr // -Rmult_assoc; lra. } + rewrite Rinv_mult_distr // -Rmult_assoc; lra. } have ->: ln (p * (1 - q) / (q * (1 - p))) = ln (p / q) + ln ((1 - q) / (1 - p)). { rewrite X3 ln_mult //. } have ->: p * (1 - q) / (q * (1 - p)) * ((1 - p) / (1 - q)) = p / q. @@ -445,7 +447,7 @@ Section chernoff_geq. Proof. rewrite -phi_lambda_min; apply: chernoff0. by apply: lambda_min_gt0. - Qed. + Qed. Lemma chernoff_geq : phat_ge_q <= exp (-2%R * eps^2 * mR). Proof. @@ -476,7 +478,7 @@ Section chernoff_leq. Variable m_gt0 : (0 < m)%nat. Notation d_prod := (@d_prod T d m). - + Variable f : 'I_m -> T -> R. Variable f_range : forall i x, 0 <= f i x <= 1. Variable f_identically_distributed : identically_distributed d f. @@ -495,19 +497,19 @@ Section chernoff_leq. Variable eps : R. Variable eps_gt0 : 0 < eps. Variable eps_lt_1p : eps < 1 - p d m_gt0 f_neg. - Variable p_nontrivial : 0 < p d m_gt0 f < 1. - + Variable p_nontrivial : 0 < p d m_gt0 f < 1. + Definition p_neg := p d m_gt0 f_neg. Lemma p_neg_one_minus_p : p_neg = 1 - p d m_gt0 f. Proof. rewrite /p_neg /p /f_neg; rewrite expValR_linear expValR_Ropp /Rminus; f_equal. apply: expValR_one => //. - Qed. - + Qed. + Lemma p_neg_nontrivial : 0 < p_neg < 1. Proof. rewrite p_neg_one_minus_p; case: p_nontrivial => H1 H2; split; lra. Qed. - + Lemma chernoff_leq : phat_ge_q d m_gt0 f_neg eps <= exp (-2%R * eps^2 * mR m). Proof. apply: chernoff_geq => //. @@ -526,18 +528,18 @@ Section chernoff_onesided. Variable m_gt0 : (0 < m)%nat. Notation d_prod := (@d_prod T d m). - + Variable f : 'I_m -> T -> R. Variable f_range : forall i x, 0 <= f i x <= 1. Variable f_identically_distributed : identically_distributed d f. Variable eps : R. Variable eps_gt0 : 0 < eps. - (*NOTE: the following assumptions are required to prove \lambda_min > 0*) + (*NOTE: the following assumptions are required to prove \lambda_min > 0*) Variable eps_lt_1p : eps < 1 - p d m_gt0 f. Variable p_nontrivial : 0 < p d m_gt0 f < 1. - (*END: the following assumptions*) - + (*END: the following assumptions*) + Lemma chernoff_aux1 : phat_ge_q d m_gt0 f eps <= exp (-2%R * eps^2 * mR m). Proof. @@ -547,14 +549,14 @@ Section chernoff_onesided. Definition p_hat x := / (mR m) * big_sum (enum 'I_m) (fun i => f i (x i)). Definition p_exp := p d m_gt0 f. - + Lemma chernoff : probOfR (prodR (fun _ => d)) (fun x => Rle_lt_dec (p_exp + eps) (p_hat x)) <= exp (-2%R * eps^2 * mR m). Proof. apply: Rle_trans; last by apply: chernoff_aux1. apply: Rle_refl. - Qed. + Qed. End chernoff_onesided. Section chernoff_twosided. @@ -566,7 +568,7 @@ Section chernoff_twosided. Variable m_gt0 : (0 < m)%nat. Notation d_prod := (@d_prod T d m). - + Variable f : 'I_m -> T -> R. Variable f_range : forall i x, 0 <= f i x <= 1. Variable f_identically_distributed : identically_distributed d f. @@ -575,10 +577,10 @@ Section chernoff_twosided. Variable eps_gt0 : 0 < eps. Variable delt_gt0 : 0 < delt. (*NOTE: the following assumptions are required to prove \lambda_min > 0*) - Variable eps_lt_p : eps < p d m_gt0 f. + Variable eps_lt_p : eps < p d m_gt0 f. Variable delt_lt_1p : delt < 1 - p d m_gt0 f. Variable p_nontrivial : 0 < p d m_gt0 f < 1. - (*END: the following assumptions*) + (*END: the following assumptions*) Definition min_eps_delt := Rmin eps delt. @@ -592,10 +594,10 @@ Section chernoff_twosided. Proof. rewrite /min_eps_delt /Rmin; case: (Rle_dec _ _) => //. move/Rnot_le_gt => H1 H2; lra. - Qed. - + Qed. + Lemma Rle_exp_delt_min : exp (- (2) * delt ^ 2 * mR m) <= exp (- (2) * min_eps_delt ^ 2 * mR m). - Proof. + Proof. rewrite !Ropp_mult_distr_l_reverse 2!exp_Ropp; apply: Rinv_le_contravar. { apply: exp_pos. } case: (Req_dec (exp (2 * min_eps_delt ^ 2 * mR m)) (exp (2 * delt ^ 2 * mR m))). @@ -604,13 +606,13 @@ Section chernoff_twosided. apply: Rmult_lt_compat_l; first by lra. rewrite -!tech_pow_Rmult /= 2!Rmult_1_r; apply: Rmult_le_0_lt_compat. { apply: Rle_0_min_eps_delt. } - { apply: Rle_0_min_eps_delt. } + { apply: Rle_0_min_eps_delt. } { by apply: Rlt_min_eps_delt_delt => Heq; rewrite Heq in Hneq; apply: Hneq. } by apply: Rlt_min_eps_delt_delt => Heq; rewrite Heq in Hneq; apply: Hneq. - Qed. + Qed. Lemma Rle_exp_eps_min : exp (- (2) * eps ^ 2 * mR m) <= exp (- (2) * min_eps_delt ^ 2 * mR m). - Proof. + Proof. rewrite !Ropp_mult_distr_l_reverse 2!exp_Ropp; apply: Rinv_le_contravar. { apply: exp_pos. } case: (Req_dec (exp (2 * min_eps_delt ^ 2 * mR m)) (exp (2 * eps ^ 2 * mR m))). @@ -619,11 +621,11 @@ Section chernoff_twosided. apply: Rmult_lt_compat_l; first by lra. rewrite -!tech_pow_Rmult /= 2!Rmult_1_r; apply: Rmult_le_0_lt_compat. { apply: Rle_0_min_eps_delt. } - { apply: Rle_0_min_eps_delt. } + { apply: Rle_0_min_eps_delt. } { by apply: Rlt_min_eps_delt_eps => Heq; rewrite Heq in Hneq; apply: Hneq. } by apply: Rlt_min_eps_delt_eps => Heq; rewrite Heq in Hneq; apply: Hneq. - Qed. - + Qed. + Lemma chernoff_twosided_aux1 : phat_ge_q d m_gt0 f delt + phat_ge_q d m_gt0 (f_neg f) eps <= 2 * exp (-2%R * min_eps_delt^2 * mR m). @@ -652,7 +654,7 @@ Section chernoff_twosided. Notation p_exp := (p_exp d m_gt0 f). Notation p_hat := (p_hat f). - + Lemma chernoff_twosided (Heq : eps = delt) : probOfR (prodR (fun _ => d)) (fun x => Rle_lt_dec eps (Rabs (p_exp - p_hat x))) <= 2 * exp (-2%R * eps^2 * mR m). @@ -686,11 +688,11 @@ Section chernoff_twosided. case: (Rle_lt_dec p_exp (p_hat x)); last first => Hle2. { (*Case 1: p_hat < p*) have Hle3: eps <= p_exp - p_hat x. - { move: Hle; rewrite Rabs_minus_sym /Rabs; case: (Rcase_abs _) => //= Hx Hy. lra. + { move: Hle; rewrite Rabs_minus_sym /Rabs; case: (Rcase_abs _) => //= Hx Hy. lra. apply Rplus_ge_compat_r with p_exp _ _ in Hx. rewrite Rplus_0_l in Hx. rewrite Rplus_assoc in Hx. rewrite Rplus_opp_l in Hx. rewrite Rplus_0_r in Hx. - exfalso. + exfalso. eapply Rlt_not_ge . apply Hle2. apply Hx. } have Hle4: p_hat x + eps <= p_exp by lra. @@ -712,7 +714,7 @@ Section chernoff_twosided. rewrite Rmult_1_r Rmult_plus_distr_l Rinv_l; last first. { move => Heq; move: (mR_gt0 m_gt0); rewrite /mR Heq => Hlt; lra. } rewrite -Ropp_mult_distr_r; apply: Rle_refl. } - have H10: eps > p_exp - p_hat x. + have H10: eps > p_exp - p_hat x. { clear - H8 H9; move: H8 H9; rewrite /p_exp; move: (p _ _) => p_exp => H1 H2. lra. } lra. } @@ -722,7 +724,7 @@ Section chernoff_twosided. apply Rplus_gt_compat_r with p_exp _ _ in Hx. rewrite Rplus_0_l in Hx. rewrite Rplus_assoc in Hx. rewrite Rplus_opp_l in Hx. rewrite Rplus_0_r in Hx. - exfalso. + exfalso. apply Rgt_not_le with p_exp (p_hat x); auto. } have Hle4: p_exp + eps <= p_hat x by lra. @@ -734,4 +736,3 @@ Section chernoff_twosided. move: (p _ _ _) => X; move: (/_ * _) => Y => H1 H2; lra. } Qed. End chernoff_twosided. - diff --git a/dist.v b/dist.v index 0673547..edd5b1e 100644 --- a/dist.v +++ b/dist.v @@ -55,18 +55,18 @@ Section support. Proof. split; first by apply: in_support. by rewrite /support in_set. - Qed. + Qed. End support. Section bind. Variable T U : finType. - Variable rty : numDomainType. + Variable rty : numDomainType. Variable d : {ffun T -> rty}. Variable f : T -> {ffun U -> rty}. Definition bind : {ffun U -> rty} := finfun (fun u : U => \sum_(t : T) (d t) * (f t u)). End bind. - + Section expectedValue. Variable T : finType. Variable rty : numDomainType. @@ -83,7 +83,7 @@ Section expectedValue. Lemma probOf_nonneg (p : pred T) : 0 <= probOf p. Proof. apply: sumr_ge0 => i Hi; apply: dist_positive. - Qed. + Qed. Definition expectedCondValue (f : T -> rty) (p : pred T) := (\sum_(t : T | p t) (d t) * (f t)) / (probOf p). @@ -109,7 +109,7 @@ Section expectedValue. { by apply/congr_big=> //= i _; rewrite mulrDr. } rewrite 3!mulr_suml -big_split /=; move: (probOf p) => e. apply: congr_big => // i _; rewrite mulrDl //. - Qed. + Qed. Lemma sum_split (f : T -> rty) p : \sum_t f t = \sum_(t | p t) f t + \sum_(t | ~~p t) f t. @@ -120,17 +120,17 @@ Section expectedValue. have ->: \sum_(i <- [seq i <- index_enum T | p i || ~~ p i]) f i = \sum_(i <- [seq i <- index_enum T | p i] ++ [seq i <- index_enum T | ~~p i]) f i. - { apply: eq_big_perm. + { apply: perm_big. have ->: [seq i <- index_enum T | ~~ p i] = [seq i <- index_enum T | predC p i] by []. - rewrite perm_eq_sym perm_filterC. + rewrite perm_sym perm_filterC. have ->: [seq i <- index_enum T | p i || ~~ p i] = index_enum T. { have ->: [seq i <- index_enum T | p i || ~~ p i] = [seq i <- index_enum T | predT i]. { by apply eq_in_filter => x; rewrite /in_mem /= => H; case: (p x). } by rewrite filter_predT. } by []. } by rewrite big_cat /= !big_filter. - Qed. - + Qed. + Definition expectedValue (f : T -> rty) := \sum_(t : T) (d t) * (f t). @@ -138,14 +138,14 @@ Section expectedValue. expectedValue f = \sum_(t | p t) d t * f t + \sum_(t | ~~p t) d t * f t. Proof. rewrite /expectedValue; rewrite ->sum_split with (p:=p); f_equal => //. - Qed. - - Lemma expectedValue_expectedCondValue f : + Qed. + + Lemma expectedValue_expectedCondValue f : expectedValue f = expectedCondValue f xpredT. Proof. by rewrite /expectedValue /expectedCondValue probOf_xpredT divr1. Qed. - + Lemma expectedValue_mull f c : expectedValue (fun t => c * f t) = c * expectedValue f. Proof. by rewrite 2!expectedValue_expectedCondValue expectedCondValue_mull. Qed. @@ -164,7 +164,7 @@ Section expectedValue. Lemma expectedValue_range f (H : forall x : T, 0 <= f x <= 1) : 0 <= expectedValue f <= 1. - Proof. + Proof. rewrite /expectedValue /expectedCondValue; apply/andP; split. apply: sumr_ge0=> i _; case H2: (f i == 0). { by move: (eqP H2)=> ->; rewrite mulr0. } @@ -177,18 +177,18 @@ Section expectedValue. { by move: (eqP H2)=> ->; rewrite mul0r. } rewrite mulrC ger_pmull; first by case: (andP (H i)). have H3: 0 <= d i by apply: dist_positive. - rewrite ltr_def; apply/andP; split=> //. + (*rewrite ltr_def; apply/andP; split=> //. by apply/eqP=> H4; rewrite H4 eq_refl in H2. - Qed. + Qed.*) Admitted. (*TODO*) Lemma expectedValue_nonneg f (H : forall x : T, 0 <= f x) : 0 <= expectedValue f. - Proof. + Proof. apply: sumr_ge0=> i _; case H2: (f i == 0). { by move: (eqP H2)=> ->; rewrite mulr0. } apply: mulr_ge0 => //; apply: dist_positive. - Qed. + Qed. Lemma expectedCondValue_nonneg f (p : pred T) (H : forall x : T, 0 <= f x) : @@ -199,7 +199,7 @@ Section expectedValue. { by move: (eqP H2)=> ->; rewrite mulr0. } apply: mulr_ge0 => //; apply: dist_positive. } apply: probOf_nonneg. - Qed. + Qed. End expectedValue. Section cdf. @@ -224,7 +224,7 @@ Section cdf. Definition inverse_cdf (p : rty) : option T := inverse_cdf_aux p 0 None (enum T). -End cdf. +End cdf. (** Product distributions *) @@ -247,7 +247,7 @@ Section product. Variable f : {ffun 'I_n -> dist T rty}. Notation type := ({ffun 'I_n -> T}). - + Definition prod_pmf : {ffun type -> rty} := finfun (fun p : type => \prod_(i : 'I_n) f i (p i)). @@ -263,8 +263,8 @@ Section product. by rewrite H prodr_const expr1n. } apply/forallP => x; rewrite /prod_pmf ffunE. by apply: prodr_ge0 => i _; apply: dist_positive. - Qed. - + Qed. + Definition prod_dist : dist [finType of type] rty := @mkDist _ _ prod_pmf prod_pmf_dist. End product. @@ -273,12 +273,12 @@ End product. Section timeAvg. Variable T : finType. Notation rty := rat_realFieldType. - (* the number of iterations (=size of history) *) + (* the number of iterations (=size of history) *) Variable n : nat. - Variable n_pos : (0 : rty) < n%:R. + Variable n_pos : (0 : rty) < n%:R. (* the distributions at each iteration: *) Variable s : {ffun 'I_n -> dist T rty}. - + Definition timeAvg_pmf : {ffun T -> rty} := finfun (fun x : T => (\sum_(i < n) s i x) / n%:R). @@ -304,7 +304,7 @@ Section timeAvg. apply: sumr_ge0 => i _; apply: dist_positive. Qed. - Definition timeAvg_dist : dist T rty := + Definition timeAvg_dist : dist T rty := @mkDist _ _ timeAvg_pmf timeAvg_pmf_dist. Lemma expectedValue_timeAvg f : @@ -329,18 +329,18 @@ Section uniform. Variable T : finType. Variable t0 : T. Notation rty := rat. - + Definition uniform_dist : {ffun T -> rty} := finfun (fun _ => 1 / #|T|%:R). - Lemma itern_addr_const n (r : rty) : iter n (+%R r) 0 = r *+ n. + Lemma itern_addr_const n (r : rty) : iter n (+%R r) 0 = r *+ n. Proof. by elim: n r=> // n IH r /=; rewrite IH mulrS. Qed. Lemma ffun_lem (r : rty) : \sum_(t : T) [ffun => r / #|T|%:R] t = \sum_(t : T) r / #|T|%:R. Proof. by apply/congr_big=> // i _; rewrite ffunE. Qed. - + Lemma uniform_normalized : dist_axiom uniform_dist. Proof. rewrite /dist_axiom ffun_lem; rewrite big_const itern_addr_const. @@ -352,7 +352,7 @@ Section uniform. have H: #|T| != 0%N. { by apply/eqP=> H; rewrite H in Hgt0. } - apply/andP; split. + apply/andP; split. { move: #|T| H=> n. rewrite div1r -[_ *+ n]mulr_natl; move/eqP=> H. apply/eqP; apply: mulfV=> //; apply/eqP=> H2; apply: H. @@ -360,7 +360,7 @@ Section uniform. by erewrite <-pnatr_eq0; apply/eqP; apply: H2. } apply/forallP=> t; rewrite /uniform_dist ffunE. - apply: divr_ge0=> //. + apply: divr_ge0=> //. by apply: ler0n. Qed. @@ -372,7 +372,7 @@ Section uniform. rewrite /expectedValue /uniformDist /= /uniform_dist. rewrite mulr_suml; apply/congr_big=> // t _; rewrite ffunE. by rewrite -mulrA mul1r mulrC. - Qed. + Qed. End uniform. (** Markov's Inequality *) @@ -386,7 +386,9 @@ Section markov. Variable d : dist T rty. Definition PRED := [pred x | f x >= a]. - + + Import mc_1_10.Num.Theory. + Lemma markov : probOf d PRED <= expectedValue d f / a. Proof. rewrite /probOf; rewrite ->expectedValue_split with (p:=PRED). @@ -403,7 +405,7 @@ Section markov. by apply/ltrW. } apply: ler_trans; first by apply: H3. apply: H2. - Qed. + Qed. End markov. (* R-valued stuff after this point: *) @@ -413,6 +415,7 @@ Require Import QArith Reals Rpower Ranalysis Fourier Lra. Section markovR. Variable T : finType. Variable a : R. + #[local] Open Scope R_scope. Variable a_gt0 : 0 < a. Variable f : T -> R. Variable f_nonneg : forall x, 0 <= f x. @@ -441,7 +444,7 @@ Section markovR. { move => c Hin; apply: d_nonneg. } by move => c; rewrite mem_filter; case/andP. Qed. - + Lemma expValR_ge0 : 0 <= expValR d f. Proof. rewrite /expValR; elim: (enum T) => /=; try apply: Rle_refl. @@ -454,25 +457,25 @@ Section markovR. rewrite /expValR; elim: (enum T) => /=; first by rewrite Rplus_0_r. move => x l ->; rewrite Rmult_plus_distr_l -!Rplus_assoc -[(_ + _) + d x * h x]Rplus_comm. by rewrite -Rplus_assoc -[d x * h x + _]Rplus_comm. - Qed. + Qed. Lemma expValR_const c g : expValR d (fun x => c * g x) = c * expValR d g. - Proof. + Proof. rewrite /expValR; elim: (enum T) => /=; first by rewrite Rmult_0_r. move => x l ->; rewrite -Rmult_assoc [d x * _]Rmult_comm Rmult_assoc Rmult_plus_distr_l //. Qed. Lemma expValR_sumconst c : expValR d (fun x => c) = c. - Proof. - by rewrite /expValR -big_sum_mult_right d_dist Rmult_1_l. + Proof. + by rewrite /expValR -big_sum_mult_right d_dist Rmult_1_l. Qed. - + Lemma expValR_Ropp g : expValR d (fun x => - g x) = - expValR d g. Proof. rewrite /expValR; elim: (enum T) => /=; first by rewrite Ropp_0. move => x l ->; rewrite Ropp_plus_distr; f_equal. by rewrite Ropp_mult_distr_r_reverse. - Qed. + Qed. Lemma expValR_one : expValR d (fun _ : T => 1) = 1. Proof. @@ -480,8 +483,8 @@ Section markovR. have ->: big_sum (enum T) (fun x : T => d x * 1) = big_sum (enum T) (fun x : T => d x). { by apply: big_sum_ext => //= x; rewrite Rmult_1_r. } apply: d_dist. - Qed. - + Qed. + Lemma expValR_split (p : pred T) : expValR d f = big_sum (filter p (enum T)) (fun x => d x * f x) + @@ -498,8 +501,8 @@ Section markovR. } by rewrite Rmult_1_r. } eapply Rmult_le_reg_r; eauto. - Qed. - + Qed. + Lemma markovR : probOfR d PREDR <= expValR d f / a. Proof. rewrite ->expValR_split with (p:=PREDR); rewrite /probOfR. @@ -525,6 +528,7 @@ Section union_bound. Variable N : nat. Variable P : 'I_N -> pred T. Variable d : T -> R. + #[local] Open Scope R_scope. Variable d_dist : big_sum (enum T) d = 1. Variable d_nonneg : forall x, 0 <= d x. @@ -534,7 +538,7 @@ Section union_bound. rewrite /probOfR big_sum_sumP. have ->: \big[bigops.Rplus/0]_i big_sum [seq x <- enum T | P i x] d - = \big[bigops.Rplus/0]_i \big[bigops.Rplus/0]_(x | P i x) d x. + = \big[bigops.Rplus/0]_i \big[bigops.Rplus/0]_(x | P i x) d x. { apply: eq_big => // i _; rewrite big_sum_sumP. apply: congr_big => //; rewrite enumT //. } rewrite (@exchange_big_dep _ _ _ _ _ _ _ _ _ xpredT) => //. @@ -557,21 +561,23 @@ Section union_bound. elim: n => /=; first by apply: Rle_refl. move => n IH; apply: Rplus_le_le_0_compat => //. } rewrite -big_sum_sumP; apply: big_sum_ge0 => //. - Qed. + Qed. End union_bound. -(** Relative entropy RE(p||q) - NOTE: This definition is nonstandard in that we use natural rather +(** Relative entropy RE(p||q) + NOTE: This definition is nonstandard in that we use natural rather than binary log. *) Section relative_entropy. Variable T : finType. Variables p q : T -> R. + #[local] Open Scope R_scope. Definition RE := big_sum (enum T) (fun x => p x * ln (p x / q x)). End relative_entropy. Module Bernoulli. Section Bernoulli. Variable p : R. + #[local] Open Scope R_scope. Variable p_range : 0 <= p <= 1. Definition t (b : bool) : R := if b then p else 1 - p. Lemma dist : big_sum (enum bool_finType) t = 1. @@ -594,6 +600,7 @@ Section relative_entropy_Bernoulli. Definition RE_Bernoulli : R := RE p_dist q_dist. + #[local] Open Scope R_scope. Lemma RE_Bernoulli_def : RE_Bernoulli = p * ln (p / q) + (1 - p) * ln ((1 - p) / (1 - q)). Proof. @@ -607,8 +614,9 @@ Section TV_Bernoulli. Variable p q : R. Notation p_dist := (@p_dist p). Notation q_dist := (@q_dist q). + #[local] Open Scope R_scope. - Definition TV_Bernoulli : R := + Definition TV_Bernoulli : R := Rmax (Rabs (p_dist true - q_dist true)) (Rabs (p_dist false - q_dist false)). @@ -623,13 +631,14 @@ End TV_Bernoulli. Section markovR_exp. Variable T : finType. Variable a : R. + #[local] Open Scope R_scope. Variable a_gt0 : 0 < a. Variable f : T -> R. Variable f_nonneg : forall x, 0 <= f x. Variable d : T -> R. Variable d_dist : big_sum (enum T) d = 1. Variable d_nonneg : forall x, 0 <= d x. - + Lemma markovR_exp : probOfR d (fun x => Rle_lt_dec (exp a) (exp (f x))) <= exp (- a) * expValR d (fun x => exp (f x)). @@ -638,20 +647,21 @@ Section markovR_exp. rewrite /Rle => x; case: (f_nonneg x) => H. { by left; apply: exp_pos_pos. } rewrite -H; left; rewrite exp_0; apply: Rlt_0_1. - Qed. + Qed. End markovR_exp. Section prodR. Variable T : finType. Variable m : nat. - Variable m_gt0 : (0 < m)%nat. + Variable m_gt0 : (0 < m)%nat. Variables d : 'I_m -> T -> R. + #[local] Open Scope R_scope. Variable d_dist : forall i, big_sum (enum T) (d i) = 1. Variable d_nonneg : forall i x, 0 <= (d i) x. Definition prodR : {ffun 'I_m -> T} -> R := fun p => big_product (enum 'I_m) (fun i : 'I_m => d i (p i)). - + Lemma prodR_dist : big_sum (enum [finType of {ffun 'I_m -> T}]) prodR = 1. Proof. rewrite /prodR -big_product_distr_sum. @@ -720,20 +730,20 @@ Section prodR. by []. } rewrite /prodR -big_product_split //. Qed. - + Lemma prodR_marginal f i : big_sum (enum {ffun 'I_m -> T}) (fun p0 => prodR p0 * f i (p0 i)) = big_sum (enum T) (fun x : T => d i x * f i x). Proof. have ->: - big_sum (enum {ffun 'I_m -> T}) (fun p0 => prodR p0 * f i (p0 i)) - = big_sum (enum {ffun 'I_m -> T}) (fun p0 => + big_sum (enum {ffun 'I_m -> T}) (fun p0 => prodR p0 * f i (p0 i)) + = big_sum (enum {ffun 'I_m -> T}) (fun p0 => (d i (p0 i) * - big_product (filter (predC (pred1 i)) (enum 'I_m)) (fun j => d j (p0 j))) * + big_product (filter (predC (pred1 i)) (enum 'I_m)) (fun j => d j (p0 j))) * f i (p0 i)). { apply: big_sum_ext => // => p; rewrite (prodR_split i) //. } rewrite 2!big_sum_sum -(marginal_unfoldR i). - set (F (x:T) y := + set (F (x:T) y := d i (y i) * big_product [seq x <- enum 'I_m | (predC (pred1 i)) x] (fun j : ordinal_finType m => d j (y j)) * @@ -751,7 +761,7 @@ Section prodR. rewrite /F /P /Q /=; apply: eq_big => // k _. have ->: \big[Rplus/0]_(j:[finType of {ffun 'I_m ->T}] | if k == j i then true else false) - (d i (j i) * big_product [seq x <- enum 'I_m | x != i] (fun j0 : 'I_m => d j0 (j j0)) * f i (j i)) + (d i (j i) * big_product [seq x <- enum 'I_m | x != i] (fun j0 : 'I_m => d j0 (j j0)) * f i (j i)) = \big[Rplus/0]_(j:[finType of {ffun 'I_m->T}] | if k == j i then true else false) (d i k * big_product [seq x <- enum 'I_m | x != i] (fun j0 : 'I_m => d j0 (j j0)) * f i k). { apply: eq_big => // ix. @@ -771,7 +781,7 @@ Section prodR. rewrite /G /cs /=; clear G cs; rewrite big_sum_sumP. have ->: \big[bigops.Rplus/0]_(i0:[finType of {ffun 'I_m->T}] | if k == i0 i then true else false) - big_product [seq x <- enum 'I_m | x != i] (fun j0 : 'I_m => d j0 (i0 j0)) + big_product [seq x <- enum 'I_m | x != i] (fun j0 : 'I_m => d j0 (i0 j0)) = \big[bigops.Rplus/0]_(i0:[finType of {ffun 'I_m->T}] | if k == i0 i then true else false) \big[bigops.Rtimes/1]_(x | x != i) d x (i0 x). { apply: eq_big => // x _; rewrite big_product_prodP //. } @@ -782,31 +792,33 @@ Section prodR. { apply: eq_big => // x; rewrite eq_sym; case: (x i == k)%B => //. } apply: prodR_sub_dist. Qed. -End prodR. +End prodR. Section convolution. Variable T : finType. Variable m : nat. Variable m_gt0 : (0 < m)%nat. Variables d : 'I_m -> T -> R. + #[local] Open Scope R_scope. Variable d_dist : forall i, big_sum (enum T) (d i) = 1. Variable d_nonneg : forall i x, 0 <= (d i) x. Variable f : 'I_m -> T -> R. Variable f_range : forall i x, 0 <= f i x <= 1. - - (** [conv r]: the probability that r is less than or equal to the average - sum of the realizations of the random variables [f i] as drawn from + + (** [conv r]: the probability that r is less than or equal to the average + sum of the realizations of the random variables [f i] as drawn from distributions [d i]. *) Definition conv (r : R) := probOfR (prodR d) (fun p => Rle_lt_dec r ((/INR m) * big_sum (enum 'I_m) (fun i => f i (p i)))). -End convolution. +End convolution. Section general_lemmas. Variable T : finType. Variables d : T -> R. + #[local] Open Scope R_scope. Variable d_dist : big_sum (enum T) d = 1. Variable d_nonneg : forall x, 0 <= d x. - + Lemma probOfR_q_exp g h c (Hlt : 0 < c) : probOfR d (fun x => Rle_lt_dec (g x) (h x)) = probOfR d (fun x => Rle_lt_dec (exp (c * g x)) (exp (c * h x))). @@ -826,5 +838,3 @@ Section general_lemmas. by move => H5; elimtype False; rewrite H5 in H4; move: (Rlt_asym _ _ H4). Qed. End general_lemmas. - - diff --git a/dyadic.v b/dyadic.v index 70577b7..4a6ffd4 100644 --- a/dyadic.v +++ b/dyadic.v @@ -41,13 +41,13 @@ Definition DOadd (d1 d2 : DO) : DO := | Dmake x1 y1, Dmake x2 y2 => if Pos.ltb y1 y2 then Dmake (Z.pow_pos 2 (y2 - y1) * x1 + x2) y2 - else if Pos.ltb y2 y1 then + else if Pos.ltb y2 y1 then Dmake (Z.pow_pos 2 (y1 - y2) * x2 + x1) y1 else Dmake (x1 + x2) y1 end. Lemma Qdiv_mult (s q r : Q) : - ~ s == 0 -> + ~ s == 0 -> (q / r) == (q * s) / (r * s). Proof. intros H; unfold Qdiv. @@ -69,10 +69,10 @@ Proof. rewrite Pos2Z.inj_xO, (Pos2Z.inj_xO y). rewrite Zdiv_mult_cancel_l; auto. inversion 1. -Qed. +Qed. Lemma Zpow_pos_2exp (x y : nat) : - (y < x)%nat -> + (y < x)%nat -> Z.pow 2 (Z.of_nat (x - y)) = (Z.pow 2 (Z.of_nat x) / Z.pow 2 (Z.of_nat y))%Z. Proof. intros H; rewrite <-!two_power_nat_equiv; unfold two_power_nat. @@ -87,7 +87,7 @@ Proof. Qed. Lemma Pos_iter_swap' T f g (r : T) (x : positive) : - (forall t, f (g t) = t) -> + (forall t, f (g t) = t) -> Pos.iter f (Pos.iter g r x) x = r. Proof. rewrite 2!Pos2Nat.inj_iter. @@ -111,16 +111,16 @@ Proof. rewrite Pos2Nat.inj_iter. apply IHn; auto. exists y; auto. -Qed. +Qed. -Lemma Pos_lt_Zpos_Zlt x y : - (x < y)%positive -> +Lemma Pos_lt_Zpos_Zlt x y : + (x < y)%positive -> (Zpos' x < Zpos' y)%Z. Proof. unfold Z.lt; simpl; rewrite <-Pos.ltb_lt. rewrite Pos.ltb_compare. destruct (Pos.compare x y); auto; try solve[inversion 1]. -Qed. +Qed. Lemma Zlt_le x y : (x < y -> x <= y)%Z. Proof. @@ -131,7 +131,7 @@ Proof. Qed. Lemma Zpow_pos_div x y : - (y < x)%positive -> + (y < x)%positive -> (Z.pow_pos 2 x # 1) * / (Z.pow_pos 2 y # 1) == Z.pow_pos 2 (x - y) # 1. Proof. intros H; rewrite !Z.pow_pos_fold. @@ -175,10 +175,10 @@ Proof. { inversion 1. } split. { apply Pos2Z.is_nonneg. } - unfold Z.le, Z.compare; rewrite H; inversion 1. + unfold Z.le, Z.compare; rewrite H; inversion 1. split. { apply Pos2Z.is_nonneg. } - unfold Z.le, Z.compare; rewrite H; inversion 1. + unfold Z.le, Z.compare; rewrite H; inversion 1. Qed. Lemma Qinv_neq (n : Q) : ~0 == n -> ~0 == / n. @@ -191,7 +191,7 @@ Proof. intros _ H. generalize (Zlt_neg_0 (Qden n * 1)). rewrite <-H; inversion 1. -Qed. +Qed. Lemma Qdiv_neq_0 n m : ~n==0 -> ~m==0 -> ~(n / m == 0). Proof. @@ -201,7 +201,7 @@ Proof. assert (H2: ~0 == m). { intros H2; rewrite H2 in H1; apply H1; apply Qeq_refl. } apply (Qinv_neq _ H2); rewrite H0; apply Qeq_refl. -Qed. +Qed. Lemma Qmake_neq_0 n m : (~n=0)%Z -> ~(n # m) == 0. Proof. @@ -222,7 +222,7 @@ Proof. Qed. Lemma Zmult_pow_plus x y r : - (r <> 0)%Z -> + (r <> 0)%Z -> x * inject_Z (Z.pow r (Z.pos y)) / inject_Z (Z.pow r (Z.pos y+Z.pos y)) == x / inject_Z (Z.pow r (Z.pos y)). Proof. @@ -242,7 +242,7 @@ Proof. { apply Qeq_refl. } apply Qmake_neq_0; intros H2. apply (Zpow_pos_neq_0 _ _ H H2). -Qed. +Qed. Lemma DOadd_ok d1 d2 : DO_to_Q (DOadd d1 d2) == DO_to_Q d1 + DO_to_Q d2. @@ -369,7 +369,7 @@ Proof. assert (inject_Z W * inject_Z (Z.pow_pos 2 X) * / inject_Z (Z.pow_pos 2 (X + X)) == inject_Z W / inject_Z (Z.pow_pos 2 X)) as ->. - { apply Zmult_pow_plus; inversion 1. } + { apply Zmult_pow_plus; inversion 1. } unfold Qdiv; rewrite <-Qmult_plus_distr_l, Qmake_Qdiv, inject_Z_plus. unfold Qdiv; rewrite shift_pos_correct, Zmult_1_r; apply Qeq_refl. Qed. @@ -386,7 +386,7 @@ Proof. induction n; simpl; auto. rewrite IHn; auto. Qed. - + Lemma DOmult_ok d1 d2 : DO_to_Q (DOmult d1 d2) = DO_to_Q d1 * DO_to_Q d2. Proof. @@ -427,7 +427,7 @@ Qed. Definition DOle (d1 d2 : DO) : Prop := - Qle (DO_to_Q d1) (DO_to_Q d2). + Qle (DO_to_Q d1) (DO_to_Q d2). (*TODO: There's probably a more efficient way to implement the following:*) Definition DOle_bool (d1 d2 : DO) : bool := @@ -440,7 +440,7 @@ Proof. Qed. Definition DOlt (d1 d2 : DO) : Prop := - Qlt (DO_to_Q d1) (DO_to_Q d2). + Qlt (DO_to_Q d1) (DO_to_Q d2). Definition DOlt_bool (d1 d2 : DO) : bool := match DO_to_Q d1 ?= DO_to_Q d2 with @@ -454,7 +454,7 @@ Proof. destruct (Qcompare_spec (DO_to_Q d1) (DO_to_Q d2)); try solve[inversion 1|auto]. unfold DOlt; rewrite Qlt_alt; intros ->; auto. -Qed. +Qed. Lemma DOeq_dec (d1 d2 : DO) : {d1=d2} + {d1<>d2}. Proof. @@ -464,7 +464,7 @@ Proof. left; subst; f_equal. right; inversion 1; subst; apply n; auto. } right; inversion 1; subst; auto. -Qed. +Qed. (*(* MICROBENCHMARK *) Fixpoint f (n : nat) (d : D) : D := @@ -557,8 +557,8 @@ Proof. rewrite Pos2Z.inj_xO. rewrite (Pos2Z.inj_xO - (nat_rect (fun _ : nat => positive) 1%positive - (fun _ : nat => xO) y')). + (nat_rect (fun _ : nat => positive) 1%positive + (fun _ : nat => xO) y')). apply Zmult_le_compat; try omega. { apply IHx'; omega. } clear - x'. @@ -566,7 +566,7 @@ Proof. simpl; rewrite Pos2Z.inj_xO. assert ((0=0*0)%Z) as -> by (rewrite Zmult_0_r; auto). apply Zmult_le_compat; try omega. -Qed. +Qed. Lemma Zpow_pos_size_le x : (x <= Z.pow_pos 2 (Zsize x))%Z. Proof. @@ -577,7 +577,7 @@ Proof. rewrite <-Pos2Z.inj_pow_pos; auto. } rewrite <-Pos2Z.inj_pow_pos. apply Zle_neg_pos. -Qed. +Qed. Lemma Pos_succ_sub_1 p : (Pos.succ p - 1 = p)%positive. Proof. @@ -591,7 +591,7 @@ Proof. rewrite !Pos2Nat.inj_succ. rewrite Pos2Nat.inj_1. omega. -Qed. +Qed. Lemma Pos_le_1_add_sub x : (x <= 1 + (x - 1))%positive. Proof. @@ -616,12 +616,12 @@ Proof. assert (H3: (1 <= Pos.iter_op Init.Nat.add p 1)%nat) by apply le_Pmult_nat. apply Peano.le_n_S; auto. } omega. -Qed. +Qed. Lemma Pos2Nat_inj_2 : Pos.to_nat 2 = 2%nat. Proof. unfold Pos.to_nat; simpl; auto. Qed. -Lemma Pos_le_2_add_sub x : +Lemma Pos_le_2_add_sub x : (1 + (x - 1) <= 2 + (x - 2))%positive. Proof. rewrite Pos2Nat.inj_le. @@ -725,7 +725,7 @@ Proof. rewrite Pplus_one_succ_l. rewrite <-Pos.add_assoc. rewrite Pos.add_xO. - rewrite <-Pos.add_assoc. + rewrite <-Pos.add_assoc. apply Pos.add_le_mono; auto. apply Pos.le_1_l. Qed. @@ -745,7 +745,7 @@ Proof. apply H; auto. } intros _; apply Pos.le_1_l. Qed. - + Local Open Scope DO_scope. Lemma DOlub_mult_le1 d : d * DOlub d <= 1. @@ -783,7 +783,7 @@ Proof. Qed. Lemma DOlub_ok (d : DO) : - 0 <= d -> + 0 <= d -> DOle 0 (d * DOlub d) /\ DOle (d * DOlub d) 1. Proof. intros H. @@ -811,12 +811,12 @@ Proof. destruct (Zodd_dec n); auto. destruct (Zeven_odd_dec n); auto. elimtype False; apply n0; auto. -Qed. +Qed. Definition DO_of_DOred' (p : Z*nat) : DO := let (x,y) := p in Dmake x (Pos.of_nat (S y)). -Definition DOred (d : DO) : DO := +Definition DOred (d : DO) : DO := DO_of_DOred' (DOred' (num d) (pred (Pos.to_nat (den d)))). Lemma DOredP d : Zodd (num (DOred d)) \/ (den (DOred d) = 1%positive). @@ -827,7 +827,7 @@ Proof. destruct (DOred' _ _); auto. } destruct (DOred' _ _); right; simpl in *. rewrite H; auto. -Qed. +Qed. Lemma DO_of_DOred'_correct x y : DO_to_Q (DO_of_DOred' (DOred' x y)) == DO_to_Q (DO_of_DOred' (x,y)). @@ -849,7 +849,7 @@ Proof. rewrite Zmult_assoc. pattern (Z.div2 x * 2)%Z; rewrite Zmult_comm; auto. } apply Qeq_refl. -Qed. +Qed. Lemma DOred_correct d : DO_to_Q (DOred d) == DO_to_Q d. Proof. @@ -864,7 +864,7 @@ Proof. intros _; simpl. rewrite (SuccNat2Pos.inv n y); auto. apply Qeq_refl. -Qed. +Qed. Lemma gcd_2_odd_1 x : Zodd x -> Z.gcd x 2 = 1%Z. Proof. @@ -889,7 +889,7 @@ Proof. intros H2; apply Znumtheory.Zdivide_mod in H2. rewrite Zmod_odd in H2. rewrite <-Zodd_bool_iff in H4; rewrite H4 in H2; inversion H2. -Qed. +Qed. Lemma gcd_2_even_2 x : Zeven x -> Z.gcd x 2 = 2%Z. Proof. @@ -912,7 +912,7 @@ Proof. destruct H; auto. elimtype False. rewrite Znumtheory.Zgcd_1_rel_prime in H. - destruct H. + destruct H. assert (H2: (2 | x)%Z). { apply Znumtheory.Zmod_divide. { inversion 1. } @@ -928,7 +928,7 @@ Proof. { apply Z.divide_pos_le; auto. omega. } omega. -Qed. +Qed. Lemma gcd_x_times2_1 x y : Zodd x -> Z.gcd x y = 1%Z -> Z.gcd x (2*y) = 1%Z. Proof. @@ -936,7 +936,7 @@ Proof. generalize (Znumtheory.Zgcd_is_gcd x y) as H2; intro. apply Znumtheory.Zis_gcd_gcd; try omega. inversion H2. - constructor; try apply Z.divide_1_l. + constructor; try apply Z.divide_1_l. intros w H4 H5. rewrite H in H3. apply Znumtheory.Gauss in H5; auto. @@ -956,7 +956,7 @@ Proof. apply Zeven_2p. } apply Zodd_not_Zeven in Hodd; auto. } apply gcd_2_odd_1; auto. -Qed. +Qed. Lemma gcd_pow2_odd_1 x n : Zodd x -> Z.gcd x (Zpower_nat 2 n) = 1%Z. Proof. @@ -968,7 +968,7 @@ Proof. generalize (IHn Hodd). intros H. apply gcd_x_times2_1; auto. -Qed. +Qed. Lemma Qred_odd_pow2 x n : Zodd x -> Qred (x # pow_pos 2 n) = x # (pow_pos 2 n). Proof. @@ -986,7 +986,7 @@ Proof. rewrite H2, Zmult_1_l in H0. subst b. auto. -Qed. +Qed. Lemma Qred_odd_2 x : Zodd x -> Qred (x # 2) = x # 2. Proof. @@ -1003,7 +1003,7 @@ Proof. rewrite H2, Zmult_1_l in H0. subst b. auto. -Qed. +Qed. Lemma shift_pos_pow_pos n : shift_pos n 1 = pow_pos 2 n. Proof. @@ -1016,7 +1016,7 @@ Proof. rewrite Pos2Nat.inj_succ; simpl; rewrite IH. unfold pow_pos; simpl; auto. rewrite Pos.iter_succ; auto. -Qed. +Qed. Lemma pow_pos_2inj p q : pow_pos 2 p = pow_pos 2 q -> p = q. Proof. @@ -1033,10 +1033,10 @@ Proof. destruct n; simpl. { inversion 1. } inversion 1; subst; f_equal; apply IHm; auto. -Qed. +Qed. Lemma Qred_even_2 x : - Zeven x -> + Zeven x -> Qred (x # 2) = Z.div2 x # 1. Proof. unfold Qred. @@ -1055,7 +1055,7 @@ Proof. rewrite H0. f_equal. destruct b; auto. -Qed. +Qed. Lemma Zdiv2_even_inj x y : Zeven x -> Zeven y -> Z.div2 x = Z.div2 y -> x=y. Proof. @@ -1063,7 +1063,7 @@ Proof. destruct x; destruct y; simpl in H2; auto; try destruct p; try destruct p0; inversion H2; try inversion H; try inversion H1; auto. -Qed. +Qed. Lemma DOred_complete d1 d2 : DO_to_Q d1 == DO_to_Q d2 -> @@ -1087,7 +1087,7 @@ Proof. f_equal. apply pow_pos_2inj; auto. } - (* den (DOred d2) = 1 *) + (* den (DOred d2) = 1 *) rewrite H0. rewrite Qred_odd_pow2; auto. intros H2. @@ -1120,7 +1120,7 @@ Proof. f_equal. apply pow_pos_2inj; auto. } - (* den (DOred d1) = 1 *) + (* den (DOred d1) = 1 *) destruct (DOredP d2). (* Zodd (num (DOred d2)) *) { rewrite H. @@ -1148,7 +1148,7 @@ Proof. inversion H2; subst. revert H3 H4 H0. destruct (DOred d2); simpl. - destruct (DOred d1); simpl. + destruct (DOred d1); simpl. intros <- Hx Hodd. simpl in H. subst den1. @@ -1181,7 +1181,7 @@ Proof. inversion 1. } rewrite !Qred_odd_2; auto. inversion 1; subst. - simpl in H0, H; subst; auto. + simpl in H0, H; subst; auto. Qed. Lemma DOred'_idem x y : @@ -1197,8 +1197,8 @@ Proof. destruct (Zeven_dec z); auto. apply Zodd_not_Zeven in H; contradiction. } destruct (DOred' x y); simpl in H|-*; rewrite H; auto. -Qed. - +Qed. + Lemma DOred_idem d : DOred (DOred d) = DOred d. Proof. unfold DOred. @@ -1229,7 +1229,7 @@ Proof. rewrite H3 in H. rewrite DOred'_idem in H. rewrite H; auto. -Qed. +Qed. Module DORed. @@ -1238,11 +1238,11 @@ Module DORed. pf : DOred d = d }. Definition build (d : DO) : t := @mk (DOred d) (DOred_idem d). - + Program Definition t0 := mk 0 _. Program Definition t1 := mk 1 _. - + Program Definition add (d1 d2 : t) : t := mk (DOred (DOadd d1.(d) d2.(d))) _. Next Obligation. @@ -1252,25 +1252,25 @@ Module DORed. Program Definition sub (d1 d2 : t) : t := mk (DOred (DOsub d1.(d) d2.(d))) _. Next Obligation. - apply DOred_complete; rewrite DOred_correct; apply Qeq_refl. + apply DOred_complete; rewrite DOred_correct; apply Qeq_refl. Qed. - Program Definition mult (d1 d2 : t) : t := + Program Definition mult (d1 d2 : t) : t := mk (DOred (DOmult d1.(d) d2.(d))) _. Next Obligation. - apply DOred_complete; rewrite DOred_correct; apply Qeq_refl. + apply DOred_complete; rewrite DOred_correct; apply Qeq_refl. Qed. - Program Definition opp (dx : t) : t := + Program Definition opp (dx : t) : t := mk (DOred (DOopp dx.(d))) _. Next Obligation. - apply DOred_complete; rewrite DOred_correct; apply Qeq_refl. + apply DOred_complete; rewrite DOred_correct; apply Qeq_refl. Qed. - Program Definition lub (dx : t) : t := + Program Definition lub (dx : t) : t := mk (DOred (DOlub dx.(d))) _. Next Obligation. - apply DOred_complete; rewrite DOred_correct; apply Qeq_refl. + apply DOred_complete; rewrite DOred_correct; apply Qeq_refl. Qed. Program Definition of_nat (n : nat) : t := @@ -1289,16 +1289,16 @@ Module DORed. intros H; assert (H2: x1 = x2). { rewrite <-pf1, <-pf2; apply DOred_complete; auto. } generalize pf1 pf2; rewrite H2; intros; f_equal; apply proof_irrelevance. - Qed. - + Qed. + Lemma addP d1 d2 : DO_to_Q (d (add d1 d2)) == (DO_to_Q (d d1) + DO_to_Q (d d2))%Q. Proof. unfold add; simpl. rewrite DOred_correct. rewrite DOadd_ok; apply Qeq_refl. - Qed. - + Qed. + Lemma addC d1 d2 : add d1 d2 = add d2 d1. Proof. apply DOred_eq; simpl; rewrite 2!DOred_correct, 2!DOadd_ok. @@ -1310,7 +1310,7 @@ Module DORed. apply DOred_eq; simpl. rewrite !DOred_correct, !DOadd_ok, !DOred_correct, !DOadd_ok. apply Qplus_assoc. - Qed. + Qed. Lemma add0l d : add t0 d = d. Proof. @@ -1318,8 +1318,8 @@ Module DORed. generalize (add_obligation_1 {|d:=0;pf:=t0_obligation_1|} d). unfold DORed.d; rewrite DOred_correct; intros e. rewrite DOadd_ok, DO_to_Q0, Qplus_0_l; apply Qeq_refl. - Qed. - + Qed. + Lemma subP d1 d2 : DO_to_Q (d (sub d1 d2)) == (DO_to_Q (d d1) - DO_to_Q (d d2))%Q. Proof. @@ -1334,8 +1334,8 @@ Module DORed. unfold mult; simpl. rewrite DOred_correct. rewrite DOmult_ok; apply Qeq_refl. - Qed. - + Qed. + Lemma multC d1 d2 : mult d1 d2 = mult d2 d1. Proof. apply DOred_eq; simpl; rewrite 2!DOred_correct, 2!DOmult_ok. @@ -1347,7 +1347,7 @@ Module DORed. apply DOred_eq; simpl. rewrite !DOred_correct, !DOmult_ok, !DOred_correct, !DOmult_ok. apply Qmult_assoc. - Qed. + Qed. Lemma oppP dx : DO_to_Q (d (opp dx)) == (- DO_to_Q (d dx))%Q. @@ -1371,7 +1371,7 @@ Module DORed. Proof. intros. apply DOred_eq. - rewrite addP. + rewrite addP. simpl. rewrite DO_to_Q0. rewrite DOred_correct. @@ -1379,7 +1379,7 @@ Module DORed. rewrite Qplus_comm. apply Qplus_opp_r. Qed. - + Lemma addNegDistr: forall d1 d2, opp (add d1 d2) = add (opp d1) (opp d2). Proof. intros. @@ -1430,7 +1430,7 @@ Module DORed. apply Qle_lteq. destruct H; auto. rewrite H. - right. + right. apply Qeq_refl. } intros. @@ -1458,7 +1458,7 @@ Module DORed. repeat (rewrite addP). apply Qplus_lt_le_compat; auto. Qed. - + Lemma plus_lt_compat_l : forall t t1 t2 : t, DOlt t1 t2 -> DOlt (add t t1) (add t t2). Proof. intros. @@ -1470,18 +1470,18 @@ Module DORed. Qed. - - + + Lemma lt_t0_t1: t0 < t1. Proof. unfold DOlt. rewrite DO_to_Q0. rewrite DO_to_Q1. unfold Qlt, Z.lt. - auto. + auto. Qed. - Lemma mult_le_compat: + Lemma mult_le_compat: forall (r1 r2 r3 r4 : t) , DOle t0 r1 -> DOle t0 r3 -> DOle r1 r2 -> DOle r3 r4 -> DOle (mult r1 r3) (mult r2 r4). Proof. @@ -1556,7 +1556,7 @@ Module DORed. rewrite Z.mul_comm with (QDen q3) (Qnum q4). auto. Qed. - + Lemma mult_lt_compat_l : forall r r1 r2 : t, DOlt t0 r -> (DOlt r1 r2 <-> DOlt (mult r r1) (mult r r2)). Proof. unfold DOlt. @@ -1606,7 +1606,7 @@ Module DORed. Lemma of_natP: forall n : nat, DO_to_Q (of_nat n) = (Qmake (2 * (Z.of_nat n)) 2). Proof. auto. Qed. - Lemma of_nat_succ_l: forall n : nat, of_nat (S n) = add t1 (of_nat (n)). + Lemma of_nat_succ_l: forall n : nat, of_nat (S n) = add t1 (of_nat (n)). Proof. intros. apply DOred_eq. @@ -1656,8 +1656,8 @@ Module DORed. Proof. intros. destruct DOeq_dec with (d d1) (d d2). - { - left. + { + left. destruct d1,d2. simpl in e. generalize pf0 pf1. @@ -1700,7 +1700,7 @@ Module DORed. intros. apply Qlt_trans with (DO_to_Q d2); auto. Qed. - + Lemma total_order_T : forall d1 d2 : t, {DOlt d1 d2} + {d1 = d2} + {DOlt d2 d1}. Proof. @@ -1715,7 +1715,7 @@ Module DORed. Qed. (* TODO: More lemmas here! *) -End DORed. +End DORed. Coercion DORed.d : DORed.t >-> DO. @@ -1747,7 +1747,7 @@ Inductive D : Set := Definition D_to_Q (d : D) := match d with - | DD d => + | DD d => DO_to_Q d | DQ q => q end. @@ -1769,7 +1769,7 @@ Proof. rewrite D_to_Q1'; unfold Qeq; simpl; auto. Qed. Definition Dadd (d1 d2 : D) : D := match d1,d2 with - | DD d1, DD d2 => + | DD d1, DD d2 => DD (DOadd d1 d2) | _, _ => DQ (D_to_Q d1 + D_to_Q d2) end. @@ -1789,7 +1789,7 @@ Qed. Definition Dmult (d1 d2 : D) : D := match d1,d2 with - | DD d1, DD d2 => + | DD d1, DD d2 => DD (DOmult d1 d2) | _, _ => DQ (D_to_Q d1 * D_to_Q d2) end. @@ -1807,7 +1807,7 @@ Qed. Definition Dopp (d : D) : D := match d with - | DD d => + | DD d => DD (DOopp d) | _ => DQ (Qopp (D_to_Q d)) end. @@ -1831,7 +1831,7 @@ Proof. Qed. Definition Dle (d1 d2 : D) : Prop := - Qle (D_to_Q d1) (D_to_Q d2). + Qle (D_to_Q d1) (D_to_Q d2). (*TODO: There's probably a more efficient way to implement the following:*) Definition Dle_bool (d1 d2 : D) : bool := @@ -1844,7 +1844,7 @@ Proof. Qed. Definition Dlt (d1 d2 : D) : Prop := - Qlt (D_to_Q d1) (D_to_Q d2). + Qlt (D_to_Q d1) (D_to_Q d2). Definition Dlt_bool (d1 d2 : D) : bool := match D_to_Q d1 ?= D_to_Q d2 with @@ -1858,7 +1858,7 @@ Proof. destruct (Qcompare_spec (D_to_Q d1) (D_to_Q d2)); try solve[inversion 1|auto]. unfold Dlt; rewrite Qlt_alt; intros ->; auto. -Qed. +Qed. Lemma Deq_dec (d1 d2 : D) : {d1=d2} + {d1<>d2}. Proof. @@ -1929,7 +1929,7 @@ Definition Dmax (d1 d2 : D) : D := Definition Dlub (max : D) : D := match max with - | DD max => + | DD max => DD (DOlub max) | DQ q => DQ (Qinv q) end. @@ -1998,7 +1998,7 @@ Proof. Qed. Lemma Dlub_ok (d : D) : - 0 <= d -> + 0 <= d -> Dle 0 (d * Dlub d) /\ Dle (d * Dlub d) 1. Proof. intros H. @@ -2026,17 +2026,14 @@ Proof. destruct (Zodd_dec n); auto. destruct (Zeven_odd_dec n); auto. elimtype False; apply n0; auto. -Qed. +Qed. Definition D_of_Dred' (p : Z*nat) : D := let (x,y) := p in DD (Dmake x (Pos.of_nat (S y))). -Eval compute in (log_inf 10). - - Fixpoint Is_Pos_Power2 (p : positive) : option positive := match p with - | xH => None + | xH => None | xO xH => Some xH | xO p' => match Is_Pos_Power2 p' with | None => None @@ -2049,7 +2046,7 @@ Definition Try_Q_to_D (q : Q) : option DO := match Is_Pos_Power2 (Qden q) with | None => if - ((Qden q) =? xH)%positive + ((Qden q) =? xH)%positive then Some (Dmake (2 * (Qnum q))%Z 1) else @@ -2060,7 +2057,7 @@ Definition Try_Q_to_D (q : Q) : option DO := Definition Dred (d : D) : D := match d with - | DD d => + | DD d => DD (DOred d) | DQ q => let qr := Qred q in @@ -2115,11 +2112,11 @@ Proof. rewrite Zmult_assoc. pattern (Z.div2 x * 2)%Z; rewrite Zmult_comm; auto. } apply Qeq_refl. -Qed. +Qed. Lemma Shift_Pos_Not_xI : forall p acc, ~exists res, shift_pos p acc = xI res. Proof. - induction p; intros. + induction p; intros. + intros Hnot; eauto. destruct Hnot. @@ -2153,7 +2150,7 @@ Proof. auto. } Qed. - + Lemma Is_Pow_Pow_Shift_inv : forall p, Is_Pos_Power2 (shift_pos p 1) = Some p. Proof. intros. @@ -2166,7 +2163,7 @@ Proof. apply Pos2Nat.id. Qed. -Lemma Is_Pow_eq_spec : forall p1 p2, +Lemma Is_Pow_eq_spec : forall p1 p2, Is_Pos_Power2 p1~0 = Is_Pos_Power2 p2~0 -> Is_Pos_Power2 p1 = Is_Pos_Power2 p2. @@ -2255,7 +2252,7 @@ Proof. Qed. Lemma Try_Q_to_D_num : forall q d, Try_Q_to_D (Qred q) = Some d -> - num d = Qnum (Qred q) \/ (num d = (2 * (Qnum (Qred q)))%Z) /\ den d = 1%positive. + num d = Qnum (Qred q) \/ (num d = (2 * (Qnum (Qred q)))%Z) /\ den d = 1%positive. Proof. intros q d H1. unfold Try_Q_to_D in H1. @@ -2314,7 +2311,7 @@ Proof. inversion H1. subst. simpl in *. - pose proof H3. + pose proof H3. rewrite <- H2 in H3. apply Is_Pow_eq in H3. destruct H3; auto. @@ -2419,7 +2416,7 @@ Proof. induction n using (well_founded_ind (well_founded_ltof nat id)); auto. Qed. -Lemma Is_Pow2_eq1' : +Lemma Is_Pow2_eq1' : forall p : positive, Is_Pos_Power2 (Pos.succ p) = Some (Pos.of_nat 1) -> 1%positive = p. Proof. destruct p; intros; auto. @@ -2463,7 +2460,7 @@ Proof. } Qed. -Lemma Is_Pow2_eq1 : +Lemma Is_Pow2_eq1 : forall p : positive, Is_Pos_Power2 p = Some (Pos.of_nat 1) -> 2%positive = p. Proof. destruct p; intros; inversion H; auto. @@ -2503,7 +2500,7 @@ Lemma Pow2_xO : forall p q : positive, Is_Pos_Power2 q = Some p -> exists q', xO q' = q. Proof. - induction q; intros; + induction q; intros; simpl in *; eauto. inversion H. @@ -2511,7 +2508,7 @@ Proof. Qed. Lemma Pos_Div2_succ2 : forall p, - (p <> 1)%positive -> + (p <> 1)%positive -> Pos.div2 (Pos.succ (Pos.succ p)) = Pos.succ (Pos.div2 p). Proof. @@ -2520,7 +2517,7 @@ Proof. simpl. lia. Qed. - + Lemma Pos_of_nat_Div2_spec : forall n, Pos.of_nat (Nat.div2 n) = Pos.div2 (Pos.of_nat n). Proof. @@ -2552,16 +2549,11 @@ Proof. rewrite Nat2Pos.inj_succ; try lia. rewrite Nat2Pos.inj_succ; lia. } - { - intros Hnot. - destruct n; auto. - rewrite Nat2Pos.inj_succ in Hnot; try lia. - } } Qed. Lemma Pos_Pow2_xO_spec : forall x p, - (x <> 1)%positive -> + (x <> 1)%positive -> Is_Pos_Power2 x~0 = Some (Pos.of_nat (S p)) -> Is_Pos_Power2 x = Some (Pos.of_nat (p)). Proof. @@ -2590,11 +2582,11 @@ Proof. simpl in *. destruct p; auto; try lia. } -Qed. +Qed. Lemma Pow2_Div : forall p q : nat, - (q > 2) -> - Is_Pos_Power2 (Pos.of_nat q) = Some (Pos.of_nat (S p)) -> + (q > 2) -> + Is_Pos_Power2 (Pos.of_nat q) = Some (Pos.of_nat (S p)) -> Is_Pos_Power2 (Pos.of_nat (q/2)) = Some (Pos.of_nat p). Proof. intros. @@ -2628,8 +2620,8 @@ Proof. Qed. Lemma shift_nat_spec : forall p q, - q <> 0 -> - shift_nat p 1 = Pos.of_nat q -> + q <> 0 -> + shift_nat p 1 = Pos.of_nat q -> shift_nat (S p) 1 = Pos.of_nat (2 * q). Proof. intros. @@ -2687,7 +2679,7 @@ Proof. destruct H0; lia. } { - destruct H0; subst; auto; + destruct H0; subst; auto; simpl in Hnot; try lia. } } @@ -2709,7 +2701,7 @@ Proof. { inversion H. } - { + { intros. simpl in H. inversion H. @@ -2727,7 +2719,7 @@ Proof. rewrite <- Nat.div2_div. destruct q; auto. { - destruct q; auto. + destruct q; auto. { simpl in *. inversion H0. @@ -2737,7 +2729,7 @@ Proof. { rewrite Nat2Pos.id; try lia. } - rewrite H1 at 2. + rewrite H1 at 2. rewrite <- H. rewrite Pos2Nat.inj_mul. rewrite Nat2Pos.id; try lia. @@ -2749,8 +2741,8 @@ Proof. Qed. Lemma Shift_Is_Pos_Pow2_inv_nat' : forall p q, - p <> 0 -> - q <> 0 -> + p <> 0 -> + q <> 0 -> Is_Pos_Power2 (Pos.of_nat q) = Some (Pos.of_nat p) -> shift_nat p 1 = (Pos.of_nat q). Proof. @@ -2826,7 +2818,7 @@ Proof. auto. Qed. -Lemma Shift_Is_Pos_Pow2_inv : forall p q, +Lemma Shift_Is_Pos_Pow2_inv : forall p q, Is_Pos_Power2 ((Qden (Qred q))) = Some p -> shift_pos p 1 = (Qden (Qred q)). Proof. @@ -2925,7 +2917,7 @@ Proof. Lemma QeqD_is_pow2 : forall q d, - q == DO_to_Q d -> + q == DO_to_Q d -> Try_Q_to_D (Qred q) = None -> False. Proof. intros q d H H1. @@ -2955,7 +2947,7 @@ Proof. destruct (num0) eqn:H2. { simpl in H1. - inversion H1; + inversion H1; subst. simpl in *. lia. @@ -3078,8 +3070,15 @@ Proof. destruct (Zeven_dec z); auto. apply Zodd_not_Zeven in H; contradiction. } destruct (Dred' x y); simpl in H|-*; rewrite H; auto. -Qed. - +Qed. + +Lemma Qred_inv : forall q, Qred (Qred q) = Qred q. +Proof. + intros. + apply Qred_complete. + apply Qred_correct. +Qed. + Lemma Dred_idem d : Dred (Dred d) = Dred d. Proof. destruct d. @@ -3098,7 +3097,7 @@ Proof. unfold DO_of_DOred'. destruct (DOred' _ _) eqn:H. rewrite Hm in H. - rewrite <- Hm in H. + rewrite <- Hm in H. destruct ((Init.Nat.pred (Pos.to_nat (den (DOred d))))) eqn:H1; subst. { @@ -3113,7 +3112,7 @@ Proof. rewrite H0. auto. } - { + { simpl in H. destruct Zeven_dec eqn:He. { @@ -3127,7 +3126,7 @@ Proof. simpl in H1. inversion H1. } - } + } { inversion H; subst; auto. rewrite Hm in *. @@ -3141,16 +3140,17 @@ Proof. { destruct (Try_Q_to_D (Qred (Qred q))) eqn:Hm1. { - (* Qred of Qred is Qred *) - admit. + rewrite Qred_inv in Hm1. + exfalso. + rewrite Hm in Hm1. + inversion Hm1. } - { - (* Qred of Qred is Qred *) - admit. + { + rewrite Qred_inv; auto. } } } -Admitted. +Qed. Close Scope positive_scope. Close Scope nat_scope. @@ -3161,11 +3161,11 @@ Module DRed. pf : Dred d = d }. Definition build (d : D) : t := @mk (Dred d) (Dred_idem d). - + Program Definition t0 := mk 0 _. Program Definition t1 := mk 1 _. - + Program Definition add (d1 d2 : t) : t := mk (Dred (Dadd d1.(d) d2.(d))) _. Next Obligation. @@ -3179,19 +3179,19 @@ Module DRed. apply Dred_idem. Qed. - Program Definition mult (d1 d2 : t) : t := + Program Definition mult (d1 d2 : t) : t := mk (Dred (Dmult d1.(d) d2.(d))) _. Next Obligation. apply Dred_idem. Qed. - Program Definition opp (dx : t) : t := + Program Definition opp (dx : t) : t := mk (Dred (Dopp dx.(d))) _. Next Obligation. apply Dred_idem. Qed. - Program Definition lub (dx : t) : t := + Program Definition lub (dx : t) : t := mk (Dred (Dlub dx.(d))) _. Next Obligation. apply Dred_idem. @@ -3211,19 +3211,19 @@ Module DRed. destruct d1 as [x1 pf1]; destruct d2 as [x2 pf2]; simpl. intros H; assert (H2: x1 = x2). { - + rewrite <-pf1, <-pf2; apply Dred_complete; auto. } generalize pf1 pf2; rewrite H2; intros; f_equal; apply proof_irrelevance. Qed. - + Lemma addP d1 d2 : D_to_Q (d (add d1 d2)) == (D_to_Q (d d1) + D_to_Q (d d2))%Q. Proof. unfold add; simpl. rewrite Dred_correct. rewrite Dadd_ok; apply Qeq_refl. - Qed. - + Qed. + Lemma addC d1 d2 : add d1 d2 = add d2 d1. Proof. apply Dred_eq; simpl; rewrite 2!Dred_correct, 2!Dadd_ok. @@ -3235,7 +3235,7 @@ Module DRed. apply Dred_eq; simpl. rewrite !Dred_correct, !Dadd_ok, !Dred_correct, !Dadd_ok. apply Qplus_assoc. - Qed. + Qed. Lemma add0l d : add t0 d = d. Proof. @@ -3243,8 +3243,8 @@ Module DRed. generalize (add_obligation_1 {|d:=0;pf:=t0_obligation_1|} d). unfold DRed.d; rewrite Dred_correct; intros e. rewrite Dadd_ok, D_to_Q0, Qplus_0_l; apply Qeq_refl. - Qed. - + Qed. + Lemma subP d1 d2 : D_to_Q (d (sub d1 d2)) == (D_to_Q (d d1) - D_to_Q (d d2))%Q. Proof. @@ -3259,8 +3259,8 @@ Module DRed. unfold mult; simpl. rewrite Dred_correct. rewrite Dmult_ok; apply Qeq_refl. - Qed. - + Qed. + Lemma multC d1 d2 : mult d1 d2 = mult d2 d1. Proof. apply Dred_eq; simpl; rewrite 2!Dred_correct, 2!Dmult_ok. @@ -3272,7 +3272,7 @@ Module DRed. apply Dred_eq; simpl. rewrite !Dred_correct, !Dmult_ok, !Dred_correct, !Dmult_ok. apply Qmult_assoc. - Qed. + Qed. Lemma oppP dx : D_to_Q (d (opp dx)) == (- D_to_Q (d dx))%Q. @@ -3296,7 +3296,7 @@ Module DRed. Proof. intros. apply Dred_eq. - rewrite addP. + rewrite addP. simpl. rewrite D_to_Q0. rewrite Dred_correct. @@ -3304,7 +3304,7 @@ Module DRed. rewrite Qplus_comm. apply Qplus_opp_r. Qed. - + Lemma addNegDistr: forall d1 d2, opp (add d1 d2) = add (opp d1) (opp d2). Proof. intros. @@ -3355,7 +3355,7 @@ Module DRed. apply Qle_lteq. destruct H; auto. rewrite H. - right. + right. apply Qeq_refl. } intros. @@ -3383,7 +3383,7 @@ Module DRed. repeat (rewrite addP). apply Qplus_lt_le_compat; auto. Qed. - + Lemma plus_lt_compat_l : forall t t1 t2 : t, Dlt t1 t2 -> Dlt (add t t1) (add t t2). Proof. intros. @@ -3395,18 +3395,18 @@ Module DRed. Qed. - - + + Lemma lt_t0_t1: t0 < t1. Proof. unfold Dlt. rewrite D_to_Q0. rewrite D_to_Q1. unfold Qlt, Z.lt. - auto. + auto. Qed. - Lemma mult_le_compat: + Lemma mult_le_compat: forall (r1 r2 r3 r4 : t) , Dle t0 r1 -> Dle t0 r3 -> Dle r1 r2 -> Dle r3 r4 -> Dle (mult r1 r3) (mult r2 r4). Proof. @@ -3462,7 +3462,7 @@ Module DRed. apply Zmult_le_0_compat. { unfold Qle in H. - simpl in *. + simpl in *. rewrite Z.mul_1_r in H. auto. } @@ -3481,7 +3481,7 @@ Module DRed. rewrite Z.mul_comm with (QDen q3) (Qnum q4). auto. Qed. - + Lemma mult_lt_compat_l : forall r r1 r2 : t, Dlt t0 r -> (Dlt r1 r2 <-> Dlt (mult r r1) (mult r r2)). Proof. unfold Dlt. @@ -3508,7 +3508,7 @@ Module DRed. 2 :{ unfold Z.lt. auto. } repeat rewrite <- Z.mul_assoc in H0. rewrite Z.mul_comm in H0. - rewrite Z.mul_comm with (Qnum (D_to_Q r)) + rewrite Z.mul_comm with (Qnum (D_to_Q r)) ((Qnum (D_to_Q r2) * Z.pos (Qden (D_to_Q r) * Qden (D_to_Q r1)))%Z) in H0. apply Zmult_gt_0_lt_reg_r in H0. @@ -3520,7 +3520,7 @@ Module DRed. repeat rewrite Pos2Z.inj_mul in H0. repeat rewrite <- Z.mul_assoc in H0. rewrite Z.mul_comm in H0. - rewrite Z.mul_comm with + rewrite Z.mul_comm with (QDen (D_to_Q r)) (QDen (D_to_Q r1) * Qnum (D_to_Q r2))%Z in H0. @@ -3533,7 +3533,7 @@ Module DRed. Lemma of_natP: forall n : nat, D_to_Q (of_nat n) = (Qmake (2 * (Z.of_nat n)) 2). Proof. auto. Qed. - Lemma of_nat_succ_l: forall n : nat, of_nat (S n) = add t1 (of_nat (n)). + Lemma of_nat_succ_l: forall n : nat, of_nat (S n) = add t1 (of_nat (n)). Proof. intros. apply Dred_eq. @@ -3583,8 +3583,8 @@ Module DRed. Proof. intros. destruct Deq_dec with (d d1) (d d2). - { - left. + { + left. destruct d1,d2. simpl in e. generalize pf0 pf1. @@ -3627,7 +3627,7 @@ Module DRed. intros. apply Qlt_trans with (D_to_Q d2); auto. Qed. - + Lemma total_order_T : forall d1 d2 : t, {Dlt d1 d2} + {d1 = d2} + {Dlt d2 d1}. Proof. @@ -3641,7 +3641,7 @@ Module DRed. auto. Qed. (* TODO: More lemmas here! *) -End DRed. +End DRed. Coercion DRed.d : DRed.t >-> D. @@ -3663,9 +3663,3 @@ Infix "*" := DRed.mult : DRed_scope. Notation "'0'" := DRed.t0 : DRed_scope. Notation "'1'" := DRed.t1 : DRed_scope. - - - - - - diff --git a/enumerables.v b/enumerables.v index e9c2790..9d95336 100644 --- a/enumerables.v +++ b/enumerables.v @@ -12,10 +12,10 @@ From mathcomp Require Import all_algebra. Import GRing.Theory Num.Def Num.Theory. Require Import OUVerT.extrema. Require Import OUVerT.numerics. -Require Import OUVerT.dyadic. +Require Import OUVerT.dyadic. Require Import OUVerT.strings. Require Import OUVerT.compile. -(*The computable state representation is an FMap over +(*The computable state representation is an FMap over player indices, represented as positive.*) Require Import Coq.FSets.FMapAVL Coq.FSets.FMapFacts. Require Import Structures.Orders NArith. @@ -31,11 +31,11 @@ Module Enum_table. Defined. - Lemma nonempty_head_correct: forall (T : Type) (l : list T) (x : T) (H : O <> length (x :: l)), + Lemma nonempty_head_correct: forall (T : Type) (l : list T) (x : T) (H : O <> length (x :: l)), @nonempty_head T (x :: l) H = x. Proof. auto. Qed. - Lemma nonempty_head_map: forall (T1 T2 : Type) (l : list T1) (f : T1->T2) + Lemma nonempty_head_map: forall (T1 T2 : Type) (l : list T1) (f : T1->T2) (H : O <> length l) (H0 : O <> length (map f l)), f (nonempty_head (l:=l) H) = @nonempty_head T2 (map f l) H0. Proof. @@ -44,7 +44,7 @@ Module Enum_table. { exfalso. auto. } rewrite -> nonempty_head_correct. auto. Qed. - + (**Finds the index of an element if it is in the list, otherwise returns the length of the list**) Fixpoint index_of (T : Type) (l : list T) (f : T->bool) : nat := @@ -66,27 +66,27 @@ Module Enum_table. Lemma nth_seq_nth_same: forall (T : Type) (l : list T) (A : T) (n : nat), nth n l A = seq.nth A l n. - Proof. intros. + Proof. intros. generalize dependent n. induction l. destruct n; auto. intros. - simpl. + simpl. destruct n; simpl; auto. - Qed. + Qed. Lemma length_size_eq: forall (T : Type) (l : list T), length l = size l. - Proof. intros. auto. Qed. + Proof. intros. auto. Qed. + - Lemma in_zip_swap: forall {T1 T2 : Type} (l1 : list T1) (l2 : list T2) (t1 : T1) (t2 : T2), In (t1,t2) (zip l1 l2) -> In (t2,t1) (zip l2 l1). - Proof. + Proof. intros. generalize dependent l1. induction l2; intros; auto. - { + { simpl in H. induction l1; auto. } @@ -97,7 +97,7 @@ Module Enum_table. inversion H. auto. Qed. - + (**Lemma eqType_eq_dec: forall (T : eqType) (x y : T), {x = y} + {x <> y}. Proof. intros. @@ -142,7 +142,7 @@ Module Enum_table. intros. induction l; auto. inversion H. - simpl. + simpl. destruct (eqb t1 a) eqn:e; auto. apply IHl. simpl in H. @@ -166,7 +166,7 @@ Module Enum_table. intros. generalize dependent l. induction n. - { + { intros. destruct l; auto. simpl. @@ -174,7 +174,7 @@ Module Enum_table. } intros. destruct l; auto. - inversion H0. + inversion H0. simpl. destruct (eqb (nth n l A) t) eqn:e; auto. { @@ -206,20 +206,20 @@ Module Enum_table. Variable T1_enum_ok : @Enum_ok T1 T1_enum. Variable T1_enum_ne : O <> length T1_enum. Variable T1_eqdec : forall t1 t2 : T1, {t1 = t2} + {t1 <> t2}. - + Record table : Type := table_mk { t_list : list T2; t_list_length : length T1_enum = length t_list - }. + }. Program Definition table_head (t : table) : T2 := @nonempty_head T2 (t_list t) _. Next Obligation. rewrite <- (t_list_length t). apply T1_enum_ne. Defined. Definition enum_head (t : table) : T1 := @nonempty_head T1 T1_enum T1_enum_ne. - + Definition lookup (t : table) (x : T1) : T2 := nth (index_of T1_enum (T1_eqdec x)) (t_list t) (table_head t). @@ -239,13 +239,13 @@ Module Enum_table. rewrite (t_list_length t). repeat rewrite length_size_eq. unfold minn. - destruct (size (t_list t) < size (t_list t))%N; auto. + destruct (size (t_list t) < size (t_list t))%nat; auto. Qed. Lemma nth_lookup: forall (t : table) (n : nat) (x A1: T1) (y A2 : T2) , (n < length T1_enum)%coq_nat -> nth n T1_enum A1 = x -> nth n (t_list t) A2 = y -> lookup t x = y. - Proof. + Proof. intros. unfold lookup. rewrite <- H0. @@ -274,17 +274,17 @@ Module Enum_table. Qed. Lemma lookup_map: forall (f : T1->T2) (x : T1), @lookup (map_to_table f) x = f x. - Proof. - intros. + Proof. + intros. unfold lookup. simpl. rewrite table_head_map. rewrite -> map_nth. rewrite nth_index_of_eqb; intros; auto. destruct T1_enum_ok. auto. - Qed. + Qed. Lemma zip_table_map: forall (f : T1->T2), zip_table (map_to_table f) = map (fun x => (x, f x)) T1_enum. - Proof. + Proof. intros. unfold map_to_table. unfold zip_table. simpl. rewrite zip_map. auto. @@ -298,17 +298,17 @@ Module Enum_table. generalize dependent (map_to_table_obligation_1 f1). rewrite -> H. intros. f_equal. apply proof_irrelevance. - Qed. - + Qed. + End enum_table. - Definition table_eqb (T1 T2 : eqType) (T1_enum : Enumerable T1) (t1 t2 : table T2 T1_enum) : bool := + Definition table_eqb (T1 T2 : eqType) (T1_enum : Enumerable T1) (t1 t2 : table T2 T1_enum) : bool := eq_op (t_list t1) (t_list t2). - Definition table_eqb_func (T1 T2 : eqType) (T1_enum : Enumerable T1) - (t : table T2 T1_enum) (f : T1->T2) : bool := + Definition table_eqb_func (T1 T2 : eqType) (T1_enum : Enumerable T1) + (t : table T2 T1_enum) (f : T1->T2) : bool := table_eqb t (map_to_table T1_enum f). @@ -316,7 +316,7 @@ Module Enum_table. Proof. intros. unfold table_eqb. - destruct (eq_op (t_list x) (t_list y)) eqn:e. + destruct (eq_op (t_list x) (t_list y)) eqn:e. { constructor. assert(t_list x = t_list y). @@ -335,7 +335,7 @@ Module Enum_table. Definition table_eqType (T1 T2: eqType) (T1_enum : Enumerable T1) := Equality.Pack (@table_eqMixin T1 T2 T1_enum) (@table T1 T2 T1_enum). **) - + End Enum_table. @@ -352,14 +352,14 @@ Proof. inversion H0. { apply In_InA; auto. rewrite <- H2. apply in_map. apply in_eq. } simpl. auto. - } + } induction l. inversion H0. inversion H0; auto. -Qed. +Qed. Lemma NoDupA_map_inj: forall (T1 T2 : Type) (l : list T1) (f : T1->T2), - NoDupA (fun x : T1 => [eta eq x]) l -> + NoDupA (fun x : T1 => [eta eq x]) l -> (forall (t1 t2 : T1), f t1 = f t2 -> t1 = t2) -> NoDupA (fun x : T2 => [eta eq x]) (map f l). Proof. @@ -386,7 +386,7 @@ Qed. Lemma prodEnumerableInstance_nodup: forall (aT bT: Type) (la : Enumerable aT) (lb : Enumerable bT), NoDupA (fun x : aT => [eta eq x]) (enumerate _ la) -> - NoDupA (fun x : bT => [eta eq x]) (enumerate _ lb) -> + NoDupA (fun x : bT => [eta eq x]) (enumerate _ lb) -> NoDupA (fun x : aT * bT => [eta eq x]) (prodEnumerableInstance la lb). Proof. intros. @@ -404,7 +404,7 @@ Proof. rewrite -> InA_alt in H5. destruct H5. destruct H5. rewrite <- H5 in H7. clear H5. clear x1. rewrite -> InA_alt in H6. - destruct H6. + destruct H6. destruct H5. rewrite <- H5 in H6. clear H5. clear x1. @@ -423,7 +423,7 @@ Lemma prodEnumerableInstance_ok (aT bT: Type) (enumerableA : Enumerable aT) (enumerableB : Enumerable bT) (enum_okA: @Enum_ok aT enumerableA) - (enum_okB: @Enum_ok bT enumerableB) + (enum_okB: @Enum_ok bT enumerableB) : @Enum_ok _ (prodEnumerableInstance enumerableA enumerableB). destruct enum_okA. destruct enum_okB. @@ -464,7 +464,7 @@ end. Lemma in_cons_all: forall (T : Type) (a : T) (l l1: list T) (l2 : list (list T)), (In a l1 /\ In l l2) <-> In (a :: l) (cons_all l1 l2). -Proof. +Proof. intros. split; intros. { @@ -484,7 +484,7 @@ Proof. split. { destruct H. - { + { rewrite -> in_map_iff in H. destruct H. destruct H. @@ -504,8 +504,8 @@ Proof. apply IHl1. auto. Qed. - - + + Lemma cons_all_nonempty: forall {T : Type} (l1 l2 : list T) (l3 : list (list T)), In l1 (cons_all l2 l3) -> l1 <> [::]. Proof. @@ -528,7 +528,7 @@ Proof. Qed. -Lemma in_list_enum_cons: forall {T : Type} (l1 l2 : list T) (x : T) (n : nat), +Lemma in_list_enum_cons: forall {T : Type} (l1 l2 : list T) (x : T) (n : nat), In l1 (list_enum l2 n) -> In l1 (list_enum (x :: l2) n). Proof. intros. @@ -562,7 +562,7 @@ Proof. exfalso. eapply cons_all_nonempty; eauto. simpl. apply in_cons_all in H. - destruct H. + destruct H. erewrite IHn; eauto. Qed. @@ -602,7 +602,7 @@ Next Obligation. apply list_enum_len with l. auto. Defined. -Lemma no_dup_cons_all: forall (T : Type) (l : list T) (l2 : list (list T)), +Lemma no_dup_cons_all: forall (T : Type) (l : list T) (l2 : list (list T)), NoDupA (fun x => [eta eq x]) l -> NoDupA (fun x => [eta eq x]) l2 -> NoDupA (fun x => [eta eq x]) (cons_all l l2). Proof. intros. @@ -611,7 +611,7 @@ Proof. { simpl. constructor. } intros. simpl. apply NoDupA_app; auto. - { + { apply NoDupA_map_inj; auto. intros. inversion H1. auto. @@ -635,12 +635,12 @@ Proof. destruct H3. destruct H3. inversion H3. rewrite H7 in H4. clear H3 H7 x0. - inversion H. apply H7. + inversion H. apply H7. apply InA_alt. eauto. Qed. -Lemma no_dup_enum_list: forall (T : Type) (l : list T) (n : nat), +Lemma no_dup_enum_list: forall (T : Type) (l : list T) (n : nat), NoDupA (fun x => [eta eq x]) l -> NoDupA (fun x => [eta eq x]) (list_enum l n). Proof. intros. @@ -662,7 +662,7 @@ Proof. simpl in *. intros. destruct H1. inversion H1. auto. - right. eapply IHl. + right. eapply IHl. assert (forall H', (list_to_list_len (l:=l) H') = (list_to_list_len (l:=l) (fun (l'0 : seq.seq T) (H0 : In l'0 l) => H l'0 (or_intror H0)))). { intros. f_equal. apply proof_irrelevance. } erewrite H2. apply H1. @@ -680,10 +680,10 @@ Proof. intros. f_equal. apply proof_irrelevance. Unshelve. auto. Qed. - + Lemma no_dup_list_to_len_list: forall (T : Type) (l : list (list T)) (n : nat) (H : forall l' : list T, In l' l -> length l' = n), NoDupA (fun x => [eta eq x]) l -> NoDupA (fun x => [eta eq x]) (@list_to_list_len T l n H). -Proof. +Proof. intros. generalize dependent n. generalize dependent H0. @@ -691,7 +691,7 @@ Proof. simpl. constructor. simpl in *. intros. - inversion H0. + inversion H0. constructor. 2: { apply IHl. auto. } unfold not. @@ -705,8 +705,8 @@ Proof. rewrite <- H5 in H6. eauto. Qed. - - + + Lemma list_len_enumerate_ok: forall (T : Type) (enum : Enumerable T) (enum_ok : @Enum_ok T enum) (n : nat), @Enum_ok (@list_len T n) (@enumerable_fun (@list_len T n) (@list_len_enumerate T enum n)). Proof. @@ -736,7 +736,7 @@ Proof. destruct a. apply in_list_to_len_list; auto. simpl. - unfold enumerable_fun in enum_total0. + unfold enumerable_fun in enum_total0. unfold list_len_enumerate in enum_total0. destruct list_len_l0. { inversion list_len_ok0. } @@ -750,10 +750,10 @@ Proof. Qed. -Program Definition enumerate_table {T1 T2 : Type} (T1_eqdec : forall a b : T1, {a = b} + {a <> b}) (T1_enum : Enumerable T1) (T2_enum : Enumerable T2) +Program Definition enumerate_table {T1 T2 : Type} (T1_eqdec : forall a b : T1, {a = b} + {a <> b}) (T1_enum : Enumerable T1) (T2_enum : Enumerable T2) (T1_enum_ok : @Enum_ok T1 T1_enum) (T2_enum_ok : @Enum_ok T2 T2_enum) (T1_enum_ne : O <> length T1_enum) : Enumerable (@Enum_table.table T1 T2 T1_enum) - := map (fun l => @Enum_table.table_mk T1 T2 T1_enum (list_len_l l) _) + := map (fun l => @Enum_table.table_mk T1 T2 T1_enum (list_len_l l) _) (list_len_enumerate (enumerate T2) (length (enumerate T1))). Next Obligation. destruct l. auto. @@ -787,7 +787,7 @@ Proof. rewrite length_cons_all. apply lt_0_neq. apply Nat.mul_pos_pos. - { + { destruct (length l). exfalso. apply H. auto. apply Nat.lt_0_succ. @@ -796,10 +796,10 @@ Proof. exfalso. apply IHn. auto. apply Nat.lt_0_succ. Qed. - -Lemma enumerate_table_nonempty: forall {T1 T2 : Type} (T1_eqdec : forall a b : T1, {a = b} + {a <> b}) T1_enum T2_enum T1_enum_ok T2_enum_ok T1_enum_ne , + +Lemma enumerate_table_nonempty: forall {T1 T2 : Type} (T1_eqdec : forall a b : T1, {a = b} + {a <> b}) T1_enum T2_enum T1_enum_ok T2_enum_ok T1_enum_ne , O <> (length T2_enum) -> O <> length (@enumerate_table T1 T2 T1_eqdec T1_enum T2_enum T1_enum_ok T2_enum_ok T1_enum_ne ). Proof. intros. @@ -808,22 +808,22 @@ Proof. rewrite Enum_table.length_size_eq. rewrite size_map. unfold list_len_enumerate. - rewrite <- Enum_table.length_size_eq. + rewrite <- Enum_table.length_size_eq. rewrite length_list_to_list_len; auto. apply list_enum_nonempty. auto. Qed. - + Lemma NoDupA_map: forall (T1 T2 : Type) (f : T1->T2) (l : list T1), (forall (x y : T1), f x = f y -> x = y) -> NoDupA (fun x=> [eta eq x]) l -> NoDupA (fun x => [eta eq x]) (map f l). -Proof. +Proof. intros. induction l; simpl; auto. constructor. { inversion H0. - unfold not. intros. + unfold not. intros. apply H3. apply In_InA; auto. rewrite -> InA_alt in H5. @@ -841,14 +841,14 @@ Qed. -Lemma enum_table_total: forall {T1 T2 : Type} (T1_eqdec : forall a b : T1, {a = b} + {a <> b}) (T1_enum : Enumerable T1) (T2_enum : Enumerable T2) +Lemma enum_table_total: forall {T1 T2 : Type} (T1_eqdec : forall a b : T1, {a = b} + {a <> b}) (T1_enum : Enumerable T1) (T2_enum : Enumerable T2) (T1_enum_ok : @Enum_ok T1 T1_enum) (T2_enum_ok : @Enum_ok T2 T2_enum) (T1_enum_ne : O <> length T1_enum) (t : (@Enum_table.table T1 T2 T1_enum)), In t (@enumerate_table T1 T2 T1_eqdec T1_enum T2_enum _ _ T1_enum_ne). Proof. intros. unfold enumerate_table. - destruct list_len_enumerate_ok with T2 T2_enum (length (enumerate T1)); auto. + destruct list_len_enumerate_ok with T2 T2_enum (length (enumerate T1)); auto. erewrite in_map_iff. destruct t. assert(length t_list = (length (enumerate T1))). @@ -861,16 +861,16 @@ Proof. Qed. -Lemma enum_table_ok: forall {T1 T2 : Type} (T1_eqdec : forall a b : T1, {a = b} + {a <> b}) (T1_enum : Enumerable T1) (T2_enum : Enumerable T2) +Lemma enum_table_ok: forall {T1 T2 : Type} (T1_eqdec : forall a b : T1, {a = b} + {a <> b}) (T1_enum : Enumerable T1) (T2_enum : Enumerable T2) (T1_enum_ok : @Enum_ok T1 T1_enum) (T2_enum_ok : @Enum_ok T2 T2_enum) (T1_enum_ne : O <> length T1_enum), @Enum_ok (@Enum_table.table T1 T2 T1_enum) (@enumerate_table T1 T2 T1_eqdec T1_enum T2_enum _ _ T1_enum_ne). Proof. intros. constructor; unfold enumerable_fun. - { + { apply NoDupA_map. - { - intros. inversion H. + { + intros. inversion H. destruct x. destruct y. unfold list_len_l in H1. generalize list_len_ok0. @@ -913,7 +913,7 @@ Proof. inversion H0. simpl in H0. destruct H0. - { + { destruct p. simpl in *. by inversion H0. @@ -957,7 +957,7 @@ Qed. Lemma enum_nat_ok: forall n : nat, @Enum_ok (enum_nat n) (enum_nat_enumerate n). Proof. - intros. + intros. constructor; unfold enumerable_fun; unfold enum_nat_enumerate. { diff --git a/expfacts.v b/expfacts.v index 18c916d..cbd9196 100644 --- a/expfacts.v +++ b/expfacts.v @@ -213,7 +213,7 @@ Proof. Qed. Lemma ln_Taylor_lower x : (x <= 1/2 -> -x - x^2 <= ln (1 - x))%R. -Proof. +Proof. intros H. rewrite -[(-x - x^2)%R] ln_exp. apply ln_le; first by apply exp_pos. @@ -273,6 +273,7 @@ Proof. move => ->; rewrite exp_ln; lra. Qed. +#[local] Open Scope R_scope. Lemma exp_mult x y : exp (x * INR y) = exp x ^ y. Proof. apply: ln_inv; try apply: exp_pos. @@ -283,19 +284,19 @@ Proof. { rewrite -IH; clear IH; case: n. { by rewrite Rmult_1_r ln_exp /= Rmult_0_r Rplus_0_r. } by move => n; rewrite ln_exp // Rmult_plus_distr_l Rmult_1_r Rplus_comm. } - apply: pow_lt; apply: exp_pos. + apply: pow_lt; apply: exp_pos. Qed. Lemma exp_le_inv : forall x y : R, exp x <= exp y -> x <= y. Proof. intros. inversion H. left. apply exp_lt_inv; auto. - right. apply exp_inv. auto. + right. apply exp_inv. auto. Qed. -Lemma derive_decreasing_interv : +Lemma derive_decreasing_interv : forall (a b : R) (f : R -> R) (pr : derivable f), - a < b -> + a < b -> (forall t : R, a < t < b -> derive_pt f t (pr t) < 0) -> forall x y : R, a <= x <= b -> a <= y <= b -> x < y -> f y < f x. Proof. @@ -343,7 +344,7 @@ Proof. erewrite derive_pt_minus. 2: (intros; reflexivity). erewrite null_derivative_0. - 2: constructor. + 2: constructor. erewrite derive_pt_id. ring_simplify. erewrite pr_nu_var. erewrite derive_pt_mult. @@ -377,19 +378,19 @@ Proof. apply derivable_const. apply derivable_id. Qed. -Lemma ln_upper_01_aux_bot c : +Lemma ln_upper_01_aux_bot c : 0 = 1 - 0 + 0 * exp c - exp (c * 0). Proof. rewrite Rmult_0_r exp_0. ring. Qed. -Lemma ln_upper_01_aux_top c : +Lemma ln_upper_01_aux_top c : 0 = 1 - 1 + 1 * exp c - exp (c * 1). Proof. rewrite Rmult_1_r Rmult_1_l. ring. Qed. -Lemma ln_upper_01_aux_deriv_at_top c : +Lemma ln_upper_01_aux_deriv_at_top c : 0 <= @derive_pt (fun x => 1 - x + x * exp c - exp (c * x)) 0 (ln_upper_01_aux_deriv c 0). Proof. @@ -398,7 +399,7 @@ Proof. move: (ln_Taylor_upper' c) => H. lra. Qed. -Lemma ln_upper_01_aux_deriv_at_bot c : +Lemma ln_upper_01_aux_deriv_at_bot c : 0 >= @derive_pt (fun x => 1 - x + x * exp c - exp (c * x)) 1(ln_upper_01_aux_deriv c 1). Proof. @@ -456,7 +457,7 @@ Proof. repeat (try apply derivable_plus; try apply derivable_id; try apply derivable_mult; - try apply derivable_opp; + try apply derivable_opp; try apply derivable_exp; try apply derivable_const). Qed. @@ -489,7 +490,7 @@ Proof. Qed. Lemma ln_upper_01_aux_deriv_2_decreasing c : - c <> 0 -> + c <> 0 -> strict_decreasing (fun x => - 1 + exp c - c * exp (c * x)). Proof. intros cNeq. @@ -548,7 +549,7 @@ Lemma ln_upper_01 x c : 0 < x < 1 -> c * x <= ln (1 - x + x * exp c). Proof. - intros. + intros. apply exp_le_inv. rewrite exp_ln. case: (Req_EM_T c 0); intros. @@ -562,7 +563,7 @@ Proof. set f' := fun x => -1 + exp c - c * exp (c * x). replace (1 - x + x * exp c - exp (c * x)) with (f x); last by auto. move: (Rolle f 0 1) => H_rolle. - assert (0 < 1) as duh by lra. + assert (0 < 1) as duh by lra. assert (f 0 = f 1) as H_bounds by (rewrite /f -(ln_upper_01_aux_bot c) -(ln_upper_01_aux_top c); auto). specialize (H_rolle @@ -611,7 +612,7 @@ Proof. replace (1 - x + x * exp c) with (1 - (x * (1 - exp c))); last by ring. assert (1 - exp c < 1). { - move: (exp_pos c) => H0. lra. + move: (exp_pos c) => H0. lra. } move: (Rtotal_order (1 - exp c) 0) => H1. apply Rlt_Rminus. @@ -619,11 +620,11 @@ Proof. * inversion H. apply (@Rlt_trans _ 0 _). apply Ropp_lt_cancel. assert (- ( 1 - exp c ) > 0) by lra. - replace (- (x * (1 - exp c))) with (x * - (1 - exp c)); last by ring. + replace (- (x * (1 - exp c))) with (x * - (1 - exp c)); last by ring. replace (- 0) with 0; last by ring. - apply Rmult_lt_0_compat; lra. lra. + apply Rmult_lt_0_compat; lra. lra. * rewrite H1. lra. - * replace 1 with (1 * 1) at 2. inversion H. + * replace 1 with (1 * 1) at 2. inversion H. apply Rmult_le_0_lt_compat; lra. ring. } Qed. @@ -644,7 +645,7 @@ Proof. { move/exp_increasing => H; left; apply: Rlt_le_trans; first by apply: H. rewrite exp_ln //; apply: Rle_refl. } move => ->; rewrite exp_ln //; apply: Rle_refl. -Qed. +Qed. (* Lemmas in support of Gibbs' inequality. *) @@ -656,7 +657,7 @@ Proof. rewrite <- exp_0 at 1. f_equal. field. Qed. -Lemma derivable_exp_minus_1_minus_x : derivable (fun x => exp(x-1) -x). +Lemma derivable_exp_minus_1_minus_x : derivable (fun x => exp(x-1) -x). Proof. rewrite /derivable => x. apply derivable_pt_minus. @@ -670,7 +671,7 @@ Proof. apply derivable_pt_id. Defined. -Lemma deriv_at_point_exp_minus_1_minus_x : +Lemma deriv_at_point_exp_minus_1_minus_x : forall x pf, derive_pt (fun x => exp(x-1) -x) x pf = exp(x-1) -1. Proof. @@ -680,7 +681,7 @@ Proof. derive_pt_comp derive_pt_minus derive_pt_id - derive_pt_const + derive_pt_const derive_pt_exp. field. Qed. diff --git a/extrema.v b/extrema.v index ddaaea0..344b923 100644 --- a/extrema.v +++ b/extrema.v @@ -20,9 +20,9 @@ Section Extrema. (** The primary parameters are: - [rty : realFieldType] A real field - [I : finType] A finite type - - [P : pred I] A subset of [I] - - [F : I -> rty] A "valuation" function over [I] - The module implements the following functions: + - [P : pred I] A subset of [I] + - [F : I -> rty] A "valuation" function over [I] + The module implements the following functions: - [arg_min] An [i : I \in P] that minimizes [F] - [arg_max] An [i : I \in P] that maximizes [F] - [min] := [F arg_min] @@ -47,7 +47,7 @@ Section Extrema. ord (F (getOrd i1 l)) (F (getOrd i2 l)). Proof. move: i1 i2; elim: l=> // a l IH i1 i2 H /=. - case H2: (ord (F i1) (F a)). + case H2: (ord (F i1) (F a)). { by case H3: (ord (F i2) (F a)); apply: IH. } case H3: (ord (F i2) _)=> //. @@ -56,7 +56,7 @@ Section Extrema. { by apply: ord_trans; first by apply: H. } by rewrite H4 in H2. - Qed. + Qed. Lemma getOrd_minimalIn i0 l : [&& ord (F (getOrd i0 l)) (F i0) @@ -69,8 +69,8 @@ Section Extrema. move=> a l IH i0. apply/andP; split. { simpl; case H2: (ord (F i0) _)=> //. - by case: (andP (IH i0)). - apply: ord_trans. + by case: (andP (IH i0)). + apply: ord_trans. case: (andP (IH a))=> H3 _; apply: H3. by case: (orP (ord_total (F i0) (F a))); first by rewrite H2. } @@ -92,7 +92,7 @@ Section Extrema. Qed. Definition getOrd_tot i0 := getOrd i0 (enum I). - + Lemma getOrd_totP i0 : [forall i, ord (F (getOrd_tot i0)) (F i)]. Proof. case: (andP (getOrd_minimalIn i0 (enum I)))=> H H2. @@ -108,8 +108,8 @@ Section Extrema. Proof. rewrite /getOrd_sub; move: (enum I)=> l. elim: l=> // a l /=. - case H: (P a)=> //=. - case: (ord _ _)=> //. + case H: (P a)=> //=. + case: (ord _ _)=> //. elim: l a H i0 Hi0 => //= a0 l IH a H i0 Hi0. case H2: (P a0)=> //=. case: (ord _ _). @@ -119,8 +119,8 @@ Section Extrema. case: (ord _ _)=> //. by apply: IH. by apply: IH. - Qed. - + Qed. + Lemma getOrd_subP i0 (Hi0 : P i0) : [&& P (getOrd_sub i0) & [forall (i | P i), ord (F (getOrd_sub i0)) (F i)]]. @@ -133,12 +133,14 @@ Section Extrema. Qed. End getOrd. + Import mc_1_10.Num.Theory. + Section default. Variable i0 : I. Hypothesis H : P i0. - + Definition arg_max := getOrd_sub ger i0. - + Lemma arg_maxP : [&& P arg_max & [forall (i | P i), F arg_max >= F i]]. Proof. apply: getOrd_subP=> //; rewrite /ger. @@ -153,14 +155,14 @@ Section Extrema. Proof. rewrite /max. by case: (andP arg_maxP). - Qed. - + Qed. + Definition arg_min := getOrd_sub ler i0. Lemma arg_minP : [&& P arg_min & [forall (i | P i), F arg_min <= F i]]. Proof. apply: getOrd_subP=> //. - by apply: ler_trans. + by apply: ler_trans. by apply: ler_total. Qed. @@ -170,8 +172,8 @@ Section Extrema. Proof. rewrite /min. by case: (andP arg_minP). - Qed. - + Qed. + Lemma min_le_max : min <= max. Proof. rewrite /min /max. @@ -220,9 +222,9 @@ Section min_lems. Variables (rty : realFieldType) (I : finType). Lemma arg_min_ext (p1 p2 : pred I) (f g : I -> rty) d1 d2 : - p1 =1 p2 -> + p1 =1 p2 -> f =1 g -> - d1 = d2 -> + d1 = d2 -> arg_min p1 f d1 = arg_min p2 g d2 . Proof. move => H1 H2 ->. @@ -232,13 +234,13 @@ Section min_lems. [seq x <- enum I | p2 x]. { rewrite (eq_in_filter (a2:=p2)) => //. } move: ([seq x <- _ | _]) d2; elim => // a l /= IH. - move => d2; rewrite !H2; case: (_ <= _) => //. + move => d2; rewrite !H2; case: (_ <= _) => //. Qed. - + Lemma min_ext (p1 p2 : pred I) (f g : I -> rty) d1 d2 : - p1 =1 p2 -> + p1 =1 p2 -> f =1 g -> - d1 = d2 -> + d1 = d2 -> min p1 f d1 = min p2 g d2 . Proof. move => H1 H2 ->; rewrite /min. @@ -247,31 +249,31 @@ Section min_lems. Qed. Lemma ler_const_inv (c x y : rat) : - 0 < c -> + 0 < c -> ((c * x <= c * y) = (x <= y)). Proof. move => Hpos; rewrite -(ler_pdivl_mull _ _ Hpos) mulrA mulVf. { by rewrite mul1r. } by apply/eqP => H; rewrite H in Hpos. - Qed. + Qed. Lemma arg_min_const (p : pred I) (f : I -> rat) (c : rat) d : - 0 < c -> + 0 < c -> arg_min p (fun x => c * f x) d = arg_min p f d. Proof. move => Hpos; rewrite /arg_min/getOrd_sub. move: ([seq x <- enum I | p x]) d; elim => // a l IH /= d. rewrite (ler_const_inv _ _ Hpos). case: (f d <= f a) => //. - Qed. - + Qed. + Lemma min_const (p : pred I) (f : I -> rat) (c : rat) d : - 0 < c -> + 0 < c -> min p (fun x => c * f x) d = c * min p f d. Proof. move => Hpos; rewrite /min; f_equal. rewrite arg_min_const //. - Qed. -End min_lems. + Qed. +End min_lems. Local Open Scope Numeric_scope. Delimit Scope Numerics_scope with Num. @@ -286,7 +288,7 @@ Module num_Extrema. Fixpoint max (l : list Nt) : option Nt := match l with | List.nil => None - | x :: l' => + | x :: l' => match max l' with | None => Some x | Some x' => @@ -299,7 +301,7 @@ Module num_Extrema. | None => def | Some x => x end. - + Fixpoint argmax {T : Type} (l : list T) (f : T -> Nt) : option T := match l with @@ -337,7 +339,7 @@ Module num_Extrema. | Some x' => Some (if leb (f x) x' then x' else (f x)) end end. - + Lemma argmax_ne_ok: forall {T : Type} (l : list T) (f : T-> Nt) (h : O <> (length l)), (argmax l f) = Some (argmax_ne f h). @@ -374,7 +376,7 @@ Module num_Extrema. Fixpoint nth_max (l : list Nt) (n : nat) : option Nt := match n with | O => max l - | S n' => + | S n' => match (max l) with | None => None | Some m => nth_max (filter (fun x => ltb x m) l) n' @@ -405,7 +407,7 @@ Module num_Extrema. simpl. destruct (max l); auto. Qed. - + Lemma max_ne_some: forall (l : list Nt), O <> length l <-> exists x, max l = Some x. Proof. intros. @@ -457,7 +459,7 @@ Module num_Extrema. intros. assert (forall (T : Type) (l : list T), length l = size l). auto. rewrite H0. - rewrite mapmax_map_max. + rewrite mapmax_map_max. rewrite <- size_map with T Nt f _. rewrite <- H0. apply max_ne_some. @@ -471,12 +473,12 @@ Module num_Extrema. { exfalso. apply H0. auto. } simpl in *. destruct l. - { simpl. exists a. split; auto. } + { simpl. exists a. split; auto. } destruct IHl; simpl; auto. destruct H1. inversion H1. destruct (length l) eqn:e. - { + { rewrite -> List.length_zero_iff_nil in e. rewrite e; simpl. eexists. split; auto. destruct (leb (f a) (f t)); auto. @@ -508,7 +510,7 @@ Module num_Extrema. inversion H1. destruct (leb (f t) (f x0)) eqn:e3. { - inversion H1. + inversion H1. inversion H2. destruct (leb (f a) (f x)); auto. } @@ -527,9 +529,9 @@ Module num_Extrema. rewrite H3. rewrite mapmax_ne_ok in H1. inversion H1. - auto. + auto. Qed. - + Lemma mapmax_ext: forall (T : Type) (f g : T->Nt) (l : list T), (forall x : T, f x = g x) -> mapmax l f = mapmax l g. Proof. intros. @@ -539,7 +541,7 @@ Module num_Extrema. rewrite H0. auto. Qed. - + Lemma argmax_ext: forall (T : Type) (f g : T->Nt) (l : list T), (forall x : T, f x = g x) -> argmax l f = argmax l g. Proof. intros. @@ -560,7 +562,7 @@ Module num_Extrema. rewrite IHl. destruct (argmax l g); auto. destruct total_order_T with (f a) (f t). - { + { destruct s. { apply le_lt_weak in l0. @@ -651,7 +653,7 @@ Module num_Extrema. repeat rewrite plus_id_l in H0. auto. Qed. - + Lemma argmax_plus_const_l: forall (T : Type) (l : list T) (f : T -> Nt) (x : Nt), argmax l f = argmax l (fun n => x + f n). Proof. @@ -663,7 +665,7 @@ Module num_Extrema. apply plus_le_compat_l_reverse in H0. auto. Qed. - + Lemma argmax_mult_pos_r: forall (T : Type) (l : list T) (f : T -> Nt) (x : Nt), 0 < x -> argmax l f = argmax l (fun n => f n * x). Proof. intros. @@ -683,7 +685,7 @@ Module num_Extrema. { apply mult_le_compat_l; auto. apply le_lt_weak. auto. } apply mult_le_compat_l_reverse in H1; auto. Qed. - + Lemma argmax_ne_mult_pos_r: forall (T : Type) (l : list T) (f : T -> Nt) (x : Nt) (H : O <> length l), 0 < x -> argmax_ne f H = argmax_ne (fun n => f n * x) H. Proof. @@ -697,7 +699,7 @@ Module num_Extrema. inversion H3. auto. Qed. - + Lemma argmax_ne_mult_pos_l: forall (T : Type) (l : list T) (f : T -> Nt) (x : Nt) (H : O <> length l), 0 < x -> argmax_ne f H = argmax_ne (fun n => x * f n) H. Proof. intros. @@ -710,7 +712,7 @@ Module num_Extrema. inversion H3. auto. Qed. - + Lemma mapmax_const: forall (T : Type) (l : list T) (x : Nt), (O <> length l) -> mapmax l (fun _ => x) = Some x. Proof. intros. @@ -722,7 +724,7 @@ Module num_Extrema. rewrite IHl; auto. destruct (leb x x); auto. Qed. - + Lemma mapmax_ne_const: forall (T : Type) (l : list T) (x : Nt) (H : O <> length l), mapmax_ne (fun _ => x) H = x. Proof. intros. @@ -767,7 +769,7 @@ Module num_Extrema. repeat rewrite argmax_ne_mapmax_ne. rewrite <- argmax_ne_mult_pos_l; auto. Qed. - + Lemma argmax_ne_plus_const_r: forall (T : Type) (l : list T) (f : T -> Nt) (x : Nt) (H : O <> length l), argmax_ne f H = argmax_ne (fun n => f n + x) H. Proof. @@ -786,7 +788,7 @@ Module num_Extrema. repeat rewrite argmax_ne_mapmax_ne. rewrite <- argmax_ne_plus_const_r; auto. Qed. - + Lemma argmax_ne_plus_const_l: forall (T : Type) (l : list T) (f : T -> Nt) (x : Nt) (H : O <> length l), argmax_ne f H = argmax_ne (fun n => x + f n) H. Proof. intros. @@ -820,7 +822,7 @@ Module num_Extrema. inversion H3. auto. Qed. - + Lemma max_correct: forall (l : list Nt) (n : Nt), List.In n l -> (exists m, Some m = max l /\ n <= m). Proof. intros. @@ -864,12 +866,12 @@ Module num_Extrema. Lemma max_in: forall (l : list Nt) (x : Nt), max l = Some x -> List.In x l. Proof. - intros. + intros. induction l. { inversion H0. } simpl in *. destruct (max l) eqn:e. - 2: { inversion H0. auto. } + 2: { inversion H0. auto. } destruct (leb a n); auto. inversion H0. auto. Qed. @@ -909,7 +911,7 @@ Module num_Extrema. Lemma filter_none: forall {T : Type} (l : list T) (f : T->bool), filter f l = [::] <-> (forall x : T, List.In x l -> f x = false). - Proof. + Proof. intros. split; intros. { @@ -973,12 +975,12 @@ Module num_Extrema. destruct i. destruct H4. rewrite H0 in H4. inversion H4. clear H4. rewrite H7 in H5. - clear H7. clear x0. + clear H7. clear x0. destruct H5; auto. exfalso. apply lt_not_le with y z; auto. assert(List.In z ([seq x0 <- n :: l | ltb x0 x])). rewrite -> List.filter_In. split; auto. apply ltb_true_iff. auto. - apply max_correct in H5. destruct H5. destruct H5. + apply max_correct in H5. destruct H5. destruct H5. rewrite H1 in H5. inversion H5. rewrite <- H8. auto. Qed. @@ -997,27 +999,27 @@ Module num_Extrema. destruct H1. apply ltb_true_iff. auto. Qed. - + Lemma exists_min_dist_to_max: forall (l : list Nt) (x : Nt), max l = Some x -> (exists e, 0 < e /\ (forall y : Nt, List.In y l -> abs (x + - y) < e -> x = y)). Proof. intros. destruct (nth_max l 1) eqn:eq. - 2:{ + 2:{ exists 1. split. apply plus_id_lt_mult_id. intros. apply second_max_none with l y in eq; auto. rewrite H0 in eq. inversion eq. auto. } exists (x + - n). split. - { + { rewrite <- plus_neg_r with n. apply plus_lt_compat_r. apply second_max_lt_max with l; auto. } intros. rewrite abs_posb in H2. - 2:{ + 2:{ apply leb_true_iff. rewrite <- plus_neg_r with y. apply plus_le_compat_r. @@ -1040,7 +1042,7 @@ Module num_Extrema. assert (max l = Some ( max_ne H0)). { apply max_ne_ok. } assert (exists m, Some m = max l /\ n <= m). - { apply max_correct. auto. } + { apply max_correct. auto. } destruct H3. destruct H3. rewrite H2 in H3. @@ -1065,9 +1067,9 @@ Module num_Extrema. apply List.in_map. auto. Qed. - - Lemma mapmax_ne_cons_le: forall (T : Type) (l : list T) (f : T -> Nt) (t : T) (H0 : O <> length l) (H1 : O <> length (t :: l)), + + Lemma mapmax_ne_cons_le: forall (T : Type) (l : list T) (f : T -> Nt) (t : T) (H0 : O <> length l) (H1 : O <> length (t :: l)), mapmax_ne f H0 <= mapmax_ne f H1. Proof. intros. @@ -1166,7 +1168,7 @@ Module num_Extrema. Lemma mapmax_ne_le_all: forall (T : Type) (l : list T) (f : T -> Nt) (H : O <> length l) (n : Nt), (forall t : T, List.In t l -> n <= f t) -> n <= mapmax_ne f H. - Proof. + Proof. intros. assert (mapmax l f = Some (mapmax_ne f H0)). apply mapmax_ne_ok. @@ -1187,7 +1189,7 @@ Module num_Extrema. apply H1; auto. Qed. - Lemma mapmax_ne_le_ext: forall (T : Type) (l : list T) (f g: T -> Nt) (H : O <> length l), + Lemma mapmax_ne_le_ext: forall (T : Type) (l : list T) (f g: T -> Nt) (H : O <> length l), (forall t : T, List.In t l -> f t <= g t) -> mapmax_ne f H <= mapmax_ne g H. Proof. intros. @@ -1195,7 +1197,7 @@ Module num_Extrema. { exfalso. apply H0. auto. } destruct l. simpl. apply H1. simpl. auto. - assert (O <> length (t :: l)). unfold not. intros. inversion H2. + assert (O <> length (t :: l)). unfold not. intros. inversion H2. destruct mapmax_ne_cons with T (t :: l) f a H2 H0. { destruct H3. @@ -1213,7 +1215,7 @@ Module num_Extrema. auto. Qed. - Lemma abs_mapmax_ne_le: forall (T : Type) (l : list T) (f: T -> Nt) (H : O <> length l), + Lemma abs_mapmax_ne_le: forall (T : Type) (l : list T) (f: T -> Nt) (H : O <> length l), Numerics.abs ( mapmax_ne f H) <= mapmax_ne (fun x => abs (f x)) H. Proof. intros. @@ -1225,7 +1227,7 @@ Module num_Extrema. apply mapmax_ne_le_ext. intros. apply Numerics.le_abs. - } + } assert (Numerics.abs (mapmax_ne (l:=l) f H0) = -mapmax_ne (l:=l) f H0). unfold Numerics.abs. rewrite e. auto. rewrite H1. @@ -1247,7 +1249,7 @@ Module num_Extrema. destruct H3. rewrite <- H3. apply Numerics.le_trans with (mapmax_ne (l:=t :: l) (fun x : T => Numerics.abs (f x)) H2). - { + { apply IHl; auto. apply Numerics.le_lt_trans with (mapmax_ne (l:=[:: a, t & l]) f H0). apply mapmax_ne_cons_le. auto. @@ -1266,7 +1268,7 @@ Module num_Extrema. rewrite <- H3. apply Numerics.le_trans with (Numerics.abs (f a)). { rewrite <- Numerics.abs_neg. apply Numerics.le_abs. } - remember ((fun x : T => Numerics.abs (f x))) as f'. + remember ((fun x : T => Numerics.abs (f x))) as f'. assert (Numerics.abs (f a) = f' a). rewrite Heqf'. auto. rewrite H5. apply mapmax_ne_correct. @@ -1284,7 +1286,7 @@ Module num_Extrema. assert(O <> length (t :: l)). unfold not. intros. inversion H1. destruct mapmax_ne_cons with T (t :: l) (fun x : T => f x + g x) a H1 H0. - { + { destruct H2. rewrite <- H2. apply Numerics.le_trans with (mapmax_ne (l:=t :: l) f H1 + mapmax_ne(l:=t :: l) g H1); auto. @@ -1295,7 +1297,7 @@ Module num_Extrema. apply Numerics.plus_le_compat; apply mapmax_ne_correct; simpl; auto. Qed. - + Lemma mapmax_ne_sub_le: forall (T : Type) (l : list T) (f g : T->Nt) (H0 : O <> length l), mapmax_ne f H0 + - mapmax_ne g H0 <= mapmax_ne(fun x => f x + - g x) H0. Proof. @@ -1318,7 +1320,7 @@ Module num_Extrema. apply mapmax_ne_plus_le. Qed. - + Lemma argmax_ne_in: forall (T : Type) (l : list T) (f : T->Nt) (H0 : O <> length l), List.In (argmax_ne f H0) l. Proof. @@ -1359,7 +1361,7 @@ Module num_Extrema. Qed. - Lemma mapmax_ne_increasing_max_ne: forall (l : list Nt) (f : Nt->Nt) (H0 : O <> length l), + Lemma mapmax_ne_increasing_max_ne: forall (l : list Nt) (f : Nt->Nt) (H0 : O <> length l), (forall x : Nt, List.In x l -> x <= f x) -> f (max_ne H0) <= mapmax_ne f H0. Proof. @@ -1367,14 +1369,14 @@ Module num_Extrema. induction l. { exfalso. apply H0. auto. } destruct (Nat.eqb O (length l)) eqn:e. - { + { apply EqNat.beq_nat_true in e. symmetry in e. rewrite -> List.length_zero_iff_nil in e. simpl. rewrite e. simpl. intros. apply le_refl. } intros. - apply EqNat.beq_nat_false in e. + apply EqNat.beq_nat_false in e. destruct max_ne_cons with l a e H0. - { + { destruct H2. rewrite <- H2. destruct mapmax_ne_cons with Nt l f a e H0. @@ -1433,7 +1435,7 @@ Module num_Extrema. rewrite <- H4. destruct mapmax_ne_cons with T l' (fun x : T => Numerics.abs (f x + - g x)) a H1 H0. { destruct H6. rewrite <- H6. apply IHl. } - destruct H6. + destruct H6. rewrite <- H6. apply Numerics.le_trans with ( mapmax_ne (fun x : T => Numerics.abs (f x + - g x)) H1); auto. } @@ -1441,7 +1443,7 @@ Module num_Extrema. rewrite <- H4. destruct mapmax_ne_cons with T l' (fun x : T => Numerics.abs (f x + - g x)) a H1 H0. { - destruct H6. + destruct H6. rewrite <- H6. destruct (Numerics.leb 0 (mapmax_ne (l:=l') f H1 + - g a)) eqn:e. { @@ -1605,7 +1607,7 @@ Module num_Extrema. simpl. auto. Qed. - Lemma mapmax_ne_le_const: forall (T : Type) (l : list T) (f : T -> Nt) (H0 : O <> length l) (c : Nt), + Lemma mapmax_ne_le_const: forall (T : Type) (l : list T) (f : T -> Nt) (H0 : O <> length l) (c : Nt), (forall n : T, List.In n l -> f n <= c) <-> (mapmax_ne f H0 <= c). Proof. intros. @@ -1622,7 +1624,7 @@ Module num_Extrema. auto. Qed. - Lemma mapmax_ne_gt_const: forall (T : Type) (l : list T) (f : T -> Nt) (H0 : O <> length l) (c : Nt), + Lemma mapmax_ne_gt_const: forall (T : Type) (l : list T) (f : T -> Nt) (H0 : O <> length l) (c : Nt), (exists n : T, List.In n l /\ c < f n) <-> (c < mapmax_ne f H0). Proof. intros. @@ -1635,12 +1637,12 @@ Module num_Extrema. auto. } exists (argmax_ne f H0). - rewrite <- argmax_ne_mapmax_ne. + rewrite <- argmax_ne_mapmax_ne. split; auto. apply argmax_ne_in. Qed. - Lemma mapmax_ne_ge_const: forall (T : Type) (l : list T) (f : T -> Nt) (H0 : O <> length l) (c : Nt), + Lemma mapmax_ne_ge_const: forall (T : Type) (l : list T) (f : T -> Nt) (H0 : O <> length l) (c : Nt), (exists n : T, List.In n l /\ c <= f n) <-> (c <= mapmax_ne f H0). Proof. intros. @@ -1653,12 +1655,12 @@ Module num_Extrema. auto. } exists (argmax_ne f H0). - rewrite <- argmax_ne_mapmax_ne. + rewrite <- argmax_ne_mapmax_ne. split; auto. apply argmax_ne_in. Qed. - Lemma mapmax_ne_lt_ext: forall (T : Type) (l : list T) (f g : T->Nt) (H0 : O <> length l), + Lemma mapmax_ne_lt_ext: forall (T : Type) (l : list T) (f g : T->Nt) (H0 : O <> length l), (forall t : T, List.In t l -> f t < g t) -> mapmax_ne f H0 < mapmax_ne g H0. Proof. intros. @@ -1689,7 +1691,7 @@ Module num_Extrema. apply List.in_eq. Qed. - Lemma mapmax_ne_lt_const: forall (T : Type) (l : list T) (f : T->Nt) (c : Nt) (H0 : O <> length l), + Lemma mapmax_ne_lt_const: forall (T : Type) (l : list T) (f : T->Nt) (c : Nt) (H0 : O <> length l), (forall t : T, List.In t l -> f t < c) <-> mapmax_ne f H0 < c . Proof. intros. @@ -1717,7 +1719,7 @@ Module num_Extrema. apply le_both_eq. apply mapmax_ne_le_const. auto. apply mapmax_ne_ge_const. exists x. split; auto. - rewrite H3. apply le_refl. + rewrite H3. apply le_refl. } split. { @@ -1734,7 +1736,7 @@ Module num_Extrema. Qed. Lemma mapmax_ne_dist_triangle: forall (T : Type) (f1 f2 f3 : T -> Nt) (l : list T) (H0 : O <> length l), - mapmax_ne (fun x => abs (f1 x + - f2 x)) H0 <= + mapmax_ne (fun x => abs (f1 x + - f2 x)) H0 <= mapmax_ne (fun x => abs (f1 x + - f3 x)) H0 + mapmax_ne (fun x => abs (f3 x + - f2 x)) H0. Proof. intros. @@ -1771,7 +1773,7 @@ Module num_Extrema. intros. induction l. { exfalso. apply H0. auto. } - + simpl.**) Lemma max_ne_In: forall (l : list Nt) (H0 : O <> length l), @@ -1801,7 +1803,7 @@ Module num_Extrema. induction l. { exfalso. apply H0. auto. } destruct l. - { + { exists 1. split. apply plus_id_lt_mult_id. intros. inversion H1; auto. inversion H2. @@ -1817,14 +1819,14 @@ Module num_Extrema. destruct H3. { exists (Numerics.min x (max_ne H1 + - a)). - split. + split. { unfold Numerics.min. destruct (leb x (max_ne H1 + - a)); auto. apply lt_diff_pos. auto. } intros. inversion H5. - { + { rewrite <- H6. right. apply le_trans with (a + (max_ne (l:=n :: l) H1 + - a)). apply plus_le_compat_l. apply ge_min_r. @@ -1846,7 +1848,7 @@ Module num_Extrema. clear IHl. destruct H4. destruct H3. - { + { exists (a + - max_ne H1). split. apply lt_diff_pos. auto. @@ -1867,10 +1869,10 @@ Module num_Extrema. intros. destruct H6; auto. destruct H5 with n0; auto. - { rewrite H3 in H7. auto. } + { rewrite H3 in H7. auto. } right. rewrite H3 in H7. auto. Qed. - + Lemma mapmax_ne_min_dist_max: forall (T : Type) (f : T->Nt) (l : list T) (H0 : O <> length l), exists c : Nt, 0 < c /\ forall t : T, List.In t l -> (f t = mapmax_ne f H0) \/ (f t + c <= mapmax_ne f H0). Proof. @@ -1893,8 +1895,8 @@ Module num_Extrema. Context (Nt:Type) `{Numeric_Props Nt}. - - + + Lemma to_R_argmax: forall (T : Type) (l : list T) (f : T->Nt), argmax l f = argmax l (fun x => to_R (f x)). Proof. @@ -1908,7 +1910,7 @@ Module num_Extrema. Qed. Lemma to_R_mapmax: forall (T : Type) (l : list T) (f : T->Nt), - O <> length l -> exists x : Nt, + O <> length l -> exists x : Nt, Some x = mapmax l f /\ Some (to_R x) = mapmax l (fun x => to_R (f x)). Proof. intros. @@ -1919,7 +1921,7 @@ Module num_Extrema. destruct IHl. { simpl. auto. } destruct H1. - simpl in *. + simpl in *. rewrite <- H1. rewrite <- H2. exists (if leb (f a) x then x else f a). @@ -1928,7 +1930,7 @@ Module num_Extrema. destruct (leb (f a) x); auto. Qed. - + Lemma to_R_argmax_ne: forall (T : Type) (l : list T) (f : T-> Nt) (H0 : O <> length l), argmax_ne f H0 = argmax_ne (fun x => to_R (f x)) H0. Proof. @@ -1942,7 +1944,7 @@ Module num_Extrema. inversion H2. auto. Qed. - + Lemma to_R_mapmax_ne: forall (T : Type) (l : list T) (f : T-> Nt) (H0 : O <> length l), to_R (mapmax_ne f H0) = mapmax_ne (fun x => to_R (f x)) H0. Proof. @@ -1953,13 +1955,9 @@ Module num_Extrema. auto. Qed. - + End use_Numerics2. End num_Extrema. - - - - diff --git a/generalized_bigops.v b/generalized_bigops.v index 86a362c..fb803f3 100644 --- a/generalized_bigops.v +++ b/generalized_bigops.v @@ -54,7 +54,7 @@ Section use_numeric_props. (fun p => let: (c, c') := p in f c = f' c') - (zip cs cs')) -> + (zip cs cs')) -> big_sum cs f = big_sum cs' f'. Proof. move=> H' H2; elim: cs cs' H' H2; first by case. @@ -67,7 +67,7 @@ Section use_numeric_props. Lemma big_sum_ext T (cs cs' : seq T) f f' : cs = cs' -> f =1 f' -> big_sum cs f = big_sum cs' f'. Proof. - by move=> <- H'; elim: cs=> //= a l ->; f_equal; apply: H'. + by move=> <- H'; elim: cs=> //= a l ->; f_equal; apply: H'. Qed. Lemma big_sum_scalar T (cs : seq T) r f : @@ -118,7 +118,7 @@ Section use_numeric_props. { by constructor. } by apply: Permutation_cons_app. } by rewrite big_sum_cat. - Qed. + Qed. Lemma big_sum_ge0 (T:eqType) (cs : seq T) f (H' : forall x, x \in cs -> Numerics.plus_id <= (f x)) : Numerics.plus_id <= (big_sum cs f). @@ -185,13 +185,13 @@ Proof. elim: cs => //=. { by rewrite Numerics.mult_plus_id_l. } move => a l /=; rewrite Numerics.plus_mult_distr_r => -> //. -Qed. +Qed. Lemma big_sum_mult_left T (cs : seq T) c f : c * (big_sum cs f) = big_sum cs (fun x => c * ( f x)). -Proof. +Proof. rewrite -> big_sum_ext with _ _ cs (fun x : T => c * f x) (fun x : T => f x * c); auto. - 2:{ + 2:{ unfold eqfun. intro x. apply Numerics.mult_comm. @@ -217,7 +217,7 @@ Proof. { intros. apply Numerics.le_lt_weak. apply Numerics.plus_id_lt_mult_id. } move=> a l IH H'. rewrite <- Numerics.mult_plus_id_l with Numerics.plus_id. - apply Numerics.mult_le_compat; try ( apply Numerics.le_refl). + apply Numerics.mult_le_compat; try ( apply Numerics.le_refl). { apply H'. rewrite in_cons. @@ -243,7 +243,7 @@ Proof. elim: cs=> /=. { intros. apply Numerics.plus_id_lt_mult_id. } move=> a l IH H'. - apply Numerics.mult_lt_0_compat; try ( apply Numerics.le_refl). + apply Numerics.mult_lt_0_compat; try ( apply Numerics.le_refl). { apply H'. rewrite in_cons. @@ -262,7 +262,7 @@ Qed. Lemma big_product_le (T : eqType) (cs : seq T) (f : T -> Nt) g : (forall c, c \in cs -> Numerics.plus_id <= (f c)) -> (forall c, c \in cs -> Numerics.plus_id <= (g c)) -> - (forall c, c \in cs -> (f c) <= (g c)) -> + (forall c, c \in cs -> (f c) <= (g c)) -> ((big_product cs f) <= (big_product cs g)). Proof. elim: cs=> //=. @@ -276,10 +276,10 @@ Proof. { by move=> c H'; apply: H1; rewrite in_cons; apply/orP; right. } { by move=> c H'; apply: H2; rewrite in_cons; apply/orP; right. } by move=> c H'; apply: H3; rewrite in_cons; apply/orP; right. -Qed. +Qed. Lemma big_sum_lt_aux (T : eqType) (cs : seq T) (f : T -> Nt) g : - (forall c, c \in cs -> (f c) < (g c)) -> + (forall c, c \in cs -> (f c) < (g c)) -> cs=[::] \/ ((big_sum cs f) < (big_sum cs g)). Proof. elim: cs=> //=. @@ -315,13 +315,13 @@ Qed. Lemma big_sum_lt (T : eqType) (cs : seq T) (f : T -> Nt) g : - (forall c, c \in cs -> (f c) < (g c)) -> + (forall c, c \in cs -> (f c) < (g c)) -> cs<>[::] -> ((big_sum cs f) < (big_sum cs g)). Proof. move => H' H1; case: (big_sum_lt_aux H') => //. Qed. - + Lemma big_product_perm T (cs1 cs2 : seq T) (H' : Permutation cs1 cs2) f : @@ -338,7 +338,7 @@ Qed. Lemma big_product_cat T (cs1 cs2 : seq T) f : (big_product (cs1++cs2) (fun c => f c) = (big_product cs1 (fun c => f c)) * (big_product cs2 (fun c => f c))). -Proof. +Proof. induction cs1. { simpl. rewrite Numerics.mult_id_l. auto. } simpl. @@ -357,22 +357,22 @@ Proof. { by constructor. } by apply: Permutation_cons_app. } by rewrite big_product_cat. -Qed. +Qed. Lemma big_product0 (T : eqType) (cs : seq T) c : - c \in cs -> + c \in cs -> big_product cs (fun _ => Numerics.plus_id) = Numerics.plus_id. Proof. by elim: cs c => // a l IH c /= _; rewrite Numerics.mult_plus_id_l. Qed. -Lemma big_sum_lift (T : Type) (ts : seq T) f g +Lemma big_sum_lift (T : Type) (ts : seq T) f g (g_zero : g Numerics.plus_id = Numerics.plus_id) (g_plus : forall x y, g (x + y) = (g x) + (g y)) : big_sum ts (fun x => g (f x)) = g (big_sum ts (fun x => f x)). Proof. by elim: ts => //= a l ->. Qed. -Lemma big_product_lift (T : Type) (ts : seq T) f g +Lemma big_product_lift (T : Type) (ts : seq T) f g (g_zero : g Numerics.mult_id = Numerics.mult_id) (g_mult : forall x y, g (x * y) = (g x) * (g y)) : big_product ts (fun x => g (f x)) = g (big_product ts (fun x => f x)). @@ -401,21 +401,21 @@ Lemma big_product_exp_sum (T : Type) (cs : seq T) (f : T -> R) : Proof. elim: cs => //=; first by rewrite exp_0. by move => a l IH; rewrite IH exp_plus. -Qed. +Qed. Lemma rat_to_R_sum T (cs : seq T) (f : T -> rat) : - rat_to_R (\sum_(c <- cs) (f c)) = + rat_to_R (\sum_(c <- cs) (f c)) = big_sum cs (fun c => (rat_to_R (f c)))%R. Proof. elim: cs=> //=; first by rewrite big_nil rat_to_R0. move=> a' l IH; rewrite big_cons. rewrite rat_to_R_plus IH. by f_equal; rewrite rat_to_R_plus rat_to_R_opp rat_to_R_mul. -Qed. +Qed. Lemma ln_big_product_sum (T : eqType) (cs : seq T) (f : T -> R) : - (forall t : T, 0 < f t)%R -> + (forall t : T, 0 < f t)%R -> ln (big_product cs f) = big_sum cs (fun c => ln (f c)). Proof. elim: cs=> /=; first by rewrite ln_1. @@ -432,14 +432,14 @@ Proof. Qed. Lemma rat_to_R_prod T (cs : seq T) (f : T -> rat) : - rat_to_R (\prod_(c <- cs) (f c)) = + rat_to_R (\prod_(c <- cs) (f c)) = big_product cs (fun c => (rat_to_R (f c)))%R. Proof. elim: cs=> //=; first by rewrite big_nil rat_to_R1. move=> a' l IH; rewrite big_cons. rewrite rat_to_R_mul IH. by f_equal; rewrite rat_to_R_plus rat_to_R_opp rat_to_R_mul. -Qed. +Qed. @@ -491,7 +491,7 @@ Section SSR_RBigops. rewrite BigOp.bigopE /index_enum enumT. by elim: (Finite.enum I) => //= a l; case Heq: (P a) => //= ->. Qed. - + Lemma big_product_prod : big_product (enum I) F = \big[Numerics.mult/Numerics.mult_id]_i F i. Proof. rewrite BigOp.bigopE /index_enum enumT. @@ -515,7 +515,7 @@ Lemma big_product_distr_sum (I J : finType) (F : I -> J -> R) : Proof. rewrite big_sum_sum big_product_prod. have ->: - \big[Rtimes/R1]_i big_sum (enum J) [eta F i] + \big[Rtimes/R1]_i big_sum (enum J) [eta F i] = \big[Rtimes/R1]_i \big[Rplus/R0]_j F i j. { by apply: eq_big => // i _; rewrite big_sum_sum. } by rewrite bigA_distr_bigA; apply: eq_big => // f _; rewrite big_product_prod. @@ -523,7 +523,7 @@ Qed. Lemma marginal_unfoldR N i (A : finType) (F : {ffun 'I_N -> A} -> R) : - let P t (p : {ffun 'I_N -> A}) := p i == t in + let P t (p : {ffun 'I_N -> A}) := p i == t in \big[Rplus/R0]_(p : [finType of (A * {ffun 'I_N -> A})] | P p.1 p.2) (F p.2) = \big[Rplus/R0]_(p : {ffun 'I_N -> A}) (F p). Proof. @@ -537,13 +537,13 @@ Proof. \big[Rplus/R0]_i0 \big[Rplus/R0]_(j : {ffun 'I_N -> A} | j i == i0) F j = \big[Rplus/R0]_i0 \big[Rplus/R0]_(j : {ffun 'I_N -> A} | predT j && (j i == i0)) F j. { by apply: eq_big. } - rewrite -partition_big //. -Qed. + rewrite -partition_big //. +Qed. Lemma prod_splitR N (i : 'I_N) (A : finType) (y : {ffun 'I_N -> A}) f : - Rmult (\big[Rtimes/R1]_(j in [set i]) (f j) (y j)) + Rmult (\big[Rtimes/R1]_(j in [set i]) (f j) (y j)) (\big[Rtimes/R1]_(j in [set~ i]) (f j) (y j)) = \big[Rtimes/R1]_(j < N) (f j) (y j). -Proof. +Proof. have ->: \big[Rtimes/R1]_(j < N) (f j) (y j) = \big[Rtimes/R1]_(j in [predU (pred1 i) & [set~ i]]) (f j) (y j). @@ -562,7 +562,7 @@ Qed. Lemma sum_splitR N (i : 'I_N) (A : finType) (y : {ffun 'I_N -> A}) f : ( \big[Rplus/R0]_(j in [set i]) (f j) (y j) + \big[Rplus/R0]_(j in [set~ i]) (f j) (y j) = \big[Rplus/R0]_(j < N) (f j) (y j) ) %R. -Proof. +Proof. have ->: \big[Rplus/R0]_(j < N) (f j) (y j) = \big[Rplus/R0]_(j in [predU (pred1 i) & [set~ i]]) (f j) (y j). @@ -582,7 +582,7 @@ Section use_Numeric2. Context {Nt:Type} `{Numerics.Numeric_Props Nt}. Lemma big_sum_le (T : eqType) (cs : seq T) (f : T -> Nt) g : - (forall c, c \in cs -> (f c) <= (g c)) -> + (forall c, c \in cs -> (f c) <= (g c)) -> ((big_sum cs f) <= (big_sum cs g)). Proof. elim: cs=> //=. @@ -606,8 +606,8 @@ Qed. Lemma perm_eq_nil (T:eqType) (cs : seq T) : perm_eq [::] cs -> cs=[::]. Proof. move => H'; apply: perm_eq_small => //. - by rewrite perm_eq_sym. -Qed. + by rewrite perm_sym. +Qed. Lemma In_mem (T:eqType) (a:T) (cs : seq T) : List.In a cs <-> a \in cs. Proof. @@ -616,7 +616,7 @@ Proof. by rewrite /in_mem/=; apply/orP; right; rewrite -(IH ax). } rewrite /in_mem/=; case/orP; first by move/eqP => <-; left. by move => H'; right; rewrite IH. -Qed. +Qed. Lemma uniq_NoDup (T:eqType) (cs : seq T) : uniq cs -> List.NoDup cs. Proof. @@ -628,21 +628,21 @@ Qed. Lemma perm_eqi (T:eqType) (cs1 cs2 : seq T) : uniq cs1 -> - uniq cs2 -> + uniq cs2 -> cs1 =i cs2 -> Permutation cs1 cs2. Proof. move => U1 U2 H'; apply: NoDup_Permutation. by apply: uniq_NoDup. - by apply: uniq_NoDup. + by apply: uniq_NoDup. move => x; split => H2. { by rewrite In_mem; rewrite -(H' x); rewrite -In_mem. } by rewrite In_mem; rewrite (H' x); rewrite -In_mem. Qed. - + Lemma perm_sub (T:eqType) (cs1 cs2 : seq T) : uniq cs1 -> - uniq cs2 -> - {subset cs1 <= cs2} -> + uniq cs2 -> + {subset cs1 <= cs2} -> Permutation cs1 [seq x <- cs2 | x \in cs1]. Proof. move => U1 U2 H'. @@ -660,10 +660,10 @@ Qed. Lemma big_sum_le3 (T : eqType) (cs1 cs2 : seq T) (f g : T -> Nt) : uniq cs1 -> - uniq cs2 -> - (forall c, c \in cs2 -> Numerics.plus_id <= (g c))%Num -> + uniq cs2 -> + (forall c, c \in cs2 -> Numerics.plus_id <= (g c))%Num -> (forall c, c \in cs1 -> c \in cs2)%Num -> - (forall c, c \in cs1 -> (f c) <= (g c))%Num -> + (forall c, c \in cs1 -> (f c) <= (g c))%Num -> ((big_sum cs1 f) <= (big_sum cs2 g))%Num. Proof. move => U1 U2 H1 H2 H'. @@ -671,11 +671,11 @@ Proof. rewrite -[big_sum cs1 _]Numerics.plus_id_r; apply: Numerics.plus_le_compat. { have Hperm: Permutation cs1 [seq x <- cs2 | [pred x in cs1] x]. { by apply: perm_sub. } - rewrite (big_sum_perm Hperm). - apply: big_sum_le => c /= Hin; apply: H'. + rewrite (big_sum_perm Hperm). + apply: big_sum_le => c /= Hin; apply: H'. rewrite mem_filter in Hin; case: (andP Hin) => Hx Hy //. } apply: big_sum_ge0 => x; rewrite mem_filter; case/andP => Hx Hy; apply: H1 => //. -Qed. +Qed. Lemma big_sum_pred (T:eqType) (cs:seq T) (f:T -> Nt) (p:pred T) : big_sum cs (fun t => if p t then f t else Numerics.plus_id) = @@ -712,9 +712,9 @@ Proof. apply IHcs. intros. destruct H0 with t. - constructor 2. apply H3. + constructor 2. apply H3. split; auto. -Qed. +Qed. Lemma big_sum_func_leq_max_l: forall (T : Type) (f1 f2 : T->Nt) (cs : seq T) (H : O <> length cs), @@ -741,7 +741,7 @@ Proof. auto. Qed. -Lemma big_sum_geometric_1: forall (r : Nt) (n l : nat), 0 <= r -> r < 1 -> +Lemma big_sum_geometric_1: forall (r : Nt) (n l : nat), 0 <= r -> r < 1 -> (1 + - r) * big_sum (List.seq n l) (fun n' => Numerics.pow_nat r n') = Numerics.pow_nat r n + - Numerics.pow_nat r (n + l). Proof. intros. @@ -771,7 +771,7 @@ Proof. auto. Qed. -(**Lemma big_sum_geometric_1_ub: forall (r : Nt) (n l: nat), 0 <= r -> r < 1 -> +(**Lemma big_sum_geometric_1_ub: forall (r : Nt) (n l: nat), 0 <= r -> r < 1 -> (1 + - r) * big_sum (List.seq n l) (fun n' => Numerics.pow_nat r n') = Numerics.pow_nat r n + - Numerics.pow_nat r (n + l).**) @@ -781,13 +781,13 @@ Proof. assert(List.seq n l.+1 = List.seq n l ++ ([:: n+l])%nat). { simpl. - generalize n. + generalize n. induction l; intros. simpl. rewrite addn0. auto. simpl. rewrite IHl. rewrite addSn. - rewrite addnS. + rewrite addnS. auto. } rewrite H0. @@ -877,4 +877,3 @@ Proof. elim: cs=> /=. rewrite N.mul_0_r. apply N.eq_refl. by move => a l IH; rewrite IH Nmult_plus_distr_l. Qed. - diff --git a/learning.v b/learning.v index 2437390..72ddc70 100644 --- a/learning.v +++ b/learning.v @@ -10,6 +10,8 @@ Require Import QArith Reals Rpower Ranalysis Fourier Lra. Require Import bigops numerics expfacts dist chernoff. +#[local] Open Scope R_scope. + Section learning. Variables A B : finType. @@ -18,21 +20,21 @@ Section learning. Variable d_nonneg : forall x, 0 <= d x. Variable m : nat. (*The number of training samples*) - Variable m_gt0 : (0 < m)%nat. + Variable m_gt0 : (0 < m)%nat. Notation mR := (INR m). - Definition i0 : 'I_m := Ordinal m_gt0. + Definition i0 : 'I_m := Ordinal m_gt0. (** Training sets *) Definition training_set : finType := [finType of {ffun 'I_m -> [finType of A*B]}]. Section error_RV. - Variable Hyp : finType. + Variable Hyp : finType. (** The (hypothesis-indexed) set of random variables being evaluated *) Variable X : Hyp -> 'I_m -> A*B -> R. Variable X_range : forall h i x, 0 <= X h i x <= 1. - + (** The empirical average of h on T *) - Definition empVal (T : training_set) (h : Hyp) := + Definition empVal (T : training_set) (h : Hyp) := (big_sum (enum 'I_m) (fun i => X h i (T i))) / mR. (** The expected value in D of X h *) @@ -41,7 +43,7 @@ Section learning. Lemma chernoff_bound_h (h : Hyp) - (Hid : identically_distributed d (X h)) + (Hid : identically_distributed d (X h)) (eps : R) (eps_gt0 : 0 < eps) (Hyp_eps : eps < 1 - expVal h) : probOfR (prodR (fun _ : 'I_m => d)) @@ -51,16 +53,16 @@ Section learning. have ->: expVal h = p_exp d m_gt0 (X h) by []. set (P := probOfR _ _). have ->: P = - probOfR + probOfR (prodR (T:=prod_finType A B) (fun _ : 'I_m => d)) (fun T => Rle_lt_dec (p_exp (T:=prod_finType A B) d m_gt0 (X h) + eps) (p_hat (X h) T)). { rewrite /probOfR; apply: big_sum_ext => //=; apply eq_in_filter => /= T Hin. have ->: empVal T h = p_hat (X h) T by rewrite /p_hat/empVal Rmult_comm. by []. } apply: chernoff => //; by case: (expVal_nontrivial h). - Qed. + Qed. - Definition eps_Hyp (eps : R) : finType := + Definition eps_Hyp (eps : R) : finType := [finType of {h : Hyp | Rlt_le_dec eps (1 - expVal h)}]. Variable identical : forall h : Hyp, identically_distributed d (X h). @@ -73,12 +75,12 @@ Section learning. in Rle_lt_dec (expVal h + eps) (empVal T h)]] <= INR #|eps_Hyp eps| * exp (-2%R * eps^2 * mR). Proof. - set (P := fun i:'I_#|eps_Hyp eps| => + set (P := fun i:'I_#|eps_Hyp eps| => [pred T : training_set | let: h := projT1 (enum_val i) in Rle_lt_dec (expVal h + eps) (empVal T h)]). change (probOfR (prodR (fun _ => d)) - [pred T:training_set | [exists i : 'I_#|eps_Hyp eps|, P i T]] + [pred T:training_set | [exists i : 'I_#|eps_Hyp eps|, P i T]] <= INR #|eps_Hyp eps| * exp (-2%R * eps^2 * mR)). apply: Rle_trans; [apply: union_bound|]. { by apply: prodR_nonneg. } @@ -95,7 +97,7 @@ Section learning. { rewrite !Rmult_0_l; apply: Rle_refl. } move => n H; rewrite iterS. have ->: - INR n.+1 * exp (- (2) * eps ^ 2 * mR) + INR n.+1 * exp (- (2) * eps ^ 2 * mR) = (exp (- (2) * eps ^ 2 * mR)) + INR n * exp (- (2) * eps ^ 2 * mR). { by rewrite S_INR Rmult_assoc Rmult_plus_distr_r Rmult_1_l Rplus_comm. } apply: Rplus_le_compat_l => //. @@ -113,7 +115,7 @@ Section learning. move => j /=; case/existsP => h H. by apply/existsP; exists (enum_rank h); rewrite enum_rankK. Qed. - + Lemma empVal_le1 T h : empVal T h <= 1. Proof. rewrite /empVal; set (f := big_sum _ _). @@ -134,12 +136,12 @@ Section learning. rewrite /Rdiv Rinv_r; first by apply: Rle_refl. apply: not_0_INR => Heq; move: m_gt0; rewrite Heq //. Qed. - + Lemma chernoff_bound3 (learn : training_set -> Hyp) (eps : R) (eps_gt0 : 0 < eps) : probOfR (prodR (fun _ : 'I_m => d)) - [pred T:training_set | - let: h := learn T in + [pred T:training_set | + let: h := learn T in Rlt_le_dec (expVal h + eps) (empVal T h)] <= INR #|eps_Hyp eps| * exp (-2%R * eps^2 * mR). Proof. @@ -159,30 +161,30 @@ Section learning. case: (Rle_lt_dec (expVal (learn T) + eps) (empVal T (learn T))) => //. move => b; lra. Qed. - + Lemma eps_Hyp_card eps : (#|eps_Hyp eps| <= #|Hyp|)%nat. Proof. rewrite /eps_Hyp /= card_sig; apply: leq_trans; first by apply: subset_leq_card. by rewrite cardsT. - Qed. + Qed. Lemma chernoff_bound (learn : training_set -> Hyp) (eps : R) (eps_gt0 : 0 < eps) : probOfR (prodR (fun _ : 'I_m => d)) - [pred T:training_set | - let: h := learn T in + [pred T:training_set | + let: h := learn T in Rlt_le_dec (expVal h + eps) (empVal T h)] <= INR #|Hyp| * exp (-2%R * eps^2 * mR). Proof. apply: Rle_trans; first by apply: chernoff_bound3. apply Rmult_le_compat_r; first by apply: Rlt_le; apply: exp_pos. apply: le_INR; apply/leP; apply: eps_Hyp_card. - Qed. - + Qed. + Lemma chernoff_bound_holdout (h : Hyp) (eps : R) (eps_gt0 : 0 < eps) (eps_lt : eps < 1 - expVal h) : probOfR (prodR (fun _ : 'I_m => d)) - [pred T:training_set | + [pred T:training_set | Rlt_le_dec (expVal h + eps) (empVal T h)] <= exp (-2%R * eps^2 * mR). Proof. @@ -190,15 +192,15 @@ Section learning. apply: probOfR_le. { move => x; apply: prodR_nonneg => _ y; apply: d_nonneg. } move => x /=; case: (Rlt_le_dec _ _) => // H1 _. - case: (Rle_lt_dec _ _) => // H2; lra. - Qed. + case: (Rle_lt_dec _ _) => // H2; lra. + Qed. Definition eps_Hyp_condition_twosided (eps : R) := [pred h : Hyp | Rlt_le_dec eps (Rmin (expVal h) (1 - expVal h))]. - + Lemma chernoff_twosided_bound_h (h : Hyp) - (Hid : identically_distributed d (X h)) + (Hid : identically_distributed d (X h)) (eps : R) (eps_gt0 : 0 < eps) (Hyp_eps : eps_Hyp_condition_twosided eps h) : probOfR (prodR (fun _ : 'I_m => d)) @@ -211,14 +213,14 @@ Section learning. have eps_range1 : eps < 1 - expVal h. { apply: Rlt_le_trans; [by apply: eps_range|by apply: Rmin_r]. } have eps_range2 : eps < expVal h. - { apply: Rlt_le_trans; [by apply: eps_range|by apply: Rmin_l]. } + { apply: Rlt_le_trans; [by apply: eps_range|by apply: Rmin_l]. } have H1: expVal h = p_exp d m_gt0 (X h) by []. have H2: - probOfR + probOfR (prodR (T:=prod_finType A B) (fun _ : 'I_m => d)) (fun T : training_set => - Rle_lt_dec eps (Rabs (p_exp (T:=prod_finType A B) d m_gt0 (X h) - empVal T h))) = - probOfR + Rle_lt_dec eps (Rabs (p_exp (T:=prod_finType A B) d m_gt0 (X h) - empVal T h))) = + probOfR (prodR (T:=prod_finType A B) (fun _ : 'I_m => d)) (fun T => Rle_lt_dec eps (Rabs (p_exp (T:=prod_finType A B) d m_gt0 (X h) - p_hat (X h) T))). { rewrite /probOfR; apply: big_sum_ext => //=; apply eq_in_filter => T Hin. @@ -231,7 +233,7 @@ Section learning. move: H1; rewrite /p_exp => <- //. Qed. - Definition eps_Hyp_twosided (eps : R) : finType := + Definition eps_Hyp_twosided (eps : R) : finType := [finType of {h : Hyp | eps_Hyp_condition_twosided eps h}]. Lemma eps_Hyp_twosided_inhabited : @@ -251,8 +253,8 @@ Section learning. case: (expVal_nontrivial h) => H1 H2; lra. } lra. } apply: (RIneq.Rle_not_lt _ _ H H1). - Qed. - + Qed. + Lemma chernoff_twosided_bound_eps_Hyp (eps : R) (eps_gt0 : 0 < eps) : probOfR (prodR (fun _ : 'I_m => d)) [pred T:training_set @@ -261,12 +263,12 @@ Section learning. in Rle_lt_dec eps (Rabs (expVal h - empVal T h))]] <= 2 * INR #|eps_Hyp_twosided eps| * exp (-2%R * eps^2 * mR). Proof. - set (P := fun i:'I_#|eps_Hyp_twosided eps| => + set (P := fun i:'I_#|eps_Hyp_twosided eps| => [pred T : training_set | let: h := projT1 (enum_val i) in Rle_lt_dec eps (Rabs (expVal h - empVal T h))]). change (probOfR (prodR (fun _ => d)) - [pred T:training_set | [exists i : 'I_#|eps_Hyp_twosided eps|, P i T]] + [pred T:training_set | [exists i : 'I_#|eps_Hyp_twosided eps|, P i T]] <= 2 * INR #|eps_Hyp_twosided eps| * exp (-2%R * eps^2 * mR)). apply: Rle_trans; [apply: union_bound|]. { by apply: prodR_nonneg. } @@ -284,7 +286,7 @@ Section learning. { rewrite !Rmult_0_l; apply: Rle_refl. } move => n H; rewrite iterS. have ->: - INR n.+1 * 2 * exp (- (2) * eps ^ 2 * mR) + INR n.+1 * 2 * exp (- (2) * eps ^ 2 * mR) = (2 * exp (- (2) * eps ^ 2 * mR)) + INR n * 2 * exp (- (2) * eps ^ 2 * mR). { rewrite S_INR Rmult_assoc Rmult_plus_distr_r Rmult_1_l Rplus_comm; f_equal. by rewrite -Rmult_assoc. } @@ -295,8 +297,8 @@ Section learning. Proof. rewrite /eps_Hyp_twosided /= card_sig; apply: leq_trans; first by apply: subset_leq_card. by rewrite cardsT. - Qed. - + Qed. + Lemma chernoff_twosided_bound1 (eps : R) (eps_gt0 : 0 < eps) : probOfR (prodR (fun _ : 'I_m => d)) [pred T:training_set @@ -330,7 +332,7 @@ Section learning. Variable predict : Params -> A -> B. (*the prediction function*) Definition accuracy01 (p : Params) (i : 'I_m) (xy : A*B) : R := - let: (x,y) := xy in if predict p x == y then 1%R else 0%R. + let: (x,y) := xy in if predict p x == y then 1%R else 0%R. Definition loss01 (p : Params) (i : 'I_m) (xy : A*B) : R := 1 - accuracy01 p i xy. @@ -339,26 +341,26 @@ Section learning. Variable learn : training_set -> Params. Variable not_perfectly_learnable : forall p : Params, 0 < expVal accuracy01 p < 1. - (*we get the the following result for any eps: the probability that - the expected accuracy of h is more than eps lower than the empirical - accuracy of h on T is less than |Params| * exp(-2eps*m), + (*we get the the following result for any eps: the probability that + the expected accuracy of h is more than eps lower than the empirical + accuracy of h on T is less than |Params| * exp(-2eps*m), where m is the number of training examples in T.*) Lemma chernoff_bound_accuracy01 (eps : R) (eps_gt0 : 0 < eps) : - probOfR (prodR (fun _ : 'I_m => d)) + probOfR (prodR (fun _ : 'I_m => d)) [pred T:training_set - | let: h := learn T in + | let: h := learn T in Rlt_le_dec (expVal accuracy01 h + eps) (empVal accuracy01 T h)] <= INR #|Params| * exp (-2%R * eps^2 * mR). Proof. apply chernoff_bound => // p i x; rewrite /accuracy01; case: x => a b. - case: (predict p a == b)%B; split; lra. + case: (predict p a == b)%B; split; lra. Qed. - (*Here's the holdout version of the above lemma (the additional condition + (*Here's the holdout version of the above lemma (the additional condition on epsilon appears to fall out -- cf. Mulzer's tutorial on Chernoff bound proofs).*) Lemma chernoff_bound_accuracy01_holdout (h : Params) (eps : R) (eps_gt0 : 0 < eps) (eps_lt : eps < 1 - expVal accuracy01 h) : - probOfR (prodR (fun _ : 'I_m => d)) + probOfR (prodR (fun _ : 'I_m => d)) [pred T:training_set | Rlt_le_dec (expVal accuracy01 h + eps) (empVal accuracy01 T h)] <= exp (-2%R * eps^2 * mR). @@ -368,9 +370,6 @@ Section learning. move => hx i x; rewrite /accuracy01; case: x => a b. case: (predict _ _ == _)%B; split; lra. } apply: Rle_refl. - Qed. + Qed. End zero_one_accuracy. End learning. - - - \ No newline at end of file diff --git a/numerics.v b/numerics.v index f1bb555..c9ce7eb 100644 --- a/numerics.v +++ b/numerics.v @@ -13,8 +13,8 @@ Require Import Lra Lia Reals. Require Import mathcomp.ssreflect.ssreflect. -From mathcomp Require Import all_ssreflect. -From mathcomp Require Import all_algebra. +From mathcomp Require Import ssreflect.all_ssreflect. +From mathcomp Require Import algebra.all_algebra. Import GRing.Theory Num.Def Num.Theory. @@ -22,8 +22,8 @@ Import GRing.Theory Num.Def Num.Theory. (** This file defines conversions between Ssreflect/MathComp and - Coq Standard Library implementations of various numeric types, - such as: + Coq Standard Library implementations of various numeric types, + such as: - int <-> Z - rat <-> Q - rat -> R @@ -39,7 +39,7 @@ Proof. rewrite subnKC; auto. assert(reflect (m <= n)%coq_nat (m <= n)%N). apply leP; auto. - inversion H0. auto. exfalso. auto. + inversion H0. auto. exfalso. auto. Qed. Module Numerics. @@ -57,7 +57,7 @@ Module Numerics. of_nat: nat -> T; plus_id: T; mult_id: T; - + lt: T->T->Prop where "n < m" := (lt n m) : Num; ltb: T->T->bool; @@ -103,14 +103,14 @@ Module Numerics. to_R_lt: forall t1 t2 : T, t1 < t2 <-> Rlt (to_R t1) (to_R t2); to_R_neg: forall t : T, Ropp (to_R t) = to_R (- t); to_R_inj: forall n m : T, to_R n = to_R m -> n = m; - + total_order_T : forall r1 r2, {r1 < r2} + {r1 = r2} + {r2 < r1}; eqb_true_iff: forall n m, eqb n m <-> n = m; ltb_true_iff: forall n m, ltb n m <-> n < m; }. - Ltac to_R_distr := + Ltac to_R_distr := repeat ( try (rewrite <- to_R_mult); try (rewrite <- to_R_plus); @@ -121,7 +121,7 @@ Module Numerics. Context {Nt:Type} `{H : Numeric Nt} . - + Definition le (n m : Nt) : Prop := n < m \/ n = m. Infix "<=" := le : Numeric_scope. @@ -132,7 +132,7 @@ Module Numerics. Lemma le_lt_or_eq: forall n m : Nt, n < m \/ n = m <-> n <= m . - Proof. + Proof. split; auto. Qed. @@ -154,7 +154,7 @@ Module Numerics. exfalso. by apply eqb_true_iff in e. Qed. - + Lemma ltb_false_iff: forall n m, ltb n m = false <-> ~ n < m. Proof. @@ -169,7 +169,7 @@ Module Numerics. destruct (ltb n m) eqn:e; auto. by apply ltb_true_iff in e. Qed. - + Lemma le_lt_dec: forall x y : Nt, {x <= y} + {y < x}. Proof. intros. @@ -189,7 +189,7 @@ Module Numerics. auto. Qed. - Program Definition numeric_ring := @mk_rt Nt plus_id mult_id plus mult minus neg eq plus_id_l + Program Definition numeric_ring := @mk_rt Nt plus_id mult_id plus mult minus neg eq plus_id_l plus_comm plus_assoc mult_id_l mult_comm mult_assoc _ _ plus_neg_r. Next Obligation. apply plus_mult_distr_r. @@ -271,7 +271,7 @@ Module Numerics. auto. Qed. - + Lemma double_neg: forall t : Nt, - - t = t. Proof. intros. @@ -291,7 +291,7 @@ Module Numerics. rewrite plus_neg_l. auto. Qed. - + Lemma plus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r. Proof. intros. @@ -299,8 +299,8 @@ Module Numerics. rewrite -> plus_comm with r2 r. apply plus_lt_compat_l. auto. - Qed. - + Qed. + Lemma mult_lt_compat_r : forall r r1 r2, plus_id < r -> (r1 < r2 <-> r1 * r < r2 * r). Proof. intros. @@ -329,7 +329,7 @@ Module Numerics. rewrite -> plus_comm with t3 t1 in H0. apply plus_elim_l in H0. auto. - Qed. + Qed. Lemma neg_pos_neg: forall t1 : Nt, plus_id < t1 <-> - t1 < plus_id. Proof. @@ -362,7 +362,7 @@ Module Numerics. apply plus_neg_l. Qed. - + Lemma mult_id_r: forall n : Nt, n * 1 = n. Proof. @@ -370,7 +370,7 @@ Module Numerics. rewrite mult_comm. apply mult_id_l. Qed. - + Lemma neg_mult_distr_l: forall n m : Nt, - (n * m) = -n * m. Proof. @@ -393,7 +393,7 @@ Module Numerics. Qed. - Lemma mult_elim_pos: forall t1 t2 t3 : Nt, plus_id < t1 -> t1 * t2 = t1 * t3 -> t2 = t3. + Lemma mult_elim_pos: forall t1 t2 t3 : Nt, plus_id < t1 -> t1 * t2 = t1 * t3 -> t2 = t3. Proof. intros. destruct total_order_T with t2 t3. @@ -410,13 +410,13 @@ Module Numerics. inversion l. Qed. - Lemma mult_elim_l: forall t1 t2 t3 : Nt, plus_id <> t1 -> t1 * t2 = t1 * t3 -> t2 = t3. + Lemma mult_elim_l: forall t1 t2 t3 : Nt, plus_id <> t1 -> t1 * t2 = t1 * t3 -> t2 = t3. Proof. intros. destruct total_order_T with t1 plus_id. { destruct s; auto. - { + { apply mult_elim_pos with (-t1). { apply neg_pos_neg. rewrite double_neg. auto. } repeat rewrite <- neg_mult_distr_l. @@ -446,7 +446,7 @@ Module Numerics. Definition min (x y : Nt) : Nt := if leb x y then x else y. - + Lemma le_lt_weak: forall (n m : Nt), n < m -> n <= m. Proof. @@ -461,7 +461,7 @@ Module Numerics. Lemma lt_not_le: forall n m : Nt, (n < m) -> ~ (m <= n). Proof. unfold not. - intros. + intros. apply le_not_lt in H0; auto. Qed. @@ -473,7 +473,7 @@ Module Numerics. Qed. Hint Immediate le_refl. - + Hint Resolve ltb_true_iff. @@ -525,7 +525,7 @@ Module Numerics. { exfalso; auto. } rewrite H1. auto. Qed. - + Lemma not_le_lt: forall n m : Nt, ~ (n <= m) -> m < n. Proof. intros. @@ -554,12 +554,12 @@ Module Numerics. apply lt_irrefl. Qed. - + Lemma eqb_refl: forall n : Nt, eqb n n. Proof. intros. rewrite eqb_true_iff. auto. Qed. - + Lemma eqb_symm: forall n m: Nt, eqb n m = eqb m n. Proof. intros. @@ -634,7 +634,7 @@ Module Numerics. apply plus_lt_le_compat. 2 : { apply le_refl. } apply plus_lt_le_compat; auto. - Qed. + Qed. Lemma le_not_eq_lt: forall x y : Nt, x <= y -> x <> y -> x < y. Proof. @@ -660,7 +660,7 @@ Module Numerics. Hint Resolve plus_id_l. Hint Resolve plus_id_r. - + Lemma mult_le_compat_l: forall x y z : Nt, plus_id <= x -> y <= z -> x * y <= x * z. Proof. intros. @@ -674,8 +674,8 @@ Module Numerics. auto. Qed. - - + + Lemma mult_le_compat_l_reverse: forall x y z : Nt, plus_id < x -> x * y <= x* z -> y <= z. Proof. intros. @@ -757,7 +757,7 @@ Module Numerics. rewrite plus_neg_l in H0. rewrite plus_id_r in H0. rewrite plus_id_l in H0. - auto. + auto. Qed. @@ -784,7 +784,7 @@ Module Numerics. rewrite H0. auto. Qed. - + Lemma mult_le_compat: forall r1 r2 r3 r4,plus_id <= r1 -> plus_id <= r3 -> r1 <= r2 -> r3 <= r4 -> (r1 * r3) <= (r2 * r4). Proof. @@ -793,7 +793,7 @@ Module Numerics. try (destruct s); try ( unfold le in H0,H1; destruct H0; destruct H1; try ( - apply mult_le_compat_l with r2 r3 r4 in H3; + apply mult_le_compat_l with r2 r3 r4 in H3; try (unfold le; auto; fail); apply mult_le_compat_l with r3 r1 r2 in H2; try (unfold le; auto; fail); @@ -890,8 +890,8 @@ Module Numerics. apply leb_false_iff in e. apply not_le_lt in e. destruct H0. - 2: { - rewrite <- H0. + 2: { + rewrite <- H0. repeat rewrite mult_plus_id_l. rewrite leb_refl. auto. @@ -907,10 +907,10 @@ Module Numerics. Qed. Lemma abs_mult_pos_r: forall n m : Nt, 0 <= n -> abs (m * n) = abs m * n. - Proof. intros. rewrite mult_comm. rewrite abs_mult_pos_l; auto. apply mult_comm. Qed. - + Proof. intros. rewrite mult_comm. rewrite abs_mult_pos_l; auto. apply mult_comm. Qed. + Lemma le_abs: forall n : Nt, n <= abs n. - Proof. + Proof. intros. unfold abs. destruct (leb 0 n) eqn:e. @@ -1012,7 +1012,7 @@ Module Numerics. Lemma abs_ge_0: forall n : Nt, 0 <= abs n. Proof. intros. - unfold abs. + unfold abs. destruct (leb 0 n) eqn:e. apply leb_true_iff. auto. apply leb_false_iff in e. @@ -1026,7 +1026,7 @@ Module Numerics. Lemma abs_0: abs 0 = 0. Proof. unfold abs. destruct (leb 0 0); auto. rewrite neg_plus_id. auto. Qed. - + Lemma pow_ge_0: forall (n : Nt) (m : nat), 0 <= n -> 0 <= pow_nat n m . Proof. @@ -1054,7 +1054,7 @@ Module Numerics. apply mult_lt_0_compat; auto. Qed. - Lemma pow_le_1: forall (n : Nt) (m : nat), 0 <= n /\ n <= 1 -> pow_nat n m <= 1. + Lemma pow_le_1: forall (n : Nt) (m : nat), 0 <= n /\ n <= 1 -> pow_nat n m <= 1. Proof. intros. induction m. @@ -1094,7 +1094,7 @@ Module Numerics. rewrite double_neg in H0. auto. Qed. - + Lemma abs_triangle: forall (x y z : Nt), abs ( x + - z ) <= abs (x + - y) + abs (y + - z). Proof. @@ -1136,8 +1136,8 @@ Module Numerics. apply H0. rewrite H1. auto. - Qed. - + Qed. + Lemma plus_id_neq_mult_id: 0 <> 1. Proof. @@ -1209,7 +1209,7 @@ Module Numerics. auto. Qed. - Lemma to_R_div_eq_iff_r: forall (n m p : Nt), m <> 0 -> + Lemma to_R_div_eq_iff_r: forall (n m p : Nt), m <> 0 -> n * m = p <-> to_R n = Rdiv (to_R p) (to_R m). Proof. intros. @@ -1230,17 +1230,17 @@ Module Numerics. auto. Qed. - Lemma to_R_div_lt_iff_r: forall (n m p : Nt), 0 < m -> + Lemma to_R_div_lt_iff_r: forall (n m p : Nt), 0 < m -> n * m < p <-> Rlt (to_R n) (Rdiv (to_R p) (to_R m)). Proof. intros. assert (to_R m <> IZR 0). - { - rewrite <- to_R_plus_id. + { + rewrite <- to_R_plus_id. rewrite <- to_R_neq. - apply lt_not_eq in H0. + apply lt_not_eq in H0. auto. - } + } split; intros. { unfold Rdiv. @@ -1253,7 +1253,7 @@ Module Numerics. rewrite <- to_R_plus_id. apply to_R_lt. auto. - } + } rewrite to_R_mult. apply to_R_lt. auto. @@ -1300,7 +1300,7 @@ Module Numerics. auto. Qed. - Lemma to_R_neg_div_distr_r: forall (n m : Nt), m <> 0 -> Ropp (Rdiv (to_R n) (to_R m)) = Rdiv (to_R (n)) (to_R (-m)). + Lemma to_R_neg_div_distr_r: forall (n m : Nt), m <> 0 -> Ropp (Rdiv (to_R n) (to_R m)) = Rdiv (to_R (n)) (to_R (-m)). Proof. intros. unfold Rdiv. @@ -1318,17 +1318,17 @@ Module Numerics. Proof. intros. split; intros. - { + { apply Ropp_le_cancel. rewrite to_R_neg_div_distr_r; auto. 2: { apply lt_not_eq. auto. } - rewrite to_R_neg. + rewrite to_R_neg. rewrite <- to_R_div_le_iff_r. rewrite <- neg_mult_distr_l. rewrite <- neg_mult_distr_r. rewrite double_neg. auto. - rewrite <- neg_plus_id. + rewrite <- neg_plus_id. rewrite <- lt_neg. auto. } @@ -1354,16 +1354,16 @@ Module Numerics. rewrite neg_mult_distr_l in H1. rewrite -> to_R_div_le_neg_l in H1; auto. rewrite <- to_R_neg_div_distr_l in H1. - 2: { apply lt_not_eq. auto. } + 2: { apply lt_not_eq. auto. } rewrite <- to_R_neg in H1. apply Ropp_le_cancel in H1. auto. - } + } rewrite <- le_neg. rewrite neg_mult_distr_l. rewrite -> to_R_div_le_neg_l; auto. rewrite <- to_R_neg_div_distr_l. - 2: { apply lt_not_eq. auto. } + 2: { apply lt_not_eq. auto. } rewrite <- to_R_neg. apply Ropp_le_contravar. auto. @@ -1396,10 +1396,10 @@ Module Numerics. rewrite <- plus_id_r with x. rewrite <- H0. rewrite plus_assoc. - rewrite plus_neg_r. + rewrite plus_neg_r. auto. Qed. - + Lemma to_R_le: forall (t1 t2 : Nt), t1 <= t2 <-> (Rle (to_R t1) (to_R t2)). Proof. intros. @@ -1437,13 +1437,13 @@ Module Numerics. apply to_R_le. auto. Qed. - + Lemma to_R_ltb_false_iff: forall t1 t2 : Nt, ltb t1 t2 = false <-> ~ Rlt (to_R t1) (to_R t2). Proof. intros. split; intros; try (apply ltb_false_iff in H0); - try (apply ltb_false_iff); + try (apply ltb_false_iff); unfold not; intros; apply H0; apply to_R_lt; auto. Qed. @@ -1452,11 +1452,11 @@ Module Numerics. intros. split; intros; try (apply leb_false_iff in H0); - try (apply leb_false_iff); + try (apply leb_false_iff); unfold not; intros; apply H0; apply to_R_le; auto. Qed. - + Lemma leb_ltb_or_eqb: forall t1 t2 : Nt, leb t1 t2 = ltb t1 t2 || eqb t1 t2. Proof. @@ -1467,7 +1467,7 @@ Module Numerics. destruct e. { apply ltb_true_iff in H0. rewrite H0. auto. } rewrite H0. - rewrite eqb_refl. + rewrite eqb_refl. rewrite orb_true_r. auto. } @@ -1507,23 +1507,27 @@ Module Numerics. auto. Qed. - Lemma to_R_pow_nat: forall x n, to_R (pow_nat x n) = (to_R x) ^ n. - Proof. - intros. - induction n. - { simpl. rewrite pow_natO. apply to_R_mult_id. } - simpl. - rewrite pow_nat_rec. - rewrite <- to_R_mult. - rewrite IHn. - auto. - Qed. + Section to_R_pow_nat. + #[local] Open Scope R_scope. + Lemma to_R_pow_nat: forall x n, to_R (pow_nat x n) = (to_R x) ^ n. + Proof. + intros. + induction n. + { simpl. rewrite pow_natO. apply to_R_mult_id. } + simpl. + rewrite pow_nat_rec. + rewrite <- to_R_mult. + rewrite IHn. + auto. + Qed. + End to_R_pow_nat. - Lemma pow_nat_ge1_le: forall x n m, 1 <= x -> Nat.le n m -> pow_nat x n <= pow_nat x m. - Proof. + Lemma pow_nat_ge1_le: forall x n m, + 1 <= x -> Nat.le n m -> pow_nat x n <= pow_nat x m. + Proof. intros. assert(forall m', pow_nat x n <= pow_nat x (n+m')). - { + { intros. induction m'. rewrite addn0. auto. rewrite addnS. rewrite <- mult_id_l with (pow_nat x n). @@ -1540,10 +1544,10 @@ Module Numerics. Qed. Lemma pow_nat_le1_le: forall x n m, 0 < x -> x <= 1 -> Nat.le n m -> pow_nat x m <= pow_nat x n. - Proof. + Proof. intros. assert(forall m', pow_nat x (n+m') <= pow_nat x n). - { + { intros. induction m'. rewrite addn0. auto. rewrite addnS. rewrite <- mult_id_l with (pow_nat x n). @@ -1557,14 +1561,14 @@ Module Numerics. Qed. Lemma lt_diff_pos: forall x y : Nt, x < y -> 0 < (y + - x). - Proof. + Proof. intros. rewrite <- plus_neg_r with x. apply plus_lt_compat_r. auto. - Qed. + Qed. Lemma min_comm: forall x y : Nt, min x y = min y x. - Proof. + Proof. intros. unfold min. destruct (total_order_T x y). { @@ -1582,9 +1586,9 @@ Module Numerics. Qed. Lemma ge_min_l: forall x y : Nt, min x y <= x. - Proof. + Proof. intros. - unfold min. + unfold min. destruct (total_order_T x y). { destruct s. @@ -1638,7 +1642,7 @@ Program Instance Numeric_Props_D: @Numerics.Numeric_Props DRed.t Numeric_D:= DRed.of_natO DRed.of_nat_succ_l - + DRed.addC DRed.addA _ @@ -1676,7 +1680,7 @@ Next Obligation. intros. apply eqR_Qeq in H. apply DRed.Dred_eq; auto. Qed. Next Obligation. split; intros. - { + { destruct (DRed.eq_dec n m); auto. by exfalso. } @@ -1699,6 +1703,8 @@ Qed. Delimit Scope R_scope with R_s. Local Open Scope R_scope. +(*TODO: This axiom (from Coq 8.9) is true only up to EM.*) +Axiom Rtotal_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}. Program Instance Numeric_R: Numeric R := @Numerics.mkNumeric @@ -1716,14 +1722,14 @@ Program Instance Numeric_R: Numeric R := _ . Next Obligation. - destruct (Raxioms.total_order_T H H0). + destruct (Rtotal_order_T H H0). destruct s. exact true. exact false. exact false. Defined. Next Obligation. - destruct (Raxioms.total_order_T H H0). + destruct (Rtotal_order_T H H0). destruct s. exact false. exact true. @@ -1758,7 +1764,7 @@ Program Instance Numeric_Props_R: @Numerics.Numeric_Props R Numeric_R:= _ _ _ - Raxioms.total_order_T + Rtotal_order_T _ _ . @@ -1769,11 +1775,11 @@ Next Obligation. simpl. rewrite Rplus_0_l. auto. Qed. Next Obligation. lra. Qed. -Next Obligation. lra. Qed. -Next Obligation. +Next Obligation. lra. Qed. +Next Obligation. split; intros. apply Rmult_lt_compat_l; auto. - rewrite <- Rmult_1_r. + rewrite <- Rmult_1_r. rewrite <- Rmult_1_r with r1. rewrite -> Rinv_r_sym with r. 2:{ apply Rlt_not_eq in H. auto. } @@ -1784,9 +1790,9 @@ Next Obligation. auto. Qed. Next Obligation. lra. Qed. -Next Obligation. +Next Obligation. unfold Numeric_R_obligation_2. - destruct (Raxioms.total_order_T n m). + destruct (Rtotal_order_T n m). { destruct s. { @@ -1806,13 +1812,13 @@ Next Obligation. Qed. Next Obligation. unfold Numeric_R_obligation_1. - destruct (Raxioms.total_order_T n m). + destruct (Rtotal_order_T n m). { destruct s. by split. split; intros. inversion H. - rewrite e in H. + rewrite e in H. by apply Rlt_irrefl in H. } split; intros. @@ -1826,19 +1832,15 @@ Lemma to_R_R: forall x : R, to_R x = x. Proof. intros. simpl. auto. Qed. -(**Undelimit Scope R_scope. -Close Scope R_scope.**) -(**Local Open Scope Z_scope.**) Delimit Scope Z_scope with Z. - Program Instance Numeric_z : Numerics.Numeric Z := @Numerics.mkNumeric Z Z.add Z.opp Z.mul - Zpower_nat + Zpower.Zpower_nat IZR Z.of_nat Z0 @@ -1865,7 +1867,7 @@ Program Instance Numeric_Props_z : @Numerics.Numeric_Props Z Numeric_z := Z.mul_comm Z.mul_assoc Z.mul_1_l - Z.mul_add_distr_l + Z.mul_add_distr_l Zlt_asym Z.lt_trans _ @@ -1883,7 +1885,7 @@ Program Instance Numeric_Props_z : @Numerics.Numeric_Props Z Numeric_z := Z.ltb_lt . Next Obligation. lia. Qed. -Next Obligation. +Next Obligation. fold (Z.of_nat n.+1). rewrite Nat2Z.inj_succ. destruct (Z.of_nat n); auto. @@ -1900,8 +1902,8 @@ Next Obligation. auto. Qed. Next Obligation. rewrite plus_IZR. auto. Qed. -Next Obligation. rewrite mult_IZR. auto. Qed. -Next Obligation. +Next Obligation. rewrite mult_IZR. auto. Qed. +Next Obligation. split. apply IZR_lt. apply lt_IZR. @@ -1911,9 +1913,6 @@ Next Obligation. destruct Z_dec' with r1 r2; auto. destruct s; auto. Qed. - - - Delimit Scope R_scope with R_s. @@ -1941,7 +1940,7 @@ Qed. apply eqb_false_iff in H0. auto. Qed. - + Lemma to_R_ltb: forall (n m : Nt), ltb n m = ltb (to_R n) (to_R m). Proof. intros. @@ -1958,7 +1957,7 @@ Qed. Lemma to_R_leb: forall (n m : Nt), leb n m = leb (to_R n) (to_R m). Proof. intros. - repeat rewrite leb_ltb_or_eqb. + repeat rewrite leb_ltb_or_eqb. rewrite to_R_ltb. rewrite to_R_eqb. auto. @@ -1967,10 +1966,10 @@ Qed. Lemma R_abs_same: forall x : R, abs x = Rabs x. Proof. intros. - unfold abs. + unfold abs. simpl. destruct (le_lt_dec 0 x). - { + { rewrite Rabs_right. apply leb_true_iff in l. rewrite l. auto. unfold Rge. @@ -1984,30 +1983,30 @@ Qed. Lemma R_dist_same: forall x y : R, abs (x + - y) = R_dist x y. Proof. intros. unfold R_dist. rewrite R_abs_same. auto. Qed. - Lemma R_lt_same: forall x y : R, x < y <-> Rlt x y. + Lemma R_lt_same: forall x y : R, x < y <-> Rlt x y. Proof. intros. split; auto. Qed. - Lemma R_le_same: forall x y : R, x <= y <-> Rle x y. + Lemma R_le_same: forall x y : R, x <= y <-> Rle x y. Proof. intros. split; auto. Qed. Lemma Zlt_iff: forall (x y : Z), (x < y)%Z <-> lt x y. Proof. intros. split; auto. Qed. Lemma Zle_iff: forall (x y : Z), (x <= y)%Z <-> le x y. - Proof. + Proof. intros. split; intros. - { + { apply Zle_lt_or_eq in H0. unfold le. - destruct H0; auto. + destruct H0; auto. } destruct H0; auto. apply Zlt_le. auto. rewrite H0. apply Z.le_refl. Qed. - + Definition of_Z (i : Z) : Nt := match i with | Z0 => plus_id @@ -2019,9 +2018,9 @@ Qed. End use_Numeric2. Definition log (x y : R) := Rdiv (ln y) (ln x). - + Lemma ln_pow: forall (x : R) (n : nat), 0 < x -> ln (x ^ n) = INR n * ln x. -Proof. +Proof. intros. induction n; auto. simpl. rewrite Rmult_0_l. apply ln_1. @@ -2037,7 +2036,7 @@ Proof. rewrite H0. simpl. rewrite ln_mult; auto. - { + { rewrite Rmult_plus_distr_r. rewrite Rmult_1_l. rewrite IHn. @@ -2059,12 +2058,12 @@ Lemma log_pow: forall (x y : R) (n : nat), 0 < x -> 0 < y -> log x (y ^ n) = INR Proof. intros. unfold log. - rewrite ln_pow; auto. + rewrite ln_pow; auto. unfold Rdiv. rewrite Rmult_assoc. auto. Qed. - + Lemma log_base: forall (x : R), 0 < x -> 1 <> x -> log x x = 1. Proof. intros. @@ -2075,8 +2074,8 @@ Proof. intros. apply H0. rewrite <- ln_1 in H1. - apply ln_inv; auto. - assert (Numerics.to_R 0 < Numerics.to_R 1)%R_s. simpl. apply Rlt_0_1. + apply ln_inv; auto. + assert (Numerics.to_R 0 < Numerics.to_R 1)%R_s. simpl. apply Rlt_0_1. apply H2. Qed. @@ -2105,11 +2104,11 @@ Proof. unfold Rdiv in H1. apply ln_inv; auto. unfold log in H3. - rewrite <- Rmult_1_r. + rewrite <- Rmult_1_r. rewrite <- Rmult_1_r with (ln y). assert (ln x <> 0)%R_s. unfold not. intros. apply H0. rewrite <- ln_1 in H4. apply ln_inv; auto. - apply Rlt_0_1. + apply Rlt_0_1. rewrite <- Rinv_l with (ln x); auto. repeat rewrite <- Rmult_assoc. unfold Rdiv in H3. @@ -2207,7 +2206,7 @@ Qed. intros. exists (Z.to_nat (up (log x y))). apply log_lt1_le_inv with x; auto. - apply pow_lt. auto. + apply pow_lt. auto. rewrite log_base_pow_nat; auto. 2:{ apply lt_not_eq in H0. auto. } rewrite INR_IZR_INZ. @@ -2235,7 +2234,7 @@ Qed. Proof. intros. destruct H. - 2: { exists (S O). rewrite <- H. rewrite pow_1. auto. } + 2: { exists (S O). rewrite <- H. rewrite pow_1. auto. } destruct exists_pow_le with x y; auto. exists (S x0). apply lt_le_trans with (x ^ x0); auto. @@ -2243,7 +2242,7 @@ Qed. rewrite <- mult_id_l. apply Rmult_lt_compat_r; auto. apply pow_lt. auto. - Qed. + Qed. Lemma R_plus_id_same: plus_id = 0%R_s. Proof. auto. Qed. @@ -2267,7 +2266,7 @@ Qed. apply to_R_le. auto. Qed. - + Lemma exists_pow_nat_lt: forall x y : Nt, 0 <= x -> x < 1 -> 0 < y -> exists n, Numerics.pow_nat x n < y. Proof. intros. @@ -2356,9 +2355,9 @@ Proof. set (P := fun p0 => Z.pos_sub p0 1 = Z.pred (Z.pos p0)). change (P p). by apply: positive_ind. -Qed. +Qed. -Lemma pos_sub_succ1 m : +Lemma pos_sub_succ1 m : Z.pos_sub (Pos.of_succ_nat m.+1) 1 = Z.pos (Pos.of_succ_nat m). Proof. rewrite pos_sub_pred. @@ -2367,7 +2366,7 @@ Proof. by rewrite Zpos_P_of_succ_nat. Qed. -Lemma pos_sub_succ m n : +Lemma pos_sub_succ m n : Z.pos_sub (Pos.succ (Pos.of_succ_nat m)) (Pos.of_succ_nat n) = Z.succ (Z.pos_sub (Pos.of_succ_nat m) (Pos.of_succ_nat n)). Proof. @@ -2376,7 +2375,7 @@ Proof. by rewrite Z.add_comm Z.add_succ_r. Qed. -Lemma pos_sub_1succ n : +Lemma pos_sub_1succ n : Z.pos_sub 1 (Pos.succ (Pos.of_succ_nat n)) = Z.neg (Pos.of_succ_nat n). Proof. @@ -2385,7 +2384,7 @@ Proof. rewrite -[Pos.succ (Pos.of_succ_nat n)]Pos2SuccNat.id_succ. by rewrite pos_sub_succ1. Qed. - + Lemma pos_of_succ_nat_sub n m : Z.pos_sub (Pos.of_succ_nat n) (Pos.of_succ_nat m) = int_to_Z (Posz n - Posz m). @@ -2413,9 +2412,9 @@ Proof. elim: n'=> // n /= IH. have H: (subn n.+1 1 = n) by move {IH}; elim: n. by rewrite H pos_sub_1succ. -Qed. +Qed. -Lemma pos_of_succ_nat_plus n m : +Lemma pos_of_succ_nat_plus n m : (Pos.of_succ_nat n + Pos.of_succ_nat m)%positive = Pos.succ (Pos.of_succ_nat (n + m)). Proof. @@ -2498,14 +2497,14 @@ Proof. case: s=> sn; move => Hs. - case: r=> rn; move => Hr. + simpl. rewrite Nat2Pos.inj_mul //; auto. - + rewrite /GRing.mul /=. + + rewrite /GRing.mul /=. have H0: ((sn * rn.+1)%N = ((sn * rn.+1 - 1).+1)%N). { apply: int_to_positive_mul_1. auto. } rewrite H0 -NegzE /= of_succ_nat_of_nat_plus_1 addn1 -H0. rewrite Nat2Pos.inj_mul; auto. rewrite of_succ_nat_of_nat_plus_1 addn1 //. - case: r=> rn; move => Hr. - + rewrite /GRing.mul /=. + + rewrite /GRing.mul /=. have H0: ((rn * sn.+1)%N = ((rn * sn.+1 - 1).+1)%N). { apply: int_to_positive_mul_1. auto. } rewrite H0 -NegzE /= of_succ_nat_of_nat_plus_1 addn1 -H0 mulnC. @@ -2514,7 +2513,7 @@ Proof. + rewrite /GRing.mul /=. case H0: ((rn + (sn * rn.+1)%Nrec)%coq_nat). * have ->: ((rn = 0)%N). - { rewrite -mulnE in H0. omega. } + { rewrite -mulnE in H0. lia. } have ->: ((sn = 0)%N). { rewrite -mulnE -addn1 in H0. case H1: (sn == 0%N). @@ -2590,12 +2589,12 @@ Proof. Qed. Lemma Zneg_Zlt r s : - Pos.gt r s -> + Pos.gt r s -> Z.lt (Zneg r) (Zneg s). Proof. rewrite /Pos.gt. by rewrite /Z.lt /= => ->. -Qed. +Qed. Lemma Zlt_Zneg r s : Z.lt (Zneg r) (Zneg s) -> @@ -2604,18 +2603,18 @@ Proof. rewrite /Pos.gt. rewrite /Z.lt /=. case: (r ?= s)%positive => //. -Qed. +Qed. Lemma Psucc_gt r s : Pos.gt (Pos.of_succ_nat r) (Pos.of_succ_nat s) -> (r > s)%coq_nat. Proof. rewrite /Pos.gt -SuccNat2Pos.inj_compare /gt -nat_compare_gt. - omega. + lia. Qed. Lemma Zneg_Zle r s : - Pos.ge r s -> + Pos.ge r s -> Z.le (Zneg r) (Zneg s). Proof. rewrite /Pos.ge /Z.le /= => H; rewrite /CompOpp. @@ -2647,10 +2646,10 @@ Proof. rewrite /Pos.gt. rewrite -Nat2Pos.inj_compare=> //. move: H. - move/leP. + move/leP. simpl. by rewrite Nat.compare_gt_iff. -Qed. +Qed. Lemma int_to_Z_inj (a b : int) : int_to_Z a = int_to_Z b -> @@ -2663,18 +2662,18 @@ Proof. { apply Nat2Z.is_nonneg. } have H2: (Z.lt (Z.neg (Pos.of_succ_nat n0)) 0). { apply Zlt_neg_0. } - omega. + lia. have H1: (Z.le 0 (Z.of_nat n0)). { apply Nat2Z.is_nonneg. } have H2: (Z.lt (Z.neg (Pos.of_succ_nat n)) 0). { apply Zlt_neg_0. } - omega. + lia. inversion H. apply SuccNat2Pos.inj_iff in H1. auto. Qed. Lemma lt_int_to_Z (s r : int) : Z.lt (int_to_Z s) (int_to_Z r) -> - ltr s r. + ltr s r. Proof. case: s=> sn; case: r=> rn //. { by rewrite /= -Nat2Z.inj_lt /ltr /=; case: (@ltP sn rn). } @@ -2684,25 +2683,26 @@ Proof. have H3: (Z.lt (Z.of_nat sn) 0)%Z. { apply: Z.lt_trans; first by apply: H. by []. } - clear - H3; case: sn H3 => //. } + clear - H3; case: sn H3 => //. } simpl. rewrite /ltr /= => H. - have H2: (sn > rn)%coq_nat. + have H2: (sn > rn)%coq_nat. { move: (Zlt_Zneg H). apply: Psucc_gt. } clear - H2. - apply/ltP; omega. + apply/ltP; lia. Qed. Lemma le_int_to_Z (s r : int) : Z.le (int_to_Z s) (int_to_Z r) -> - ler s r. + ler s r. Proof. - - move/Zle_lt_or_eq; case; first by move/lt_int_to_Z; apply/ltrW. + move/Zle_lt_or_eq; case. + { move/lt_int_to_Z. + apply/mc_1_10.Num.Theory.ltrW. } move/int_to_Z_inj => -> //. -Qed. +Qed. Lemma int_to_Z_le (s r : int) : ler s r -> @@ -2728,27 +2728,29 @@ Proof. rewrite /Pos.ge. rewrite -Nat2Pos.inj_compare=> //. move: H. - move/leP. + move/leP. simpl. by rewrite Nat.compare_ge_iff. -Qed. +Qed. Section rat_to_Q. Variable r : rat. - + Definition rat_to_Q : Q := let: (n, d) := valq r in Qmake (int_to_Z n) (int_to_positive d). End rat_to_Q. +Import Order.POrderTheory. + Section rat_to_Q_lemmas. Local Open Scope ring_scope. - Delimit Scope R with R_ssr. + Delimit Scope R with R_ssr. Delimit Scope R_scope with R. Lemma rat_to_Q0 : rat_to_Q 0 = inject_Z 0. Proof. by []. Qed. - + Lemma Z_of_nat_pos_of_nat (a : nat): (0 < a)%N -> Z.of_nat a = @@ -2799,7 +2801,7 @@ Section rat_to_Q_lemmas. { apply dvdn_leq => //. rewrite absz_gt0. - rewrite ltr_neqAle in H. + rewrite lt_neqAle in H. case/andP: H => H1 H4. apply/eqP. move/eqP: H1 => H1 H5. @@ -2809,7 +2811,7 @@ Section rat_to_Q_lemmas. { rewrite gcdn_gt0. apply/orP; right. rewrite absz_gt0. - rewrite ltr_neqAle in H. + rewrite lt_neqAle in H. case/andP: H => H1 H4. apply/eqP. move/eqP: H1 => H1 H5. @@ -2825,13 +2827,13 @@ Section rat_to_Q_lemmas. case: (dvdn_gcdl `|a| `|b|)%N => H3. apply dvdn_leq => //. rewrite absz_gt0. - rewrite ltr_neqAle in H2. + rewrite lt_neqAle in H2. case/andP: H2 => //. } { rewrite gcdn_gt0. apply/orP; right. rewrite absz_gt0. - rewrite ltr_neqAle in H. + rewrite lt_neqAle in H. case/andP: H => H1 H4. apply/eqP. move/eqP: H1 => H1 H5. @@ -2850,6 +2852,8 @@ Section rat_to_Q_lemmas. inversion H. Qed. + Import mc_1_10.Num.Theory. + Lemma rat_to_Q_fracq_pos_leib (x y : int) : 0 < y -> coprime `|x| `|y| -> @@ -2890,9 +2894,9 @@ Section rat_to_Q_lemmas. induction y => //. } Qed. - + Lemma rat_to_Q_fracq_pos (x y : int) : - 0 < y -> + 0 < y -> Qeq (rat_to_Q (fracq (x, y))) (int_to_Z x # int_to_positive y). Proof. move=> H. @@ -2918,12 +2922,12 @@ Section rat_to_Q_lemmas. rewrite [_%N * y] mulrC mulrA [y * -1] mulrC -mulrA. have H1: (`|y| = y%N) by apply: gtz0_abs. rewrite -{1}H1. - have H3: ((@normr int_numDomainType y) = absz y) by []. + have H3: ((@normr int_numDomainType int_normedZmodType y) = absz y) by []. rewrite H3 /=. rewrite pos_muln -muln_divCA_gcd. rewrite mulN1r -pos_muln -mulNr. have H4: (`|x| = - x). { apply ltz0_abs. by apply: H2. } - have H5: ((@normr int_numDomainType x) = absz x) by []. + have H5: ((@normr int_numDomainType int_normedZmodType x) = absz x) by []. by rewrite -H5 H4 opprK. } rewrite /nat_of_bool /Qeq /Qnum /Qden expr0z. apply negbT in H2. rewrite -lerNgt in H2. @@ -2944,8 +2948,8 @@ Section rat_to_Q_lemmas. rewrite mulrC. have H1: (`|y| = y%N) by apply: gtz0_abs. rewrite -{1}H1. - have H3: ((@normr int_numDomainType y) = absz y) by []. - rewrite H3 /=. rewrite 2!pos_muln. + have H3: ((@normr int_numDomainType int_normedZmodType y) = absz y) by []. + rewrite H3 /=. rewrite 2!pos_muln. by rewrite -muln_divCA_gcd. } Qed. @@ -2958,7 +2962,7 @@ Section rat_to_Q_lemmas. move: H2 => /eqP H2. by rewrite H2 in H0. by move: H2 => /eqP H2. Qed. - + Lemma rat_to_Q_plus (r s : rat) : Qeq (rat_to_Q (r + s)) (Qplus (rat_to_Q r) (rat_to_Q s)). Proof. @@ -2983,7 +2987,7 @@ Section rat_to_Q_lemmas. apply: lt_and_P_ne_0 H. apply: lt_and_P_ne_0 H2. Qed. - + Lemma rat_to_Q_mul (r s : rat) : Qeq (rat_to_Q (r * s)) (Qmult (rat_to_Q r) (rat_to_Q s)). Proof. @@ -3009,7 +3013,7 @@ Section rat_to_Q_lemmas. rewrite /Qlt /rat_to_Q; case: r => x y /=; case: s => z w /=. case: x y => x1 z2 /= y; case: z w => z1 x2 /= w. case: (andP y) => H1 H2. - case: (andP w) => H3 H4. + case: (andP w) => H3 H4. rewrite int_to_positive_to_Z => //. rewrite int_to_positive_to_Z => //. rewrite /ltr /= /lt_rat /numq /denq /=. @@ -3023,7 +3027,7 @@ Section rat_to_Q_lemmas. rewrite /Qlt /rat_to_Q; case: r => x y /=; case: s => z w /=. case: x y => x1 z2 /= y; case: z w => z1 x2 /= w. case: (andP y) => H1 H2. - case: (andP w) => H3 H4. + case: (andP w) => H3 H4. rewrite int_to_positive_to_Z => //. rewrite int_to_positive_to_Z => //. rewrite /ltr /= /lt_rat /numq /denq /=. @@ -3044,7 +3048,7 @@ Proof. apply lt_rat_to_Q => //. Qed. -End rat_to_Q_lemmas. +End rat_to_Q_lemmas. Section rat_to_R. Variable r : rat. @@ -3055,7 +3059,7 @@ End rat_to_R. Section rat_to_R_lemmas. Local Open Scope ring_scope. Delimit Scope R_scope with R. - + Lemma rat_to_R0 : rat_to_R 0 = 0%R. Proof. by rewrite /rat_to_R /rat_to_Q /= /Q2R /= Rmult_0_l. Qed. @@ -3064,7 +3068,7 @@ Section rat_to_R_lemmas. Lemma rat_to_R2 : rat_to_R 2%:R = 2%R. Proof. by rewrite /rat_to_R /rat_to_Q /= /Q2R /= Rinv_1 Rmult_1_r. Qed. - + Lemma rat_to_R_lt (r s : rat) : lt_rat r s -> (rat_to_R r < rat_to_R s)%R. @@ -3103,7 +3107,7 @@ Section rat_to_R_lemmas. Lemma rat_to_R_le' (r s : rat) : (rat_to_R r <= rat_to_R s)%R -> - le_rat r s. + le_rat r s. Proof. rewrite /rat_to_R /rat_to_Q /=. move/Rle_Qle. @@ -3117,7 +3121,7 @@ Section rat_to_R_lemmas. rewrite 2!int_to_Z_mul in H3. by apply: le_int_to_Z. Qed. - + Lemma rat_to_R_plus (r s : rat) : rat_to_R (r + s) = (rat_to_R r + rat_to_R s)%R. Proof. @@ -3154,7 +3158,7 @@ Section rat_to_R_lemmas. rewrite <- Nat2Z.inj_0 in H. apply Nat2Z.inj in H. rewrite H. auto. - Qed. + Qed. Lemma rat_to_R_inv (r : rat) : (r != 0) -> rat_to_R r^-1 = Rinv (rat_to_R r). Proof. @@ -3174,7 +3178,7 @@ Section rat_to_R_lemmas. apply rat_to_R_0_center in H0. apply negbTE in H. congruence. move => H0. apply rat_to_R_0_center in H0. apply negbTE in H. congruence. - Qed. + Qed. Lemma rat_to_R_opp (r : rat) : rat_to_R (- r) = Ropp (rat_to_R r). Proof. have ->: -r = -1 * r by rewrite mulNr mul1r. @@ -3188,7 +3192,7 @@ Section rat_to_R_lemmas. Lemma rat_to_R1n : rat_to_R (-1) = (-1)%R. Proof. rewrite rat_to_R_opp rat_to_R1 //. - Qed. + Qed. End rat_to_R_lemmas. Section Z_to_int. @@ -3206,19 +3210,19 @@ Lemma Pos_to_natNS p : S (Pos.to_nat p).-1 = Pos.to_nat p. Proof. rewrite -(S_pred _ 0) => //. apply: Pos2Nat.is_pos. -Qed. +Qed. Lemma PosN0 p : Pos.to_nat p != O%N. Proof. apply/eqP => H. move: (Pos2Nat.is_pos p); rewrite H. inversion 1. -Qed. +Qed. Section Z_to_int_lemmas. Lemma Z_to_int0 : Z_to_int 0 = 0%R. Proof. by []. Qed. - + Lemma Z_to_int_pos_sub p q : Z_to_int (Z.pos_sub q p) = (Posz (Pos.to_nat q) + Negz (Pos.to_nat p).-1)%R. Proof. @@ -3250,8 +3254,8 @@ Section Z_to_int_lemmas. { apply IHn in H2. rewrite -minus_Sn_m. rewrite !intS H2 addrA => //. - omega. omega. - } + lia. lia. + } case: (Pos.compare_lt_iff q p) => H1 _. apply Pos.compare_gt_iff. apply H1 in H => //. case: (Pos.compare_lt_iff q p) => H1 H2. @@ -3279,11 +3283,11 @@ Section Z_to_int_lemmas. { apply IHn in H2. rewrite -minus_Sn_m. rewrite !intS H2 addrA => //. - omega. + lia. } by []. } - Qed. + Qed. Lemma Z_to_int_plus (r s : Z) : Z_to_int (r + s) = (Z_to_int r + Z_to_int s)%R. @@ -3303,7 +3307,7 @@ Section Z_to_int_lemmas. rewrite addn_gt0. apply /orP. left. apply /ltP. by apply: Pos2Nat.is_pos. Qed. - + Lemma Z_to_int_mul (r s : Z) : Z_to_int (r * s) = (Z_to_int r * Z_to_int s)%R. Proof. @@ -3340,7 +3344,7 @@ Section Z_to_int_lemmas. apply: Pos.le_refl. } move => _; move: H. by rewrite Pcompare_eq_Gt; rewrite /Pos.gt /Pos.ge => ->. - Qed. + Qed. Lemma Z_to_int_le (r s : Z) : Z.le r s -> (Z_to_int r <= Z_to_int s)%R. @@ -3351,13 +3355,13 @@ Section Z_to_int_lemmas. { case: s. { move => p H. move: (Pos2Z.is_pos p) => H2. - omega. } + lia. } { move => p q. rewrite /Z.le -(Pos2Z.inj_compare q p) Pos.compare_le_iff Pos2Nat.inj_le. move/leP => //. } move => p q; move: (Zle_neg_pos p q); move/Zle_not_lt => H H2. have H3: Z.pos q <> Z.neg p by discriminate. - omega. } + lia. } case: s => //. move => p q; move/Zneg_Zle'; rewrite Pos.ge_le_iff Pos2Nat.inj_le. move/leP => H. @@ -3370,7 +3374,7 @@ Section Z_to_int_lemmas. Z_to_int (Z.opp r) = (- Z_to_int r)%R. Proof. by rewrite Z.opp_eq_mul_m1 Z_to_int_mul /= NegzE mulrC mulN1r. Qed. End Z_to_int_lemmas. - + Section Q_to_rat. Variable q : Q. @@ -3381,10 +3385,10 @@ End Q_to_rat. Section Q_to_rat_lemmas. Lemma Q_to_rat0 : Q_to_rat 0 = 0%R. Proof. by rewrite /Q_to_rat /= Pos2Nat.inj_1 fracqE /= divr1. Qed. - + Lemma Q_to_rat1 : Q_to_rat 1 = 1%R. Proof. by rewrite /Q_to_rat /= Pos2Nat.inj_1 fracqE /= divr1. Qed. - + Lemma Q_to_rat_plus (r s : Q) : Q_to_rat (r + s) = (Q_to_rat r + Q_to_rat s)%Q. Proof. @@ -3394,7 +3398,7 @@ Section Q_to_rat_lemmas. f_equal; rewrite /addq_subdef //=; f_equal. by rewrite Pos2Nat.inj_mul. by apply: PosN0. - by apply: PosN0. + by apply: PosN0. Qed. Lemma Q_to_rat_mul (r s : Q) : @@ -3415,7 +3419,7 @@ Section Q_to_rat_lemmas. rewrite invr_gt0. by rewrite -ltz_nat -(ltr_int rat_realFieldType) in H2. Qed. - + Lemma Q_to_rat_opp r : Q_to_rat (Qopp r) = (- (Q_to_rat r))%R. Proof. @@ -3458,8 +3462,8 @@ Section Q_to_rat_lemmas. Q_to_rat (r / s) = (Q_to_rat r / Q_to_rat s)%R. Proof. rewrite Q_to_rat_mul Q_to_rat_inv => //. - Qed. - + Qed. + Lemma Q_to_rat_le (r s : Q) : Qle r s -> (Q_to_rat r <= Q_to_rat s)%R. Proof. @@ -3467,7 +3471,7 @@ Section Q_to_rat_lemmas. have <-: Q_to_rat (s + - r) = (Q_to_rat s - Q_to_rat r)%R. { rewrite Q_to_rat_plus Q_to_rat_opp //. } apply: Q_to_rat_le0. - Qed. + Qed. End Q_to_rat_lemmas. (** The proofs in this section need to be incorporated into @@ -3475,9 +3479,9 @@ End Q_to_rat_lemmas. the rat_to_Q_lemmas **) Section rat_to_Q_lemmas_cont. Local Open Scope ring_scope. - Delimit Scope R with R_ssr. + Delimit Scope R with R_ssr. Delimit Scope R_scope with R. - + Lemma cancel_Z2I x : Z_to_int (int_to_Z x) = x. Proof. destruct x => //=. @@ -3555,10 +3559,10 @@ Section rat_to_Q_lemmas_cont. 0 <= s -> 0 <= r -> (int_to_nat s) = (int_to_nat r) <-> s = r. Proof. - split; move: H H0; case: s; case: r => //; auto. + split; move: H H0; case: s; case: r => //; auto. move=> n m H0 H1 H2. by inversion H2. Qed. - + Lemma int_to_nat_inj_neg_l (s r : int) : 0 <= s -> r <= 0 -> @@ -3572,7 +3576,7 @@ Section rat_to_Q_lemmas_cont. - move => n m H0 H1 H2. rewrite NegzE /=. rewrite NegzE in H2. rewrite GRing.opprK in H2. by inversion H2. Qed. - + Lemma int_to_nat_inj_neg_r (s r : int) : s < 0 -> 0 <= r -> @@ -3620,7 +3624,7 @@ Section rat_to_Q_lemmas_cont. rewrite /Z.divide. case Hn: (0 <= n); case Hm: (0 <= m). { exists (int_to_Z (Posz k)). - rewrite int_to_Z_mul. f_equal. + rewrite int_to_Z_mul. f_equal. have H0: (`|n| = n) by apply gez0_abs. have H1: (`|m| = m) by apply gez0_abs. rewrite -H0 -H1. @@ -3666,7 +3670,7 @@ Section rat_to_Q_lemmas_cont. rewrite GRing.opprK. by apply mulr_ge0. } { exists (int_to_Z (Posz k)). - rewrite int_to_Z_mul. f_equal. + rewrite int_to_Z_mul. f_equal. have H': (n < 0) by destruct n. have H0: (`|n| = - n) by apply ltz0_abs. have Hmlt0: (m < 0) by destruct m => // . @@ -3763,9 +3767,9 @@ Section rat_to_Q_lemmas_cont. Lemma rat_to_QK1 q : rat_to_Q (Q_to_rat q) = Qred q. Proof. rewrite rat_to_Q_red. apply Qred_complete. - by rewrite cancel_rat_to_Q. + by rewrite cancel_rat_to_Q. Qed. - + Lemma rat_to_QK2 q r : Qeq q (rat_to_Q r) -> Q_to_rat q = r. Proof. move => H0. @@ -3803,7 +3807,7 @@ Proof. have ->: N.succ n = N.add 1 n. { by elim: n => // p; rewrite /N.add /Pos.add; case: p. } rewrite N_to_Q_plus; f_equal. -Qed. +Qed. Definition N_to_D (n : N.t) : D := DD (Dmake (2*NtoZ n) 1). @@ -3824,7 +3828,7 @@ Proof. rewrite Pos2Z.inj_xO /Zmult. by rewrite Pos.mul_comm. } by rewrite /Qeq /= Pos.mul_1_r Pos2Z.neg_xO /Zmult Pos.mul_comm. -Qed. +Qed. Lemma rat_to_Q_N_to_Q n : Qeq (rat_to_Q n%:R) (N_to_Q (N.of_nat n)). Proof. @@ -3839,7 +3843,7 @@ Lemma Qred_idem (q : Q) : Qred (Qred q) = Qred q. Proof. apply: Qred_complete. by rewrite Qred_correct. -Qed. +Qed. (** Dyadic real field values *) @@ -3884,7 +3888,7 @@ Proof. move => p'; rewrite /P => [][]n IH. exists (S n). by rewrite nat_of_succ_pos IH. -Qed. +Qed. Lemma nat_of_pos_inj p1 p2 : nat_of_pos p1 = nat_of_pos p2 -> p1=p2. Proof. @@ -3925,7 +3929,7 @@ Proof. Qed. Lemma N2Nat_lt n m : - (N.to_nat n < N.to_nat m)%N -> + (N.to_nat n < N.to_nat m)%N -> (n < m)%N. Proof. move: n m; apply: N.peano_ind. @@ -3936,10 +3940,10 @@ Proof. rewrite nat_of_bin_succ N2Nat.inj_succ => H. have H2: (N.to_nat n < N.to_nat m)%N. { move: H; move: (N.to_nat n); move: (N.to_nat m) => x y. - move/ltP => H; apply/ltP; omega. } + move/ltP => H; apply/ltP; lia. } suff: (n < m)%N => //. by apply: (IH _ H2). -Qed. +Qed. Lemma rat_to_R_opp_neq (n:nat) : rat_to_R n%:R = (Ropp R1) -> False. Proof. @@ -3950,11 +3954,11 @@ Proof. } { rewrite -rat_to_R0; apply: rat_to_R_le. - Local Open Scope ring_scope. + Local Open Scope ring_scope. change ((0:rat) <= n%:R). - apply: ler0n. + apply: ler0n. } -Qed. +Qed. (** END random lemmas *) diff --git a/orderedtypes.v b/orderedtypes.v index 1b9475f..db41bad 100644 --- a/orderedtypes.v +++ b/orderedtypes.v @@ -3,6 +3,7 @@ From mathcomp Require Import all_ssreflect. From mathcomp Require Import all_algebra. Require Import ProofIrrelevance. +Require Import Coq.micromega.Lia. Require Import String. Require Import QArith. Require Import Coq.FSets.FMapFacts. @@ -64,7 +65,7 @@ End OrderedFinType. Module MyOrderedType_of_OrderedFinType (A : OrderedFinType) <: MyOrderedType. - Include A. + Include A. End MyOrderedType_of_OrderedFinType. (* We now begin defining functors for constructing @@ -77,10 +78,10 @@ Module OrderedProd (A B : MyOrderedType) <: MyOrderedType. Definition t := (A.t*B.t)%type. Definition t0 := (A.t0, B.t0). Existing Instance A.enumerable. - Existing Instance B.enumerable. + Existing Instance B.enumerable. Definition enumerable : Enumerable t := _. Existing Instance A.showable. - Existing Instance B.showable. + Existing Instance B.showable. Definition show_prod (p : A.t*B.t) : string := let s1 := to_string p.1 in let s2 := to_string p.2 in @@ -94,7 +95,7 @@ Module OrderedProd (A B : MyOrderedType) <: MyOrderedType. A.lt a1 a2 \/ (A.eq a1 a2 /\ B.lt b1 b2) end. - + Lemma lt_trans : forall x y z, lt x y -> lt y z -> lt x z. Proof. case => a b; case => c d; case => e f; rewrite /lt. @@ -107,7 +108,7 @@ Module OrderedProd (A B : MyOrderedType) <: MyOrderedType. case; first by move => H3; left. case => H3 H4; right; split => //. by apply: (B.lt_trans _ _ _ H2 H4). - Qed. + Qed. Lemma lt_not_eq : forall x y, lt x y -> ~eq x y. Proof. @@ -118,7 +119,7 @@ Module OrderedProd (A B : MyOrderedType) <: MyOrderedType. case => H H1 []H2 H3. by apply: (B.lt_not_eq _ _ H1). Qed. - + Lemma compare : forall x y, Compare lt eq x y. Proof. move => x y. @@ -146,8 +147,8 @@ Module OrderedProd (A B : MyOrderedType) <: MyOrderedType. have H2: lt y x. { clear - gt_pf; move: gt_pf; case: x => a b; case: y => c d /= H. by left. } - by apply: GT H2. - Qed. + by apply: GT H2. + Qed. Lemma eq_dec : forall x y, {eq x y} + {~eq x y}. Proof. @@ -175,9 +176,9 @@ Module OrderedProd (A B : MyOrderedType) <: MyOrderedType. End OrderedProd. Module OrderedFinProd (X Y : OrderedFinType) <: OrderedFinType. - Module A := OrderedProd X Y. + Module A := OrderedProd X Y. Include A. - + Definition xE := EqType X.t X.eq_mixin. Definition xC := ChoiceType xE X.choice_mixin. Definition xF := FinType xC X.fin_mixin. @@ -185,7 +186,7 @@ Module OrderedFinProd (X Y : OrderedFinType) <: OrderedFinType. Definition yE := EqType Y.t Y.eq_mixin. Definition yC := ChoiceType yE Y.choice_mixin. Definition yF := FinType yC Y.fin_mixin. - + Definition eq_mixin := prod_eqMixin xE yE. Definition choice_mixin := prod_choiceMixin xC yC. Definition fin_mixin := prod_finMixin xF yF. @@ -207,7 +208,7 @@ Module MyOrdNatDep (B : BOUND) <: MyOrderedType. | S m' => @mk (N.of_nat m) _ :: enumerate_rec m' _ end . Next Obligation. by rewrite Nat2N.id. Qed. - + (**Program Fixpoint enumerate_rec (m : nat) (pf : (m < n)%nat) : list t := (match m as x return _ = x -> list t with | O => fun _ => t0 :: nil @@ -225,9 +226,9 @@ Module MyOrdNatDep (B : BOUND) <: MyOrderedType. Lemma gt0_pred_lt n : (0 < n -> n.-1 < n)%nat. Proof. elim: n => //. Qed. - + Definition enumerate_t : list t := - match lt_dec 0 n with + match lt_dec 0 n with | left pfn => enumerate_rec (Nat.pred n) (gt0_pred_lt _ pfn) | right _ => nil end. @@ -247,8 +248,8 @@ Module MyOrdNatDep (B : BOUND) <: MyOrderedType. f_equal. apply: proof_irrelevance. Qed. -End MyOrdNatDep. - +End MyOrdNatDep. + Module MyOrdNatDepProps (B : BOUND). Module M := MyOrdNatDep B. Include M. @@ -278,17 +279,17 @@ Module MyOrdNatDepProps (B : BOUND). move: 1%nat => nx; elim: n nx => //= n IH nx; f_equal. have ->: (n.+1 +nx = n + nx.+1)%nat by rewrite addSnnS. apply: IH. - Qed. - + Qed. + Lemma enumerate_rec_map_erased_nat m : map N.to_nat (enumerate_rec_erased m) = enumerate_rec_erased_nat m. Proof. elim: m => // m IH /=; f_equal => //. by rewrite SuccNat2Pos.id_succ. - Qed. + Qed. Lemma notin_gtn m n : - (m > n)%nat -> + (m > n)%nat -> ~InA (fun x : nat => [eta Logic.eq x]) m (enumerate_rec_erased_nat n). Proof. elim: n m. @@ -298,9 +299,9 @@ Module MyOrdNatDepProps (B : BOUND). { apply: ltn_trans; last by apply: H. by []. } inversion H2; subst => //. - move: (ltP H) => H3; omega. - Qed. - + move: (ltP H) => H3; lia. + Qed. + Lemma enumerate_rec_erased_nat_nodup m : NoDupA (fun x : nat => [eta Logic.eq x]) (enumerate_rec_erased_nat m). Proof. @@ -319,7 +320,7 @@ Module MyOrdNatDepProps (B : BOUND). move => m IH n H; case: (Nat.eq_dec n m.+1) => [pf|pf]. { by left; subst n. } right; apply: IH. - apply/leP; move: (leP H) => H2; omega. + apply/leP; move: (leP H) => H2; lia. Qed. Lemma enumerate_rec_erased_total n m : @@ -337,10 +338,10 @@ Module MyOrdNatDepProps (B : BOUND). by move: (N2Nat.inj _ _ H) => H2; subst n. } rewrite enumerate_rec_map_erased_nat. apply: (enumerate_rec_erased_nat_total _ _ H). - Qed. + Qed. Lemma enumerate_rec_total m (pf : (m < n)%nat) (x : t) : - (m.+1 = n)%nat -> + (m.+1 = n)%nat -> In x (enumerate_rec _ pf). Proof. move => Hsucc. @@ -370,18 +371,18 @@ Module MyOrdNatDepProps (B : BOUND). rewrite Nat2N.id. apply/leP; move: (ltP pfx) (ltP pf); move: (N.to_nat vx) => n0. rewrite -Hsucc => X Y. - omega. - Qed. - + lia. + Qed. + Lemma InA_map A B (f : A -> B) (l : list A) x : - InA (fun x => [eta Logic.eq x]) x l -> + InA (fun x => [eta Logic.eq x]) x l -> InA (fun x => [eta Logic.eq x]) (f x) (map f l). Proof. elim: l; first by inversion 1. move => a l IH; inversion 1; subst; first by constructor. by apply: InA_cons_tl; apply: IH. Qed. - + Lemma enumerate_rec_erased_nodup m : NoDupA (fun x => [eta Logic.eq x]) (enumerate_rec_erased m). Proof. @@ -392,7 +393,7 @@ Module MyOrdNatDepProps (B : BOUND). apply: (IH H2). } rewrite enumerate_rec_map_erased_nat. apply: enumerate_rec_erased_nat_nodup. - Qed. + Qed. Lemma enumerate_rec_nodup m pf : NoDupA (fun x : t => [eta Logic.eq x]) (enumerate_rec m pf). @@ -423,7 +424,7 @@ Module MyOrdNatDepProps (B : BOUND). case: (lt_dec 0 n) => [pf|pf]; last first. { destruct x as [vx pfx]. move: (ltP pfx) (leP pf) => X Y. - omega. } + lia. } have H: (n = S n.-1). { rewrite (ltn_predK (m:=0)) => //. } symmetry in H. @@ -447,13 +448,13 @@ Module MyOrdNatDepProps (B : BOUND). match x with Ordinal n _ => N.of_nat n end. - + Lemma rev_enumerate_enum : List.rev (List.map Ordinal_of_t enumerate_t) = enum 'I_n. Proof. rewrite /enumerate_t; case: (lt_dec 0 n); last first. - { move => a; move: (leP a) => H; move: (ltP B.n_gt0) => Hx; omega. } + { move => a; move: (leP a) => H; move: (ltP B.n_gt0) => Hx; lia. } move => pf. suff: (List.rev (map val (enumerate_rec n.-1 (gt0_pred_lt n pf))) = List.map val_of_Ordinal (enum 'I_n)). @@ -496,7 +497,7 @@ Module MyOrdNatDepProps (B : BOUND). by case: a => // m i; rewrite /val_of_Ordinal Nat2N.id. } rewrite -val_enum_ord //. } have ->: (S n.-1 = n). - { move: (ltP pf) => Hx; omega. } + { move: (ltP pf) => Hx; lia. } by []. Qed. End MyOrdNatDepProps.