From 35bd8708dacfb508f896d957d7b1189ca7decb3e Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Wed, 13 May 2020 13:11:14 +0900
Subject: Revise proofs in ssreflect/*.v

This change reduces
- use of numerical occurrence selectors (#436) and
- use of non ssreflect tactics such as `auto`,
and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`,
`ltngtP`, and `eqVneq`.
---
 mathcomp/ssreflect/fintype.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'mathcomp/ssreflect/fintype.v')

diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 432c30f..9ddabcb 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1440,7 +1440,7 @@ Definition option_finMixin := Eval hnf in FinMixin option_enumP.
 Canonical option_finType := Eval hnf in FinType (option T) option_finMixin.
 
 Lemma card_option : #|{: option T}| = #|T|.+1.
-Proof. by rewrite !cardT !enumT {1}unlock /= !size_map. Qed.
+Proof. by rewrite !cardT !enumT [in LHS]unlock /= !size_map. Qed.
 
 End OptionFinType.
 
@@ -1714,7 +1714,7 @@ Proof. by apply: val_inj; apply: nth_enum_ord. Qed.
 
 Lemma index_enum_ord (i : 'I_n) : index i (enum 'I_n) = i.
 Proof.
-by rewrite -{1}(nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).
+by rewrite -[in LHS](nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).
 Qed.
 
 End OrdinalEnum.
@@ -2158,7 +2158,7 @@ Canonical tag_finType := Eval hnf in FinType {i : I & T_ i} tag_finMixin.
 Lemma card_tagged :
   #|{: {i : I & T_ i}}| = sumn (map (fun i => #|T_ i|) (enum I)).
 Proof.
-rewrite cardE !enumT {1}unlock size_flatten /shape -map_comp.
+rewrite cardE !enumT [in LHS]unlock size_flatten /shape -map_comp.
 by congr (sumn _); apply: eq_map => i; rewrite /= size_map -enumT -cardE.
 Qed.
 
@@ -2184,7 +2184,6 @@ Definition sum_finMixin := Eval hnf in UniqFinMixin sum_enum_uniq mem_sum_enum.
 Canonical sum_finType := Eval hnf in FinType (T1 + T2) sum_finMixin.
 
 Lemma card_sum : #|{: T1 + T2}| = #|T1| + #|T2|.
-Proof. by rewrite !cardT !enumT {1}unlock size_cat !size_map. Qed.
-
+Proof. by rewrite !cardT !enumT [in LHS]unlock size_cat !size_map. Qed.
 
 End SumFinType.
-- 
cgit v1.2.3


From 37a49513f22a3f792a1ac3241962a7d17455f7e5 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Sat, 16 May 2020 09:02:13 +0900
Subject: A few more revisions

---
 mathcomp/ssreflect/fintype.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'mathcomp/ssreflect/fintype.v')

diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 9ddabcb..67f88a6 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -737,9 +737,7 @@ Proof. by []. Qed.
 
 Lemma properP A B :
   reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B).
-Proof.
-by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn].
-Qed.
+Proof. by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn]. Qed.
 
 Lemma proper_sub A B : A \proper B -> A \subset B.
 Proof. by case/andP. Qed.
-- 
cgit v1.2.3