diff options
42 files changed, 1230 insertions, 668 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 3a626796a6..78b4b16eff 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -62,6 +62,7 @@ before_script: # TODO figure out how to build doc for installed Coq .build-template: stage: stage-1 + interruptible: true artifacts: name: "$CI_JOB_NAME" paths: @@ -98,6 +99,7 @@ before_script: # Template for building Coq + stdlib, typical use: overload the switch .dune-template: stage: stage-1 + interruptible: true dependencies: [] script: - set -e @@ -117,6 +119,7 @@ before_script: .dune-ci-template: stage: stage-2 + interruptible: true needs: - build:edge+flambda:dune:dev dependencies: @@ -143,6 +146,7 @@ before_script: .doc-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -158,6 +162,7 @@ before_script: # set dependencies when using .test-suite-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -179,6 +184,7 @@ before_script: # set dependencies when using .validate-template: stage: stage-2 + interruptible: true dependencies: - not-a-real-job script: @@ -195,6 +201,7 @@ before_script: .ci-template: stage: stage-2 + interruptible: true script: - set -e - echo 'start:coq.test' @@ -218,6 +225,7 @@ before_script: .windows-template: stage: stage-1 + interruptible: true artifacts: name: "%CI_JOB_NAME%" paths: @@ -320,6 +328,7 @@ lint: pkg:opam: stage: stage-1 + interruptible: true # OPAM will build out-of-tree so no point in importing artifacts dependencies: [] script: @@ -336,6 +345,7 @@ pkg:opam: .nix-template: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git + interruptible: true stage: stage-1 variables: # By default we use coq.cachix.org as an extra substituter but this can be overridden diff --git a/Makefile.doc b/Makefile.doc index 125a4b33d5..50c4acb416 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -129,6 +129,8 @@ doc/unreleased.rst: $(wildcard doc/changelog/00-title.rst doc/changelog/*/*.rst) # Standard library ###################################################################### +DOCLIBS=-R theories Coq -R plugins Coq -Q user-contrib/Ltac2 Ltac2 + ### Standard library (browsable html format) ifdef QUICK @@ -139,7 +141,7 @@ endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ - -R theories Coq -R plugins Coq $(VFILES) + $(DOCLIBS) $(VFILES) mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index @@ -178,12 +180,12 @@ doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex ifdef QUICK doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq -R plugins Coq $(VFILES) > $@ + $(DOCLIBS) $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp else doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(ALLVO) $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ - -R theories Coq -R plugins Coq $(VFILES) > $@ + $(DOCLIBS) $(VFILES) > $@ sed -i.tmp -e 's///g' $@ && rm $@.tmp endif diff --git a/default.nix b/default.nix index cfadca54d2..174e199014 100644 --- a/default.nix +++ b/default.nix @@ -42,7 +42,6 @@ stdenv.mkDerivation rec { buildInputs = [ hostname python3 time # coq-makefile timing tools - dune ] ++ (with ocamlPackages; [ ocaml findlib num ]) ++ optionals buildIde [ @@ -67,6 +66,7 @@ stdenv.mkDerivation rec { [ jq curl gitFull gnupg ] # Dependencies of the merging script ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ocamlformat ]) # Dev tools ++ [ graphviz ] # Useful for STM debugging + ++ [ dune_2 ] # Maybe the next build system ); src = @@ -111,7 +111,7 @@ stdenv.mkDerivation rec { setupHook = writeText "setupHook.sh" " addCoqPath () { if test -d \"$1/lib/coq/${coq-version}/user-contrib\"; then - export COQPATH=\"$COQPATH\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\" + export COQPATH=\"\${COQPATH-}\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\" fi } diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index a9cc91170f..f08a08531f 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -60,9 +60,23 @@ let iris = (coqPackages.iris.override { inherit coq stdpp; }) let unicoq = callPackage ./unicoq { inherit coq; }; in +let StructTact = coqPackages.StructTact.overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/StructTact/tarball/master"; + }); in + +let Cheerios = (coqPackages.Cheerios.override { inherit StructTact; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/cheerios/tarball/master"; + }); in + +let Verdi = (coqPackages.Verdi.override { inherit Cheerios ssreflect; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/uwplse/verdi/tarball/master"; + }); in + let callPackage = newScope { inherit coq bignums coq-ext-lib coqprime corn iris math-classes - mathcomp simple-io ssreflect stdpp unicoq; + mathcomp simple-io ssreflect stdpp unicoq Verdi; }; in # Environments for building CI libraries with this Coq @@ -89,6 +103,7 @@ let projects = { mtac2 = callPackage ./mtac2.nix {}; oddorder = callPackage ./oddorder.nix {}; quickchick = callPackage ./quickchick.nix {}; + verdi-raft = callPackage ./verdi-raft.nix {}; VST = callPackage ./VST.nix {}; }; in diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix index 0f0ee91387..1105fba7a6 100644 --- a/dev/ci/nix/fiat_crypto.nix +++ b/dev/ci/nix/fiat_crypto.nix @@ -1,6 +1,6 @@ -{ coqprime }: +{ ocamlPackages }: { - coqBuildInputs = [ coqprime ]; + buildInputs = with ocamlPackages; [ ocaml findlib ]; configure = "git submodule update --init --recursive && ulimit -s 32768"; - make = "make new-pipeline c-files"; + make = "make c-files printlite lite && make -j 1 coq"; } diff --git a/dev/ci/nix/verdi-raft.nix b/dev/ci/nix/verdi-raft.nix new file mode 100644 index 0000000000..6a98f4ef47 --- /dev/null +++ b/dev/ci/nix/verdi-raft.nix @@ -0,0 +1,5 @@ +{ Verdi }: +{ + coqBuildInputs = [ Verdi ]; + configure = "./configure"; +} diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 0fc0a413ba..f0b8d6630f 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -5,8 +5,7 @@ for his [vscoq](https://github.com/siegebell/vscoq/) project. Here, the aim is to provide a "hands on" description of the XML protocol that coqtop and IDEs use to communicate. The protocol first appeared -with Coq 8.5, and is used by CoqIDE. It will also be used in upcoming -versions of Proof General. +with Coq 8.5, and is used by CoqIDE, [vscoq](https://github.com/siegebell/vscoq/), and other user interfaces. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/v8.10/etc/notes/coq-notes.md). diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index 677377f868..54baaee1fe 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/f4ad230f90ef312695adc26f256036203e9c70af.tar.gz"; - sha256 = "0cdd275dz3q51sknn7s087js81zvaj5riz8f29id6j6chnyikzjq"; + url = "https://github.com/NixOS/nixpkgs/archive/8da81465c19fca393a3b17004c743e4d82a98e4f.tar.gz"; + sha256 = "1f3s27nrssfk413pszjhbs70wpap43bbjx2pf4zq5x2c1kd72l6y"; }) diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst new file mode 100644 index 0000000000..5ecd46bced --- /dev/null +++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Regression of ``lia`` due to more powerful ``zify`` + (`#11362 <https://github.com/coq/coq/pull/11362>`_, + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, + by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst new file mode 100644 index 0000000000..4eb2732106 --- /dev/null +++ b/doc/changelog/04-tactics/11370-zify-elim-let.rst @@ -0,0 +1,3 @@ +- **Changed** + Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml. + (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson). diff --git a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst new file mode 100644 index 0000000000..10952c6b2c --- /dev/null +++ b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst @@ -0,0 +1,5 @@ +- **Fixed:** + ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints + commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, + fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, + by Karl Palmskog). diff --git a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst new file mode 100644 index 0000000000..2dc3992b9c --- /dev/null +++ b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst @@ -0,0 +1,5 @@ +- **Changed:** + CoqIDE now uses the GtkSourceView native implementation of + the autocomplete mechanism. + (`#11400 <https://github.com/coq/coq/pull/11400>`_, + by Pierre-Marie Pédrot). diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 7fe2493fbf..828caecabc 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,8 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins)) + (source_tree %{project_root}/plugins) + (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} ; On windows run will fail @@ -17,6 +18,7 @@ ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) (source_tree %{project_root}/plugins) + (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) ; For .glob files, should be gone when Coq Dune is smarter. @@ -24,7 +26,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index ac611926b3..5e13214a1a 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -626,6 +626,31 @@ through the <tt>Require Import</tt> command.</p> plugins/ssr/ssrfun.v </dd> + <dt> <b>Ltac2</b>: + The Ltac2 tactic programming language + </dt> + <dd> + user-contrib/Ltac2/Ltac2.v + user-contrib/Ltac2/Array.v + user-contrib/Ltac2/Bool.v + user-contrib/Ltac2/Char.v + user-contrib/Ltac2/Constr.v + user-contrib/Ltac2/Control.v + user-contrib/Ltac2/Env.v + user-contrib/Ltac2/Fresh.v + user-contrib/Ltac2/Ident.v + user-contrib/Ltac2/Init.v + user-contrib/Ltac2/Int.v + user-contrib/Ltac2/List.v + user-contrib/Ltac2/Ltac1.v + user-contrib/Ltac2/Message.v + user-contrib/Ltac2/Notations.v + user-contrib/Ltac2/Option.v + user-contrib/Ltac2/Pattern.v + user-contrib/Ltac2/Std.v + user-contrib/Ltac2/String.v + </dd> + <dt> <b>Unicode</b>: Unicode-based notations </dt> diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index bea6f24098..732f15b78a 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash # Instantiate links to library files in index template @@ -8,9 +8,14 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native` +LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native` for k in $LIBDIRS; do + if [[ $k =~ "user-contrib" ]]; then + BASE_PREFIX="" + else + BASE_PREFIX="Coq." + fi d=`basename $k` ls $k | grep -q \.v'$' if [ $? = 0 ]; then @@ -26,7 +31,7 @@ for k in $LIBDIRS; do echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1 else p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'` - sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 + sed -e "s:$k/$b.v:<a href=\"$BASE_PREFIX$p.$b.html\">$b</a>:g" tmp > tmp2 mv -f tmp2 tmp fi else diff --git a/ide/coqide.ml b/ide/coqide.ml index fc30690544..918c196968 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -618,7 +618,7 @@ let printopts_callback opts v = let get_current_word term = (* First look to find if autocompleting *) - match term.script#complete_popup#proposal with + match term.script#proposal with | Some p -> p | None -> (* Then look at the current selected word *) diff --git a/ide/preferences.ml b/ide/preferences.ml index 4ee5669877..d3cf08e90e 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -388,6 +388,9 @@ let window_height = let auto_complete = new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool) +let auto_complete_delay = + new preference ~name:["auto_complete_delay"] ~init:250 ~repr:Repr.(int) + let stop_before = new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool) @@ -831,10 +834,26 @@ let configure ?(apply=(fun () -> ())) parent = let but = GButton.check_button ~label:text ~active ~packing:box#pack () in ignore (but#connect#toggled ~callback:(fun () -> pref#set but#active)) in + let spin text ~min ~max (pref : int preference) = + let box = GPack.hbox ~packing:box#pack () in + let but = GEdit.spin_button + ~numeric:true ~update_policy:`IF_VALID ~digits:0 + ~packing:box#pack () + in + let _ = GMisc.label ~text:"Delay (ms)" ~packing:box#pack () in + let () = but#adjustment#set_bounds + ~lower:(float_of_int min) ~upper:(float_of_int max) + ~step_incr:1. + () + in + let () = but#set_value (float_of_int pref#get) in + ignore (but#connect#value_changed ~callback:(fun () -> pref#set but#value_as_int)) + in let () = button "Dynamic word wrap" dynamic_word_wrap in let () = button "Show line number" show_line_number in let () = button "Auto indentation" auto_indent in let () = button "Auto completion" auto_complete in + let () = spin "Auto completion delay" ~min:0 ~max:5000 auto_complete_delay in let () = button "Show spaces" show_spaces in let () = button "Show right margin" show_right_margin in let () = button "Show progress bar" show_progress_bar in diff --git a/ide/preferences.mli b/ide/preferences.mli index 4b04326cec..7b43079b4f 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -82,6 +82,7 @@ val show_toolbar : bool preference val window_width : int preference val window_height : int preference val auto_complete : bool preference +val auto_complete_delay : int preference val stop_before : bool preference val reset_on_tab_switch : bool preference val line_ending : line_ending preference diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index ac6712909e..396939cfcc 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -69,387 +69,101 @@ let is_substring s1 s2 = if !break then len2 - len1 else -1 -class type complete_model_signals = - object ('a) - method after : 'a - method disconnect : GtkSignal.id -> unit - method start_completion : callback:(int -> unit) -> GtkSignal.id - method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id - method end_completion : callback:(unit -> unit) -> GtkSignal.id - end - -let complete_model_signals - (start_s : int GUtil.signal) - (update_s : (int * string * Proposals.t) GUtil.signal) - (end_s : unit GUtil.signal) : complete_model_signals = -let signals = [ - start_s#disconnect; - update_s#disconnect; - end_s#disconnect; -] in -object (self : 'a) - inherit GUtil.ml_signals signals - method start_completion = start_s#connect ~after - method update_completion = update_s#connect ~after - method end_completion = end_s#connect ~after -end - -class complete_model coqtop (buffer : GText.buffer) = - let cols = new GTree.column_list in - let column = cols#add Gobject.Data.string in - let store = GTree.list_store cols in - let filtered_store = GTree.model_filter store in - let start_completion_signal = new GUtil.signal () in - let update_completion_signal = new GUtil.signal () in - let end_completion_signal = new GUtil.signal () in -object (self) - - val signals = complete_model_signals - start_completion_signal update_completion_signal end_completion_signal - val mutable active = false - val mutable auto_complete_length = 3 - (* this variable prevents CoqIDE from autocompleting when we have deleted something *) - val mutable is_auto_completing = false - (* this mutex ensure that CoqIDE will not try to autocomplete twice *) - val mutable cache = (-1, "", Proposals.empty) - val mutable insert_offset = -1 - val mutable current_completion = ("", Proposals.empty) - val mutable lock_auto_completing = true +class completion_provider coqtop = + let self_provider = ref None in + let active = ref true in + let provider = object (self) - method connect = signals + val mutable auto_complete_length = 3 + val mutable cache = (-1, "", Proposals.empty) + val mutable insert_offset = -1 - method active = active + method name = "" - method set_active b = active <- b + method icon = None - method private handle_insert iter s = - (* we're inserting, so we may autocomplete *) - is_auto_completing <- true + method private update_proposals pref = + let (_, _, props) = cache in + let filter prop = 0 <= is_substring pref prop in + let props = Proposals.filter filter props in + props - method private handle_delete ~start ~stop = - (* disable autocomplete *) - is_auto_completing <- false - - method store = filtered_store - - method column = column - - method handle_proposal path = - let row = filtered_store#get_iter path in - let proposal = filtered_store#get ~row ~column in - let (start_offset, _, _) = cache in - (* [iter] might be invalid now, get a new one to please gtk *) - let iter = buffer#get_iter `INSERT in - (* We cancel completion when the buffer has changed recently *) - if iter#offset = insert_offset then begin - let suffix = - let len1 = String.length proposal in - let len2 = insert_offset - start_offset in - String.sub proposal len2 (len1 - len2) + method private add_proposals ctx props = + let mk text = + let item = GSourceView3.source_completion_item ~text ~label:text () in + (item :> GSourceView3.source_completion_proposal) in - buffer#begin_user_action (); - ignore (buffer#insert_interactive ~iter suffix); - buffer#end_user_action (); - end - - method private init_proposals pref props = - let () = store#clear () in - let iter prop = - let iter = store#append () in - store#set ~row:iter ~column prop - in - let () = current_completion <- (pref, props) in - Proposals.iter iter props - - method private update_proposals pref = - let (_, _, props) = cache in - let filter prop = 0 <= is_substring pref prop in - let props = Proposals.filter filter props in - let () = current_completion <- (pref, props) in - let () = filtered_store#refilter () in - props - - method private do_auto_complete k = - let iter = buffer#get_iter `INSERT in - let () = insert_offset <- iter#offset in - let log = Printf.sprintf "Completion at offset: %i" insert_offset in - let () = Minilib.log log in - let prefix = - if Gtk_parsing.ends_word iter then - let start = Gtk_parsing.find_word_start iter in - let w = buffer#get_text ~start ~stop:iter () in - if String.length w >= auto_complete_length then Some (w, start) - else None - else None - in - match prefix with - | Some (w, start) -> + let props = List.map mk (Proposals.elements props) in + ctx#add_proposals (Option.get !self_provider) props true + + method populate ctx = + let iter = ctx#iter in + let buffer = new GText.buffer iter#buffer in + let start = Gtk_parsing.find_word_start iter in + let w = start#get_text ~stop:iter in let () = Minilib.log ("Completion of prefix: '" ^ w ^ "'") in let (off, prefix, props) = cache in let start_offset = start#offset in (* check whether we have the last request in cache *) if (start_offset = off) && (0 <= is_substring prefix w) then let props = self#update_proposals w in - let () = update_completion_signal#call (start_offset, w, props) in - k () + self#add_proposals ctx props else - let () = start_completion_signal#call start_offset in + let cancel = ref false in + let _ = ctx#connect#cancelled ~callback:(fun () -> cancel := true) in let update props = let () = cache <- (start_offset, w, props) in - let () = self#init_proposals w props in - update_completion_signal#call (start_offset, w, props) + if not !cancel then self#add_proposals ctx props in (* If not in the cache, we recompute it: first syntactic *) let synt = get_syntactic_completion buffer w Proposals.empty in (* Then semantic *) - let next prop = - let () = update prop in - Coq.lift k + let next props = + update props; + Coq.return () in let query = Coq.bind (get_semantic_completion w synt) next in (* If coqtop is computing, do the syntactic completion altogether *) - let occupied () = - let () = update synt in - k () - in + let occupied () = update synt in Coq.try_grab coqtop query occupied - | None -> end_completion_signal#call (); k () - - method private may_auto_complete () = - if active && is_auto_completing && lock_auto_completing then begin - let () = lock_auto_completing <- false in - let unlock () = lock_auto_completing <- true in - self#do_auto_complete unlock - end - - initializer - let filter_prop model row = - let (_, props) = current_completion in - let prop = store#get ~row ~column in - Proposals.mem prop props - in - let () = filtered_store#set_visible_func filter_prop in - (* Install auto-completion *) - ignore (buffer#connect#insert_text ~callback:self#handle_insert); - ignore (buffer#connect#delete_range ~callback:self#handle_delete); - ignore (buffer#connect#after#end_user_action ~callback:self#may_auto_complete); - -end - -class complete_popup (model : complete_model) (view : GText.view) = - let obj = GWindow.window ~kind:`POPUP ~show:false () in - let frame = GBin.scrolled_window - ~hpolicy:`NEVER ~vpolicy:`NEVER - ~shadow_type:`OUT ~packing:obj#add () - in -(* let frame = GBin.frame ~shadow_type:`OUT ~packing:obj#add () in *) - let data = GTree.view - ~vadjustment:frame#vadjustment ~hadjustment:frame#hadjustment - ~rules_hint:true ~headers_visible:false - ~model:model#store ~packing:frame#add () - in - let renderer = GTree.cell_renderer_text [], ["text", model#column] in - let col = GTree.view_column ~renderer () in - let _ = data#append_column col in - let () = col#set_sizing `AUTOSIZE in - let page_size = 16 in - -object (self) - - method coerce = view#coerce - - method private refresh_style () = - let (renderer, _) = renderer in - let font = Pango.Font.from_string Preferences.text_font#get in - renderer#set_properties [`FONT_DESC font; `XPAD 10] - - method private coordinates pos = - (* Toplevel position w.r.t. screen *) - let (x, y) = Gdk.Window.get_position view#misc#toplevel#misc#window in - (* Position of view w.r.t. window *) - let (ux, uy) = Gdk.Window.get_position view#misc#window in - (* Relative buffer position to view *) - let (dx, dy) = view#window_to_buffer_coords ~tag:`WIDGET ~x:0 ~y:0 in - (* Iter position *) - let iter = view#buffer#get_iter pos in - let coords = view#get_iter_location iter in - let lx = Gdk.Rectangle.x coords in - let ly = Gdk.Rectangle.y coords in - let w = Gdk.Rectangle.width coords in - let h = Gdk.Rectangle.height coords in - (* Absolute position *) - (x + lx + ux - dx, y + ly + uy - dy, w, h) - - method private select_any f = - let sel = data#selection#get_selected_rows in - let path = match sel with - | [] -> - begin match model#store#get_iter_first with - | None -> None - | Some iter -> Some (model#store#get_path iter) - end - | path :: _ -> Some path - in - match path with - | None -> () - | Some path -> - let path = f path in - let _ = data#selection#select_path path in - data#scroll_to_cell ~align:(0.,0.) path col - - method private select_previous () = - let prev path = - let copy = GTree.Path.copy path in - if GTree.Path.prev path then path - else copy - in - self#select_any prev - - method private select_next () = - let next path = - let () = GTree.Path.next path in - path - in - self#select_any next - method private select_previous_page () = - let rec up i path = - if i = 0 then path - else - let copy = GTree.Path.copy path in - let has_prev = GTree.Path.prev path in - if has_prev then up (pred i) path - else copy - in - self#select_any (up page_size) + method matched ctx = + if !active then + let iter = ctx#iter in + let () = insert_offset <- iter#offset in + let log = Printf.sprintf "Completion at offset: %i" insert_offset in + let () = Minilib.log log in + if Gtk_parsing.ends_word iter#backward_char then + let start = Gtk_parsing.find_word_start iter in + iter#offset - start#offset >= auto_complete_length + else false + else false - method private select_next_page () = - let rec down i path = - if i = 0 then path - else - let copy = GTree.Path.copy path in - let iter = model#store#get_iter path in - let has_next = model#store#iter_next iter in - if has_next then down (pred i) (model#store#get_path iter) - else copy - in - self#select_any (down page_size) + method activation = [`INTERACTIVE; `USER_REQUESTED] - method private select_first () = - let rec up path = - let copy = GTree.Path.copy path in - let has_prev = GTree.Path.prev path in - if has_prev then up path - else copy - in - self#select_any up + method info_widget proposal = None - method private select_last () = - let rec down path = - let copy = GTree.Path.copy path in - let iter = model#store#get_iter path in - let has_next = model#store#iter_next iter in - if has_next then down (model#store#get_path iter) - else copy - in - self#select_any down + method update_info proposal info = () - method private select_enter () = - let sel = data#selection#get_selected_rows in - match sel with - | [] -> () - | path :: _ -> - let () = model#handle_proposal path in - self#hide () + method start_iter ctx proposal iter = false - method proposal = - let sel = data#selection#get_selected_rows in - if obj#misc#visible then match sel with - | [] -> None - | path :: _ -> - let row = model#store#get_iter path in - let column = model#column in - let proposal = model#store#get ~row ~column in - Some proposal - else None + method activate_proposal proposal iter = false - method private manage_scrollbar () = - (* HACK: we don't have access to the treeview size because of the lack of - LablGTK binding for certain functions, so we bypass it by approximating - it through the size of the proposals *) - let height = match model#store#get_iter_first with - | None -> -1 - | Some iter -> - let path = model#store#get_path iter in - let area = data#get_cell_area ~path ~col () in - let height = Gdk.Rectangle.height area in - let height = page_size * height in - height - in - let len = ref 0 in - let () = model#store#foreach (fun _ _ -> incr len; false) in - if !len > page_size then - let () = frame#set_vpolicy `ALWAYS in - data#misc#set_size_request ~height () - else - data#misc#set_size_request ~height:(-1) () + method interactive_delay = (-1) - method private refresh () = - let () = frame#set_vpolicy `NEVER in - let () = self#select_first () in - let () = obj#misc#show () in - let () = self#manage_scrollbar () in - obj#resize ~width:1 ~height:1 + method priority = 0 - method private start_callback off = - let (x, y, w, h) = self#coordinates (`OFFSET off) in - let () = obj#move ~x ~y:(y + 3 * h / 2) in - () + end in + let provider = GSourceView3.source_completion_provider provider in + object (self) - method private update_callback (off, word, props) = - if Proposals.is_empty props then self#hide () - else if Proposals.mem word props then self#hide () - else self#refresh () + inherit GSourceView3.source_completion_provider provider#as_source_completion_provider - method private end_callback () = - obj#misc#hide () + method active = !active - method private hide () = self#end_callback () + method set_active b = active := b - initializer - let move_cb _ _ ~extend = self#hide () in - let key_cb ev = - let eval cb = cb (); true in - let ev_key = GdkEvent.Key.keyval ev in - if obj#misc#visible then - if ev_key = GdkKeysyms._Up then eval self#select_previous - else if ev_key = GdkKeysyms._Down then eval self#select_next - else if ev_key = GdkKeysyms._Tab then eval self#select_enter - else if ev_key = GdkKeysyms._Return then eval self#select_enter - else if ev_key = GdkKeysyms._Escape then eval self#hide - else if ev_key = GdkKeysyms._Page_Down then eval self#select_next_page - else if ev_key = GdkKeysyms._Page_Up then eval self#select_previous_page - else if ev_key = GdkKeysyms._Home then eval self#select_first - else if ev_key = GdkKeysyms._End then eval self#select_last - else false - else false - in - (* Style handling *) - let _ = view#misc#connect#style_set ~callback:self#refresh_style in - let _ = self#refresh_style () in - let _ = data#set_resize_mode `PARENT in - let _ = frame#set_resize_mode `PARENT in - (* Callback to model *) - let _ = model#connect#start_completion ~callback:self#start_callback in - let _ = model#connect#update_completion ~callback:self#update_callback in - let _ = model#connect#end_completion ~callback:self#end_callback in - (* Popup interaction *) - let _ = view#event#connect#key_press ~callback:key_cb in - (* Hiding the popup when necessary*) - let _ = view#misc#connect#hide ~callback:obj#misc#hide in - let _ = view#event#connect#button_press ~callback:(fun _ -> self#hide (); false) in - let _ = view#connect#move_cursor ~callback:move_cb in - let _ = view#event#connect#focus_out ~callback:(fun _ -> self#hide (); false) in - () + initializer + self_provider := Some (self :> GSourceView3.source_completion_provider) -end + end diff --git a/ide/wg_Completion.mli b/ide/wg_Completion.mli index ac9e6cd94f..020fe26cfb 100644 --- a/ide/wg_Completion.mli +++ b/ide/wg_Completion.mli @@ -10,27 +10,9 @@ module Proposals : sig type t end -class type complete_model_signals = - object ('a) - method after : 'a - method disconnect : GtkSignal.id -> unit - method start_completion : callback:(int -> unit) -> GtkSignal.id - method update_completion : callback:(int * string * Proposals.t -> unit) -> GtkSignal.id - method end_completion : callback:(unit -> unit) -> GtkSignal.id - end - -class complete_model : Coq.coqtop -> GText.buffer -> +class completion_provider : Coq.coqtop -> object + inherit GSourceView3.source_completion_provider method active : bool - method connect : complete_model_signals method set_active : bool -> unit - method store : GTree.model_filter - method column : string GTree.column - method handle_proposal : Gtk.tree_path -> unit -end - -class complete_popup : complete_model -> GText.view -> -object - method coerce : GObj.widget - method proposal : string option end diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 769ce61ee1..b7a35d7e94 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -287,18 +287,17 @@ end class script_view (tv : source_view) (ct : Coq.coqtop) = let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in -let completion = new Wg_Completion.complete_model ct view#buffer in -let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in +let provider = new Wg_Completion.completion_provider ct in object (self) inherit GSourceView3.source_view (Gobject.unsafe_cast tv) val undo_manager = new undo_manager view#buffer - method auto_complete = completion#active + method auto_complete = provider#active method set_auto_complete flag = - completion#set_active flag + provider#set_active flag method recenter_insert = self#scroll_to_mark @@ -448,7 +447,7 @@ object (self) self#buffer#delete_mark (`MARK insert_mark) - method complete_popup = popup + method proposal : string option = None (* FIXME *) method undo = undo_manager#undo method redo = undo_manager#redo @@ -527,10 +526,15 @@ object (self) stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs; stick tab_length self self#set_tab_width; stick auto_complete self self#set_auto_complete; + stick auto_complete_delay self (fun d -> self#completion#set_auto_complete_delay d); let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in stick text_font self cb; + let () = self#completion#set_accelerators 0 in + let () = self#completion#set_show_headers false in + let _ = self#completion#add_provider (provider :> GSourceView3.source_completion_provider) in + () end diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index 91c8e758a5..4b6591e063 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -28,7 +28,7 @@ object method uncomment : unit -> unit method apply_unicode_binding : unit -> unit method recenter_insert : unit - method complete_popup : Wg_Completion.complete_popup + method proposal : string option end val script_view : Coq.coqtop -> diff --git a/plugins/micromega/Zify.v b/plugins/micromega/Zify.v index 785a53fafa..18cd196148 100644 --- a/plugins/micromega/Zify.v +++ b/plugins/micromega/Zify.v @@ -87,4 +87,4 @@ Ltac applySpec S := (** [zify_post_hook] is there to be redefined. *) Ltac zify_post_hook := idtac. -Ltac zify := zify_op ; (iter_specs applySpec) ; zify_post_hook. +Ltac zify := zify_op ; (zify_iter_specs applySpec) ; zify_post_hook. diff --git a/plugins/micromega/ZifyInst.v b/plugins/micromega/ZifyInst.v index 97f6fe0613..edfb5a2a94 100644 --- a/plugins/micromega/ZifyInst.v +++ b/plugins/micromega/ZifyInst.v @@ -523,3 +523,22 @@ Instance SatProdPos : Saturate Z.mul := SatOk := Z.mul_pos_pos |}. Add Saturate SatProdPos. + +Lemma pow_pos_strict : + forall a b, + 0 < a -> 0 < b -> 0 < a ^ b. +Proof. + intros. + apply Z.pow_pos_nonneg; auto. + apply Z.lt_le_incl;auto. +Qed. + + +Instance SatPowPos : Saturate Z.pow := + {| + PArg1 := fun x => 0 < x; + PArg2 := fun y => 0 < y; + PRes := fun r => 0 < r; + SatOk := pow_pos_strict + |}. +Add Saturate SatPowPos. diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index cb15274736..61234145e1 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -395,50 +395,40 @@ let saturate_by_linear_equalities sys = output_sys sys output_sys sys'; sys' -(* let saturate_linear_equality_non_linear sys0 = - let (l,_) = extract_all (is_substitution false) sys0 in - let rec elim l acc = - match l with - | [] -> acc - | (v,pc)::l' -> - let nc = saturate (non_linear_pivot sys0 pc v) (sys0@acc) in - elim l' (nc@acc) in - elim l [] - *) - -let bounded_vars (sys : WithProof.t list) = - let l = fst (extract_all (fun ((p, o), prf) -> LinPoly.is_variable p) sys) in - List.fold_left (fun acc (i, wp) -> IMap.add i wp acc) IMap.empty l - -let rec power n p = if n = 1 then p else WithProof.product p (power (n - 1) p) - -let bound_monomial mp m = - if Monomial.is_var m || Monomial.is_const m then None - else - try - Some - (Monomial.fold - (fun v i acc -> - let wp = IMap.find v mp in - WithProof.product (power i wp) acc) - m (WithProof.const (Int 1))) - with Not_found -> None - let bound_monomials (sys : WithProof.t list) = - let mp = bounded_vars sys in - let m = + let l = + extract_all + (fun ((p, o), _) -> + match LinPoly.get_bound p with + | None -> None + | Some Vect.Bound.{cst; var; coeff} -> + Some (Monomial.degree (LinPoly.MonT.retrieve var))) + sys + in + let deg = + List.fold_left (fun acc ((p, o), _) -> max acc (LinPoly.degree p)) 0 sys + in + let vars = List.fold_left - (fun acc ((p, _), _) -> - Vect.fold - (fun acc v _ -> - let m = LinPoly.MonT.retrieve v in - match bound_monomial mp m with - | None -> acc - | Some r -> IMap.add v r acc) - acc p) - IMap.empty sys + (fun acc ((p, o), _) -> ISet.union (LinPoly.monomials p) acc) + ISet.empty sys + in + let bounds = + saturate_bin + (fun (i1, w1) (i2, w2) -> + if i1 + i2 > deg then None + else + match WithProof.mul_bound w1 w2 with + | None -> None + | Some b -> Some (i1 + i2, b)) + (fst l) + in + let has_mon (_, ((p, o), _)) = + match LinPoly.get_bound p with + | None -> false + | Some Vect.Bound.{cst; var; coeff} -> ISet.mem var vars in - IMap.fold (fun _ e acc -> e :: acc) m [] + List.map snd (List.filter has_mon bounds) @ snd l let develop_constraints prfdepth n_spec sys = LinPoly.MonT.clear (); diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg index 66f263c0b1..2b5fac32a2 100644 --- a/plugins/micromega/g_zify.mlg +++ b/plugins/micromega/g_zify.mlg @@ -34,12 +34,13 @@ VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF END TACTIC EXTEND ITER -| [ "iter_specs" tactic(t)] -> { Zify.iter_specs t } +| [ "zify_iter_specs" tactic(t)] -> { Zify.iter_specs t } END TACTIC EXTEND TRANS | [ "zify_op" ] -> { Zify.zify_tac } -| [ "saturate" ] -> { Zify.saturate } +| [ "zify_saturate" ] -> { Zify.saturate } +| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t } END VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 03f042647c..160b492d3d 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -140,6 +140,25 @@ let saturate p f sys = Printexc.print_backtrace stdout; raise x +let saturate_bin (f : 'a -> 'a -> 'a option) (l : 'a list) = + let rec map_with acc e l = + match l with + | [] -> acc + | e' :: l' -> ( + match f e e' with + | None -> map_with acc e l' + | Some r -> map_with (r :: acc) e l' ) + in + let rec map2_with acc l' = + match l' with [] -> acc | e' :: l' -> map2_with (map_with acc e' l) l' + in + let rec iterate acc l' = + match map2_with [] l' with + | [] -> List.rev_append l' acc + | res -> iterate (List.rev_append l' acc) res + in + iterate [] l + open Num open Big_int diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index ef8d154b13..5dcaf3be44 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -116,6 +116,7 @@ val simplify : ('a -> 'a option) -> 'a list -> 'a list option val saturate : ('a -> 'b option) -> ('b * 'a -> 'a -> 'a option) -> 'a list -> 'a list +val saturate_bin : ('a -> 'a -> 'a option) -> 'a list -> 'a list val generate : ('a -> 'b option) -> 'a list -> 'b list val app_funs : ('a -> 'b option) list -> 'a -> 'b option val command : string -> string array -> 'a -> 'b diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index a4f9b60b14..b20213979b 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -379,6 +379,8 @@ module LinPoly = struct else acc) [] l + let get_bound p = Vect.Bound.of_vect p + let min_list (l : int list) = match l with [] -> None | e :: l -> Some (List.fold_left min e l) @@ -892,8 +894,9 @@ module WithProof = struct if Vect.is_null r && n >/ Int 0 then ((LinPoly.product p p1, o1), ProofFormat.mul_cst_proof n prf1) else ( - Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output - ((p1, o1), prf1); + if debug then + Printf.printf "mult_error %a [*] %a\n" LinPoly.pp p output + ((p1, o1), prf1); raise InvalidProof ) let cutting_plane ((p, o), prf) = @@ -1027,6 +1030,31 @@ module WithProof = struct else None in saturate select gen sys0 + + open Vect.Bound + + let mul_bound w1 w2 = + let (p1, o1), prf1 = w1 in + let (p2, o2), prf2 = w2 in + match (LinPoly.get_bound p1, LinPoly.get_bound p2) with + | None, _ | _, None -> None + | ( Some {cst = c1; var = v1; coeff = c1'} + , Some {cst = c2; var = v2; coeff = c2'} ) -> ( + let good_coeff b o = + match o with + | Eq -> Some (minus_num b) + | _ -> if b <=/ Int 0 then Some (minus_num b) else None + in + match (good_coeff c1 o2, good_coeff c2 o1) with + | None, _ | _, None -> None + | Some c1, Some c2 -> + let ext_mult c w = + if c =/ Int 0 then zero else mult (LinPoly.constant c) w + in + Some + (addition + (addition (product w1 w2) (ext_mult c1 w2)) + (ext_mult c2 w1)) ) end (* Local Variables: *) diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index 7e905ac69b..4b56b037e0 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -224,6 +224,8 @@ module LinPoly : sig p is linear in x i.e x does not occur in b and a is a constant such that [pred a] *) + val get_bound : t -> Vect.Bound.t option + val product : t -> t -> t (** [product p q] @return the product of the polynomial [p*q] *) @@ -372,4 +374,5 @@ module WithProof : sig val saturate_subst : bool -> t list -> t list val is_substitution : bool -> t -> var option + val mul_bound : t -> t -> t option end diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 5d8ae83853..e71c89b4db 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -965,6 +965,43 @@ let trans_concl t = let tclTHENOpt e tac tac' = match e with None -> tac' | Some e' -> Tacticals.New.tclTHEN (tac e') tac' +let assert_inj t = + init_cache (); + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + try + ignore (get_injection env evd t); + Tacticals.New.tclIDTAC + with Not_found -> + Tacticals.New.tclFAIL 0 (Pp.str " InjTyp does not exist")) + +let do_let tac (h : Constr.named_declaration) = + match h with + | Context.Named.Declaration.LocalAssum _ -> Tacticals.New.tclIDTAC + | Context.Named.Declaration.LocalDef (id, t, ty) -> + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + try + ignore (get_injection env evd (EConstr.of_constr ty)); + tac id.Context.binder_name t ty + with Not_found -> Tacticals.New.tclIDTAC) + +let iter_let tac = + Proofview.Goal.enter (fun gl -> + let env = Tacmach.New.pf_env gl in + let sign = Environ.named_context env in + Tacticals.New.tclMAP (do_let tac) sign) + +let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) = + init_cache (); + iter_let (fun (id : Names.Id.t) (t : Constr.types) (ty : Constr.types) -> + Ltac_plugin.Tacinterp.Value.apply tac + [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id) + ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr t) + ; Ltac_plugin.Tacinterp.Value.of_constr (EConstr.of_constr ty) ]) + let zify_tac = Proofview.Goal.enter (fun gl -> Coqlib.check_required_library ["Coq"; "micromega"; "ZifyClasses"]; diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli index 9e3cf5d24c..4930a845c9 100644 --- a/plugins/micromega/zify.mli +++ b/plugins/micromega/zify.mli @@ -27,3 +27,5 @@ module Saturate : S val zify_tac : unit Proofview.tactic val saturate : unit Proofview.tactic val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic +val assert_inj : EConstr.constr -> unit Proofview.tactic +val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index f5d53cbbf3..34533670f8 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -573,27 +573,16 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. Require Import ZifyClasses ZifyInst. Require Zify. - -(** [is_inj T] returns true iff the type T has an injection *) -Ltac is_inj T := - match T with - | _ => let x := constr:(_ : InjTyp T _ ) in true - | _ => false - end. - (* [elim_let] replaces a let binding (x := e : t) by an equation (x = e) if t is an injected type *) -Ltac elim_let := - repeat - match goal with - | x := ?t : ?ty |- _ => - let b := is_inj ty in - match b with - | true => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x - end - end. +Ltac elim_binding x t ty := + let h := fresh "heq_" x in + pose proof (@eq_refl ty x : @eq ty x t) as h; + try clearbody x. + +Ltac elim_let := zify_iter_let elim_binding. Ltac zify := intros ; elim_let ; - Zify.zify ; ZifyInst.saturate. + Zify.zify ; ZifyInst.zify_saturate. diff --git a/test-suite/bugs/closed/bug_11133.v b/test-suite/bugs/closed/bug_11133.v new file mode 100644 index 0000000000..87f15a4a19 --- /dev/null +++ b/test-suite/bugs/closed/bug_11133.v @@ -0,0 +1,18 @@ +Module Type Universe. +Parameter U : nat. +End Universe. + +Module Univ_prop (Univ : Universe). +Include Univ. +End Univ_prop. + +Module Monad (Univ : Universe). +Module UP := (Univ_prop Univ). +End Monad. + +Module Rules (Univ:Universe). +Module MP := Monad Univ. +Include MP. +Import UP. +Definition M := UP.U. (* anomaly here *) +End Rules. diff --git a/test-suite/bugs/closed/bug_11168.v b/test-suite/bugs/closed/bug_11168.v new file mode 100644 index 0000000000..6e109e33e6 --- /dev/null +++ b/test-suite/bugs/closed/bug_11168.v @@ -0,0 +1,5 @@ +Axiom f : forall T, T. +Arguments f &. +Check f _ _. +Check f (_ -> _) _. +Check f (forall x, _) _. diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out new file mode 100644 index 0000000000..0b4b4b6e37 --- /dev/null +++ b/test-suite/coqdoc/bug11353.html.out @@ -0,0 +1,39 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" +"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug11353</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug11353</h1> + +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> := 0. #[ <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/> +<span class="id" title="keyword">Inductive</span> <a name="mysum"><span class="id" title="inductive">mysum</span></a> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/> + | <a name="myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a><br/> + | <a name="myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><span class="id" title="variable">B</span></a>.<br/> + +<br/> +#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a name="b"><span class="id" title="definition">b</span></a> := 1.<br/> +</div> +</div> + +<div id="footer"> +<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> +</div> + +</div> + +</body> +</html>
\ No newline at end of file diff --git a/test-suite/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out new file mode 100644 index 0000000000..a6478682d8 --- /dev/null +++ b/test-suite/coqdoc/bug11353.tex.out @@ -0,0 +1,34 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug11353}{Library }{Coqdoc.bug11353} + +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug11353.a}{a}{\coqdocdefinition{a}} := 0. \#[ \coqdocvar{universes}( \coqdocvar{template}) ]\coqdoceol +\coqdocnoindent +\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdocvar{A} \coqdocvar{B}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqdocvariable{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqdocvariable{B} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}.\coqdoceol +\coqdocemptyline +\coqdocnoindent +\#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug11353.v b/test-suite/coqdoc/bug11353.v new file mode 100644 index 0000000000..b68902c8cc --- /dev/null +++ b/test-suite/coqdoc/bug11353.v @@ -0,0 +1,7 @@ +(* -*- coq-prog-args: ("-g") -*- *) +Definition a := 0. #[ (* templatize *) universes( template) ] +Inductive mysum (A B:Type) : Type := + | myinl : A -> mysum A B + | myinr : B -> mysum A B. + +#[local]Definition b := 1. diff --git a/test-suite/micromega/bug_11191a.v b/test-suite/micromega/bug_11191a.v new file mode 100644 index 0000000000..57c1d7d52f --- /dev/null +++ b/test-suite/micromega/bug_11191a.v @@ -0,0 +1,6 @@ +Require Import ZArith Lia. + +Goal forall p n, (0 < Z.pos (p ^ n))%Z. + intros. + lia. +Qed. diff --git a/test-suite/micromega/bug_11191b.v b/test-suite/micromega/bug_11191b.v new file mode 100644 index 0000000000..007470c5b3 --- /dev/null +++ b/test-suite/micromega/bug_11191b.v @@ -0,0 +1,6 @@ +Require Import ZArith Lia. + +Goal forall p, (0 < Z.pos (p ^ 2))%Z. + intros. + lia. +Qed. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 38723e291f..74335da2f1 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -120,62 +120,6 @@ Section Facts. Qed. - (************************) - (** *** Facts about [In] *) - (************************) - - - (** Characterization of [In] *) - - Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). - Proof. - simpl; auto. - Qed. - - Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). - Proof. - simpl; auto. - Qed. - - Theorem not_in_cons (x a : A) (l : list A): - ~ In x (a::l) <-> x<>a /\ ~ In x l. - Proof. - simpl. intuition. - Qed. - - Theorem in_nil : forall a:A, ~ In a []. - Proof. - unfold not; intros a H; inversion_clear H. - Qed. - - Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. - Proof. - induction l; simpl; destruct 1. - subst a; auto. - exists [], l; auto. - destruct (IHl H) as (l1,(l2,H0)). - exists (a::l1), l2; simpl. apply f_equal. auto. - Qed. - - (** Inversion *) - Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. - Proof. - intros a b l H; inversion_clear H; auto. - Qed. - - (** Decidability of [In] *) - Theorem in_dec : - (forall x y:A, {x = y} + {x <> y}) -> - forall (a:A) (l:list A), {In a l} + {~ In a l}. - Proof. - intro H; induction l as [| a0 l IHl]. - right; apply in_nil. - destruct (H a0 a); simpl; auto. - destruct IHl; simpl; auto. - right; unfold not; intros [Hc1| Hc2]; auto. - Defined. - - (**************************) (** *** Facts about [app] *) (**************************) @@ -255,6 +199,14 @@ Section Facts. apply app_cons_not_nil in H1 as []. Qed. + Lemma elt_eq_unit : forall l1 l2 (a b : A), + l1 ++ a :: l2 = [b] -> a = b /\ l1 = [] /\ l2 = []. + Proof. + intros l1 l2 a b Heq. + apply app_eq_unit in Heq. + now destruct Heq as [[Heq1 Heq2]|[Heq1 Heq2]]; inversion_clear Heq2. + Qed. + Lemma app_inj_tail : forall (x y:list A) (a b:A), x ++ [a] = y ++ [b] -> x = y /\ a = b. Proof. @@ -281,6 +233,61 @@ Section Facts. induction l; simpl; auto. Qed. + Lemma last_length : forall (l : list A) a, length (l ++ a :: nil) = S (length l). + Proof. + intros ; rewrite app_length ; simpl. + rewrite <- plus_n_Sm, plus_n_O; reflexivity. + Qed. + + Lemma app_inv_head: + forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + Proof. + induction l; simpl; auto; injection 1; auto. + Qed. + + Lemma app_inv_tail: + forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + Proof. + intros l l1 l2; revert l1 l2 l. + induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; + simpl; auto; intros l H. + absurd (length (x2 :: l2 ++ l) <= length l). + simpl; rewrite app_length; auto with arith. + rewrite <- H; auto with arith. + absurd (length (x1 :: l1 ++ l) <= length l). + simpl; rewrite app_length; auto with arith. + rewrite H; auto with arith. + injection H as [= H H0]; f_equal; eauto. + Qed. + + (************************) + (** *** Facts about [In] *) + (************************) + + + (** Characterization of [In] *) + + Theorem in_eq : forall (a:A) (l:list A), In a (a :: l). + Proof. + simpl; auto. + Qed. + + Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l). + Proof. + simpl; auto. + Qed. + + Theorem not_in_cons (x a : A) (l : list A): + ~ In x (a::l) <-> x<>a /\ ~ In x l. + Proof. + simpl. intuition. + Qed. + + Theorem in_nil : forall a:A, ~ In a []. + Proof. + unfold not; intros a H; inversion_clear H. + Qed. + Lemma in_app_or : forall (l m:list A) (a:A), In a (l ++ m) -> In a l \/ In a m. Proof. intros l m a. @@ -314,27 +321,48 @@ Section Facts. split; auto using in_app_or, in_or_app. Qed. - Lemma app_inv_head: - forall l l1 l2 : list A, l ++ l1 = l ++ l2 -> l1 = l2. + Theorem in_split : forall x (l:list A), In x l -> exists l1 l2, l = l1++x::l2. Proof. - induction l; simpl; auto; injection 1; auto. + induction l; simpl; destruct 1. + subst a; auto. + exists [], l; auto. + destruct (IHl H) as (l1,(l2,H0)). + exists (a::l1), l2; simpl. apply f_equal. auto. Qed. - Lemma app_inv_tail: - forall l l1 l2 : list A, l1 ++ l = l2 ++ l -> l1 = l2. + Lemma in_elt : forall (x:A) l1 l2, In x (l1 ++ x :: l2). Proof. - intros l l1 l2; revert l1 l2 l. - induction l1 as [ | x1 l1]; destruct l2 as [ | x2 l2]; - simpl; auto; intros l H. - absurd (length (x2 :: l2 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite <- H; auto with arith. - absurd (length (x1 :: l1 ++ l) <= length l). - simpl; rewrite app_length; auto with arith. - rewrite H; auto with arith. - injection H as [= H H0]; f_equal; eauto. + intros. + apply in_or_app. + right; left; reflexivity. + Qed. + + Lemma in_elt_inv : forall (x y : A) l1 l2, + In x (l1 ++ y :: l2) -> x = y \/ In x (l1 ++ l2). + Proof. + intros x y l1 l2 Hin. + apply in_app_or in Hin. + destruct Hin as [Hin|[Hin|Hin]]; [right|left|right]; try apply in_or_app; intuition. Qed. + (** Inversion *) + Lemma in_inv : forall (a b:A) (l:list A), In b (a :: l) -> a = b \/ In b l. + Proof. easy. Qed. + + (** Decidability of [In] *) + Theorem in_dec : + (forall x y:A, {x = y} + {x <> y}) -> + forall (a:A) (l:list A), {In a l} + {~ In a l}. + Proof. + intro H; induction l as [| a0 l IHl]. + right; apply in_nil. + destruct (H a0 a); simpl; auto. + destruct IHl; simpl; auto. + right; unfold not; intros [Hc1| Hc2]; auto. + Defined. + + + End Facts. Hint Resolve app_assoc app_assoc_reverse: datatypes. @@ -463,6 +491,22 @@ Section Elts. - intros; simpl; rewrite IHl; auto with arith. Qed. + Lemma app_nth2_plus : forall l l' d n, + nth (length l + n) (l ++ l') d = nth n l' d. + Proof. + intros. + rewrite app_nth2, minus_plus; trivial. + auto with arith. + Qed. + + Lemma nth_middle : forall l l' a d, + nth (length l) (l ++ a :: l') d = a. + Proof. + intros. + rewrite plus_n_O at 1. + apply app_nth2_plus. + Qed. + Lemma nth_split n l d : n < length l -> exists l1, exists l2, l = l1 ++ nth n l d :: l2 /\ length l1 = n. Proof. @@ -473,6 +517,20 @@ Section Elts. exists (a::l1); exists l2; simpl; split; now f_equal. Qed. + Lemma nth_ext : forall l l' d, length l = length l' -> + (forall n, nth n l d = nth n l' d) -> l = l'. + Proof. + induction l; intros l' d Hlen Hnth; destruct l' as [| b l']. + - reflexivity. + - inversion Hlen. + - inversion Hlen. + - change a with (nth 0 (a :: l) d). + change b with (nth 0 (b :: l') d). + rewrite Hnth; f_equal. + apply IHl with d; [ now inversion Hlen | ]. + intros n; apply (Hnth (S n)). + Qed. + (** Results about [nth_error] *) Lemma nth_error_In l n x : nth_error l n = Some x -> In x l. @@ -556,31 +614,9 @@ Section Elts. rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity. Qed. - (*****************) - (** ** Remove *) - (*****************) - - Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. - - Fixpoint remove (x : A) (l : list A) : list A := - match l with - | [] => [] - | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) - end. - - Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). - Proof. - induction l as [|x l]; auto. - intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. - apply IHl. - unfold not; intro HF; simpl in HF; destruct HF; auto. - apply (IHl y); assumption. - Qed. - - -(******************************) -(** ** Last element of a list *) -(******************************) + (******************************) + (** ** Last element of a list *) + (******************************) (** [last l d] returns the last element of the list [l], or the default value [d] if [l] is empty. *) @@ -592,6 +628,13 @@ Section Elts. | a :: l => last l d end. + Lemma last_last : forall l a d, last (l ++ [a]) d = a. + Proof. + induction l; intros; [ reflexivity | ]. + simpl; rewrite IHl. + destruct l; reflexivity. + Qed. + (** [removelast l] remove the last element of [l] *) Fixpoint removelast (l:list A) : list A := @@ -638,6 +681,119 @@ Section Elts. destruct (l++l'); [elim H0; auto|f_equal; auto]. Qed. + Lemma removelast_last : forall l a, removelast (l ++ [a]) = l. + Proof. + intros. + rewrite removelast_app. + - apply app_nil_r. + - intros Heq; inversion Heq. + Qed. + + + (*****************) + (** ** Remove *) + (*****************) + + Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. + + Fixpoint remove (x : A) (l : list A) : list A := + match l with + | [] => [] + | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) + end. + + Lemma remove_cons : forall x l, remove x (x :: l) = remove x l. + Proof. + intros x l; simpl; destruct (eq_dec x x); [ reflexivity | now exfalso ]. + Qed. + + Lemma remove_app : forall x l1 l2, + remove x (l1 ++ l2) = remove x l1 ++ remove x l2. + Proof. + induction l1; intros l2; simpl. + - reflexivity. + - destruct (eq_dec x a). + + apply IHl1. + + rewrite <- app_comm_cons; f_equal. + apply IHl1. + Qed. + + Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l). + Proof. + induction l as [|x l]; auto. + intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. + apply IHl. + unfold not; intro HF; simpl in HF; destruct HF; auto. + apply (IHl y); assumption. + Qed. + + Lemma notin_remove: forall l x, ~ In x l -> remove x l = l. + Proof. + intros l x; induction l as [|y l]; simpl; intros Hnin. + - reflexivity. + - destruct (eq_dec x y); subst; intuition. + f_equal; assumption. + Qed. + + Lemma in_remove: forall l x y, In x (remove y l) -> In x l /\ x <> y. + Proof. + induction l as [|z l]; intros x y Hin. + - inversion Hin. + - simpl in Hin. + destruct (eq_dec y z) as [Heq|Hneq]; subst; split. + + right; now apply IHl with z. + + intros Heq; revert Hin; subst; apply remove_In. + + inversion Hin; subst; [left; reflexivity|right]. + now apply IHl with y. + + destruct Hin as [Hin|Hin]; subst. + * now intros Heq; apply Hneq. + * intros Heq; revert Hin; subst; apply remove_In. + Qed. + + Lemma in_in_remove : forall l x y, x <> y -> In x l -> In x (remove y l). + Proof. + induction l as [|z l]; simpl; intros x y Hneq Hin. + - apply Hin. + - destruct (eq_dec y z); subst. + + destruct Hin. + * exfalso; now apply Hneq. + * now apply IHl. + + simpl; destruct Hin; [now left|right]. + now apply IHl. + Qed. + + Lemma remove_remove_comm : forall l x y, + remove x (remove y l) = remove y (remove x l). + Proof. + induction l as [| z l]; simpl; intros x y. + - reflexivity. + - destruct (eq_dec y z); simpl; destruct (eq_dec x z); try rewrite IHl; auto. + + subst; symmetry; apply remove_cons. + + simpl; destruct (eq_dec y z); tauto. + Qed. + + Lemma remove_remove_eq : forall l x, remove x (remove x l) = remove x l. + Proof. intros l x; now rewrite (notin_remove _ _ (remove_In l x)). Qed. + + Lemma remove_length_le : forall l x, length (remove x l) <= length l. + Proof. + induction l as [|y l IHl]; simpl; intros x; trivial. + destruct (eq_dec x y); simpl. + - rewrite IHl; constructor; reflexivity. + - apply (proj1 (Nat.succ_le_mono _ _) (IHl x)). + Qed. + + Lemma remove_length_lt : forall l x, In x l -> length (remove x l) < length l. + Proof. + induction l as [|y l IHl]; simpl; intros x Hin. + - contradiction Hin. + - destruct Hin as [-> | Hin]. + + destruct (eq_dec x x); intuition. + apply Nat.lt_succ_r, remove_length_le. + + specialize (IHl _ Hin); destruct (eq_dec x y); simpl; auto. + now apply Nat.succ_lt_mono in IHl. + Qed. + (******************************************) (** ** Counting occurrences of an element *) @@ -743,6 +899,12 @@ Section ListOps. rewrite IHl; auto. Qed. + Lemma rev_eq_app : forall l l1 l2, rev l = l1 ++ l2 -> l = rev l2 ++ rev l1. + Proof. + intros l l1 l2 Heq. + rewrite <- (rev_involutive l), Heq. + apply rev_app_distr. + Qed. (** Compatibility with other operations *) @@ -820,30 +982,27 @@ Section ListOps. Section Reverse_Induction. - Lemma rev_list_ind : - forall P:list A-> Prop, - P [] -> - (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> - forall l:list A, P (rev l). + Lemma rev_list_ind : forall P:list A-> Prop, + P [] -> + (forall (a:A) (l:list A), P (rev l) -> P (rev (a :: l))) -> + forall l:list A, P (rev l). Proof. induction l; auto. Qed. - Theorem rev_ind : - forall P:list A -> Prop, - P [] -> - (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. + Theorem rev_ind : forall P:list A -> Prop, + P [] -> + (forall (x:A) (l:list A), P l -> P (l ++ [x])) -> forall l:list A, P l. Proof. intros. generalize (rev_involutive l). intros E; rewrite <- E. apply (rev_list_ind P). - auto. - - simpl. - intros. - apply (H0 a (rev l0)). - auto. + - auto. + - simpl. + intros. + apply (H0 a (rev l0)). + auto. Qed. End Reverse_Induction. @@ -871,10 +1030,28 @@ Section ListOps. Lemma concat_app : forall l1 l2, concat (l1 ++ l2) = concat l1 ++ concat l2. Proof. intros l1; induction l1 as [|x l1 IH]; intros l2; simpl. - + reflexivity. - + rewrite IH; apply app_assoc. + - reflexivity. + - rewrite IH; apply app_assoc. Qed. + Lemma in_concat : forall l y, + In y (concat l) <-> exists x, In x l /\ In y x. + Proof. + induction l; simpl; split; intros. + contradiction. + destruct H as (x,(H,_)); contradiction. + destruct (in_app_or _ _ _ H). + exists a; auto. + destruct (IHl y) as (H1,_); destruct (H1 H0) as (x,(H2,H3)). + exists x; auto. + apply in_or_app. + destruct H as (x,(H0,H1)); destruct H0. + subst; auto. + right; destruct (IHl y) as (_,H2); apply H2. + exists x; auto. + Qed. + + (***********************************) (** ** Decidable equality on lists *) (***********************************) @@ -944,6 +1121,13 @@ Section Map. intros; rewrite IHl; auto. Qed. + Lemma map_last : forall l a, + map (l ++ [a]) = (map l) ++ [f a]. + Proof. + induction l; intros; [ reflexivity | ]. + simpl; rewrite IHl; reflexivity. + Qed. + Lemma map_rev : forall l, map (rev l) = rev (map l). Proof. induction l; simpl; auto. @@ -956,6 +1140,26 @@ Section Map. destruct l; simpl; reflexivity || discriminate. Qed. + Lemma map_eq_cons : forall l l' b, + map l = b :: l' -> exists a tl, l = a :: tl /\ b = f a /\ l' = map tl. + Proof. + intros l l' b Heq. + destruct l; inversion_clear Heq. + exists a, l; repeat split. + Qed. + + Lemma map_eq_app : forall l l1 l2, + map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ l1 = map l1' /\ l2 = map l2'. + Proof. + induction l; simpl; intros l1 l2 Heq. + - symmetry in Heq; apply app_eq_nil in Heq; destruct Heq; subst. + exists nil, nil; repeat split. + - destruct l1; simpl in Heq; inversion Heq as [[Heq2 Htl]]. + + exists nil, (a :: l); repeat split. + + destruct (IHl _ _ Htl) as (l1' & l2' & ? & ? & ?); subst. + exists (a :: l1'), l2'; repeat split. + Qed. + (** [map] and count of occurrences *) Hypothesis decA: forall x1 x2 : A, {x1 = x2} + {x1 <> x2}. @@ -969,10 +1173,10 @@ Section Map. - reflexivity. - specialize (Hrec x). destruct (decA a x) as [H1|H1], (decB (f a) (f x)) as [H2|H2]. - * rewrite Hrec. reflexivity. - * contradiction H2. rewrite H1. reflexivity. - * specialize (Hfinjective H2). contradiction H1. - * assumption. + + rewrite Hrec. reflexivity. + + contradiction H2. rewrite H1. reflexivity. + + specialize (Hfinjective H2). contradiction H1. + + assumption. Qed. (** [flat_map] *) @@ -984,10 +1188,18 @@ Section Map. | cons x t => (f x)++(flat_map t) end. + Lemma flat_map_app : forall f l1 l2, + flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2. + Proof. + intros F l1 l2. + induction l1; [ reflexivity | simpl ]. + rewrite IHl1, app_assoc; reflexivity. + Qed. + Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B), In y (flat_map f l) <-> exists x, In x l /\ In y (f x). - Proof using A B. - clear Hfinjective. + Proof. + clear f Hfinjective. induction l; simpl; split; intros. contradiction. destruct H as (x,(H,_)); contradiction. @@ -1008,15 +1220,22 @@ Lemma flat_map_concat_map : forall A B (f : A -> list B) l, flat_map f l = concat (map f l). Proof. intros A B f l; induction l as [|x l IH]; simpl. -+ reflexivity. -+ rewrite IH; reflexivity. +- reflexivity. +- rewrite IH; reflexivity. Qed. Lemma concat_map : forall A B (f : A -> B) l, map f (concat l) = concat (map (map f) l). Proof. intros A B f l; induction l as [|x l IH]; simpl. -+ reflexivity. -+ rewrite map_app, IH; reflexivity. +- reflexivity. +- rewrite map_app, IH; reflexivity. +Qed. + +Lemma remove_concat A (eq_dec : forall x y : A, {x = y}+{x <> y}) : forall l x, + remove eq_dec x (concat l) = flat_map (remove eq_dec x) l. +Proof. + intros l x; induction l; [ reflexivity | simpl ]. + rewrite remove_app, IHl; reflexivity. Qed. Lemma map_id : forall (A :Type) (l : list A), @@ -1057,6 +1276,25 @@ Proof. intros; apply map_ext_in; auto. Qed. +Lemma flat_map_ext : forall (A B : Type)(f g : A -> list B), + (forall a, f a = g a) -> forall l, flat_map f l = flat_map g l. +Proof. + intros A B f g Hext l. + rewrite 2 flat_map_concat_map. + now rewrite map_ext with (g := g). +Qed. + +Lemma nth_nth_nth_map A : forall (l : list A) n d ln dn, n < length ln \/ length l <= dn -> + nth (nth n ln dn) l d = nth n (map (fun x => nth x l d) ln) d. +Proof. + intros l n d ln dn; revert n; induction ln; intros n Hlen. + - destruct Hlen as [Hlen|Hlen]. + + inversion Hlen. + + now rewrite nth_overflow; destruct n. + - destruct n; simpl; [ reflexivity | apply IHln ]. + destruct Hlen; [ left; apply lt_S_n | right ]; assumption. +Qed. + (************************************) (** Left-to-right iterator on lists *) @@ -1168,8 +1406,8 @@ End Fold_Right_Recursor. Fixpoint existsb (l:list A) : bool := match l with - | nil => false - | a::l => f a || existsb l + | nil => false + | a::l => f a || existsb l end. Lemma existsb_exists : @@ -1208,8 +1446,8 @@ End Fold_Right_Recursor. Fixpoint forallb (l:list A) : bool := match l with - | nil => true - | a::l => f a && forallb l + | nil => true + | a::l => f a && forallb l end. Lemma forallb_forall : @@ -1231,12 +1469,13 @@ End Fold_Right_Recursor. solve[auto]. case (f a); simpl; solve[auto]. Qed. + (** [filter] *) Fixpoint filter (l:list A) : list A := match l with - | nil => nil - | x :: l => if f x then x::(filter l) else filter l + | nil => nil + | x :: l => if f x then x::(filter l) else filter l end. Lemma filter_In : forall x l, In x (filter l) <-> In x l /\ f x = true. @@ -1265,8 +1504,8 @@ End Fold_Right_Recursor. Fixpoint find (l:list A) : option A := match l with - | nil => None - | x :: tl => if f x then Some x else find tl + | nil => None + | x :: tl => if f x then Some x else find tl end. Lemma find_some l x : find l = Some x -> In x l /\ f x = true. @@ -1288,9 +1527,9 @@ End Fold_Right_Recursor. Fixpoint partition (l:list A) : list A * list A := match l with - | nil => (nil, nil) - | x :: tl => let (g,d) := partition tl in - if f x then (x::g,d) else (g,x::d) + | nil => (nil, nil) + | x :: tl => let (g,d) := partition tl in + if f x then (x::g,d) else (g,x::d) end. Theorem partition_cons1 a l l1 l2: @@ -1405,8 +1644,8 @@ End Fold_Right_Recursor. Fixpoint split (l:list (A*B)) : list A * list B := match l with - | [] => ([], []) - | (x,y) :: tl => let (left,right) := split tl in (x::left, y::right) + | [] => ([], []) + | (x,y) :: tl => let (left,right) := split tl in (x::left, y::right) end. Lemma in_split_l : forall (l:list (A*B))(p:A*B), @@ -1460,8 +1699,8 @@ End Fold_Right_Recursor. Fixpoint combine (l : list A) (l' : list B) : list (A*B) := match l,l' with - | x::tl, y::tl' => (x,y)::(combine tl tl') - | _, _ => nil + | x::tl, y::tl' => (x,y)::(combine tl tl') + | _, _ => nil end. Lemma split_combine : forall (l: list (A*B)), @@ -1528,8 +1767,8 @@ End Fold_Right_Recursor. Fixpoint list_prod (l:list A) (l':list B) : list (A * B) := match l with - | nil => nil - | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l') + | nil => nil + | cons x t => (map (fun y:B => (x, y)) l')++(list_prod t l') end. Lemma in_prod_aux : @@ -1544,17 +1783,17 @@ End Fold_Right_Recursor. Lemma in_prod : forall (l:list A) (l':list B) (x:A) (y:B), - In x l -> In y l' -> In (x, y) (list_prod l l'). + In x l -> In y l' -> In (x, y) (list_prod l l'). Proof. induction l; - [ simpl; tauto - | simpl; intros; apply in_or_app; destruct H; - [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. + [ simpl; tauto + | simpl; intros; apply in_or_app; destruct H; + [ left; rewrite H; apply in_prod_aux; assumption | right; auto ] ]. Qed. Lemma in_prod_iff : forall (l:list A)(l':list B)(x:A)(y:B), - In (x,y) (list_prod l l') <-> In x l /\ In y l'. + In (x,y) (list_prod l l') <-> In x l /\ In y l'. Proof. split; [ | intros; apply in_prod; intuition ]. induction l; simpl; intros. @@ -1650,6 +1889,18 @@ Section SetIncl. Definition incl (l m:list A) := forall a:A, In a l -> In a m. Hint Unfold incl : core. + Lemma incl_nil_l : forall l, incl nil l. + Proof. + intros l a Hin; inversion Hin. + Qed. + + Lemma incl_l_nil : forall l, incl l nil -> l = nil. + Proof. + destruct l; intros Hincl. + - reflexivity. + - exfalso; apply Hincl with a; simpl; auto. + Qed. + Lemma incl_refl : forall l:list A, incl l l. Proof. auto. @@ -1694,6 +1945,13 @@ Section SetIncl. Qed. Hint Resolve incl_cons : core. + Lemma incl_cons_inv : forall (a:A) (l m:list A), + incl (a :: l) m -> In a m /\ incl l m. + Proof. + intros a l m Hi. + split; [ | intros ? ? ]; apply Hi; simpl; auto. + Qed. + Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. Proof. unfold incl; simpl; intros l m n H H0 a H1. @@ -1702,6 +1960,34 @@ Section SetIncl. Qed. Hint Resolve incl_app : core. + Lemma incl_app_app : forall l1 l2 m1 m2:list A, + incl l1 m1 -> incl l2 m2 -> incl (l1 ++ l2) (m1 ++ m2). + Proof. + intros. + apply incl_app; [ apply incl_appl | apply incl_appr]; assumption. + Qed. + + Lemma incl_app_inv : forall l1 l2 m : list A, + incl (l1 ++ l2) m -> incl l1 m /\ incl l2 m. + Proof. + induction l1; intros l2 m Hin; split; auto. + - apply incl_nil_l. + - intros b Hb; inversion_clear Hb; subst; apply Hin. + + now constructor. + + simpl; apply in_cons. + apply incl_appl with l1; [ apply incl_refl | assumption ]. + - apply IHl1. + now apply incl_cons_inv in Hin. + Qed. + + Lemma remove_incl (eq_dec : forall x y : A, {x = y} + {x <> y}) : forall l1 l2 x, + incl l1 l2 -> incl (remove eq_dec x l1) (remove eq_dec x l2). + Proof. + intros l1 l2 x Hincl y Hin. + apply in_remove in Hin; destruct Hin as [Hin Hneq]. + apply in_in_remove; intuition. + Qed. + End SetIncl. Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons @@ -1825,9 +2111,11 @@ Section Cutting. Lemma skipn_cons n a l: skipn (S n) (a::l) = skipn n l. Proof. reflexivity. Qed. - Lemma skipn_none : forall l, skipn (length l) l = []. + Lemma skipn_all : forall l, skipn (length l) l = nil. Proof. now induction l. Qed. +#[deprecated(since="8.12",note="Use skipn_all instead.")] Notation skipn_none := skipn_all. + Lemma skipn_all2 n: forall l, length l <= n -> skipn n l = []. Proof. intros l L%Nat.sub_0_le; rewrite <-(firstn_all l) at 1. @@ -1855,9 +2143,6 @@ Section Cutting. - destruct l; simpl; auto. Qed. - Lemma skipn_all l: skipn (length l) l = nil. - Proof. now induction l. Qed. - Lemma skipn_app n : forall l1 l2, skipn n (l1 ++ l2) = (skipn n l1) ++ (skipn (n - length l1) l2). Proof. induction n; auto; intros [|]; simpl; auto. Qed. @@ -1884,7 +2169,7 @@ Section Cutting. intros x l; rewrite firstn_skipn_rev, rev_involutive, <-rev_length. destruct (Nat.le_ge_cases (length (rev l)) x) as [L | L]. - rewrite skipn_all2; [apply Nat.sub_0_le in L | trivial]. - now rewrite L, Nat.sub_0_r, skipn_none. + now rewrite L, Nat.sub_0_r, skipn_all. - replace (length (rev l) - (length (rev l) - x)) with (length (rev l) + x - length (rev l)). rewrite minus_plus. reflexivity. @@ -1911,6 +2196,13 @@ Section Cutting. inversion_clear H0. Qed. + Lemma removelast_firstn_len : forall l, + removelast l = firstn (pred (length l)) l. + Proof. + induction l; [ reflexivity | simpl ]. + destruct l; [ | rewrite IHl ]; reflexivity. + Qed. + Lemma firstn_removelast : forall n l, n < length l -> firstn n (removelast l) = firstn n l. Proof. @@ -2082,6 +2374,16 @@ Section ReDun. + now constructor. Qed. + Lemma NoDup_rev l : NoDup l -> NoDup (rev l). + Proof. + induction l; simpl; intros Hnd; [ constructor | ]. + inversion_clear Hnd as [ | ? ? Hnin Hndl ]. + assert (Add a (rev l) (rev l ++ a :: nil)) as Hadd + by (rewrite <- (app_nil_r (rev l)) at 1; apply Add_app). + apply NoDup_Add in Hadd; apply Hadd; intuition. + now apply Hnin, in_rev. + Qed. + (** Effective computation of a list without duplicates *) Hypothesis decA: forall x y : A, {x = y} + {x <> y}. @@ -2110,6 +2412,11 @@ Section ReDun. * reflexivity. Qed. + Lemma nodup_incl l1 l2 : incl l1 (nodup l2) <-> incl l1 l2. + Proof. + split; intros Hincl a Ha; apply nodup_In; intuition. + Qed. + Lemma NoDup_nodup l: NoDup (nodup l). Proof. induction l as [|a l' Hrec]; simpl. @@ -2252,6 +2559,11 @@ Section NatSeq. | S len => start :: seq (S start) len end. + Lemma cons_seq : forall len start, start :: seq (S start) len = seq start (S len). + Proof. + reflexivity. + Qed. + Lemma seq_length : forall len start, length (seq start len) = len. Proof. induction len; simpl; auto. @@ -2284,8 +2596,8 @@ Section NatSeq. - rewrite <- plus_n_O. split;[easy|]. intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')). - rewrite IHlen, <- plus_n_Sm; simpl; split. - * intros [H|H]; subst; intuition auto with arith. - * intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. + + intros [H|H]; subst; intuition auto with arith. + + intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition. Qed. Lemma seq_NoDup len start : NoDup (seq start len). @@ -2302,6 +2614,14 @@ Section NatSeq. - now rewrite Nat.add_succ_r, IHlen. Qed. + Lemma seq_S : forall len start, seq start (S len) = seq start len ++ [start + len]. + Proof. + intros len start. + change [start + len] with (seq (start + len) 1). + rewrite <- seq_app. + rewrite <- plus_n_Sm, <- plus_n_O; reflexivity. + Qed. + End NatSeq. Section Exists_Forall. @@ -2328,6 +2648,21 @@ Section Exists_Forall. - induction l; firstorder; subst; auto. Qed. + Lemma Exists_nth l : + Exists l <-> exists i d, i < length l /\ P (nth i l d). + Proof. + split. + - intros HE; apply Exists_exists in HE. + destruct HE as [a [Hin HP]]. + apply In_nth with (d := a) in Hin; destruct Hin as [i [Hl Heq]]. + rewrite <- Heq in HP. + now exists i; exists a. + - intros [i [d [Hl HP]]]. + apply Exists_exists; exists (nth i l d); split. + apply nth_In; assumption. + assumption. + Qed. + Lemma Exists_nil : Exists nil <-> False. Proof. split; inversion 1. Qed. @@ -2335,6 +2670,21 @@ Section Exists_Forall. Exists (x::l) <-> P x \/ Exists l. Proof. split; inversion 1; auto. Qed. + Lemma Exists_app l1 l2 : + Exists (l1 ++ l2) <-> Exists l1 \/ Exists l2. + Proof. + induction l1; simpl; split; intros HE; try now intuition. + - inversion_clear HE; intuition. + - destruct HE as [HE|HE]; intuition. + inversion_clear HE; intuition. + Qed. + + Lemma Exists_rev l : Exists l -> Exists (rev l). + Proof. + induction l; intros HE; intuition. + inversion_clear HE; simpl; apply Exists_app; intuition. + Qed. + Lemma Exists_dec l: (forall x:A, {P x} + { ~ P x }) -> {Exists l} + {~ Exists l}. @@ -2342,12 +2692,25 @@ Section Exists_Forall. intro Pdec. induction l as [|a l' Hrec]. - right. abstract now rewrite Exists_nil. - destruct Hrec as [Hl'|Hl']. - * left. now apply Exists_cons_tl. - * destruct (Pdec a) as [Ha|Ha]. - + left. now apply Exists_cons_hd. - + right. abstract now inversion 1. + + left. now apply Exists_cons_tl. + + destruct (Pdec a) as [Ha|Ha]. + * left. now apply Exists_cons_hd. + * right. abstract now inversion 1. Defined. + Lemma Exists_fold_right l : + Exists l <-> fold_right (fun x => or (P x)) False l. + Proof. + induction l; simpl; split; intros HE; try now inversion HE; intuition. + Qed. + + Lemma incl_Exists l1 l2 : incl l1 l2 -> Exists l1 -> Exists l2. + Proof. + intros Hincl HE. + apply Exists_exists in HE; destruct HE as [a [Hin HP]]. + apply Exists_exists; exists a; intuition. + Qed. + Inductive Forall : list A -> Prop := | Forall_nil : Forall nil | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l). @@ -2362,11 +2725,49 @@ Section Exists_Forall. - induction l; firstorder. Qed. + Lemma Forall_nth l : + Forall l <-> forall i d, i < length l -> P (nth i l d). + Proof. + split. + - intros HF i d Hl. + apply Forall_forall with (x := nth i l d) in HF. + assumption. + apply nth_In; assumption. + - intros HF. + apply Forall_forall; intros a Hin. + apply In_nth with (d := a) in Hin; destruct Hin as [i [Hl Heq]]. + rewrite <- Heq; intuition. + Qed. + Lemma Forall_inv : forall (a:A) l, Forall (a :: l) -> P a. Proof. intros; inversion H; trivial. Qed. + Theorem Forall_inv_tail : forall (a:A) l, Forall (a :: l) -> Forall l. + Proof. + intros; inversion H; trivial. + Qed. + + Lemma Forall_app l1 l2 : + Forall (l1 ++ l2) <-> Forall l1 /\ Forall l2. + Proof. + induction l1; simpl; split; intros HF; try now intuition. + - inversion_clear HF; intuition. + - destruct HF as [HF1 HF2]; inversion HF1; intuition. + Qed. + + Lemma Forall_elt a l1 l2 : Forall (l1 ++ a :: l2) -> P a. + Proof. + intros HF; apply Forall_app in HF; destruct HF as [HF1 HF2]; now inversion HF2. + Qed. + + Lemma Forall_rev l : Forall l -> Forall (rev l). + Proof. + induction l; intros HF; intuition. + inversion_clear HF; simpl; apply Forall_app; intuition. + Qed. + Lemma Forall_rect : forall (Q : list A -> Type), Q [] -> (forall b l, P b -> Q (b :: l)) -> forall l, Forall l -> Q l. Proof. @@ -2386,53 +2787,89 @@ Section Exists_Forall. + right. abstract now inversion 1. Defined. + Lemma Forall_fold_right l : + Forall l <-> fold_right (fun x => and (P x)) True l. + Proof. + induction l; simpl; split; intros HF; try now inversion HF; intuition. + Qed. + + Lemma incl_Forall l1 l2 : incl l2 l1 -> Forall l1 -> Forall l2. + Proof. + intros Hincl HF. + apply Forall_forall; intros a Ha. + apply Forall_forall with (x:=a) in HF; intuition. + Qed. + End One_predicate. - Theorem Forall_inv_tail - : forall (P : A -> Prop) (x0 : A) (xs : list A), Forall P (x0 :: xs) -> Forall P xs. + Lemma map_ext_Forall B : forall (f g : A -> B) l, + Forall (fun x => f x = g x) l -> map f l = map g l. Proof. - intros P x0 xs H. - apply Forall_forall with (l := xs). - assert (H0 : forall x : A, In x (x0 :: xs) -> P x). - apply Forall_forall with (P := P) (l := x0 :: xs). - exact H. - assert (H1 : forall (x : A) (H2 : In x xs), P x). - intros x H2. - apply (H0 x). - right. - exact H2. - intros x H2. - apply (H1 x H2). + intros; apply map_ext_in, Forall_forall; assumption. Qed. - Theorem Exists_impl - : forall (P Q : A -> Prop), (forall x : A, P x -> Q x) -> forall xs : list A, Exists P xs -> Exists Q xs. + Theorem Exists_impl : forall (P Q : A -> Prop), (forall a : A, P a -> Q a) -> + forall l, Exists P l -> Exists Q l. Proof. - intros P Q H xs H0. + intros P Q H l H0. induction H0. apply (Exists_cons_hd Q x l (H x H0)). apply (Exists_cons_tl x IHExists). Qed. + Lemma Exists_or : forall (P Q : A -> Prop) l, + Exists P l \/ Exists Q l -> Exists (fun x => P x \/ Q x) l. + Proof. + induction l; intros [H | H]; inversion H; subst. + 1,3: apply Exists_cons_hd; auto. + all: apply Exists_cons_tl, IHl; auto. + Qed. + + Lemma Exists_or_inv : forall (P Q : A -> Prop) l, + Exists (fun x => P x \/ Q x) l -> Exists P l \/ Exists Q l. + Proof. + induction l; intro Hl; inversion Hl as [ ? ? H | ? ? H ]; subst. + - inversion H; now repeat constructor. + - destruct (IHl H); now repeat constructor. + Qed. + + Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> + forall l, Forall P l -> Forall Q l. + Proof. + intros P Q H l. rewrite !Forall_forall. firstorder. + Qed. + + Lemma Forall_and : forall (P Q : A -> Prop) l, + Forall P l -> Forall Q l -> Forall (fun x => P x /\ Q x) l. + Proof. + induction l; intros HP HQ; constructor; inversion HP; inversion HQ; auto. + Qed. + + Lemma Forall_and_inv : forall (P Q : A -> Prop) l, + Forall (fun x => P x /\ Q x) l -> Forall P l /\ Forall Q l. + Proof. + induction l; intro Hl; split; constructor; inversion Hl; firstorder. + Qed. + Lemma Forall_Exists_neg (P:A->Prop)(l:list A) : - Forall (fun x => ~ P x) l <-> ~(Exists P l). + Forall (fun x => ~ P x) l <-> ~(Exists P l). Proof. - rewrite Forall_forall, Exists_exists. firstorder. + rewrite Forall_forall, Exists_exists. firstorder. Qed. Lemma Exists_Forall_neg (P:A->Prop)(l:list A) : (forall x, P x \/ ~P x) -> Exists (fun x => ~ P x) l <-> ~(Forall P l). Proof. - intro Dec. - split. - - rewrite Forall_forall, Exists_exists; firstorder. - - intros NF. - induction l as [|a l IH]. - + destruct NF. constructor. - + destruct (Dec a) as [Ha|Ha]. - * apply Exists_cons_tl, IH. contradict NF. now constructor. - * now apply Exists_cons_hd. + intro Dec. + split. + - rewrite Forall_forall, Exists_exists; firstorder. + - intros NF. + induction l as [|a l IH]. + + destruct NF. constructor. + + destruct (Dec a) as [Ha|Ha]. + * apply Exists_cons_tl, IH. contradict NF. now constructor. + * now apply Exists_cons_hd. Qed. Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) : @@ -2455,17 +2892,61 @@ Section Exists_Forall. now apply neg_Forall_Exists_neg. Defined. - Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) -> - forall l, Forall P l -> Forall Q l. - Proof. - intros P Q H l. rewrite !Forall_forall. firstorder. - Qed. - End Exists_Forall. Hint Constructors Exists : core. Hint Constructors Forall : core. +Lemma exists_Forall A B : forall (P : A -> B -> Prop) l, + (exists k, Forall (P k) l) -> Forall (fun x => exists k, P k x) l. +Proof. + induction l; intros [k HF]; constructor; inversion_clear HF. + - now exists k. + - now apply IHl; exists k. +Qed. + +Lemma Forall_image A B : forall (f : A -> B) l, + Forall (fun y => exists x, y = f x) l <-> exists l', l = map f l'. +Proof. + induction l; split; intros HF. + - exists nil; reflexivity. + - constructor. + - inversion_clear HF as [| ? ? [x Hx] HFtl]; subst. + destruct (proj1 IHl HFtl) as [l' Heq]; subst. + now exists (x :: l'). + - destruct HF as [l' Heq]. + symmetry in Heq; apply map_eq_cons in Heq. + destruct Heq as (x & tl & ? & ? & ?); subst. + constructor. + + now exists x. + + now apply IHl; exists tl. +Qed. + +Lemma concat_nil_Forall A : forall (l : list (list A)), + concat l = nil <-> Forall (fun x => x = nil) l. +Proof. + induction l; simpl; split; intros Hc; auto. + - apply app_eq_nil in Hc. + constructor; firstorder. + - inversion Hc; subst; simpl. + now apply IHl. +Qed. + +Lemma in_flat_map_Exists A B : forall (f : A -> list B) x l, + In x (flat_map f l) <-> Exists (fun y => In x (f y)) l. +Proof. + intros f x l; rewrite in_flat_map. + split; apply Exists_exists. +Qed. + +Lemma notin_flat_map_Forall A B : forall (f : A -> list B) x l, + ~ In x (flat_map f l) <-> Forall (fun y => ~ In x (f y)) l. +Proof. + intros f x l; rewrite Forall_Exists_neg. + apply not_iff_compat, in_flat_map_Exists. +Qed. + + Section Forall2. (** [Forall2]: stating that elements of two lists are pairwise related. *) @@ -2567,6 +3048,96 @@ Section ForallPairs. Qed. End ForallPairs. +Section Repeat. + + Variable A : Type. + Fixpoint repeat (x : A) (n: nat ) := + match n with + | O => [] + | S k => x::(repeat x k) + end. + + Theorem repeat_length x n: + length (repeat x n) = n. + Proof. + induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. + Qed. + + Theorem repeat_spec n x y: + In y (repeat x n) -> y=x. + Proof. + induction n as [|k Hrec]; simpl; destruct 1; auto. + Qed. + + Lemma repeat_cons n a : + a :: repeat a n = repeat a n ++ (a :: nil). + Proof. + induction n; simpl. + - reflexivity. + - f_equal; apply IHn. + Qed. + +End Repeat. + +Lemma repeat_to_concat A n (a:A) : + repeat a n = concat (repeat [a] n). +Proof. + induction n; simpl. + - reflexivity. + - f_equal; apply IHn. +Qed. + + +(** Sum of elements of a list of [nat]: [list_sum] *) + +Definition list_sum l := fold_right plus 0 l. + +Lemma list_sum_app : forall l1 l2, + list_sum (l1 ++ l2) = list_sum l1 + list_sum l2. +Proof. +induction l1; intros l2; [ reflexivity | ]. +simpl; rewrite IHl1. +apply Nat.add_assoc. +Qed. + +(** Max of elements of a list of [nat]: [list_max] *) + +Definition list_max l := fold_right max 0 l. + +Lemma list_max_app : forall l1 l2, + list_max (l1 ++ l2) = max (list_max l1) (list_max l2). +Proof. +induction l1; intros l2; [ reflexivity | ]. +now simpl; rewrite IHl1, Nat.max_assoc. +Qed. + +Lemma list_max_le : forall l n, + list_max l <= n <-> Forall (fun k => k <= n) l. +Proof. +induction l; simpl; intros n; split; intros H; intuition. +- apply Nat.max_lub_iff in H. + now constructor; [ | apply IHl ]. +- inversion_clear H as [ | ? ? Hle HF ]. + apply IHl in HF; apply Nat.max_lub; assumption. +Qed. + +Lemma list_max_lt : forall l n, l <> nil -> + list_max l < n <-> Forall (fun k => k < n) l. +Proof. +induction l; simpl; intros n Hnil; split; intros H; intuition. +- destruct l. + + repeat constructor. + now simpl in H; rewrite Nat.max_0_r in H. + + apply Nat.max_lub_lt_iff in H. + now constructor; [ | apply IHl ]. +- destruct l; inversion_clear H as [ | ? ? Hlt HF ]. + + now simpl; rewrite Nat.max_0_r. + + apply IHl in HF. + * now apply Nat.max_lub_lt_iff. + * intros Heq; inversion Heq. +Qed. + + (** * Inversion of predicates over lists based on head symbol *) Ltac is_list_constr c := @@ -2633,27 +3204,5 @@ Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) Hint Resolve app_nil_end : datatypes. (* end hide *) -Section Repeat. - - Variable A : Type. - Fixpoint repeat (x : A) (n: nat ) := - match n with - | O => [] - | S k => x::(repeat x k) - end. - - Theorem repeat_length x n: - length (repeat x n) = n. - Proof. - induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity. - Qed. - - Theorem repeat_spec n x y: - In y (repeat x n) -> y=x. - Proof. - induction n as [|k Hrec]; simpl; destruct 1; auto. - Qed. - -End Repeat. (* Unset Universe Polymorphism. *) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a44ddf7467..13913cabc3 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -547,6 +547,9 @@ rule coq_bol = parse comment lexbuf end else skipped_comment lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | space* "#[" { + let eol = begin backtrack lexbuf; body_bol lexbuf end + in if eol then coq_bol lexbuf else coq lexbuf } | eof { () } | _ @@ -643,6 +646,11 @@ and coq = parse Output.ident s None; let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } + | "#[" + { ignore(lexeme lexbuf); + Output.char '#'; Output.char '['; + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space+ { Output.char ' '; coq lexbuf } | eof { () } |