diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 57 | ||||
| -rw-r--r-- | mathcomp/test_suite/test_intro_rw.v | 23 |
3 files changed, 81 insertions, 1 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 185d5c1..7da7ebc 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. |