aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml46
-rw-r--r--CHANGELOG_UNRELEASED.md3
-rw-r--r--mathcomp/algebra/ssrnum.v2
-rw-r--r--mathcomp/ssreflect/ssreflect.v57
-rw-r--r--mathcomp/test_suite/test_intro_rw.v23
5 files changed, 84 insertions, 47 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7b7ae64..607ff61 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -89,9 +89,6 @@ make-coq-latest:
variables:
- $CRON_MODE == "nightly"
-coq-8.9:
- extends: .opam-build-once
-
coq-8.10:
extends: .opam-build-once
@@ -173,11 +170,6 @@ test-coq-8.10:
variables:
COQ_VERSION: "8.10"
-test-coq-8.9:
- extends: .test-once
- variables:
- COQ_VERSION: "8.9"
-
# set CONTRIB_URL, script, COQ_VERSION, CONTRIB_VERSION when using
.ci:
stage: test
@@ -222,11 +214,6 @@ test-coq-8.9:
- make -j "${NJOBS}"
- make install
-ci-fourcolor-8.9:
- extends: .ci-fourcolor
- variables:
- COQ_VERSION: "8.9"
-
ci-fourcolor-8.10:
extends: .ci-fourcolor
variables:
@@ -257,11 +244,6 @@ ci-fourcolor-dev:
- make -j "${NJOBS}"
- make install
-ci-odd-order-8.9:
- extends: .ci-odd-order
- variables:
- COQ_VERSION: "8.9"
-
ci-odd-order-8.10:
extends: .ci-odd-order
variables:
@@ -322,11 +304,6 @@ ci-lemma-overloading-dev:
- opam pin add -n -k path coq-mathcomp-bigenough .
- opam install -y -v -j "${NJOBS}" coq-mathcomp-bigenough
-ci-bigenough-8.9:
- extends: .ci-bigenough
- variables:
- COQ_VERSION: "8.9"
-
ci-bigenough-8.10:
extends: .ci-bigenough
variables:
@@ -358,11 +335,6 @@ ci-bigenough-dev:
# - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed
# - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed
#
-# ci-real-closed-8.9:
-# extends: .ci-real-closed
-# variables:
-# COQ_VERSION: "8.9"
-#
# ci-real-closed-dev:
# extends: .ci-real-closed
# variables:
@@ -379,16 +351,6 @@ ci-bigenough-dev:
# - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-analysis
# - opam install -y -v -j "${NJOBS}" coq-mathcomp-analysis
#
-# ci-analysis-8.8:
-# extends: .ci-analysis
-# variables:
-# COQ_VERSION: "8.8"
-#
-# ci-analysis-8.9:
-# extends: .ci-analysis
-# variables:
-# COQ_VERSION: "8.9"
-#
# ci-analysis-dev:
# extends: .ci-analysis
# variables:
@@ -405,11 +367,6 @@ ci-bigenough-dev:
- opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-finmap
- opam install -y -v -j "${NJOBS}" coq-mathcomp-finmap
-ci-finmap-8.9:
- extends: .ci-finmap
- variables:
- COQ_VERSION: "8.9"
-
ci-finmap-8.10:
extends: .ci-finmap
variables:
@@ -502,9 +459,6 @@ ci-fcsl-pcm-dev:
variables:
- $CRON_MODE == "nightly"
-mathcomp-dev_coq-8.9:
- extends: .docker-deploy-once
-
mathcomp-dev_coq-8.10:
extends: .docker-deploy-once
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 46ba30d..ffc1cab 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -58,6 +58,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
- Added a factory `distrLatticePOrderMixin` in order.v to build a
`distrLatticeType` from a `porderType`.
+- Added intro pattern ltac views for dup, swap, apply:
+ `/[apply]`, `/[swap]` and `/[dup]`.
+
- in `bigop.v` new lemma `sig_big_dep`, analogous to `pair_big_dep`
but with an additional dependency in the index types `I` and `J`.
- in `fintype.v` adds lemma `split_ordP`, a variant of `splitP` which
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index a2a2395..fc24a4b 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1678,7 +1678,7 @@ Hint Resolve real1 : core.
Lemma realn n : n%:R \is @real R. Proof. by rewrite ger0_real. Qed.
Lemma ler_leVge x y : x <= 0 -> y <= 0 -> (x <= y) || (y <= x).
-Proof. by rewrite -!oppr_ge0 => /(ger_leVge _) h /h; rewrite !ler_opp2. Qed.
+Proof. by rewrite -!oppr_ge0 => /(ger_leVge _) /[apply]; rewrite !ler_opp2. Qed.
Lemma real_leVge x y : x \is real -> y \is real -> (x <= y) || (y <= x).
Proof. by rewrite -comparabler0 -comparable0r => /comparabler_trans P/P. Qed.
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index 2925496..888f98d 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -28,6 +28,14 @@ Global Set Bullet Behavior "None".
(* triggered by such evars under binders. *)
(* Import Deprecation.Silent :: turn off deprecation warning messages. *)
(* Import Deprecation.Reject :: raise an error instead of only warning. *)
+(* *)
+(* Intro pattern ltac views: *)
+(* - top of the stack actions: *)
+(* => /[apply] := => hyp {}/hyp *)
+(* => /[swap] := => x y; move: y x *)
+(* (also swap and perserves let bindings) *)
+(* => /[dup] := => x; have copy := x; move: copy x *)
+(* (also copies and preserves let bindings) *)
(******************************************************************************)
Module NonPropType.
@@ -94,3 +102,52 @@ End Exports.
End Deprecation.
Export Deprecation.Exports.
+
+Module Export ipat.
+
+Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f))
+ (at level 0, only parsing) : ssripat_scope.
+
+(* we try to preserve the naming by matching the names from the goal *)
+(* we do move to perform a hnf before trying to match *)
+Notation "'[' 'swap' ']'" := (ltac:(move;
+ lazymatch goal with
+ | |- forall (x : _), _ => let x := fresh x in move=> x; move;
+ lazymatch goal with
+ | |- forall (y : _), _ => let y := fresh y in move=> y; move: y x
+ | |- let y := _ in _ => let y := fresh y in move=> y; move: @y x
+ | _ => let y := fresh "_top_" in move=> y; move: y x
+ end
+ | |- let x := _ in _ => let x := fresh x in move => x; move;
+ lazymatch goal with
+ | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x
+ | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x
+ | _ => let y := fresh "_top_" in move=> y; move: y x
+ end
+ | _ => let x := fresh "_top_" in let x := fresh x in move=> x; move;
+ lazymatch goal with
+ | |- forall (y : _), _ => let y := fresh y in move=> y; move: y @x
+ | |- let y := _ in _ => let y := fresh y in move=> y; move: @y @x
+ | _ => let y := fresh "_top_" in move=> y; move: y x
+ end
+ end))
+ (at level 0, only parsing) : ssripat_scope.
+
+(* we try to preserve the naming by matching the names from the goal *)
+(* we do move to perform a hnf before trying to match *)
+Notation "'[' 'dup' ']'" := (ltac:(move;
+ lazymatch goal with
+ | |- forall (x : _), _ =>
+ let x := fresh x in move=> x;
+ let copy := fresh x in have copy := x; move: copy x
+ | |- let x := _ in _ =>
+ let x := fresh x in move=> x;
+ let copy := fresh x in pose copy := x;
+ do [unfold x in (value of copy)]; move: @copy @x
+ | |- _ =>
+ let x := fresh "_top_" in move=> x;
+ let copy := fresh "_top" in have copy := x; move: copy x
+ end))
+ (at level 0, only parsing) : ssripat_scope.
+
+End ipat.
diff --git a/mathcomp/test_suite/test_intro_rw.v b/mathcomp/test_suite/test_intro_rw.v
new file mode 100644
index 0000000..dd1486f
--- /dev/null
+++ b/mathcomp/test_suite/test_intro_rw.v
@@ -0,0 +1,23 @@
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Lemma test_dup1 : forall n : nat, odd n.
+Proof. move=> /[dup] m n; suff: odd n by []. Abort.
+
+Lemma test_dup2 : let n := 1 in False.
+Proof. move=> /[dup] m n; have : m = n := erefl. Abort.
+
+Lemma test_swap1 : forall (n : nat) (b : bool), odd n = b.
+Proof. move=> /[swap] b n; suff: odd n = b by []. Abort.
+
+Lemma test_swap1 : let n := 1 in let b := true in False.
+Proof. move=> /[swap] b n; have : odd n = b := erefl. Abort.
+
+Lemma test_apply A B : forall (f : A -> B) (a : A), False.
+Proof.
+move=> /[apply] b.
+Check (b : B).
+Abort.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:37:08 +0000