From eac1d28204c93f082771dedb90fc5a1edec6e6f8 Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Tue, 28 May 2019 22:57:38 +0300 Subject: Add eqsP view to destruct not only x == y, but also y == x --- mathcomp/ssreflect/eqtype.v | 9 +++++++++ mathcomp/ssreflect/seq.v | 6 +++--- 2 files changed, 12 insertions(+), 3 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 3fbc110..895a86e 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -196,6 +196,15 @@ Proof. exact/eqP/eqP. Qed. Hint Resolve eq_refl eq_sym : core. +Variant eq_xor_neq_sym (T : eqType) (x y : T) : bool -> bool -> Set := + | EqNotNeqSym of x = y : eq_xor_neq_sym x y true true + | NeqNotEqSym of x <> y : eq_xor_neq_sym x y false false. + +Lemma eqsP (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y). +Proof. by rewrite eq_sym; case: eqP; constructor. Qed. + +Arguments eqsP {T x y}. + Section Contrapositives. Variables (T1 T2 : eqType). diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 00e0a27..516dc95 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1191,7 +1191,7 @@ Proof. by rewrite -has_pred1 has_count -eqn0Ngt; apply: eqP. Qed. Lemma count_uniq_mem s x : uniq s -> count_mem x s = (x \in s). Proof. elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. -by rewrite in_cons eq_sym; case: eqP => // ->; rewrite s'y. +by rewrite in_cons; case: eqsP => // <-; rewrite s'y. Qed. Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. @@ -1303,7 +1303,7 @@ Lemma rot_to s x : x \in s -> rot_to_spec s x. Proof. move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s). rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs. -by rewrite eq_sym in_cons; case: eqP => // -> _; rewrite drop0. +by rewrite in_cons; case: eqsP => // -> _; rewrite drop0. Qed. End EqSeq. @@ -2167,7 +2167,7 @@ Lemma nth_index_map s x0 x : {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x. Proof. elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //. -move: s_x; rewrite inE eq_sym; case: eqP => [-> | _] //=; apply: IHs. +move: s_x; rewrite inE; case: eqsP => [-> | _] //=; apply: IHs. by apply: sub_in2 inj_f => z; apply: predU1r. Qed. -- cgit v1.2.3 From c7c344f2f08f3910c884d9c3bb1bd5cfe3c2a1d7 Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Wed, 29 May 2019 12:38:48 +0300 Subject: Rename eqsP to eqPsym as suggested by @CohenCyril --- mathcomp/ssreflect/eqtype.v | 4 ++-- mathcomp/ssreflect/seq.v | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 895a86e..1f700fa 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -200,10 +200,10 @@ Variant eq_xor_neq_sym (T : eqType) (x y : T) : bool -> bool -> Set := | EqNotNeqSym of x = y : eq_xor_neq_sym x y true true | NeqNotEqSym of x <> y : eq_xor_neq_sym x y false false. -Lemma eqsP (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y). +Lemma eqPsym (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y). Proof. by rewrite eq_sym; case: eqP; constructor. Qed. -Arguments eqsP {T x y}. +Arguments eqPsym {T x y}. Section Contrapositives. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 516dc95..2ed0ee1 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1191,7 +1191,7 @@ Proof. by rewrite -has_pred1 has_count -eqn0Ngt; apply: eqP. Qed. Lemma count_uniq_mem s x : uniq s -> count_mem x s = (x \in s). Proof. elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. -by rewrite in_cons; case: eqsP => // <-; rewrite s'y. +by rewrite in_cons; case: eqPsym => // <-; rewrite s'y. Qed. Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. @@ -1303,7 +1303,7 @@ Lemma rot_to s x : x \in s -> rot_to_spec s x. Proof. move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s). rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs. -by rewrite in_cons; case: eqsP => // -> _; rewrite drop0. +by rewrite in_cons; case: eqPsym => // -> _; rewrite drop0. Qed. End EqSeq. @@ -2167,7 +2167,7 @@ Lemma nth_index_map s x0 x : {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x. Proof. elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //. -move: s_x; rewrite inE; case: eqsP => [-> | _] //=; apply: IHs. +move: s_x; rewrite inE; case: eqPsym => [-> | _] //=; apply: IHs. by apply: sub_in2 inj_f => z; apply: predU1r. Qed. -- cgit v1.2.3 From 1aa27b589c437b88cc6fb556edfceac42da449ea Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Wed, 29 May 2019 12:52:42 +0300 Subject: Canonical way of expressing dis-equality on an eqType is x != y Addressing a suggestion by @CohenCyril --- mathcomp/ssreflect/eqtype.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 1f700fa..75a04ef 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -198,10 +198,10 @@ Hint Resolve eq_refl eq_sym : core. Variant eq_xor_neq_sym (T : eqType) (x y : T) : bool -> bool -> Set := | EqNotNeqSym of x = y : eq_xor_neq_sym x y true true - | NeqNotEqSym of x <> y : eq_xor_neq_sym x y false false. + | NeqNotEqSym of x != y : eq_xor_neq_sym x y false false. Lemma eqPsym (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y). -Proof. by rewrite eq_sym; case: eqP; constructor. Qed. +Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed. Arguments eqPsym {T x y}. -- cgit v1.2.3 From 42db44ce8df9f24d90c321d57e81e2d5bf83bd48 Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Wed, 29 May 2019 15:17:39 +0300 Subject: Replace eqVneq with eqPsym Also changed eqsVneq. --- mathcomp/ssreflect/eqtype.v | 13 +++++-------- mathcomp/ssreflect/finset.v | 6 ++++-- mathcomp/ssreflect/seq.v | 6 +++--- 3 files changed, 12 insertions(+), 13 deletions(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 75a04ef..e4e0003 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -196,14 +196,14 @@ Proof. exact/eqP/eqP. Qed. Hint Resolve eq_refl eq_sym : core. -Variant eq_xor_neq_sym (T : eqType) (x y : T) : bool -> bool -> Set := - | EqNotNeqSym of x = y : eq_xor_neq_sym x y true true - | NeqNotEqSym of x != y : eq_xor_neq_sym x y false false. +Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set := + | EqNotNeq of x = y : eq_xor_neq x y true true + | NeqNotEq of x != y : eq_xor_neq x y false false. -Lemma eqPsym (T : eqType) (x y : T) : eq_xor_neq_sym x y (y == x) (x == y). +Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y). Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed. -Arguments eqPsym {T x y}. +Arguments eqVneq {T} x y, {T x y}. Section Contrapositives. @@ -379,9 +379,6 @@ Proof. by move->; rewrite eqxx. Qed. Lemma predU1r : b -> (x == y) || b. Proof. by move->; rewrite orbT. Qed. -Lemma eqVneq : {x = y} + {x != y}. -Proof. by case: eqP; [left | right]. Qed. - End EqPred. Arguments predU1P {T x y b}. diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 204843a..c01fb39 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -232,14 +232,16 @@ Definition setTfor (phT : phant T) := [set x : T | true]. Lemma in_setT x : x \in setTfor (Phant T). Proof. by rewrite in_set. Qed. -Lemma eqsVneq A B : {A = B} + {A != B}. -Proof. exact: eqVneq. Qed. +Lemma eqsVneq A B : eq_xor_neq A B (B == A) (A == B). +Proof. by apply: eqVneq. Qed. Lemma eq_finset (pA pB : pred T) : pA =1 pB -> finset pA = finset pB. Proof. by move=> eq_p; apply/setP => x; rewrite !(in_set, inE) eq_p. Qed. End BasicSetTheory. +Arguments eqsVneq {T} A B, {T A B}. + Definition inE := (in_set, inE). Arguments set0 {T}. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 2ed0ee1..9581a95 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1191,7 +1191,7 @@ Proof. by rewrite -has_pred1 has_count -eqn0Ngt; apply: eqP. Qed. Lemma count_uniq_mem s x : uniq s -> count_mem x s = (x \in s). Proof. elim: s => //= y s IHs /andP[/negbTE s'y /IHs-> {IHs}]. -by rewrite in_cons; case: eqPsym => // <-; rewrite s'y. +by rewrite in_cons; case: eqVneq => // <-; rewrite s'y. Qed. Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x]. @@ -1303,7 +1303,7 @@ Lemma rot_to s x : x \in s -> rot_to_spec s x. Proof. move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s). rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs. -by rewrite in_cons; case: eqPsym => // -> _; rewrite drop0. +by rewrite in_cons; case: eqVneq => // -> _; rewrite drop0. Qed. End EqSeq. @@ -2167,7 +2167,7 @@ Lemma nth_index_map s x0 x : {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x. Proof. elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //. -move: s_x; rewrite inE; case: eqPsym => [-> | _] //=; apply: IHs. +move: s_x; rewrite inE; case: eqVneq => [-> | _] //=; apply: IHs. by apply: sub_in2 inj_f => z; apply: predU1r. Qed. -- cgit v1.2.3 From e9c284b97b76e214f417ccc33907853bc0b8aa8e Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Wed, 29 May 2019 15:37:31 +0300 Subject: incorporate new suggestions by @CohenCyril --- mathcomp/ssreflect/eqtype.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/ssreflect') diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index e4e0003..7e1cdc8 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -201,7 +201,7 @@ Variant eq_xor_neq (T : eqType) (x y : T) : bool -> bool -> Set := | NeqNotEq of x != y : eq_xor_neq x y false false. Lemma eqVneq (T : eqType) (x y : T) : eq_xor_neq x y (y == x) (x == y). -Proof. by rewrite eq_sym; case: eqP=> [|/eqP]; constructor. Qed. +Proof. by rewrite eq_sym; case: (altP eqP); constructor. Qed. Arguments eqVneq {T} x y, {T x y}. -- cgit v1.2.3