diff options
| -rw-r--r-- | mathcomp/ssreflect/path.v | 29 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 36 | ||||
| -rw-r--r-- | mathcomp/test_suite/test_intro_rw.v | 24 |
3 files changed, 52 insertions, 37 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index fa66807..676471d 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1446,13 +1446,21 @@ Notation "@ 'eq_sorted'" := (deprecate eq_sorted sorted_eq) (at level 10, only parsing) : fun_scope. Notation "@ 'eq_sorted_irr'" := (deprecate eq_sorted_irr irr_sorted_eq) (at level 10, only parsing) : fun_scope. -Notation "@ 'sorted_lt_nth'" := (deprecate sorted_lt_nth sorted_ltn_nth) +Notation "@ 'sorted_lt_nth'" := + (fun (T : Type) (leT : rel T) (leT_tr : transitive leT) => + deprecate sorted_lt_nth sorted_ltn_nth leT_tr) (at level 10, only parsing) : fun_scope. -Notation "@ 'sorted_le_nth'" := (deprecate sorted_le_nth sorted_leq_nth) +Notation "@ 'sorted_le_nth'" := + (fun (T : Type) (leT : rel T) (leT_tr : transitive leT) => + deprecate sorted_le_nth sorted_leq_nth leT_tr) (at level 10, only parsing) : fun_scope. -Notation "@ 'ltn_index'" := (deprecate ltn_index sorted_ltn_index) +Notation "@ 'ltn_index'" := + (fun (T : eqType) (leT : rel T) (leT_tr : transitive leT) => + deprecate ltn_index sorted_ltn_index leT_tr) (at level 10, only parsing) : fun_scope. -Notation "@ 'leq_index'" := (deprecate leq_index sorted_leq_index) +Notation "@ 'leq_index'" := + (fun (T : eqType) (leT : rel T) (leT_tr : transitive leT) => + deprecate leq_index sorted_leq_index leT_tr) (at level 10, only parsing) : fun_scope. Notation "@ 'subseq_order_path'" := (deprecate subseq_order_path subseq_path) (at level 10, only parsing) : fun_scope. @@ -1462,15 +1470,12 @@ Notation eq_sorted := Notation eq_sorted_irr := (fun le_tr le_irr => @eq_sorted_irr _ _ le_tr le_irr _ _) (only parsing). Notation sorted_lt_nth := - (fun leT_tr x0 s_sorted => @sorted_lt_nth _ _ leT_tr x0 _ s_sorted _ _) - (only parsing). + (fun leT_tr x0 => @sorted_lt_nth _ _ leT_tr x0 _) (only parsing). Notation sorted_le_nth := - (fun leT_tr leT_refl x0 s_sorted => - @sorted_le_nth _ _ leT_tr leT_refl x0 _ s_sorted _ _) (only parsing). -Notation ltn_index := - (fun leT_tr s_sorted => @ltn_index _ _ leT_tr _ s_sorted _ _) (only parsing). + (fun leT_tr leT_refl x0 => @sorted_le_nth _ _ leT_tr leT_refl x0 _) + (only parsing). +Notation ltn_index := (fun leT_tr => @ltn_index _ _ leT_tr _) (only parsing). Notation leq_index := - (fun leT_tr leT_refl s_sorted => - @leq_index _ _ leT_tr leT_refl _ s_sorted _ _) (only parsing). + (fun leT_tr leT_refl => @leq_index _ _ leT_tr leT_refl _) (only parsing). Notation subseq_order_path := (fun leT_tr => @subseq_order_path _ _ leT_tr _ _ _) (only parsing). diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v index 888f98d..e1e1b71 100644 --- a/mathcomp/ssreflect/ssreflect.v +++ b/mathcomp/ssreflect/ssreflect.v @@ -111,26 +111,12 @@ Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f)) (* 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)) + let x := lazymatch goal with + | |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_" + end in intro x; move; + let y := lazymatch goal with + | |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_" + end in intro y; revert x; revert y)) (at level 0, only parsing) : ssripat_scope. (* we try to preserve the naming by matching the names from the goal *) @@ -138,15 +124,15 @@ Notation "'[' 'swap' ']'" := (ltac:(move; 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 := fresh x in intro x; + let copy := fresh x in have copy := x; revert x; revert copy | |- let x := _ in _ => - let x := fresh x in move=> x; + let x := fresh x in intro x; let copy := fresh x in pose copy := x; - do [unfold x in (value of copy)]; move: @copy @x + do [unfold x in (value of copy)]; revert x; revert copy | |- _ => let x := fresh "_top_" in move=> x; - let copy := fresh "_top" in have copy := x; move: copy x + let copy := fresh "_top" in have copy := x; revert x; revert copy end)) (at level 0, only parsing) : ssripat_scope. diff --git a/mathcomp/test_suite/test_intro_rw.v b/mathcomp/test_suite/test_intro_rw.v index dd1486f..827b810 100644 --- a/mathcomp/test_suite/test_intro_rw.v +++ b/mathcomp/test_suite/test_intro_rw.v @@ -21,3 +21,27 @@ Proof. move=> /[apply] b. Check (b : B). Abort. + +Lemma test_swap_plus P Q : P -> Q -> False. +Proof. +move=> + /[dup] q. +suff: P -> Q -> False by []. +Abort. + +Lemma test_dup_plus2 P : P -> let x := 0 in False. +Proof. +move=> + /[dup] y. +suff: P -> let x := 0 in False by []. +Abort. + +Lemma test_swap_plus P Q R : P -> Q -> R -> False. +Proof. +move=> + /[swap]. +suff: P -> R -> Q -> False by []. +Abort. + +Lemma test_swap_plus2 P : P -> let x := 0 in let y := 1 in False. +Proof. +move=> + /[swap]. +suff: P -> let y := 1 in let x := 0 in False by []. +Abort. |