diff options
| -rw-r--r-- | .gitlab-ci.yml | 12 | ||||
| -rw-r--r-- | Makefile.ci | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-gappa.sh | 12 | ||||
| -rw-r--r-- | dev/ci/docker/bionic_coq/Dockerfile | 2 | ||||
| -rw-r--r-- | doc/changelog/06-ssreflect/13490-backport-ssrbool.rst | 5 | ||||
| -rw-r--r-- | theories/ssr/ssrbool.v | 114 |
6 files changed, 146 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index bd015a40b6..af54edfa21 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -19,7 +19,7 @@ stages: variables: # Format: $IMAGE-V$DATE-$hash # The $hash is the first 10 characters of the md5 of the dockerfile - CACHEKEY: "bionic_coq-V2020-11-26-db194d584e" + CACHEKEY: "bionic_coq-V2020-11-26-50e9456f22" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -847,6 +847,16 @@ library:ci-corn: - build:edge+flambda - library:ci-math_classes +plugin:ci-gappa: + extends: .ci-template-flambda + stage: stage-3 + needs: + - build:edge+flambda + - library:ci-flocq + dependencies: + - build:edge+flambda + - library:ci-flocq + library:ci-geocoq: extends: .ci-template-flambda diff --git a/Makefile.ci b/Makefile.ci index 9f08de662f..d549ed1b39 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -35,6 +35,7 @@ CI_TARGETS= \ ci-fiat_parsers \ ci-flocq \ ci-fourcolor \ + ci-gappa \ ci-geocoq \ ci-coqhammer \ ci-hott \ @@ -94,6 +95,7 @@ ci-metacoq: ci-equations ci-vst: ci-flocq ci-compcert: ci-menhir ci-flocq +ci-gappa: ci-flocq # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: diff --git a/dev/ci/ci-gappa.sh b/dev/ci/ci-gappa.sh new file mode 100755 index 0000000000..c346354b70 --- /dev/null +++ b/dev/ci/ci-gappa.sh @@ -0,0 +1,12 @@ + #!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download gappa_tool + +( cd "${CI_BUILD_DIR}/gappa_tool" && ( if [ ! -x ./configure ]; then autoreconf && touch stamp-config_h.in && ./configure --prefix=${CI_INSTALL_DIR}; fi ) && ./remake "-j${NJOBS}" && ./remake install ) + +git_download gappa_plugin + +( cd "${CI_BUILD_DIR}/gappa_plugin" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 96d96328f8..1aefebb007 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -15,6 +15,8 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ perl libgmp-dev libgmp-dev:i386 \ # Dependencies of lablgtk (for CoqIDE) libgtksourceview-3.0-dev \ + # Dependencies of Gappa + libboost1.65-all-dev libmpfr-dev autoconf-archive bison flex \ # Dependencies of stdlib and sphinx doc texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \ diff --git a/doc/changelog/06-ssreflect/13490-backport-ssrbool.rst b/doc/changelog/06-ssreflect/13490-backport-ssrbool.rst new file mode 100644 index 0000000000..096c9d574b --- /dev/null +++ b/doc/changelog/06-ssreflect/13490-backport-ssrbool.rst @@ -0,0 +1,5 @@ +- **Added:** + Lemmas about interaction between :n:`{in _, _}`, :n:`{on _, _}`, and :n:`sig` + have been backported from Mathematical Components 1.12.0 + (`#13490 <https://github.com/coq/coq/pull/13490>`_, + by Kazuhiko Sakaguchi). diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index a563dcbf95..d8eb005ab2 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -1944,7 +1944,121 @@ Proof. by move=> subD [g' fK g'K]; exists g' => x; move/subD; [apply: fK | apply: g'K]. Qed. +Lemma in_on1P : {in D1, {on D2, allQ1 f}} <-> + {in [pred x in D1 | f x \in D2], allQ1 f}. +Proof. +split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP. +by move=> ? ?; apply: Q1f; apply/andP. +Qed. + +Lemma in_on1lP : {in D1, {on D2, allQ1l f & h}} <-> + {in [pred x in D1 | f x \in D2], allQ1l f h}. +Proof. +split => allf x; have := allf x; rewrite inE => Q1f; first by case/andP. +by move=> ? ?; apply: Q1f; apply/andP. +Qed. + +Lemma in_on2P : {in D1 &, {on D2 &, allQ2 f}} <-> + {in [pred x in D1 | f x \in D2] &, allQ2 f}. +Proof. +split => allf x y; have := allf x y; rewrite !inE => Q2f. + by move=> /andP[? ?] /andP[? ?]; apply: Q2f. +by move=> ? ? ? ?; apply: Q2f; apply/andP. +Qed. + +Lemma on1W_in : {in D1, allQ1 f} -> {in D1, {on D2, allQ1 f}}. +Proof. by move=> D1f ? /D1f. Qed. + +Lemma on1lW_in : {in D1, allQ1l f h} -> {in D1, {on D2, allQ1l f & h}}. +Proof. by move=> D1f ? /D1f. Qed. + +Lemma on2W_in : {in D1 &, allQ2 f} -> {in D1 &, {on D2 &, allQ2 f}}. +Proof. by move=> D1f ? ? ? ? ? ?; apply: D1f. Qed. + +Lemma in_on1W : allQ1 f -> {in D1, {on D2, allQ1 f}}. +Proof. by move=> allf ? ? ?; apply: allf. Qed. + +Lemma in_on1lW : allQ1l f h -> {in D1, {on D2, allQ1l f & h}}. +Proof. by move=> allf ? ? ?; apply: allf. Qed. + +Lemma in_on2W : allQ2 f -> {in D1 &, {on D2 &, allQ2 f}}. +Proof. by move=> allf ? ? ? ? ? ?; apply: allf. Qed. + +Lemma on1S : (forall x, f x \in D2) -> {on D2, allQ1 f} -> allQ1 f. +Proof. by move=> ? fD1 ?; apply: fD1. Qed. + +Lemma on1lS : (forall x, f x \in D2) -> {on D2, allQ1l f & h} -> allQ1l f h. +Proof. by move=> ? fD1 ?; apply: fD1. Qed. + +Lemma on2S : (forall x, f x \in D2) -> {on D2 &, allQ2 f} -> allQ2 f. +Proof. by move=> ? fD1 ? ?; apply: fD1. Qed. + +Lemma on1S_in : {homo f : x / x \in D1 >-> x \in D2} -> + {in D1, {on D2, allQ1 f}} -> {in D1, allQ1 f}. +Proof. by move=> fD fD1 ? ?; apply/fD1/fD. Qed. + +Lemma on1lS_in : {homo f : x / x \in D1 >-> x \in D2} -> + {in D1, {on D2, allQ1l f & h}} -> {in D1, allQ1l f h}. +Proof. by move=> fD fD1 ? ?; apply/fD1/fD. Qed. + +Lemma on2S_in : {homo f : x / x \in D1 >-> x \in D2} -> + {in D1 &, {on D2 &, allQ2 f}} -> {in D1 &, allQ2 f}. +Proof. by move=> fD fD1 ? ? ? ?; apply: fD1 => //; apply: fD. Qed. + +Lemma in_on1S : (forall x, f x \in D2) -> {in T1, {on D2, allQ1 f}} -> allQ1 f. +Proof. by move=> fD2 fD1 ?; apply: fD1. Qed. + +Lemma in_on1lS : (forall x, f x \in D2) -> + {in T1, {on D2, allQ1l f & h}} -> allQ1l f h. +Proof. by move=> fD2 fD1 ?; apply: fD1. Qed. + +Lemma in_on2S : (forall x, f x \in D2) -> + {in T1 &, {on D2 &, allQ2 f}} -> allQ2 f. +Proof. by move=> fD2 fD1 ? ?; apply: fD1. Qed. + End LocalGlobal. +Arguments in_on1P {T1 T2 D1 D2 f Q1}. +Arguments in_on1lP {T1 T2 T3 D1 D2 f h Q1l}. +Arguments in_on2P {T1 T2 D1 D2 f Q2}. +Arguments on1W_in {T1 T2 D1} D2 {f Q1}. +Arguments on1lW_in {T1 T2 T3 D1} D2 {f h Q1l}. +Arguments on2W_in {T1 T2 D1} D2 {f Q2}. +Arguments in_on1W {T1 T2} D1 D2 {f Q1}. +Arguments in_on1lW {T1 T2 T3} D1 D2 {f h Q1l}. +Arguments in_on2W {T1 T2} D1 D2 {f Q2}. +Arguments on1S {T1 T2} D2 {f Q1}. +Arguments on1lS {T1 T2 T3} D2 {f h Q1l}. +Arguments on2S {T1 T2} D2 {f Q2}. +Arguments on1S_in {T1 T2 D1} D2 {f Q1}. +Arguments on1lS_in {T1 T2 T3 D1} D2 {f h Q1l}. +Arguments on2S_in {T1 T2 D1} D2 {f Q2}. +Arguments in_on1S {T1 T2} D2 {f Q1}. +Arguments in_on1lS {T1 T2 T3} D2 {f h Q1l}. +Arguments in_on2S {T1 T2} D2 {f Q2}. + +Section in_sig. + +Variables T1 T2 T3 : Type. +Variables (D1 : {pred T1}) (D2 : {pred T2}) (D3 : {pred T3}). +Variable P1 : T1 -> Prop. +Variable P2 : T1 -> T2 -> Prop. +Variable P3 : T1 -> T2 -> T3 -> Prop. + +Lemma in1_sig : {in D1, {all1 P1}} -> forall x : sig D1, P1 (sval x). +Proof. by move=> DP [x Dx]; have := DP _ Dx. Qed. + +Lemma in2_sig : {in D1 & D2, {all2 P2}} -> + forall (x : sig D1) (y : sig D2), P2 (sval x) (sval y). +Proof. by move=> DP [x Dx] [y Dy]; have := DP _ _ Dx Dy. Qed. + +Lemma in3_sig : {in D1 & D2 & D3, {all3 P3}} -> + forall (x : sig D1) (y : sig D2) (z : sig D3), P3 (sval x) (sval y) (sval z). +Proof. by move=> DP [x Dx] [y Dy] [z Dz]; have := DP _ _ _ Dx Dy Dz. Qed. + +End in_sig. +Arguments in1_sig {T1 D1 P1}. +Arguments in2_sig {T1 T2 D1 D2 P2}. +Arguments in3_sig {T1 T2 T3 D1 D2 D3 P3}. Lemma sub_in2 T d d' (P : T -> T -> Prop) : sub_mem d d' -> forall Ph : ph {all2 P}, prop_in2 d' Ph -> prop_in2 d Ph. |